- reverted defineFun changes

Author: DavidGalllob

src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java

@@ -56,6 +56,7 @@
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_assertContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_declareConstContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_declareFunContext;
+import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_defineFunContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_defineSortContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_popContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_pushContext;
@@ -2300,4 +2301,9 @@ public Object visitResp_get_model(Resp_get_modelContext ctx) {
     isModel = true;
     return visitChildren(ctx);
   }
+
+  @Override
+  public Object visitCmd_defineFun(Cmd_defineFunContext ctx) {
+    throw new UnsupportedOperationException("JavaSMT does not support \"define-fun\"");
+  }
 }

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

@@ -3145,165 +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()
       throws IOException, SolverException, InterruptedException, InvalidConfigurationException {

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

@@ -24,7 +24,7 @@
 import org.sosy_lab.java_smt.api.StringFormula;
 import org.sosy_lab.java_smt.basicimpl.Generator;
 
-@SuppressWarnings({"CheckReturnValue", "ReturnValueIgnored","EqualsIncompatibleType"})
+@SuppressWarnings({"CheckReturnValue", "ReturnValueIgnored", "EqualsIncompatibleType"})
 public class SMTLIB2StringTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
   @Before
   public void setUp() {
@@ -343,7 +343,6 @@ public void testRegexIntersection()
 
     BooleanFormula actualResult = mgr.universalParseFromString(x);
 
-
     assertThat(
         actualResult.equals(
             "(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (str.to_re " + "\"\\Qb\\E\")))"));