Tests: Enable tests that were previously disabled, but are now running fine

Author: daniel-raffler

src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java

@@ -269,13 +269,12 @@ public void testDisjunctionArgsExtractionRecursive()
 
   @Test
   public void simplificationTest() {
-    // Boolector and CVC5 fail this as it either simplifies to much, or nothing
-    // TODO: maybe this is just a matter of options, check!
+    // Boolector fail this as it either simplifies to much, or nothing
     assume()
         .withMessage(
             "Solver %s fails on this test as it does not simplify any formulas.", solverToUse())
         .that(solverToUse())
-        .isNoneOf(Solvers.BOOLECTOR, Solvers.CVC5);
+        .isNotEqualTo(Solvers.BOOLECTOR);
 
     BooleanFormula tru = bmgr.makeBoolean(true);
     BooleanFormula fals = bmgr.makeBoolean(false);

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -1082,15 +1082,12 @@ private List<Float> getListOfFloats() {
             Float.POSITIVE_INFINITY,
             Float.NEGATIVE_INFINITY,
             0.0f,
+            -0.0f,
             1f,
             -1f,
             2f,
             -2f);
 
-    if (solverToUse() != Solvers.MATHSAT5) {
-      flts.add(-0.0f); // MathSat5 fails for NEGATIVE_ZERO
-    }
-
     for (int i = 1; i < 10; i++) {
       for (int j = 1; j < 10; j++) {
         flts.add((float) (i * Math.pow(10, j)));
@@ -1119,15 +1116,12 @@ private List<Double> getListOfDoubles() {
             Double.POSITIVE_INFINITY,
             Double.NEGATIVE_INFINITY,
             0.0,
+            -0.0,
             1d,
             -1d,
             2d,
             -2d);
 
-    if (solverToUse() != Solvers.MATHSAT5) {
-      dbls.add(-0.0); // MathSat5 fails for NEGATIVE_ZERO
-    }
-
     for (int i = 1; i < 10; i++) {
       for (int j = 1; j < 10; j++) {
         dbls.add(i * Math.pow(10, j));

src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java

@@ -165,7 +165,6 @@ public void test_ABVIRA() {
     requireBitvectors();
     requireIntegers();
     requireRationals();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     String query =
         NUMERAL_VARS
             + BV_VARS
@@ -180,7 +179,6 @@ public void test_ABV() {
     requireArrays();
     requireQuantifiers();
     requireBitvectors();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     String query =
         BOOL_VARS
             + BV_VARS
@@ -195,7 +193,6 @@ public void test_QF_AUFBV() {
     requireParser();
     requireArrays();
     requireBitvectors();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     String query = BV_VARS + "(assert (and (= bv bv2) (= bvarr bvarr2) (= (bvfoo bv) bv2)" + "))";
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_AUFBV");
@@ -205,7 +202,8 @@ public void test_QF_AUFBV() {
   public void test_QF_BV() {
     requireParser();
     requireBitvectors();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
+    // Princess rewrites the formula and replaces the bitvector constant with an integer term
+    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
     String query = BV_VARS + "(assert (bvult bv (bvadd bv #x1)))";
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_BV");
@@ -236,7 +234,6 @@ public void test_QF_NIA() {
     requireIntegers();
     requireNonlinear();
     String query = NUMERAL_VARS + "(assert (< xx (* x x)))";
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_NIA");
   }
@@ -258,7 +255,6 @@ public void test_QF_UFLIRA() {
     requireIntegers();
     requireRationals(); // NUMERAL_VARS includes REALs
     String query = NUMERAL_VARS + "(assert (= (foo x) x))";
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_UF");
   }
@@ -271,11 +267,11 @@ public void test_QF_UF() {
         .withMessage("MathSAT does not support functions with Bool arguments")
         .that(solverToUse())
         .isNotEqualTo(Solvers.MATHSAT5);
-    classifier.visit(mgr.parse(query));
     assume()
+        .withMessage("Princess will rewrite UFs with boolean arguments")
         .that(solverToUse())
-        .isNotEqualTo(Solvers.PRINCESS); // Princess classifies it as QF_UFLIA
-    // TODO: see why Princess classifies this wrongly
+        .isNotEqualTo(Solvers.PRINCESS);
+    classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_UF");
   }
 
@@ -285,7 +281,6 @@ public void test_QF_UFBVLIRA() {
     requireBitvectors();
     requireRationals();
     requireIntegers();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     String query = NUMERAL_VARS + BV_VARS + "(assert (and (= bv bv2) (= (foo x) x)))";
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_UFBV");
@@ -295,7 +290,6 @@ public void test_QF_UFBVLIRA() {
   public void test_QF_UFBV() {
     requireParser();
     requireBitvectors();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     String query = BV_VARS + "(assert (and (= bv bv2) (= (bvfoo bv) bv2)))";
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_UFBV");
@@ -307,7 +301,6 @@ public void test_QF_UFLIRA2() {
     requireIntegers();
     requireRationals(); // NUMERAL_VARS includes REALs
     String query = NUMERAL_VARS + "(assert (< xx (+ x (foo x))))";
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     classifier.visit(mgr.parse(query));
     assertThat(classifier.toString()).isEqualTo("QF_UFLIA");
   }
@@ -349,7 +342,7 @@ public void test_UFNRA() {
     requireParser();
     requireRationals();
     requireNonlinear();
-    requireQuantifiers(); // TODO SMTInterpol fails when parsing this
+    requireQuantifiers();
     String query = NUMERAL_VARS + "(assert (exists ((zz Real)) (< (* y yy) (bar y))))";
     assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula
     classifier.visit(mgr.parse(query));

src/org/sosy_lab/java_smt/test/FormulaManagerTest.java

@@ -35,7 +35,6 @@ public class FormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBase
   public void testEmptySubstitution() throws SolverException, InterruptedException {
     requireSubstitution();
     requireIntegers();
-    assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS);
 
     IntegerFormula variable1 = imgr.makeVariable("variable1");
     IntegerFormula variable2 = imgr.makeVariable("variable2");
@@ -56,7 +55,6 @@ public void testEmptySubstitution() throws SolverException, InterruptedException
   public void testNoSubstitution() throws SolverException, InterruptedException {
     requireSubstitution();
     requireIntegers();
-    assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS);
 
     IntegerFormula variable1 = imgr.makeVariable("variable1");
     IntegerFormula variable2 = imgr.makeVariable("variable2");

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

@@ -199,11 +199,6 @@ public <T> void binaryInterpolationWithConstantFalse()
   public <T> void binaryBVInterpolation1() throws SolverException, InterruptedException {
     requireBitvectors();
 
-    assume()
-        .withMessage("Solver %s runs into timeout on this test", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
     int i = index.getFreshId();

src/org/sosy_lab/java_smt/test/ModelTest.java

@@ -1155,7 +1155,7 @@ public void testGetArrays3() throws SolverException, InterruptedException {
     assume()
         .withMessage("As of now, only Princess does not support multi-dimensional arrays")
         .that(solver)
-        .isNotSameInstanceAs(Solvers.PRINCESS);
+        .isNotEqualTo(Solvers.PRINCESS);
 
     // create formula for "arr[5][3][1]==x && x==123"
     BooleanFormula f =
@@ -1741,12 +1741,7 @@ private void checkModelAssignmentsValid(
   public void ufTest() throws SolverException, InterruptedException {
     requireQuantifiers();
     requireBitvectors();
-    // only Z3 fulfills these requirements
-
-    assume()
-        .withMessage("solver does not implement optimisation")
-        .that(solverToUse())
-        .isEqualTo(Solvers.Z3);
+    requireOptimization();
 
     BitvectorType t32 = FormulaType.getBitvectorTypeWithSize(32);
     FunctionDeclaration<BitvectorFormula> si1 = fmgr.declareUF("*signed_int@1", t32, t32);

src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java

@@ -117,11 +117,6 @@ private SolverException handleSolverException(SolverException e) throws SolverEx
 
   @Test
   public void testLIAForallArrayConjunctUnsat() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT
     setUpLIA();
 
@@ -134,15 +129,8 @@ public void testLIAForallArrayConjunctUnsat() throws SolverException, Interrupte
 
   @Test
   public void testBVForallArrayConjunctUnsat() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT
     setUpBV();
-    // Princess does not support bitvectors in arrays
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula f =
         bmgr.and(
@@ -184,8 +172,6 @@ public void testBVForallArrayConjunctSat() throws SolverException, InterruptedEx
 
     // (forall x . b[x] = 0) AND (b[123] = 0) is SAT
     setUpBV();
-    // Princess does not support bitvectors in arrays
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula f =
         bmgr.and(
@@ -246,11 +232,6 @@ public void testLIAForallArrayDisjunctSat2() throws SolverException, Interrupted
 
   @Test
   public void testLIANotExistsArrayConjunct1() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     // (not exists x . not b[x] = 0) AND (b[123] = 1) is UNSAT
     setUpLIA();
     BooleanFormula f =
@@ -286,11 +267,6 @@ public void testLIANotExistsArrayConjunct2() throws SolverException, Interrupted
 
   @Test
   public void testLIANotExistsArrayConjunct3() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     // (not exists x . b[x] = 0) AND (b[123] = 0) is UNSAT
     setUpLIA();
     BooleanFormula f =
@@ -358,8 +334,6 @@ public void testLIAExistsArrayConjunct1() throws SolverException, InterruptedExc
   public void testBVExistsArrayConjunct1() throws SolverException, InterruptedException {
     // (exists x . b[x] = 0) AND (b[123] = 1) is SAT
     setUpBV();
-    // Princess does not support bitvectors in arrays
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula f =
         bmgr.and(
@@ -373,11 +347,6 @@ public void testBVExistsArrayConjunct1() throws SolverException, InterruptedExce
   @Test
   public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedException {
     setUpLIA();
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     // (exists x . b[x] = 1) AND  (forall x . b[x] = 0) is UNSAT
 
     BooleanFormula f =
@@ -387,15 +356,8 @@ public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedExc
 
   @Test
   public void testBVExistsArrayConjunct2() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT
     setUpBV();
-    // Princess does not support bitvectors in arrays
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula f =
         bmgr.and(qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_1), bv_forall_x_a_at_x_eq_0);
@@ -463,8 +425,10 @@ public void testLIAExistsArrayDisjunct1() throws SolverException, InterruptedExc
   public void testBVExistsArrayDisjunct1() throws SolverException, InterruptedException {
     // (exists x . b[x] = 0) OR (forall x . b[x] = 1) is SAT
     setUpBV();
-    // Princess does not support bitvectors in arrays
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
+    assume()
+        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula f =
         bmgr.or(
@@ -489,8 +453,6 @@ public void testLIAExistsArrayDisjunct2() throws SolverException, InterruptedExc
   public void testBVExistsArrayDisjunct2() throws SolverException, InterruptedException {
     // (exists x . b[x] = 1) OR (exists x . b[x] = 1) is SAT
     setUpBV();
-    // Princess does not support bitvectors in arrays
-    assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
 
     BooleanFormula f =
         bmgr.or(
@@ -822,11 +784,6 @@ public void testIntrospectionExistsInteger() {
 
   @Test
   public void testEmpty() {
-    assume()
-        .withMessage("TODO: The JavaSMT code for Princess explicitly allows this.")
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.PRINCESS);
-
     // An empty list of quantified variables throws an exception.
     assertThrows(
         IllegalArgumentException.class,
@@ -884,11 +841,10 @@ public void checkBVQuantifierEliminationFail() throws InterruptedException, Solv
     requireBitvectors();
     requireQuantifierElimination();
     // 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.PRINCESS);
+        .isNotEqualTo(Solvers.CVC5);
 
     int width = 2;
     BitvectorFormula xx = bvmgr.makeVariable(width, "x_bv");
@@ -941,8 +897,6 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE
     // quantifier-free equivalent: (and (= b2 #x00000006)
     //                                  (= a3 #x00000000))
 
-    // Z3 fails this currently. Remove once that's not longer the case!
-    assume().that(solverToUse()).isNotEqualTo(Solvers.Z3);
     int width = 32;
 
     BitvectorFormula a2 = bvmgr.makeVariable(width, "a2");
@@ -968,11 +922,6 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE
   @Test
   public void testExistsRestrictedRange() throws SolverException, InterruptedException {
     setUpLIA();
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     ArrayFormula<IntegerFormula, IntegerFormula> b =
         amgr.makeArray("b", FormulaType.IntegerType, FormulaType.IntegerType);
     BooleanFormula bAtXEq1 = imgr.equal(amgr.select(b, x), imgr.makeNumber(1));
@@ -1026,10 +975,6 @@ public void testExistsRestrictedRangeWithoutInconclusiveSolvers()
   @Test
   public void testForallRestrictedRange() throws SolverException, InterruptedException {
     setUpLIA();
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
 
     ArrayFormula<IntegerFormula, IntegerFormula> b =
         amgr.makeArray("b", FormulaType.IntegerType, FormulaType.IntegerType);

src/org/sosy_lab/java_smt/test/SolverAllSatTest.java

@@ -77,9 +77,6 @@ public void setupEnvironment() {
         // TODO how can we support allsat in MathSat5-interpolation-prover?
         assume().that(solverToUse()).isNotEqualTo(Solvers.MATHSAT5);
 
-        // CVC4 and Boolector do not support interpolation
-        assume().that(solverToUse()).isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.Z3);
-
         env = context.newProverEnvironmentWithInterpolation(ProverOptions.GENERATE_ALL_SAT);
         break;
 

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -349,7 +349,6 @@ protected void requireParser() {
   }
 
   protected void requireArrayModel() {
-    // INFO: OpenSmt does not support model generation for array
     assume()
         .withMessage("Solver %s does not support model generation for arrays", solverToUse())
         .that(solverToUse())