adding test where Princess failed before
Z3 seems to fail for this test.
@@ -25,6 +25,7 @@ import org.junit.runners.Parameterized.Parameters;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.BasicProverEnvironment;
import org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback;
+import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -188,4 +189,47 @@ public class SolverAllSatTest extends SolverBasedTest0 {
ImmutableList.of(ImmutableList.of(v1, v2), ImmutableList.of(v1, bmgr.not(v2))),
ImmutableList.of(ImmutableList.of(v1, bmgr.not(v2)), ImmutableList.of(v1, v2)));
}
+
+ @Test
+ public void allSatTest_withQuantifier() throws SolverException, InterruptedException {
+ requireBitvectors();
+ requireQuantifiers();
+
+ // (y = 1)
+ // & (PRED1 <-> (y = 1))
+ // & (PRED3 <-> ALL x_0. (3 * x_0 != y))
+ // query ALLSAT for predicates [PRED1, PRED3] --> {[PRED1, -PRED3]}
+
+ // ugly detail in bitvector theory: 2863311531*3=1 mod 2^32,
+ // thus the quantified part from above is FALSE.
+
+ int bitsize = 32;
+ BitvectorFormula y = bvmgr.makeVariable(bitsize, "y");
+ BitvectorFormula one = bvmgr.makeBitvector(bitsize, 1);
+ BitvectorFormula three = bvmgr.makeBitvector(bitsize, 3);
+ BitvectorFormula bound = bvmgr.makeVariable(bitsize, "x_0");
+ BooleanFormula pred1 = bmgr.makeVariable("pred1");
+ BooleanFormula pred3 = bmgr.makeVariable("pred3");
+
+ BooleanFormula query =
+ bmgr.and(
+ bvmgr.equal(y, one),
+ bmgr.equivalence(pred1, bvmgr.equal(y, one)),
+ bmgr.equivalence(
+ pred3,
+ qmgr.forall(
+ ImmutableList.of(bound),
+ bmgr.not(bvmgr.equal(y, bvmgr.multiply(three, bound))))));
+
+ env.push(query);
+
+ assertThatFormula(query).isSatisfiable();
+
+ TestAllSatCallback callback = new TestAllSatCallback();
+
+ assertThat(env.allSat(callback, ImmutableList.of(pred1, pred3))).isEqualTo(EXPECTED_RESULT);
+
+ assertThat(callback.models)
+ .isEqualTo(ImmutableList.of(ImmutableList.of(pred1, bmgr.not(pred3))));
+ }
}
