Bitwuzla: Fix handling of quoted symbol names while parsing SMTLIB formulas

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

@@ -21,12 +21,9 @@
 import java.util.Collection;
 import java.util.Deque;
 import java.util.HashMap;
-import java.util.Iterator;
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
-import java.util.Map.Entry;
-import java.util.Optional;
 import java.util.Set;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -59,8 +56,32 @@
 public class BitwuzlaFormulaCreator extends FormulaCreator<Term, Sort, Void, BitwuzlaDeclaration> {
   private final TermManager termManager;
 
+  /**
+   * Variable cache, contains terms for all declared symbols
+   *
+   * <p>Bitwuzla allows the variables to be declared multiple times. Each of these instances will be
+   * considered a separate variable, even if the names and types are the same. We fix this by
+   * keeping track of all declared variables in this cache. If a variable is already defined we
+   * return it from the cache, otherwise a new Term for the variable is created and added to the
+   * cache.
+   *
+   * <p>It is important to keep this cache synchronized with the variable declarations for the
+   * parser. This is handled in {@link BitwuzlaFormulaManager#parse(String)}.
+   */
   private final Table<String, Sort, Term> formulaCache = HashBasedTable.create();
 
+  /**
+   * Remove SMTLIB quotes from a symbol name.
+   *
+   * <p>If the symbol is not quoted, just return it as is .
+   */
+  static String removeQuotes(String pSymbol) {
+    if (pSymbol.startsWith("|") && pSymbol.endsWith("|")) {
+      return pSymbol.substring(1, pSymbol.length() - 1);
+    }
+    return pSymbol;
+  }
+
   /**
    * This mapping stores symbols and their constraints, such as from fp-to-bv casts with their
    * defining equation.
@@ -400,11 +421,11 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Term f)
     if (f.is_value()) {
       return visitor.visitConstant(formula, convertValue(f));
     } else if (f.is_const()) {
-      String name = f.symbol();
+      String name = removeQuotes(f.symbol());
       return visitor.visitFreeVariable(formula, name);
 
     } else if (f.is_variable()) {
-      String name = f.symbol();
+      String name = removeQuotes(f.symbol());
       Sort sort = f.sort();
       Term originalVar = formulaCache.get(name, sort);
       return visitor.visitBoundVariable(encapsulate(getFormulaType(originalVar), originalVar), 0);
@@ -422,7 +443,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Term f)
       for (int i = 0; i < size - 1; i++) {
         Term boundVar = children.get(i);
         boundVars[i] = boundVar;
-        String name = boundVar.symbol();
+        String name = removeQuotes(boundVar.symbol());
         assert name != null;
         Sort sort = boundVar.sort();
         Term freeVar;
@@ -555,26 +576,10 @@ public BooleanFormula encapsulateBoolean(Term pTerm) {
     return new BitwuzlaBooleanFormula(pTerm);
   }
 
-  protected Table<String, Sort, Term> getCache() {
+  Table<String, Sort, Term> getCache() {
     return formulaCache;
   }
 
-  // True if the entered String has an existing variable in the cache.
-  protected boolean formulaCacheContains(String variable) {
-    // There is always only 1 type permitted per variable
-    return formulaCache.containsRow(variable);
-  }
-
-  // Optional that contains the variable to the entered String if there is one.
-  protected Optional<Term> getFormulaFromCache(String variable) {
-    Iterator<Entry<Sort, Term>> entrySetIter = formulaCache.row(variable).entrySet().iterator();
-    if (entrySetIter.hasNext()) {
-      // If there is a non-empty row for an entry, there is only one entry
-      return Optional.of(entrySetIter.next().getValue());
-    }
-    return Optional.empty();
-  }
-
   @Override
   public Object convertValue(Term term) {
     Preconditions.checkArgument(term.is_value(), "Term \"%s\" is not a value.", term);

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java

@@ -73,11 +73,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException {
         declParser.parse(token, true, false);
         Term parsed = declParser.get_declared_funs().get(0);
 
-        String symbol = parsed.symbol();
-        if (symbol.startsWith("|") && symbol.endsWith("|")) {
-          // Strip quotes from the name
-          symbol = symbol.substring(1, symbol.length() - 1);
-        }
+        String symbol = BitwuzlaFormulaCreator.removeQuotes(parsed.symbol());
         Sort sort = parsed.sort();
 
         // Check if the symbol is already defined in the variable cache
@@ -137,12 +133,13 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     // Process the symbols from the parser
     Map_TermTerm subst = new Map_TermTerm();
     for (Term term : declared) {
-      if (cache.containsRow(term.symbol())) {
+      String symbol = BitwuzlaFormulaCreator.removeQuotes(term.symbol());
+      if (cache.containsRow(symbol)) {
         // Symbol is from the context: add the original term to the substitution map
-        subst.put(term, cache.get(term.symbol(), term.sort()));
+        subst.put(term, cache.get(symbol, term.sort()));
       } else {
         // Symbol is new, add it to the context
-        cache.put(term.symbol(), term.sort(), term);
+        cache.put(symbol, term.sort(), term);
       }
     }
 

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaNativeApiTest.java

@@ -719,6 +719,16 @@ private Vector_Term parse(String smt2dump) {
     return parser.bitwuzla().get_assertions();
   }
 
+  private Term parseVariable(String pName) {
+    return parse(String.format("(declare-const %s Bool)(assert %s)", pName, pName)).get(0);
+  }
+
+  private String dump(Term pTerm) {
+    Bitwuzla prover = new Bitwuzla(termManager, createOptions());
+    prover.assert_formula(pTerm);
+    return prover.print_formula();
+  }
+
   // Bitwuzla currently REWRITES terms when parsing
   @Ignore
   @Test
@@ -770,4 +780,90 @@ public void parserFailTest() {
     String badInput = "(declare-const a Bool)(assert (or a b))";
     parse(badInput);
   }
+
+  @Test
+  public void noVariableCacheTest() {
+    // Bitwuzla allows us to create the same variable twice
+    // Here t1 and t2 are treated as different variables, even though they share a name and have
+    // the same sort
+    Sort sortBool = termManager.mk_bool_sort();
+    Term t1 = termManager.mk_const(sortBool, "var");
+    Term t2 = termManager.mk_const(sortBool, "var");
+
+    bitwuzla.assert_formula(termManager.mk_term(Kind.NOT, termManager.mk_term(Kind.IFF, t1, t2)));
+    assertThat(bitwuzla.check_sat()).isEqualTo(Result.SAT);
+
+    boolean r1 = bitwuzla.get_value(t1).is_true();
+    boolean r2 = bitwuzla.get_value(t2).is_true();
+    assertThat(r1).isNotEqualTo(r2);
+  }
+
+  @Test
+  public void quotedSymbolTest() {
+    // When parsing formulas Bitwuzla will preserve any || quotes in the name.
+    // The parser still makes sure that "var" and "|var|" can't be declared in the same file as
+    // both names are identical accoridng to the SMTLIB standard
+    assertThat(parseVariable("var").symbol()).isEqualTo("var");
+    assertThat(parseVariable("|var|").symbol()).isEqualTo("|var|");
+  }
+
+  @Test
+  @Ignore
+  public void illegalSmtlibTest() {
+    // Bitwuzla does not put reserved variable names in quotes while printing and will produce
+    // illegal output
+    Sort sortBool = termManager.mk_bool_sort();
+    Term t1 = termManager.mk_const(sortBool, "exit");
+
+    String expected =
+        "(set-logic ALL)\n"
+            + "(declare-const |exit| Bool)\n"
+            + "(assert |exit|)\n"
+            + "(check-sat)\n"
+            + "(exit)\n";
+    assertThat(dump(t1)).isEqualTo(expected);
+  }
+
+  @Test
+  @Ignore
+  public void illegalSmtlibParseTest() {
+    // Even with the quotes added Bitwuzla will not parse keywords
+    // Won't fix, see https://github.com/bitwuzla/bitwuzla/issues/151
+    String input =
+        "(set-logic ALL)\n"
+            + "(declare-const |exit| Bool)\n"
+            + "(assert |exit|)\n"
+            + "(check-sat)\n"
+            + "(exit)\n";
+    assertThat(parse(input).get(0).symbol()).isEqualTo("|exit|");
+  }
+
+  @Test
+  @Ignore
+  public void illegalSmtlibNumberTest() {
+    // Bitwuzla also won't quote variable names that are numbers (like "1" or "1.4") while printing
+    Sort sortBool = termManager.mk_bool_sort();
+    Term t1 = termManager.mk_const(sortBool, "1");
+
+    String expected =
+        "(set-logic ALL)\n"
+            + "(declare-const |1| Bool)\n"
+            + "(assert |1|)\n"
+            + "(check-sat)\n"
+            + "(exit)\n";
+    assertThat(dump(t1)).isEqualTo(expected);
+  }
+
+  @Test
+  @Ignore
+  public void illegalSmtlibParseNumberTest() {
+    // Even though it can read back input with quoted numbers as variable names
+    String input =
+        "(set-logic ALL)\n"
+            + "(declare-const |1| Bool)\n"
+            + "(assert |1|)\n"
+            + "(check-sat)\n"
+            + "(exit)\n";
+    assertThat(parse(input).get(0).symbol()).isEqualTo("|1|");
+  }
 }