Skip to content

Commit 1834dee

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #459 from sosy-lab/mathsat-support-integer-mod
Add support for integer modulo in MathSAT
2 parents abfb233 + 40ec014 commit 1834dee

File tree

4 files changed

+122
-31
lines changed

4 files changed

+122
-31
lines changed

‎src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5IntegerFormulaManager.java

+23
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
package org.sosy_lab.java_smt.solvers.mathsat5;
1010

1111
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_divide;
12+
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal;
1213
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_floor;
1314
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_modular_congruence;
1415
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_number;
@@ -17,6 +18,7 @@
1718
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_term_ite;
1819
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_times;
1920

21+
import com.google.common.collect.ImmutableList;
2022
import java.math.BigDecimal;
2123
import java.math.BigInteger;
2224
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
@@ -26,9 +28,15 @@ class Mathsat5IntegerFormulaManager
2628
extends Mathsat5NumeralFormulaManager<IntegerFormula, IntegerFormula>
2729
implements IntegerFormulaManager {
2830

31+
// Reserved UF symbol for modulo(a,0)
32+
private final long modZeroUF;
33+
2934
Mathsat5IntegerFormulaManager(
3035
Mathsat5FormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic) {
3136
super(pCreator, pNonLinearArithmetic);
37+
modZeroUF =
38+
pCreator.declareUFImpl(
39+
"_%0", pCreator.getIntegerType(), ImmutableList.of(pCreator.getIntegerType()));
3240
}
3341

3442
@Override
@@ -69,6 +77,21 @@ public Long divide(Long pNumber1, Long pNumber2) {
6977
msat_make_floor(mathsatEnv, div));
7078
}
7179

80+
@Override
81+
protected Long modulo(Long pNumber1, Long pNumber2) {
82+
// The modulo can be calculated by the formula:
83+
// remainder = dividend - floor(dividend/divisor)*divisor
84+
// However, this will fail if the divisor is zero as SMTLIB then allows the solver to return
85+
// any value for the remainder. We solve this by first checking the divisor and returning an
86+
// UF symbol "modZeroUF(dividend)" if it is zero. Otherwise, the formula is used to calculate
87+
// the remainder.
88+
return msat_make_term_ite(
89+
mathsatEnv,
90+
msat_make_equal(mathsatEnv, pNumber2, msat_make_int_number(mathsatEnv, 0)),
91+
getFormulaCreator().callFunctionImpl(modZeroUF, ImmutableList.of(pNumber1)),
92+
subtract(pNumber1, multiply(divide(pNumber1, pNumber2), pNumber2)));
93+
}
94+
7295
@Override
7396
protected Long modularCongruence(Long pNumber1, Long pNumber2, BigInteger pModulo) {
7497
return modularCongruence0(pNumber1, pNumber2, pModulo.toString());

‎src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java

+8-2
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,12 @@ public void testModuloConstantUnsatisfiable() throws SolverException, Interrupte
110110
handleExpectedException(() -> imgr.modulo(a, imgr.makeNumber(3)))));
111111

112112
// INFO: OpenSMT does support modulo with constants
113-
if (ImmutableSet.of(Solvers.SMTINTERPOL, Solvers.CVC4, Solvers.YICES2, Solvers.OPENSMT)
113+
if (ImmutableSet.of(
114+
Solvers.SMTINTERPOL,
115+
Solvers.CVC4,
116+
Solvers.YICES2,
117+
Solvers.OPENSMT,
118+
Solvers.MATHSAT5)
114119
.contains(solver)
115120
&& nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
116121
// some solvers support modulo with constants
@@ -148,7 +153,8 @@ public void testModuloUnsatisfiable() throws SolverException, InterruptedExcepti
148153
imgr.makeNumber(1),
149154
handleExpectedException(() -> imgr.modulo(imgr.makeNumber(5), a))));
150155

