Merge pull request #449 from sosy-lab/remove_boolector_quantifiers_standalone

Remove boolector quantifiers standalone

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java

@@ -18,7 +18,6 @@ final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, L
       BoolectorUFManager pFunctionManager,
       BoolectorBooleanFormulaManager pBooleanManager,
       BoolectorBitvectorFormulaManager pBitvectorManager,
-      BoolectorQuantifiedFormulaManager pQuantifierManager,
       BoolectorArrayFormulaManager pArrayManager) {
     super(
         pFormulaCreator,
@@ -28,7 +27,7 @@ final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, L
         null,
         pBitvectorManager,
         null,
-        pQuantifierManager,
+        null,
         pArrayManager,
         null,
         null,

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorQuantifiedFormulaManager.java

@@ -94,12 +94,10 @@ public static BoolectorSolverContext create(
     BoolectorBooleanFormulaManager booleanTheory = new BoolectorBooleanFormulaManager(creator);
     BoolectorBitvectorFormulaManager bitvectorTheory =
         new BoolectorBitvectorFormulaManager(creator, booleanTheory);
-    BoolectorQuantifiedFormulaManager quantifierTheory =
-        new BoolectorQuantifiedFormulaManager(creator);
     BoolectorArrayFormulaManager arrayTheory = new BoolectorArrayFormulaManager(creator);
     BoolectorFormulaManager manager =
         new BoolectorFormulaManager(
-            creator, functionTheory, booleanTheory, bitvectorTheory, quantifierTheory, arrayTheory);
+            creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory);
     return new BoolectorSolverContext(manager, creator, pShutdownNotifier);
   }
 

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java

@@ -85,10 +85,6 @@ public void setUpBV() {
     requireBitvectors();
     requireArrays();
     requireQuantifiers();
-    assume()
-        .withMessage("Solver %s does not support quantifiers via JavaSMT", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.BOOLECTOR);
 
     xbv = bvmgr.makeVariable(bvWidth, "xbv");
     bvArray =
@@ -143,8 +139,6 @@ public void testBVForallArrayConjunctUnsat() throws SolverException, Interrupted
     requireBitvectors();
     // Princess does not support bitvectors in arrays
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula f =
         bmgr.and(
@@ -188,8 +182,6 @@ public void testBVForallArrayConjunctSat() throws SolverException, InterruptedEx
     requireBitvectors();
     // Princess does not support bitvectors in arrays
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula f =
         bmgr.and(
@@ -364,8 +356,6 @@ public void testBVExistsArrayConjunct1() throws SolverException, InterruptedExce
     requireBitvectors();
     // Princess does not support bitvectors in arrays
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula f =
         bmgr.and(
@@ -402,8 +392,6 @@ public void testBVExistsArrayConjunct2() throws SolverException, InterruptedExce
     requireBitvectors();
     // Princess does not support bitvectors in arrays
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula f =
         bmgr.and(qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_1), bv_forall_x_a_at_x_eq_0);
@@ -435,11 +423,10 @@ public void testBVExistsArrayConjunct3() throws SolverException, InterruptedExce
     // (exists x . b[x] = 0) AND (forall x . b[x] = 0) is SAT
     requireBitvectors();
     // Princess does not support bitvectors in arrays
-    // Boolector quants need to be reworked
     assume()
         .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
         .that(solverToUse())
-        .isNoneOf(Solvers.CVC5, Solvers.CVC4, Solvers.BOOLECTOR);
+        .isNoneOf(Solvers.CVC5, Solvers.CVC4);
 
     BooleanFormula f =
         bmgr.and(qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_0), bv_forall_x_a_at_x_eq_0);
@@ -474,8 +461,6 @@ public void testBVExistsArrayDisjunct1() throws SolverException, InterruptedExce
     requireBitvectors();
     // Princess does not support bitvectors in arrays
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula f =
         bmgr.or(
@@ -502,8 +487,6 @@ public void testBVExistsArrayDisjunct2() throws SolverException, InterruptedExce
     requireBitvectors();
     // Princess does not support bitvectors in arrays
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula f =
         bmgr.or(
@@ -526,8 +509,6 @@ public void testLIAContradiction() throws SolverException, InterruptedException
   public void testBVContradiction() throws SolverException, InterruptedException {
     // forall x . x = x+1 is UNSAT
     requireBitvectors();
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     int width = 16;
     BitvectorFormula z = bvmgr.makeVariable(width, "z");
@@ -555,8 +536,6 @@ public void testLIASimple() throws SolverException, InterruptedException {
   public void testBVSimple() throws SolverException, InterruptedException {
     // forall z . z+2 = z+1+1 is SAT
     requireBitvectors();
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     int width = 16;
     BitvectorFormula z = bvmgr.makeVariable(width, "z");
@@ -585,8 +564,6 @@ public void testLIAEquality() throws SolverException, InterruptedException {
   @Test
   public void testBVEquality() throws SolverException, InterruptedException {
     requireBitvectors();
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z");
     BitvectorFormula y = bvmgr.makeVariable(bvWidth, "y");
@@ -598,8 +575,6 @@ public void testBVEquality() throws SolverException, InterruptedException {
   @Test
   public void testBVEquality2() throws SolverException, InterruptedException {
     requireBitvectors();
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z");
     BitvectorFormula y = bvmgr.makeVariable(bvWidth, "y");
@@ -612,8 +587,6 @@ public void testBVEquality3() throws SolverException, InterruptedException {
     // exists z . (forall y . z = y && z + 2 > z)
     // UNSAT because of bv behaviour
     requireBitvectors();
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z");
     BitvectorFormula zPlusTwo =
@@ -644,8 +617,6 @@ public void testLIABoundVariables() throws SolverException, InterruptedException
   public void testBVBoundVariables() throws SolverException, InterruptedException {
     // If the free and bound vars are equal, this will be UNSAT
     requireBitvectors();
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
 
     int width = 2;
     BitvectorFormula aa = bvmgr.makeVariable(width, "aa");
@@ -803,12 +774,11 @@ public void checkBVQuantifierEliminationFail() throws InterruptedException, Solv
     // build formula: (exists x : arr[x] = 3) && (forall y: arr[y] = 2)
     // as there is no quantifier free equivalent, it should return the input formula.
     requireBitvectors();
-    // Boolector quants need to be reworked
     // Princess does not support bitvectors in arrays
     assume()
         .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
         .that(solverToUse())
-        .isNoneOf(Solvers.CVC5, Solvers.BOOLECTOR, Solvers.PRINCESS);
+        .isNoneOf(Solvers.CVC5, Solvers.PRINCESS);
 
     int width = 2;
     BitvectorFormula xx = bvmgr.makeVariable(width, "x_bv");
@@ -836,8 +806,6 @@ public void checkBVQuantifierElimination() throws InterruptedException, SolverEx
     // quantifier-free equivalent: x = 1 | x = 3
     //                      or     extract_0_0 x = 1
 
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
     int i = index.getFreshId();
     int width = 2;
 
@@ -862,8 +830,6 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE
     // quantifier-free equivalent: (and (= b2 #x00000006)
     //                                  (= a3 #x00000000))
 
-    // Boolector quants need to be reworked
-    assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR);
     // Z3 fails this currently. Remove once thats not longer the case!
     assume().that(solverToUse()).isNotEqualTo(Solvers.Z3);
     int width = 32;