Cvc5: Fix parsing bug

src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java

@@ -581,13 +581,4 @@ public Object convertValue(
       @SuppressWarnings("unused") TFormulaInfo pAdditionalF, TFormulaInfo pF) {
     return convertValue(pF);
   }
-
-  /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */
-  protected static String dequote(String s) {
-    int l = s.length();
-    if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') {
-      return s.substring(1, l - 1);
-    }
-    return s;
-  }
 }

src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java

@@ -23,6 +23,15 @@ public final class Tokenizer {
 
   private Tokenizer() {}
 
+  /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */
+  public static String dequote(String s) {
+    int l = s.length();
+    if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') {
+      return s.substring(1, l - 1);
+    }
+    return s;
+  }
+
   /**
    * Split up a sequence of lisp expressions.
    *

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -56,6 +56,7 @@
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4ArrayFormula;
 import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4BitvectorFormula;
 import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4BooleanFormula;
@@ -304,7 +305,7 @@ static String getName(Expr e) {
     if (!e.isConst() && !e.isVariable()) {
       e = e.getOperator();
     }
-    return dequote(e.toString());
+    return Tokenizer.dequote(e.toString());
   }
 
   @SuppressWarnings("deprecation")

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -65,6 +65,7 @@
 import org.sosy_lab.java_smt.api.visitors.TraversalProcess;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5ArrayFormula;
 import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5BitvectorFormula;
 import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5BooleanFormula;
@@ -383,10 +384,10 @@ String getName(Term e) {
       // Functions are packaged like this: (functionName arg1 arg2 ...)
       // But can use |(name)| to enable () inside of the variable name
       // TODO what happens for function names containing whitespace?
-      String dequoted = dequote(repr);
+      String dequoted = Tokenizer.dequote(repr);
       return Iterables.get(Splitter.on(' ').split(dequoted.substring(1)), 0);
     } else {
-      return dequote(repr);
+      return Tokenizer.dequote(repr);
     }
   }
 
@@ -457,7 +458,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         return visitor.visitQuantifier((BooleanFormula) formula, quant, freeVars, fBody);
 
       } else if (f.getKind() == Kind.CONSTANT) {
-        return visitor.visitFreeVariable(formula, dequote(f.toString()));
+        return visitor.visitFreeVariable(formula, Tokenizer.dequote(f.toString()));
 
       } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) {
         checkState(

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Parser.java

@@ -34,6 +34,7 @@
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 import org.sosy_lab.common.collect.Collections3;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 
 class CVC5Parser {
 
@@ -251,7 +252,7 @@ private Map<Term, Term> getSymbolSubstitutions(
    * cached one is recorded in the given substitutions map.
    */
   private void registerNewTermSymbols(Term declaration, Map<Term, Term> substitutions) {
-    final String parsedTermString = declaration.toString();
+    final String parsedTermString = Tokenizer.dequote(declaration.toString());
     final Sort parsedSort = declaration.getSort();
     final String parsedSortString = parsedSort.toString();
 

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java

@@ -21,6 +21,7 @@
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtFormula.OpenSmtArrayFormula;
 import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtFormula.OpenSmtBooleanFormula;
 import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtFormula.OpenSmtIntegerFormula;
@@ -358,7 +359,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, PTRef f) {
 
     if (logic.isVar(f)) {
       String varName = logic.getSymName(logic.getSymRef(f));
-      return visitor.visitFreeVariable(formula, dequote(varName));
+      return visitor.visitFreeVariable(formula, Tokenizer.dequote(varName));
     }
 
     String varName = logic.getSymName(logic.getSymRef(f));

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java

@@ -33,6 +33,7 @@
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 
 class SmtInterpolFormulaCreator extends FormulaCreator<Term, Sort, Script, FunctionSymbol> {
 
@@ -212,7 +213,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula f, final Term input) {
         } else if (app.equals(environment.getTheory().mFalse)) {
           return visitor.visitConstant(f, false);
         } else if (func.getDefinition() == null) {
-          return visitor.visitFreeVariable(f, dequote(input.toString()));
+          return visitor.visitFreeVariable(f, Tokenizer.dequote(input.toString()));
         } else {
           throw new UnsupportedOperationException("Unexpected nullary function " + input);
         }
@@ -254,7 +255,7 @@ String getName(Term t) {
       assert t instanceof ApplicationTerm;
       return ((ApplicationTerm) t).getFunction().getName();
     } else {
-      return dequote(t.toString());
+      return Tokenizer.dequote(t.toString());
     }
   }
 

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

