diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5IntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5IntegerFormulaManager.java index 2064ed3a7d..663b4ebeb5 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5IntegerFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5IntegerFormulaManager.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.mathsat5; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_divide; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_floor; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_modular_congruence; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_number; @@ -17,6 +18,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_term_ite; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_times; +import com.google.common.collect.ImmutableList; import java.math.BigDecimal; import java.math.BigInteger; import org.sosy_lab.java_smt.api.IntegerFormulaManager; @@ -26,9 +28,15 @@ class Mathsat5IntegerFormulaManager extends Mathsat5NumeralFormulaManager implements IntegerFormulaManager { + // Reserved UF symbol for modulo(a,0) + private final long modZeroUF; + Mathsat5IntegerFormulaManager( Mathsat5FormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic) { super(pCreator, pNonLinearArithmetic); + modZeroUF = + pCreator.declareUFImpl( + "_%0", pCreator.getIntegerType(), ImmutableList.of(pCreator.getIntegerType())); } @Override @@ -69,6 +77,21 @@ public Long divide(Long pNumber1, Long pNumber2) { msat_make_floor(mathsatEnv, div)); } + @Override + protected Long modulo(Long pNumber1, Long pNumber2) { + // The modulo can be calculated by the formula: + // remainder = dividend - floor(dividend/divisor)*divisor + // However, this will fail if the divisor is zero as SMTLIB then allows the solver to return + // any value for the remainder. We solve this by first checking the divisor and returning an + // UF symbol "modZeroUF(dividend)" if it is zero. Otherwise, the formula is used to calculate + // the remainder. + return msat_make_term_ite( + mathsatEnv, + msat_make_equal(mathsatEnv, pNumber2, msat_make_int_number(mathsatEnv, 0)), + getFormulaCreator().callFunctionImpl(modZeroUF, ImmutableList.of(pNumber1)), + subtract(pNumber1, multiply(divide(pNumber1, pNumber2), pNumber2))); + } + @Override protected Long modularCongruence(Long pNumber1, Long pNumber2, BigInteger pModulo) { return modularCongruence0(pNumber1, pNumber2, pModulo.toString()); diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java index 39a516a1cb..c4b595d93d 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java @@ -110,7 +110,12 @@ public void testModuloConstantUnsatisfiable() throws SolverException, Interrupte handleExpectedException(() -> imgr.modulo(a, imgr.makeNumber(3))))); // INFO: OpenSMT does support modulo with constants - if (ImmutableSet.of(Solvers.SMTINTERPOL, Solvers.CVC4, Solvers.YICES2, Solvers.OPENSMT) + if (ImmutableSet.of( + Solvers.SMTINTERPOL, + Solvers.CVC4, + Solvers.YICES2, + Solvers.OPENSMT, + Solvers.MATHSAT5) .contains(solver) && nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) { // some solvers support modulo with constants @@ -148,7 +153,8 @@ public void testModuloUnsatisfiable() throws SolverException, InterruptedExcepti imgr.makeNumber(1), handleExpectedException(() -> imgr.modulo(imgr.makeNumber(5), a)))); - if (Solvers.CVC4 == solver && nonLinearArithmetic != NonLinearArithmetic.APPROXIMATE_ALWAYS) { + if (ImmutableSet.of(Solvers.CVC4, Solvers.MATHSAT5).contains(solver) + && nonLinearArithmetic != NonLinearArithmetic.APPROXIMATE_ALWAYS) { // some solvers support non-linear multiplication (partially) assertThatFormula(f).isUnsatisfiable(); diff --git a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java index 4461a7495a..61a6e0b62f 100644 --- a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java @@ -9,12 +9,14 @@ package org.sosy_lab.java_smt.test; import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; import com.google.common.collect.ImmutableList; import java.util.ArrayList; import java.util.List; import org.junit.Test; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; @@ -26,6 +28,78 @@ public class NumeralFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { + @Test + public void divZeroTest() throws SolverException, InterruptedException { + requireIntegers(); + assume().that(solver).isNoneOf(Solvers.OPENSMT, Solvers.YICES2); // No division by zero + + IntegerFormula zero = imgr.makeNumber(0); + IntegerFormula three = imgr.makeNumber(3); + IntegerFormula seven = imgr.makeNumber(7); + + // Show that 3/0=0 and 3/0=7 can hold separately + IntegerFormula f1 = imgr.divide(three, zero); + assertThatFormula(imgr.equal(f1, zero)).isSatisfiable(); + assertThatFormula(imgr.equal(f1, seven)).isSatisfiable(); + + // But if 3/0=0 in the model, it can't also be another value + IntegerFormula var = imgr.makeVariable("var"); + IntegerFormula f2 = imgr.divide(var, zero); + IntegerFormula res = imgr.makeVariable("res"); + assertThatFormula( + bmgr.and( + imgr.equal(f1, zero), + imgr.equal(var, three), + imgr.equal(f2, res), + bmgr.not(imgr.equal(res, zero)))) + .isUnsatisfiable(); + + // Show that a=b => a/0=b/0 + IntegerFormula var1 = imgr.makeVariable("arg1"); + IntegerFormula var2 = imgr.makeVariable("arg2"); + assertThatFormula( + bmgr.implication( + imgr.equal(var1, var2), + imgr.equal(imgr.divide(var1, zero), imgr.divide(var2, zero)))) + .isTautological(); + } + + @Test + public void modZeroTest() throws SolverException, InterruptedException { + requireIntegers(); + assume().that(solver).isNoneOf(Solvers.OPENSMT, Solvers.YICES2); // No division by zero + + IntegerFormula zero = imgr.makeNumber(0); + IntegerFormula three = imgr.makeNumber(3); + IntegerFormula seven = imgr.makeNumber(7); + + // Show that 3%0=0 and 3%0=7 can hold separately + IntegerFormula f1 = imgr.modulo(three, zero); + assertThatFormula(imgr.equal(f1, zero)).isSatisfiable(); + assertThatFormula(imgr.equal(f1, seven)).isSatisfiable(); + + // But if 3%0=0 in the model, it can't also be another value + IntegerFormula var = imgr.makeVariable("var"); + IntegerFormula f2 = imgr.modulo(var, zero); + IntegerFormula res = imgr.makeVariable("res"); + assertThatFormula( + bmgr.and( + imgr.equal(f1, zero), + imgr.equal(var, three), + imgr.equal(f2, res), + bmgr.not(imgr.equal(res, zero)))) + .isUnsatisfiable(); + + // Show that a=b => a%0=b%0 + IntegerFormula var1 = imgr.makeVariable("arg1"); + IntegerFormula var2 = imgr.makeVariable("arg2"); + assertThatFormula( + bmgr.implication( + imgr.equal(var1, var2), + imgr.equal(imgr.modulo(var1, zero), imgr.modulo(var2, zero)))) + .isTautological(); + } + @Test public void distinctTest() throws SolverException, InterruptedException { requireIntegers(); diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index e75e8b7ff0..36411bb61e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -257,23 +257,17 @@ public void intTest3_DivModLinear() throws SolverException, InterruptedException assertDivision(a, num3, numNeg4, aEqNeg10); assertDivision(a, numNeg3, num4, aEqNeg10); - switch (solverToUse()) { - case MATHSAT5: // modulo not supported - assertThrows(UnsupportedOperationException.class, () -> buildModulo(num10, num5, num0)); - break; - default: - assertModulo(num10, num5, num0); - assertModulo(num10, num3, num1, aEq10); - assertModulo(numNeg10, num5, num0); - assertModulo(numNeg10, num3, num2); - assertModulo(numNeg10, numNeg3, num2); - - assertModulo(a, num5, num0, aEq10); - assertModulo(a, num3, num1, aEq10); - assertModulo(a, num5, num0, aEqNeg10); - assertModulo(a, num3, num2, aEqNeg10); - assertModulo(a, numNeg3, num2, aEqNeg10); - } + assertModulo(num10, num5, num0); + assertModulo(num10, num3, num1, aEq10); + assertModulo(numNeg10, num5, num0); + assertModulo(numNeg10, num3, num2); + assertModulo(numNeg10, numNeg3, num2); + + assertModulo(a, num5, num0, aEq10); + assertModulo(a, num3, num1, aEq10); + assertModulo(a, num5, num0, aEqNeg10); + assertModulo(a, num3, num2, aEqNeg10); + assertModulo(a, numNeg3, num2, aEqNeg10); } @Test @@ -319,8 +313,7 @@ public void intTest3_DivModLinear_zeroDenominator() throws SolverException, Inte IllegalArgumentException.class, () -> assertThatFormula(buildModulo(num10, num0, num10)).isSatisfiable()); break; - case OPENSMT: // INFO - case MATHSAT5: // modulo not supported + case OPENSMT: // INFO: OpenSMT does not allow division by zero assertThrows(UnsupportedOperationException.class, () -> buildModulo(num10, num0, num10)); break; default: @@ -365,11 +358,6 @@ public void intTest3_DivModNonLinear() throws SolverException, InterruptedExcept assertThrows(UnsupportedOperationException.class, () -> buildDivision(a, b, num5)); assertThrows(UnsupportedOperationException.class, () -> buildModulo(a, b, num0)); break; - case MATHSAT5: // modulo not supported - assertDivision(a, b, num5, aEq10, bEq2); - assertDivision(a, b, num5, aEqNeg10, bEqNeg2); - assertThrows(UnsupportedOperationException.class, () -> buildModulo(num10, num5, num0)); - break; default: assertDivision(a, b, num5, aEq10, bEq2); assertDivision(a, b, num5, aEqNeg10, bEqNeg2); @@ -753,7 +741,7 @@ public void testMakeBitVectorArray() { switch (solver) { case MATHSAT5: // Mathsat5 has a different internal representation of the formula - assertThat(_b_at_i.toString()).isEqualTo("(`read_T(18)_T(20)` b i)"); + assertThat(_b_at_i.toString()).isEqualTo("(`read_T(19)_T(21)` b i)"); break; case BOOLECTOR: assume() @@ -784,7 +772,7 @@ public void testNestedIntegerArray() { switch (solver) { case MATHSAT5: assertThat(valueInMulti.toString()) - .isEqualTo("(`read_int_int` (`read_int_T(17)` multi i) i)"); + .isEqualTo("(`read_int_int` (`read_int_T(18)` multi i) i)"); break; case PRINCESS: assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); @@ -812,7 +800,7 @@ public void testNestedRationalArray() { switch (solver) { case MATHSAT5: assertThat(valueInMulti.toString()) - .isEqualTo("(`read_int_rat` (`read_int_T(17)` multi i) i)"); + .isEqualTo("(`read_int_rat` (`read_int_T(18)` multi i) i)"); break; case PRINCESS: assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); @@ -845,8 +833,8 @@ public void testNestedBitVectorArray() { switch (solver) { case MATHSAT5: - String readWrite = "(`read_int_T(18)` (`read_int_T(19)` multi i) i)"; - assertThat(valueInMulti.toString()).isEqualTo(readWrite); + assertThat(valueInMulti.toString()) + .isEqualTo("(`read_int_T(19)` (`read_int_T(20)` multi " + "i) i)"); break; default: assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)");