diff --git a/src/org/sosy_lab/java_smt/api/NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/api/NumeralFormulaManager.java index 3bf9defc39..9b02cb7c6a 100644 --- a/src/org/sosy_lab/java_smt/api/NumeralFormulaManager.java +++ b/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< *

For rational formulas, SMTlib2 denotes this operation as {@code to_int}. */ IntegerFormula floor(ParamFormulaType formula); + + RationalFormula toRational(ParamFormulaType number); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java index 72d3e65574..967532d8a2 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java +++ b/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); } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingNumeralFormulaManager.java index 53db20c9ce..aefe2291f7 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingNumeralFormulaManager.java +++ b/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; + } } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsNumeralFormulaManager.java index bb05a5adcc..067c78cddb 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsNumeralFormulaManager.java +++ b/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); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedNumeralFormulaManager.java index ead3f3c977..0edb2140a1 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedNumeralFormulaManager.java +++ b/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); + } + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java index aacd719cab..ce5ee3bdb8 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java @@ -186,4 +186,9 @@ protected Expr distinctImpl(List pParam) { return exprManager.mkExpr(Kind.DISTINCT, param); } } + + @Override + public Expr toRational(Expr formula) { + return exprManager.mkExpr(Kind.TO_REAL, formula); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java index d591680a08..5737478a4a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java @@ -195,4 +195,9 @@ protected Term distinctImpl(List pParam) { Kind.DISTINCT, pParam.stream().map(this::toType).toArray(Term[]::new)); } } + + @Override + public Term toRational(Term formula) { + return termManager.mkTerm(Kind.TO_REAL, formula); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NumeralFormulaManager.java index 3d7579a017..0209b7be38 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NumeralFormulaManager.java +++ b/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; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNumeralFormulaManager.java index 2396c231f4..e4daa2fd51 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNumeralFormulaManager.java +++ b/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 pParam) { return osmtLogic.mkDistinct(new VectorPTRef(pParam)); } + + @Override + public PTRef toRational(PTRef formula) { + throw new UnsupportedOperationException("OpenSMT does not support mixed integer-real logic"); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java index a73fbaee79..4f4e45a2e6 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java +++ b/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 pNumbers) { return IExpression.distinct(asScala(Iterables.filter(pNumbers, ITerm.class))); } + + @Override + public IExpression toRational(IExpression formula) { + return PrincessEnvironment.rationalTheory.int2ring((ITerm) formula); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java index 31984ec0a3..5bb290573b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/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 diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java index 7c7657d1d1..145b4b3c08 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java +++ b/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); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NumeralFormulaManager.java index 48d8bb4d75..4a8a1b2421 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NumeralFormulaManager.java +++ b/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; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java index ea834fbdb1..b8195f5454 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java +++ b/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); + } } diff --git a/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java b/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java index 2a6610c98f..03ab49e901 100644 --- a/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java +++ b/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 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(