Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for integer modulo in MathSAT #459

Merged
merged 5 commits into from
Mar 22, 2025
Merged

Add support for integer modulo in MathSAT #459

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c3cd334
MathSAT: Add support for integer modulo
daniel-raffler Mar 18, 2025
65fbbe4
MathSAT: Enable modulo support for integer formulas in the tests
daniel-raffler Mar 18, 2025
b41f3fc
MathSAT: Add special treatment for integer modulo when the divisor is…
daniel-raffler Mar 18, 2025
e04d83c
MathSAT: Fix broken tests
daniel-raffler Mar 18, 2025
40ec014
Add tests for division by zero
daniel-raffler Mar 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 23 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5IntegerFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -26,9 +28,15 @@ class Mathsat5IntegerFormulaManager
extends Mathsat5NumeralFormulaManager<IntegerFormula, IntegerFormula>
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
Expand Down Expand Up @@ -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)));
}

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Be aware that UFs return the same value for the same parameters.
If SMTLIB allows "any return value", then the return value could be random and return a different result at second call.
From technical point, returning the same result on second call would be fully ok for me. From SMTLIB point, please check what the standard and other solvers return for x/0 == x/0. Is this always satisfied?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Be aware that UFs return the same value for the same parameters

I've added some test in the last commit, and this seems to match what the other solvers are doing.

SMTLIB says:

"Since in SMT-LIB logic all function symbols are interpreted as total
 functions, terms of the form (/ t 0) *are* meaningful in every 
 instance of Reals. However, the declaration imposes no constraints
 on their value. This means in particular that 
 - for every instance theory T and
 - for every value v (as defined in the :values attribute) and 
   closed term t of sort Real,
 there is a model of T that satisfies (= v (/ t 0)).
"

The definition talks about reals, but it also applies to integers. It's not entirely clear from it, but I would argue that x/0 == x/0 must hold as / is still a (mathematical) function and the same argument means that the result is the same.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Valid point. Lets approve it.

@Override
protected Long modularCongruence(Long pNumber1, Long pNumber2, BigInteger pModulo) {
return modularCongruence0(pNumber1, pNumber2, pModulo.toString());
Expand Down
10 changes: 8 additions & 2 deletions src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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();

Expand Down
74 changes: 74 additions & 0 deletions src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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();
Expand Down
46 changes: 17 additions & 29 deletions src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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)");
Expand Down Expand Up @@ -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)");
Expand Down Expand Up @@ -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)");
Expand Down