Add a new method toRational() to NumeralFormulaManager

src/org/sosy_lab/java_smt/api/NumeralFormulaManager.java

@@ -13,6 +13,7 @@
 import java.util.List;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 
 /**
  * This interface represents the Numeral Theory.
@@ -106,4 +107,6 @@ public interface NumeralFormulaManager<
    * <p>For rational formulas, SMTlib2 denotes this operation as {@code to_int}.
    */
   IntegerFormula floor(ParamFormulaType formula);
+
+  RationalFormula toRational(ParamFormulaType number);
 }

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

@@ -24,6 +24,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.NumeralFormulaManager;
 
 /**
@@ -445,4 +446,16 @@ protected TFormulaInfo floor(TFormulaInfo number) {
   protected TFormulaInfo toType(TFormulaInfo param) {
     return param;
   }
+
+  @Override
+  public RationalFormula toRational(ParamFormulaType number) {
+    if (number instanceof RationalFormula) {
+      return (RationalFormula) number;
+    } else {
+      return getFormulaCreator()
+          .encapsulate(FormulaType.RationalType, toRational(extractInfo(number)));
+    }
+  }
+
+  protected abstract TFormulaInfo toRational(TFormulaInfo number);
 }

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingNumeralFormulaManager.java

@@ -18,6 +18,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.NumeralFormulaManager;
 
 @SuppressWarnings("ClassTypeParameterName")
@@ -225,4 +226,13 @@ public IntegerFormula floor(ParamFormulaType formula) {
     debugging.addFormulaTerm(result);
     return result;
   }
+
+  @Override
+  public RationalFormula toRational(ParamFormulaType formula) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(formula);
+    RationalFormula result = delegate.toRational(formula);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
 }

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsNumeralFormulaManager.java

@@ -18,6 +18,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.NumeralFormulaManager;
 
 @SuppressWarnings("ClassTypeParameterName")
@@ -160,4 +161,10 @@ public IntegerFormula floor(ParamFormulaType pNumber) {
     stats.numericOperations.getAndIncrement();
     return delegate.floor(pNumber);
   }
+
+  @Override
+  public RationalFormula toRational(ParamFormulaType formula) {
+    stats.numericOperations.getAndIncrement();
+    return delegate.toRational(formula);
+  }
 }

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedNumeralFormulaManager.java

@@ -18,6 +18,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.NumeralFormulaManager;
 import org.sosy_lab.java_smt.api.SolverContext;
 
@@ -181,4 +182,11 @@ public IntegerFormula floor(ParamFormulaType pNumber) {
       return delegate.floor(pNumber);
     }
   }
+
+  @Override
+  public RationalFormula toRational(ParamFormulaType formula) {
+    synchronized (sync) {
+      return delegate.toRational(formula);
+    }
+  }
 }

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java

@@ -186,4 +186,9 @@ protected Expr distinctImpl(List<Expr> pParam) {
       return exprManager.mkExpr(Kind.DISTINCT, param);
     }
   }
+
+  @Override
+  public Expr toRational(Expr formula) {
+    return exprManager.mkExpr(Kind.TO_REAL, formula);
+  }
 }

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

@@ -195,4 +195,9 @@ protected Term distinctImpl(List<Term> pParam) {
           Kind.DISTINCT, pParam.stream().map(this::toType).toArray(Term[]::new));
     }
   }
+
+  @Override
+  public Term toRational(Term formula) {
+    return termManager.mkTerm(Kind.TO_REAL, formula);
+  }
 }

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NumeralFormulaManager.java

@@ -135,4 +135,9 @@ protected Long lessOrEquals(Long pNumber1, Long pNumber2) {
   protected Long floor(Long pNumber) {
     return msat_make_floor(mathsatEnv, pNumber);
   }
+
+  @Override
+  protected Long toRational(Long pNumber) {
+    return pNumber;
+  }
 }

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNumeralFormulaManager.java

@@ -122,4 +122,9 @@ protected PTRef lessOrEquals(PTRef pParam1, PTRef pParam2) {
   protected PTRef distinctImpl(List<PTRef> pParam) {
     return osmtLogic.mkDistinct(new VectorPTRef(pParam));
   }
+
+  @Override
+  public PTRef toRational(PTRef formula) {
+    throw new UnsupportedOperationException("OpenSMT does not support mixed integer-real logic");
+  }
 }

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

@@ -44,4 +44,9 @@ protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {
   protected IExpression distinctImpl(List<IExpression> pNumbers) {
     return IExpression.distinct(asScala(Iterables.filter(pNumbers, ITerm.class)));
   }
+
+  @Override
+  public IExpression toRational(IExpression formula) {
+    return PrincessEnvironment.rationalTheory.int2ring((ITerm) formula);
+  }
 }

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

@@ -54,18 +54,14 @@ protected boolean isNumeral(IExpression value) {
     return false;
   }
 
-  protected IExpression fromInteger(ITerm i) {
-    return PrincessEnvironment.rationalTheory.int2ring(i);
-  }
-
   @Override
   protected IExpression makeNumberImpl(long i) {
-    return fromInteger(ifmgr.makeNumberImpl(i));
+    return toRational(ifmgr.makeNumberImpl(i));
   }
 
   @Override
   protected IExpression makeNumberImpl(BigInteger i) {
-    return fromInteger(ifmgr.makeNumberImpl(i));
+    return toRational(ifmgr.makeNumberImpl(i));
   }
 
   @Override

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

@@ -174,4 +174,9 @@ public Term lessThan(Term pNumber1, Term pNumber2) {
   public Term lessOrEquals(Term pNumber1, Term pNumber2) {
     return env.term("<=", pNumber1, pNumber2);
   }
+
+  @Override
+  public Term toRational(Term formula) {
+    return env.term("to_real", formula);
+  }
 }

src/org/sosy_lab/java_smt/solvers/yices2/Yices2NumeralFormulaManager.java

@@ -136,4 +136,9 @@ public Integer lessOrEquals(Integer pParam1, Integer pParam2) {
   protected Integer floor(Integer pNumber) {
     return yices_floor(pNumber);
   }
+
+  @Override
+  public Integer toRational(Integer formula) {
+    return formula;
+  }
 }

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

@@ -123,4 +123,9 @@ protected Long lessThan(Long pNumber1, Long pNumber2) {
   protected Long lessOrEquals(Long pNumber1, Long pNumber2) {
     return Native.mkLe(z3context, pNumber1, pNumber2);
   }
+
+  @Override
+  protected Long toRational(Long number) {
+    return Native.mkInt2real(z3context, number);
+  }
 }

src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java

@@ -65,6 +65,20 @@ private void testIntegerOperation(
     assertThat(mgr.getFormulaType(f.apply(arg)).isIntegerType()).isTrue();
   }
 
+  /**
+   * Same as binary testRationalOperation(), but we expect both arguments, and result to be integer
+   * terms.
+   */
+  private void testIntegerOperation(
+      BiFunction<IntegerFormula, IntegerFormula, IntegerFormula> f,
+      IntegerFormula arg1,
+      IntegerFormula arg2,
+      IntegerFormula expected)
+      throws SolverException, InterruptedException {
+    assertThatFormula(imgr.equal(f.apply(arg1, arg2), expected)).isTautological();
+    assertThat(mgr.getFormulaType(f.apply(arg1, arg2)).isIntegerType()).isTrue();
+  }
+
   @Test
   public void createIntegerNumberTest() throws SolverException, InterruptedException {
     IntegerFormula num1 = imgr.makeNumber(1.0);
@@ -169,6 +183,7 @@ public void subtractTest() throws SolverException, InterruptedException {
 
   @Test
   public void divideTest() throws SolverException, InterruptedException {
+    testIntegerOperation(imgr::divide, imgr.makeNumber(5), imgr.makeNumber(2), imgr.makeNumber(2));
     testRationalOperation(
         rmgr::divide, imgr.makeNumber(1), imgr.makeNumber(2), rmgr.makeNumber(0.5));
     testRationalOperation(