- removed all define-fun tests, because they didn't even test define-fun and JavaSMT does not support it.

Author: DavidGalllob

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

@@ -3145,164 +3145,6 @@ public void testExceptionPush()
 
   /*PARSE MODEL TESTS*/
 
-  @Test
-  public void testDefineFunctionBoolEmptyInput()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-
-    String x = "(define-fun bla () Bool true)\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-
-    BooleanFormula constraint = bmgr.makeTrue();
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionBoolWithInput()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireBooleanUFs();
-
-    String x = "(define-fun bla ((x Bool)) Bool (= x true))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-
-    BooleanFormula constraint = bmgr.makeTrue();
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionInt()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireIntegers();
-
-    String x = "(define-fun bla () Int (- 3 4))\n" + "(assert (= bla bla))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-    IntegerFormula drei = imgr.makeNumber(3);
-    IntegerFormula vier = imgr.makeNumber(4);
-    IntegerFormula sub = imgr.subtract(drei, vier);
-    BooleanFormula constraint = imgr.equal(sub, sub);
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionIntWithInput()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireIntegers();
-
-    String x = "(define-fun bla ((x Int)) Int (- 3 x))\n" + "(assert (= bla bla))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-    IntegerFormula drei = imgr.makeNumber(3);
-    IntegerFormula xVar = imgr.makeVariable("x");
-    IntegerFormula sub = imgr.subtract(drei, xVar);
-    BooleanFormula constraint = imgr.equal(sub, sub);
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionReal()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireRationals();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.OPENSMT);
-
-    String x = "(define-fun bla () Real (- 3 4.0))\n" + "(assert (= bla bla))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-    IntegerFormula drei = imgr.makeNumber(3);
-    RationalFormula vier = Objects.requireNonNull(rmgr).makeNumber(4.0);
-    RationalFormula sub = rmgr.subtract(drei, vier);
-    BooleanFormula constraint = rmgr.equal(sub, sub);
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionRealWithInput()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireRationals();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.OPENSMT);
-
-    String x = "(define-fun bla ((x Real)) Real (- 3 x))\n" + "(assert (= bla bla))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-    IntegerFormula drei = imgr.makeNumber(3);
-    RationalFormula xVar = Objects.requireNonNull(rmgr).makeVariable("x");
-    RationalFormula sub = rmgr.subtract(drei, xVar);
-    BooleanFormula constraint = rmgr.equal(sub, sub);
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionBitVec()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireBitvectors();
-
-    String x =
-        "(define-fun bla () (_ BitVec 5) (bvsub #b10000 #b00001))\n" + "(assert (= bla bla))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-    BitvectorFormula first = Objects.requireNonNull(bvmgr).makeBitvector(5, 16);
-    BitvectorFormula second = bvmgr.makeBitvector(5, 1);
-    BitvectorFormula sub = bvmgr.subtract(first, second);
-    BooleanFormula constraint = bvmgr.equal(sub, sub);
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionBitVecWithInput()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireBitvectors();
-
-    String x =
-        "(define-fun bla ((x (_ BitVec 5))) (_ BitVec 5) (bvsub #b10000 x))\n"
-            + "(assert (= bla bla))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-    BitvectorFormula first = Objects.requireNonNull(bvmgr).makeBitvector(5, 16);
-    BitvectorFormula second = bvmgr.makeVariable(5, "x");
-    BitvectorFormula sub = bvmgr.subtract(first, second);
-    BooleanFormula constraint = bvmgr.equal(sub, sub);
-
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  @Test
-  public void testDefineFunctionArray()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireIntegers();
-    requireArrays();
-
-    String x =
-        "(declare-const a (Array Int Int))\n"
-            + "(define-fun bla () (Array Int Int) a)\n"
-            + "(assert (= a a))\n";
-    BooleanFormula actualResult = mgr.universalParseFromString(x);
-
-    ArrayFormula<IntegerFormula, IntegerFormula> a =
-        Objects.requireNonNull(amgr)
-            .makeArray("a", FormulaType.IntegerType, FormulaType.IntegerType);
-    BooleanFormula constraint = amgr.equivalence(a, a);
-    BooleanFormula expectedResult = constraint;
-
-    assertThat(actualResult).isEqualTo(expectedResult);
-  }
-
-  /* OTHER FUNCTION TESTS*/
 
   @Test
   public void testLetExpression()