151-
if (Solvers.CVC4 == solver && nonLinearArithmetic != NonLinearArithmetic.APPROXIMATE_ALWAYS) {
156+
if (ImmutableSet.of(Solvers.CVC4, Solvers.MATHSAT5).contains(solver)
157+
&& nonLinearArithmetic != NonLinearArithmetic.APPROXIMATE_ALWAYS) {
152158
// some solvers support non-linear multiplication (partially)
153159
assertThatFormula(f).isUnsatisfiable();
154160

‎src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java

+74
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,14 @@
99
package org.sosy_lab.java_smt.test;
1010

1111
import static com.google.common.truth.Truth.assertThat;
12+
import static com.google.common.truth.TruthJUnit.assume;
1213
import static org.junit.Assert.assertThrows;
1314

1415
import com.google.common.collect.ImmutableList;
1516
import java.util.ArrayList;
1617
import java.util.List;
1718
import org.junit.Test;
19+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
1820
import org.sosy_lab.java_smt.api.BooleanFormula;
1921
import org.sosy_lab.java_smt.api.Formula;
2022
import org.sosy_lab.java_smt.api.FormulaType;
@@ -26,6 +28,78 @@
2628

2729
public class NumeralFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
2830

31+
@Test
32+
public void divZeroTest() throws SolverException, InterruptedException {
33+
requireIntegers();
34+
assume().that(solver).isNoneOf(Solvers.OPENSMT, Solvers.YICES2); // No division by zero
35+
36+
IntegerFormula zero = imgr.makeNumber(0);
37+
IntegerFormula three = imgr.makeNumber(3);
38+
IntegerFormula seven = imgr.makeNumber(7);
39+
40+
// Show that 3/0=0 and 3/0=7 can hold separately
41+
IntegerFormula f1 = imgr.divide(three, zero);
42+
assertThatFormula(imgr.equal(f1, zero)).isSatisfiable();
43+
assertThatFormula(imgr.equal(f1, seven)).isSatisfiable();
44+
45+
// But if 3/0=0 in the model, it can't also be another value
46+
IntegerFormula var = imgr.makeVariable("var");
47+
IntegerFormula f2 = imgr.divide(var, zero);
48+
IntegerFormula res = imgr.makeVariable("res");
49+
assertThatFormula(
50+
bmgr.and(
51+
imgr.equal(f1, zero),
52+
imgr.equal(var, three),
53+
imgr.equal(f2, res),
54+
bmgr.not(imgr.equal(res, zero))))
55+
.isUnsatisfiable();
56+
57+
// Show that a=b => a/0=b/0
58+
IntegerFormula var1 = imgr.makeVariable("arg1");
59+
IntegerFormula var2 = imgr.makeVariable("arg2");
60+
assertThatFormula(
61+
bmgr.implication(
62+
imgr.equal(var1, var2),
63+
imgr.equal(imgr.divide(var1, zero), imgr.divide(var2, zero))))
64+
.isTautological();
65+
}
66+
67+
@Test
68+
public void modZeroTest() throws SolverException, InterruptedException {
69+
requireIntegers();
70+
assume().that(solver).isNoneOf(Solvers.OPENSMT, Solvers.YICES2); // No division by zero
71+
72+
IntegerFormula zero = imgr.makeNumber(0);
73+
IntegerFormula three = imgr.makeNumber(3);
74+
IntegerFormula seven = imgr.makeNumber(7);
75+
76+
// Show that 3%0=0 and 3%0=7 can hold separately
77+
IntegerFormula f1 = imgr.modulo(three, zero);
78+
assertThatFormula(imgr.equal(f1, zero)).isSatisfiable();
79+
assertThatFormula(imgr.equal(f1, seven)).isSatisfiable();
80+
81+
// But if 3%0=0 in the model, it can't also be another value
82+
IntegerFormula var = imgr.makeVariable("var");
83+
IntegerFormula f2 = imgr.modulo(var, zero);
84+
IntegerFormula res = imgr.makeVariable("res");
85+
assertThatFormula(
86+
bmgr.and(
87+
imgr.equal(f1, zero),
88+
imgr.equal(var, three),
89+
imgr.equal(f2, res),
90+
bmgr.not(imgr.equal(res, zero))))
91+
.isUnsatisfiable();
92+
93+
// Show that a=b => a%0=b%0
94+
IntegerFormula var1 = imgr.makeVariable("arg1");
95+
IntegerFormula var2 = imgr.makeVariable("arg2");
96+
assertThatFormula(
97+
bmgr.implication(
98+
imgr.equal(var1, var2),
99+
imgr.equal(imgr.modulo(var1, zero), imgr.modulo(var2, zero))))
100+
.isTautological();
101+
}
102+
29103
@Test
30104
public void distinctTest() throws SolverException, InterruptedException {
31105
requireIntegers();

‎src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java

+17-29
Original file line numberDiff line numberDiff line change
@@ -257,23 +257,17 @@ public void intTest3_DivModLinear() throws SolverException, InterruptedException
257257
assertDivision(a, num3, numNeg4, aEqNeg10);
258258
assertDivision(a, numNeg3, num4, aEqNeg10);
259259

260-
switch (solverToUse()) {
261-
case MATHSAT5: // modulo not supported
262-
assertThrows(UnsupportedOperationException.class, () -> buildModulo(num10, num5, num0));
263-
break;
264-
default:
265-
assertModulo(num10, num5, num0);
266-
assertModulo(num10, num3, num1, aEq10);
267-
assertModulo(numNeg10, num5, num0);
268-
assertModulo(numNeg10, num3, num2);
269-
assertModulo(numNeg10, numNeg3, num2);
270-
271-
assertModulo(a, num5, num0, aEq10);
272-
assertModulo(a, num3, num1, aEq10);
273-
assertModulo(a, num5, num0, aEqNeg10);
274-
assertModulo(a, num3, num2, aEqNeg10);
275-
assertModulo(a, numNeg3, num2, aEqNeg10);
276-
}
260+
assertModulo(num10, num5, num0);
261+
assertModulo(num10, num3, num1, aEq10);
262+
assertModulo(numNeg10, num5, num0);
263+
assertModulo(numNeg10, num3, num2);
264+
assertModulo(numNeg10, numNeg3, num2);
265+
266+
assertModulo(a, num5, num0, aEq10);
267+
assertModulo(a, num3, num1, aEq10);
268+
assertModulo(a, num5, num0, aEqNeg10);
269+
assertModulo(a, num3, num2, aEqNeg10);
270+
assertModulo(a, numNeg3, num2, aEqNeg10);
277271
}
278272

279273
@Test
@@ -319,8 +313,7 @@ public void intTest3_DivModLinear_zeroDenominator() throws SolverException, Inte
319313
IllegalArgumentException.class,
320314
() -> assertThatFormula(buildModulo(num10, num0, num10)).isSatisfiable());
321315
break;
322-
case OPENSMT: // INFO
323-
case MATHSAT5: // modulo not supported
316+
case OPENSMT: // INFO: OpenSMT does not allow division by zero
324317
assertThrows(UnsupportedOperationException.class, () -> buildModulo(num10, num0, num10));
325318
break;
326319
default:
@@ -365,11 +358,6 @@ public void intTest3_DivModNonLinear() throws SolverException, InterruptedExcept
365358
assertThrows(UnsupportedOperationException.class, () -> buildDivision(a, b, num5));
366359
assertThrows(UnsupportedOperationException.class, () -> buildModulo(a, b, num0));
367360
break;
368-
case MATHSAT5: // modulo not supported
369-
assertDivision(a, b, num5, aEq10, bEq2);
370-
assertDivision(a, b, num5, aEqNeg10, bEqNeg2);
371-
assertThrows(UnsupportedOperationException.class, () -> buildModulo(num10, num5, num0));
372-
break;
373361
default:
374362
assertDivision(a, b, num5, aEq10, bEq2);
375363
assertDivision(a, b, num5, aEqNeg10, bEqNeg2);
@@ -753,7 +741,7 @@ public void testMakeBitVectorArray() {
753741
switch (solver) {
754742
case MATHSAT5:
755743
// Mathsat5 has a different internal representation of the formula
756-
assertThat(_b_at_i.toString()).isEqualTo("(`read_T(18)_T(20)` b i)");
744+
assertThat(_b_at_i.toString()).isEqualTo("(`read_T(19)_T(21)` b i)");
757745
break;
758746
case BOOLECTOR:
759747
assume()
@@ -784,7 +772,7 @@ public void testNestedIntegerArray() {
784772
switch (solver) {
785773
case MATHSAT5:
786774
assertThat(valueInMulti.toString())
787-
.isEqualTo("(`read_int_int` (`read_int_T(17)` multi i) i)");
775+
.isEqualTo("(`read_int_int` (`read_int_T(18)` multi i) i)");
788776
break;
789777
case PRINCESS:
790778
assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)");
@@ -812,7 +800,7 @@ public void testNestedRationalArray() {
812800
switch (solver) {
813801
case MATHSAT5:
814802
assertThat(valueInMulti.toString())
815-
.isEqualTo("(`read_int_rat` (`read_int_T(17)` multi i) i)");
803+
.isEqualTo("(`read_int_rat` (`read_int_T(18)` multi i) i)");
816804
break;
817805
case PRINCESS:
818806
assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)");
@@ -845,8 +833,8 @@ public void testNestedBitVectorArray() {
845833

846834
switch (solver) {
847835
case MATHSAT5:
848-
String readWrite = "(`read_int_T(18)` (`read_int_T(19)` multi i) i)";
849-
assertThat(valueInMulti.toString()).isEqualTo(readWrite);
836+
assertThat(valueInMulti.toString())
837+
.isEqualTo("(`read_int_T(19)` (`read_int_T(20)` multi " + "i) i)");
850838
break;
851839
default:
852840
assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)");

0 commit comments

Comments
 (0)