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.
@@ -404,7 +425,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Term f)
       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);
       }
     }