Add explicit cast in mixed integer-real term

src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -17,6 +17,7 @@
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.List;
+import java.util.stream.Collectors;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
@@ -180,7 +181,7 @@ public ResultFormulaType makeVariable(String pVar) {
   @Override
   public ResultFormulaType negate(ParamFormulaType pNumber) {
     TFormulaInfo param1 = extractInfo(pNumber);
-    return wrap(negate(param1));
+    return wrap(negate(toType(param1)));
   }
 
   protected abstract TFormulaInfo negate(TFormulaInfo pParam1);
@@ -190,14 +191,19 @@ public ResultFormulaType add(ParamFormulaType pNumber1, ParamFormulaType pNumber
     TFormulaInfo param1 = extractInfo(pNumber1);
     TFormulaInfo param2 = extractInfo(pNumber2);
 
-    return wrap(add(param1, param2));
+    return wrap(add(toType(param1), toType(param2)));
   }
 
   protected abstract TFormulaInfo add(TFormulaInfo pParam1, TFormulaInfo pParam2);
 
   @Override
   public ResultFormulaType sum(List<ParamFormulaType> operands) {
-    return wrap(sumImpl(Lists.transform(operands, this::extractInfo)));
+    return wrap(
+        sumImpl(
+            operands.stream()
+                .map(this::extractInfo)
+                .map(this::toType)
+                .collect(Collectors.toList())));
   }
 
   protected TFormulaInfo sumImpl(List<TFormulaInfo> operands) {
@@ -213,7 +219,7 @@ public ResultFormulaType subtract(ParamFormulaType pNumber1, ParamFormulaType pN
     TFormulaInfo param1 = extractInfo(pNumber1);
     TFormulaInfo param2 = extractInfo(pNumber2);
 
-    return wrap(subtract(param1, param2));
+    return wrap(subtract(toType(param1), toType(param2)));
   }
 
   protected abstract TFormulaInfo subtract(TFormulaInfo pParam1, TFormulaInfo pParam2);
@@ -231,7 +237,7 @@ public ResultFormulaType divide(ParamFormulaType pNumber1, ParamFormulaType pNum
       result = makeUf(divUfDecl, param1, param2);
     } else {
       try {
-        result = divide(param1, param2);
+        result = divide(toType(param1), toType(param2));
       } catch (UnsupportedOperationException e) {
         if (nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
           result = makeUf(divUfDecl, param1, param2);
@@ -263,7 +269,7 @@ public ResultFormulaType modulo(ParamFormulaType pNumber1, ParamFormulaType pNum
       result = makeUf(modUfDecl, param1, param2);
     } else {
       try {
-        result = modulo(param1, param2);
+        result = modulo(toType(param1), toType(param2));
       } catch (UnsupportedOperationException e) {
         if (nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
           result = makeUf(modUfDecl, param1, param2);
@@ -337,7 +343,7 @@ public ResultFormulaType multiply(ParamFormulaType pNumber1, ParamFormulaType pN
       result = makeUf(multUfDecl, param1, param2);
     } else {
       try {
-        result = multiply(param1, param2);
+        result = multiply(toType(param1), toType(param2));
       } catch (UnsupportedOperationException e) {
         if (nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
           result = makeUf(multUfDecl, param1, param2);
@@ -434,4 +440,9 @@ protected TFormulaInfo floor(TFormulaInfo number) {
         "method should only be called for RationalFormulae, but type is "
             + getFormulaCreator().getFormulaType(number));
   }
+
+  /** Make sure the value is of correct type (Int vs. Real) and add a cast if necessary. */
+  protected TFormulaInfo toType(TFormulaInfo param) {
+    return param;
+  }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java

@@ -163,7 +163,7 @@ protected Term subtract(Term pParam1, Term pParam2) {
 
   @Override
   protected Term equal(Term pParam1, Term pParam2) {
-    return termManager.mkTerm(Kind.EQUAL, pParam1, pParam2);
+    return termManager.mkTerm(Kind.EQUAL, toType(pParam1), toType(pParam2));
   }
 
   @Override
@@ -191,7 +191,8 @@ protected Term distinctImpl(List<Term> pParam) {
     if (pParam.size() < 2) {
       return termManager.mkTrue();
     } else {
-      return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0]));
+      return termManager.mkTerm(
+          Kind.DISTINCT, pParam.stream().map(this::toType).toArray(Term[]::new));
     }
   }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -40,6 +40,11 @@ protected Term makeNumberImpl(BigDecimal pNumber) {
     return makeNumberImpl(pNumber.toPlainString());
   }
 
+  @Override
+  protected Term toType(Term pNumber) {
+    return pNumber.getSort().isInteger() ? termManager.mkTerm(Kind.TO_REAL, pNumber) : pNumber;
+  }
+
   @Override
   public Term divide(Term pParam1, Term pParam2) {
     return termManager.mkTerm(Kind.DIVISION, pParam1, pParam2);

src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java

@@ -10,6 +10,7 @@
 
 import ap.basetypes.IdealInt;
 import ap.parser.IExpression;
+import ap.parser.IFormula;
 import ap.parser.IIntLit;
 import ap.parser.ITerm;
 import ap.theories.nia.GroebnerMultiplication;
@@ -105,4 +106,39 @@ protected boolean isNumeral(IExpression val) {
   protected IExpression floor(IExpression pNumber) {
     return pNumber; // identity for integers
   }
+
+  @Override
+  protected ITerm negate(IExpression pNumber) {
+    return ((ITerm) pNumber).unary_$minus();
+  }
+
+  @Override
+  protected ITerm add(IExpression pNumber1, IExpression pNumber2) {
+    return ((ITerm) pNumber1).$plus((ITerm) pNumber2);
+  }
+
+  @Override
+  protected ITerm subtract(IExpression pNumber1, IExpression pNumber2) {
+    return ((ITerm) pNumber1).$minus((ITerm) pNumber2);
+  }
+
+  @Override
+  protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {
+    return ((ITerm) pNumber1).$greater((ITerm) pNumber2);
+  }
+
+  @Override
+  protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {
+    return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2);
+  }
+
+  @Override
+  protected IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {
+    return ((ITerm) pNumber1).$less((ITerm) pNumber2);
+  }
+
+  @Override
+  protected IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {
+    return ((ITerm) pNumber1).$less$eq((ITerm) pNumber2);
+  }
 }

src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java

@@ -35,21 +35,6 @@ abstract class PrincessNumeralFormulaManager<
     super(pCreator, pNonLinearArithmetic);
   }
 
-  @Override
-  protected ITerm negate(IExpression pNumber) {
-    return ((ITerm) pNumber).unary_$minus();
-  }
-
-  @Override
-  protected ITerm add(IExpression pNumber1, IExpression pNumber2) {
-    return ((ITerm) pNumber1).$plus((ITerm) pNumber2);
-  }
-
-  @Override
-  protected ITerm subtract(IExpression pNumber1, IExpression pNumber2) {
-    return ((ITerm) pNumber1).$minus((ITerm) pNumber2);
-  }
-
   @Override
   protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2);
@@ -59,24 +44,4 @@ protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {
   protected IExpression distinctImpl(List<IExpression> pNumbers) {
     return IExpression.distinct(asScala(Iterables.filter(pNumbers, ITerm.class)));
   }
-
-  @Override
-  protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {
-    return ((ITerm) pNumber1).$greater((ITerm) pNumber2);
-  }
-
-  @Override
-  protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {
-    return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2);
-  }
-
-  @Override
-  protected IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {
-    return ((ITerm) pNumber1).$less((ITerm) pNumber2);
-  }
-
-  @Override
-  protected IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {
-    return ((ITerm) pNumber1).$less$eq((ITerm) pNumber2);
-  }
 }

src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java

@@ -8,17 +8,17 @@
 
 package org.sosy_lab.java_smt.solvers.princess;
 
-import ap.basetypes.IdealInt;
 import ap.parser.IExpression;
+import ap.parser.IFormula;
 import ap.parser.IFunApp;
-import ap.parser.IIntLit;
 import ap.parser.ITerm;
+import ap.theories.rationals.Rationals;
 import com.google.common.collect.ImmutableList;
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.List;
+import java.util.stream.Collectors;
 import org.sosy_lab.common.rationals.Rational;
-import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.RationalFormulaManager;
@@ -107,30 +107,72 @@ protected IExpression makeVariableImpl(String varName) {
     return getFormulaCreator().makeVariable(PrincessEnvironment.FRACTION_SORT, varName);
   }
 
+  @Override
+  protected ITerm toType(IExpression param) {
+    ITerm number = (ITerm) param;
+    return formulaCreator.getFormulaType(number).isIntegerType()
+        ? Rationals.int2ring(number)
+        : number;
+  }
+
   @Override
   protected IExpression floor(IExpression number) {
     throw new UnsupportedOperationException("floor is not supported in Princess");
   }
 
   @Override
-  protected IExpression multiply(IExpression number1, IExpression number2) {
-    FormulaType<?> sort1 = getFormulaCreator().getFormulaType(number1);
-    FormulaType<?> sort2 = getFormulaCreator().getFormulaType(number1);
+  protected ITerm negate(IExpression number) {
+    return Rationals.minus(toType(number));
+  }
 
-    IExpression result = PrincessEnvironment.rationalTheory.mul((ITerm) number1, (ITerm) number2);
+  @Override
+  protected ITerm add(IExpression number1, IExpression number2) {
+    return Rationals.plus(toType(number1), toType(number2));
+  }
 
-    if (result instanceof IIntLit && ((IIntLit) result).value().equals(IdealInt.apply(0))) {
-      // If the result is (integer) zero we may have lost our type
-      // Check the type of both arguments and convert the result back to rational if needed
-      if (sort1.isRationalType() || sort2.isRationalType()) {
-        result = PrincessEnvironment.rationalTheory.int2ring((IIntLit) result);
-      }
-    }
-    return result;
+  @Override
+  protected ITerm subtract(IExpression number1, IExpression number2) {
+    return Rationals.minus(toType(number1), toType(number2));
+  }
+
+  @Override
+  protected IExpression multiply(IExpression number1, IExpression number2) {
+    return Rationals.mul(toType(number1), toType(number2));
   }
 
   @Override
   protected IExpression divide(IExpression number1, IExpression number2) {
-    return PrincessEnvironment.rationalTheory.div((ITerm) number1, (ITerm) number2);
+    return Rationals.div(toType(number1), toType(number2));
+  }
+
+  @Override
+  protected IFormula equal(IExpression number1, IExpression number2) {
+    return super.equal(toType(number1), toType(number2));
+  }
+
+  @Override
+  protected IExpression distinctImpl(List<IExpression> operands) {
+    List<IExpression> castedOps = operands.stream().map(this::toType).collect(Collectors.toList());
+    return super.distinctImpl(castedOps);
+  }
+
+  @Override
+  protected IFormula greaterThan(IExpression number1, IExpression number2) {
+    return Rationals.gt(toType(number1), toType(number2));
+  }
+
+  @Override
+  protected IFormula greaterOrEquals(IExpression number1, IExpression number2) {
+    return Rationals.geq(toType(number1), toType(number2));
+  }
+
+  @Override
+  protected IFormula lessThan(IExpression number1, IExpression number2) {
+    return Rationals.lt(toType(number1), toType(number2));
+  }
+
+  @Override
+  protected IFormula lessOrEquals(IExpression number1, IExpression number2) {
+    return Rationals.leq(toType(number1), toType(number2));
   }
 }

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java

@@ -33,7 +33,7 @@ abstract class SmtInterpolNumeralFormulaManager<
 
   /** Operators for arithmetic functions that return a numeric value. */
   private static final ImmutableSet<String> NUMERIC_FUNCTIONS =
-      ImmutableSet.of("+", "-", "*", "/", "div", "mod");
+      ImmutableSet.of("+", "-", "*", "/", "div", "mod", "to_real");
 
   protected final Script env;
 

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolRationalFormulaManager.java

@@ -65,13 +65,15 @@ protected Term makeVariableImpl(String varName) {
     return getFormulaCreator().makeVariable(t, varName);
   }
 
+  @Override
+  protected Term toType(Term pNumber) {
+    Sort intSort = pNumber.getTheory().getNumericSort();
+    return pNumber.getSort().equals(intSort) ? env.term("to_real", pNumber) : pNumber;
+  }
+
   @Override
   public Term divide(Term pNumber1, Term pNumber2) {
     if (consistsOfNumerals(pNumber2)) {
-      Sort intSort = pNumber1.getTheory().getNumericSort();
-      Sort realSort = pNumber1.getTheory().getRealSort();
-      assert intSort.equals(pNumber1.getSort()) || realSort.equals(pNumber1.getSort());
-      assert intSort.equals(pNumber2.getSort()) || realSort.equals(pNumber2.getSort());
       return env.term("/", pNumber1, pNumber2);
     } else {
       return super.divide(pNumber1, pNumber2);

src/org/sosy_lab/java_smt/solvers/z3/Z3RationalFormulaManager.java

@@ -36,6 +36,17 @@ protected Long makeNumberImpl(BigDecimal pNumber) {
     return makeNumberImpl(pNumber.toPlainString());
   }
 
+  @Override
+  protected Long toType(Long pNumber) {
+    if (Native.getSort(z3context, pNumber) == formulaCreator.getIntegerType()) {
+      long castedNumber = Native.mkInt2real(z3context, pNumber);
+      Native.incRef(z3context, castedNumber);
+      return castedNumber;
+    } else {
+      return pNumber;
+    }
+  }
+
   @Override
   protected Long floor(Long pNumber) {
     return Native.mkReal2int(z3context, pNumber);