@@ -11,6 +11,7 @@
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.TruthJUnit.assume;
 import static org.junit.Assert.assertThrows;
+import static org.sosy_lab.java_smt.api.FormulaType.BooleanType;
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Iterables;
@@ -31,21 +32,21 @@ public void setUp() {
   }
 
   @Test
-  public void testParseAll_valid_simpleBoolean() {
+  public void parseAllSimpleBooleanTest() {
     String smt = "(assert true)";
     assertThat(mgr.parseAll(smt)).containsExactly(bmgr.makeTrue());
   }
 
   @Test
-  public void testParseAll_valid_simpleInteger() {
+  public void parseAllSimpleIntegerTest() {
     requireIntegers();
     String smt = "(declare-fun x () Int)(assert (= x 1))";
     assertThat(mgr.parseAll(smt))
         .containsExactly(imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(1)));
   }
 
   @Test
-  public void testParseAll_valid_defineFun() throws SolverException, InterruptedException {
+  public void parseAllDefineFunTest() throws SolverException, InterruptedException {
     requireIntegers();
     assume()
         .withMessage("Solver %s does not support parsing function definitions", solverToUse())
@@ -79,7 +80,7 @@ public void testParseAll_valid_defineFun() throws SolverException, InterruptedEx
   }
 
   @Test
-  public void testParseAll_valid_multipleAssertions() {
+  public void parseAllMultipleAssertionsTest() {
     requireIntegers();
     String smt = "(declare-fun x () Int)(assert (> x 0))(assert (< x 10))";
     BooleanFormula gt = imgr.greaterThan(imgr.makeVariable("x"), imgr.makeNumber(0));
@@ -88,7 +89,7 @@ public void testParseAll_valid_multipleAssertions() {
   }
 
   @Test
-  public void testParseAll_valid_differentTypes() {
+  public void parseAllDifferentTypesTest() {
     requireIntegers();
     String smt = "(declare-fun x () Int)(declare-fun y () Bool)(assert (= x 1))(assert y)";
     BooleanFormula intEq = imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(1));
@@ -97,7 +98,7 @@ public void testParseAll_valid_differentTypes() {
   }
 
   @Test
-  public void testParseAll_valid_functionApplication() {
+  public void parseAllFunctionApplicationTest() {
     requireIntegers();
     String smt = "(declare-fun f (Int) Int)(declare-fun x () Int)(assert (= (f x) 1))";
     IntegerFormula x = imgr.makeVariable("x");
@@ -107,7 +108,7 @@ public void testParseAll_valid_functionApplication() {
   }
 
   @Test
-  public void testParseAll_valid_bitvector() throws SolverException, InterruptedException {
+  public void parseAllBitvectorTest() throws SolverException, InterruptedException {
     requireBitvectors();
     String smt = "(declare-fun x () (_ BitVec 8))(assert (= x #x01))";
     List<BooleanFormula> parsed = mgr.parseAll(smt);
@@ -117,7 +118,7 @@ public void testParseAll_valid_bitvector() throws SolverException, InterruptedEx
   }
 
   @Test
-  public void testParseAll_valid_quantifier() {
+  public void parseAllQuantifierTest() {
     requireQuantifiers();
     requireIntegers();
     String smt = "(declare-fun p (Int) Bool)(assert (forall ((x Int)) (p x)))";
@@ -129,7 +130,7 @@ public void testParseAll_valid_quantifier() {
   }
 
   @Test
-  public void testParseAll_valid_string() throws SolverException, InterruptedException {
+  public void parseAllStringTest() throws SolverException, InterruptedException {
     requireStrings();
     assume()
         .withMessage("Solver %s does not support parsing strings", solverToUse())
@@ -144,7 +145,7 @@ public void testParseAll_valid_string() throws SolverException, InterruptedExcep
   }
 
   @Test
-  public void testParseAll_valid_floatingPointFromInt() {
+  public void parseAllFloatingPointFromIntTest() {
     requireFloats();
     requireIntegers();
     String smt = "(declare-fun x () Int)(assert (= x 1.0))";
@@ -153,7 +154,7 @@ public void testParseAll_valid_floatingPointFromInt() {
   }
 
   @Test
-  public void testParseAll_valid_floatingPointFromReal() {
+  public void parseAllFloatingPointFromRealTest() {
     requireFloats();
     requireRationals();
     String smt = "(declare-fun x () Real)(assert (= x 1.0))";
@@ -162,7 +163,7 @@ public void testParseAll_valid_floatingPointFromReal() {
   }
 
   @Test
-  public void testParseAll_valid_complexNested() {
+  public void parseAllComplexNestedTest() {
     requireIntegers();
     String smt =
         "(declare-fun x () Int)(declare-fun y () Int)(assert (or (= x 1) (and (> y 0) (< y 10))))";
@@ -177,7 +178,7 @@ public void testParseAll_valid_complexNested() {
   }
 
   @Test
-  public void testParseAll_valid_letBinding() {
+  public void parseAllLetBindingTest() {
     requireIntegers();
     String smt = "(declare-fun x () Int)(assert (let ((a x)) (= a 1)))";
     // For now, just check if it parses without error and returns a formula.
@@ -187,19 +188,19 @@ public void testParseAll_valid_letBinding() {
   }
 
   @Test
-  public void testParseAll_invalid_syntaxError() {
+  public void parseAllSyntaxErrorTest() {
     String smt = "(assert (= x 1)"; // Missing closing parenthesis
     assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt));
   }
 
   @Test
-  public void testParseAll_invalid_undeclaredVariable() {
+  public void parseAllUndeclaredVariableTest() {
     String smt = "(assert (= x 1))"; // 'x' not declared
     assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt));
   }
 
   @Test
-  public void testParseAll_invalid_typeMismatch() throws SolverException, InterruptedException {
+  public void parseAllTypeMismatchTest() throws SolverException, InterruptedException {
     requireIntegers();
     String smt = "(declare-fun x () Int)(assert (= x true))"; // Int vs Bool
     if (solverToUse() == Solvers.Z3) {
@@ -214,45 +215,45 @@ public void testParseAll_invalid_typeMismatch() throws SolverException, Interrup
   }
 
   @Test
-  public void testParseAll_invalid_unknownCommandWithAssertion() {
+  public void parseAllUnknownCommandWithAssertionTest() {
     String smt = "(unknown-command)(assert true)";
     assertThat(mgr.parseAll(smt)).hasSize(1);
     assertThat(mgr.parseAll(smt).get(0)).isEqualTo(bmgr.makeTrue());
   }
 
   @Test
-  public void testParseAll_invalid_unknownCommand() {
+  public void parseAllUnknownCommandTest() {
     String smt = "(unknown-command)";
     assertThat(mgr.parseAll(smt)).isEmpty();
   }
 
   @Test
-  public void testParseAll_invalid_emptyString() {
+  public void parseAllEmptyStringTest() {
     String smt = "";
     assertThat(mgr.parseAll(smt)).isEmpty();
   }
 
   @Test
-  public void testParseAll_invalid_emptyString2() {
+  public void parseAllEmptyString2Test() {
     String smt = "   ";
     assertThat(mgr.parseAll(smt)).isEmpty();
   }
 
   @Test
-  public void testParseAll_invalid_emptyString3() {
+  public void parseAllEmptyString3Test() {
     String smt = "\n\t  \n";
     assertThat(mgr.parseAll(smt)).isEmpty();
   }
 
   @Test
-  public void testParseAll_invalid_incorrectFunctionArity() {
+  public void parseAllIncorrectFunctionArityTest() {
     requireIntegers();
     String smt = "(declare-fun f (Int) Int)(assert (f))"; // f expects 1 arg, got 0
     assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt));
   }
 
   @Test
-  public void testParseAll_invalid_reservedKeyword() throws SolverException, InterruptedException {
+  public void parseAllReservedKeywordTest() throws SolverException, InterruptedException {
     requireIntegers();
     // 'assert' is a reserved keyword, cannot be used as a function name in most solvers
     String smt = "(declare-fun assert () Int)(assert (= assert 1))";
@@ -265,4 +266,23 @@ public void testParseAll_invalid_reservedKeyword() throws SolverException, Inter
       assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt));
     }
   }
+
+  @Test
+  public void parseAllQuotedSymbolTest() {
+    // Capture a variable from the context
+    var f = mgr.makeVariable(BooleanType, "my variable");
+    var g = mgr.parse("(assert |my variable|)");
+
+    assertThat(g).isEqualTo(f);
+  }
+
+  @Test
+  public void parseAllQuotedSymbolRedefinitionTest() {
+    // Parse a variable that was already defined in the context
+    var f = mgr.makeVariable(BooleanType, "my variable");
+    var str = "(declare-fun |my variable| () Bool) (assert |my variable|)";
+    var g = mgr.parse(str);
+
+    assertThat(g).isEqualTo(f);
+  }
 }