diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java index 5c4cbe26b8..72d3e65574 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java +++ b/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 +// SPDX-FileCopyrightText: 2025 Dirk Beyer // // 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 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 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; + } } 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 aa4132b4cb..d591680a08 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java +++ b/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 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)); } } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java index a3017ccb85..cf76ed35fd 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java +++ b/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 +// SPDX-FileCopyrightText: 2025 Dirk Beyer // // 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); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java index 971a5770fa..0ffa256696 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java +++ b/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); + } } 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 708024a9a1..a73fbaee79 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java +++ b/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 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); - } } 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 16a9aa2fd3..971554c171 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/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 operands) { + List 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)); } } 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 34313bb28d..7c7657d1d1 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java +++ b/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 NUMERIC_FUNCTIONS = - ImmutableSet.of("+", "-", "*", "/", "div", "mod"); + ImmutableSet.of("+", "-", "*", "/", "div", "mod", "to_real"); protected final Script env; diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolRationalFormulaManager.java index 23bd96f950..880bc6cb37 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolRationalFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3RationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3RationalFormulaManager.java index ae0ff67a28..1f8dbfccbe 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3RationalFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java b/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java new file mode 100644 index 0000000000..2a6610c98f --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java @@ -0,0 +1,277 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.TruthJUnit.assume; + +import com.google.common.collect.ImmutableList; +import java.math.BigDecimal; +import java.math.BigInteger; +import java.util.List; +import java.util.function.BiFunction; +import java.util.function.Function; +import org.junit.Before; +import org.junit.Test; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +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.SolverException; + +public class MixedArithmeticsTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { + + /** Require that the solver supports mixed integer-real arithmetics. */ + @Before + public void requireMixedArithmetics() { + requireIntegers(); + requireRationals(); + assume().that(solver).isNotEqualTo(Solvers.OPENSMT); // OpenSMT does not support mixed terms + } + + /** Check if this unary operation returns the expected value. */ + private void testRationalOperation( + Function f, NumeralFormula arg, NumeralFormula expected) + throws SolverException, InterruptedException { + assertThatFormula(rmgr.equal(f.apply(arg), expected)).isTautological(); + assertThat(mgr.getFormulaType(f.apply(arg)).isRationalType()).isTrue(); + } + + /** Check if this binary operation returns the expected value. */ + private void testRationalOperation( + BiFunction f, + NumeralFormula arg1, + NumeralFormula arg2, + NumeralFormula expected) + throws SolverException, InterruptedException { + assertThatFormula(rmgr.equal(f.apply(arg1, arg2), expected)).isTautological(); + assertThat(mgr.getFormulaType(f.apply(arg1, arg2)).isRationalType()).isTrue(); + } + + /** Same as unary testRationalOperation(), but we expect the result to be an integer term. */ + private void testIntegerOperation( + Function f, NumeralFormula arg, IntegerFormula expected) + throws SolverException, InterruptedException { + assertThatFormula(imgr.equal(f.apply(arg), expected)).isTautological(); + assertThat(mgr.getFormulaType(f.apply(arg)).isIntegerType()).isTrue(); + } + + @Test + public void createIntegerNumberTest() throws SolverException, InterruptedException { + IntegerFormula num1 = imgr.makeNumber(1.0); + for (IntegerFormula num2 : + List.of( + imgr.makeNumber(1.0), + imgr.makeNumber("1"), + imgr.makeNumber(1), + imgr.makeNumber(BigInteger.ONE), + imgr.makeNumber(BigDecimal.ONE), + imgr.makeNumber(Rational.ONE))) { + assertThatFormula(imgr.equal(num1, num2)).isTautological(); + assertThat(mgr.getFormulaType(num2).isIntegerType()).isTrue(); + assertThat(num2).isEqualTo(num1); + } + } + + @Test + public void createRationalNumberTest() throws SolverException, InterruptedException { + RationalFormula num1 = rmgr.makeNumber(1.0); + for (RationalFormula num2 : + List.of( + rmgr.makeNumber(1.0), + rmgr.makeNumber("1"), + rmgr.makeNumber(1), + rmgr.makeNumber(BigInteger.ONE), + rmgr.makeNumber(BigDecimal.ONE), + rmgr.makeNumber(Rational.ONE))) { + assertThatFormula(rmgr.equal(num1, num2)).isTautological(); + assertThat(mgr.getFormulaType(num2).isRationalType()).isTrue(); + assertThat(num2).isEqualTo(num1); + } + } + + @Test + public void createRational2NumberTest() throws SolverException, InterruptedException { + RationalFormula num1 = rmgr.makeNumber(1.5); + for (RationalFormula num2 : + List.of( + rmgr.makeNumber(1.5), + rmgr.makeNumber("1.5"), + rmgr.makeNumber(BigDecimal.valueOf(1.5)), + rmgr.makeNumber(Rational.ofLongs(3, 2)))) { + assertThatFormula(rmgr.equal(num1, num2)).isTautological(); + assertThat(mgr.getFormulaType(num2).isRationalType()).isTrue(); + // assertThat(num2).isEqualTo(num1); // some solvers do not normalize rational numbers + } + } + + @Test + public void negateTest() throws SolverException, InterruptedException { + testRationalOperation(rmgr::negate, imgr.makeNumber(1.5), rmgr.makeNumber(-1.0)); + testRationalOperation(rmgr::negate, rmgr.makeNumber(1.5), rmgr.makeNumber(-1.5)); + } + + @Test + public void addTest() throws SolverException, InterruptedException { + testRationalOperation(rmgr::add, imgr.makeNumber(2), imgr.makeNumber(1), rmgr.makeNumber(3.0)); + testRationalOperation( + rmgr::add, imgr.makeNumber(2), rmgr.makeNumber(1.5), rmgr.makeNumber(3.5)); + testRationalOperation( + rmgr::add, rmgr.makeNumber(1.5), imgr.makeNumber(2), rmgr.makeNumber(3.5)); + testRationalOperation( + rmgr::add, rmgr.makeNumber(1.5), rmgr.makeNumber(2.5), rmgr.makeNumber(4.0)); + } + + @Test + public void sumTest() throws SolverException, InterruptedException { + assertThatFormula( + rmgr.equal( + rmgr.sum(ImmutableList.of(imgr.makeNumber(1), imgr.makeNumber(2))), + rmgr.makeNumber(3))) + .isTautological(); + assertThatFormula( + rmgr.equal( + rmgr.sum(ImmutableList.of(imgr.makeNumber(1), rmgr.makeNumber(1.5))), + rmgr.makeNumber(2.5))) + .isTautological(); + assertThatFormula( + rmgr.equal( + rmgr.sum(ImmutableList.of(rmgr.makeNumber(1.5), imgr.makeNumber(1))), + rmgr.makeNumber(2.5))) + .isTautological(); + assertThatFormula( + rmgr.equal( + rmgr.sum(ImmutableList.of(rmgr.makeNumber(0.5), rmgr.makeNumber(1.5))), + rmgr.makeNumber(2))) + .isTautological(); + } + + @Test + public void subtractTest() throws SolverException, InterruptedException { + testRationalOperation( + rmgr::subtract, imgr.makeNumber(2), imgr.makeNumber(1), rmgr.makeNumber(1.0)); + testRationalOperation( + rmgr::subtract, imgr.makeNumber(2), rmgr.makeNumber(1.5), rmgr.makeNumber(0.5)); + testRationalOperation( + rmgr::subtract, rmgr.makeNumber(1.5), imgr.makeNumber(2), rmgr.makeNumber(-0.5)); + testRationalOperation( + rmgr::subtract, rmgr.makeNumber(1.5), rmgr.makeNumber(0.5), rmgr.makeNumber(1.0)); + } + + @Test + public void divideTest() throws SolverException, InterruptedException { + testRationalOperation( + rmgr::divide, imgr.makeNumber(1), imgr.makeNumber(2), rmgr.makeNumber(0.5)); + testRationalOperation( + rmgr::divide, imgr.makeNumber(1), rmgr.makeNumber(2.0), rmgr.makeNumber(0.5)); + testRationalOperation( + rmgr::divide, rmgr.makeNumber(1.0), imgr.makeNumber(2), rmgr.makeNumber(0.5)); + testRationalOperation( + rmgr::divide, rmgr.makeNumber(1.0), rmgr.makeNumber(0.5), rmgr.makeNumber(2.0)); + } + + @Test + public void multiplyTest() throws SolverException, InterruptedException { + testRationalOperation( + rmgr::multiply, imgr.makeNumber(2), imgr.makeNumber(3), rmgr.makeNumber(6.0)); + testRationalOperation( + rmgr::multiply, imgr.makeNumber(2), rmgr.makeNumber(1.25), rmgr.makeNumber(2.5)); + testRationalOperation( + rmgr::multiply, rmgr.makeNumber(1.25), imgr.makeNumber(2), rmgr.makeNumber(2.5)); + testRationalOperation( + rmgr::multiply, rmgr.makeNumber(1.5), rmgr.makeNumber(2.5), rmgr.makeNumber(3.75)); + } + + @Test + public void equalTest() throws SolverException, InterruptedException { + assertThatFormula(rmgr.equal(imgr.makeNumber(1.5), rmgr.makeNumber(1.0))).isTautological(); + assertThatFormula(rmgr.equal(rmgr.makeNumber(1.0), imgr.makeNumber(1.5))).isTautological(); + } + + @Test + public void distinctTest() throws SolverException, InterruptedException { + assertThatFormula(rmgr.distinct(ImmutableList.of(imgr.makeNumber(1), imgr.makeNumber(2)))) + .isTautological(); + assertThatFormula(rmgr.distinct(ImmutableList.of(imgr.makeNumber(1), rmgr.makeNumber(1.5)))) + .isTautological(); + assertThatFormula(rmgr.distinct(ImmutableList.of(rmgr.makeNumber(1.5), imgr.makeNumber(2)))) + .isTautological(); + assertThatFormula(rmgr.distinct(ImmutableList.of(rmgr.makeNumber(1.5), imgr.makeNumber(1.0)))) + .isTautological(); + } + + @Test + public void greaterThanTest() throws SolverException, InterruptedException { + assertThatFormula(rmgr.greaterThan(imgr.makeNumber(1.5), rmgr.makeNumber(0.5))) + .isTautological(); + assertThatFormula(rmgr.greaterThan(rmgr.makeNumber(1.5), imgr.makeNumber(1.5))) + .isTautological(); + + assertThatFormula(rmgr.greaterThan(rmgr.makeNumber(1.5), imgr.makeNumber(1.5))) + .isTautological(); + assertThatFormula(rmgr.greaterThan(rmgr.makeNumber(1.5), rmgr.makeNumber(1.5))) + .isUnsatisfiable(); + assertThatFormula(rmgr.greaterThan(imgr.makeNumber(0.5), rmgr.makeNumber(0))).isUnsatisfiable(); + assertThatFormula(rmgr.greaterThan(imgr.makeNumber(0), rmgr.makeNumber(0))).isUnsatisfiable(); + assertThatFormula(rmgr.greaterThan(imgr.makeNumber(0), rmgr.makeNumber(0.5))).isUnsatisfiable(); + assertThatFormula(rmgr.greaterThan(imgr.makeNumber(1), rmgr.makeNumber(0.5))).isTautological(); + assertThatFormula(rmgr.greaterThan(imgr.makeNumber(1.5), rmgr.makeNumber(0.5))) + .isTautological(); + } + + @Test + public void greaterOrEqualTest() throws SolverException, InterruptedException { + assertThatFormula(rmgr.greaterOrEquals(imgr.makeNumber(1.5), rmgr.makeNumber(1.0))) + .isTautological(); + assertThatFormula(rmgr.greaterOrEquals(rmgr.makeNumber(1.5), imgr.makeNumber(1.5))) + .isTautological(); + } + + @Test + public void lessThanTest() throws SolverException, InterruptedException { + assertThatFormula(rmgr.lessThan(imgr.makeNumber(1.5), rmgr.makeNumber(1.5))).isTautological(); + assertThatFormula(rmgr.lessThan(rmgr.makeNumber(1.5), rmgr.makeNumber(1.5))).isUnsatisfiable(); + assertThatFormula(rmgr.lessThan(rmgr.makeNumber(0), imgr.makeNumber(0.5))).isUnsatisfiable(); + assertThatFormula(rmgr.lessThan(rmgr.makeNumber(0), imgr.makeNumber(0))).isUnsatisfiable(); + assertThatFormula(rmgr.lessThan(rmgr.makeNumber(0.5), imgr.makeNumber(0))).isUnsatisfiable(); + assertThatFormula(rmgr.lessThan(rmgr.makeNumber(0.5), imgr.makeNumber(1))).isTautological(); + assertThatFormula(rmgr.lessThan(rmgr.makeNumber(0.5), imgr.makeNumber(1.5))).isTautological(); + } + + @Test + public void lessOrEqualTest() throws SolverException, InterruptedException { + assertThatFormula(rmgr.lessOrEquals(imgr.makeNumber(1.5), rmgr.makeNumber(1.0))) + .isTautological(); + assertThatFormula(rmgr.lessOrEquals(rmgr.makeNumber(1.5), imgr.makeNumber(2.0))) + .isTautological(); + } + + @Test + public void floorTest() throws SolverException, InterruptedException { + requireRationalFloor(); + testIntegerOperation(rmgr::floor, imgr.makeNumber(1.0), imgr.makeNumber(1.0)); + testIntegerOperation(rmgr::floor, rmgr.makeNumber(1.5), imgr.makeNumber(1.0)); + } + + @Test + public void simplificationTest() throws InterruptedException { + IntegerFormula sumInt = imgr.add(imgr.makeNumber(2), imgr.makeNumber(1)); + assertThat(mgr.getFormulaType(sumInt).isIntegerType()).isTrue(); + IntegerFormula simplifiedSumInt = mgr.simplify(sumInt); + assertThat(mgr.getFormulaType(simplifiedSumInt).isIntegerType()).isTrue(); + + RationalFormula sumRat = rmgr.add(rmgr.makeNumber(2.0), imgr.makeNumber(1.0)); + assertThat(mgr.getFormulaType(sumRat).isRationalType()).isTrue(); + RationalFormula simplifiedSumRat = mgr.simplify(sumRat); + assertThat(mgr.getFormulaType(simplifiedSumRat).isRationalType()).isTrue(); + } +} diff --git a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java index 45010e3141..d3160b4372 100644 --- a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java @@ -188,7 +188,7 @@ public void testSubTypes() { IntegerFormula uf = fmgr.callUF(ufDecl, a, r); mgr.visit( - bmgr.and(rmgr.equal(uf, imgr.makeNumber(0))), + bmgr.and(imgr.equal(uf, imgr.makeNumber(0))), new DefaultFormulaVisitor() { @Override