Bitwuzla: Make the code less error prone by identifying |var| and var directly in the variable cache

Author: daniel-raffler

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

@@ -12,13 +12,14 @@
 import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;
 
 import com.google.common.base.Preconditions;
-import com.google.common.collect.HashBasedTable;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Table;
+import com.google.common.collect.TreeBasedTable;
 import java.math.BigInteger;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Comparator;
 import java.util.Deque;
 import java.util.HashMap;
 import java.util.Iterator;
@@ -59,7 +60,31 @@
 public class BitwuzlaFormulaCreator extends FormulaCreator<Term, Sort, Void, BitwuzlaDeclaration> {
   private final TermManager termManager;
 
-  private final Table<String, Sort, Term> formulaCache = HashBasedTable.create();
+  /**
+   * Returns the symbol name without any SMTLIB quotes.
+   *
+   * <p>Will turn <code>| 1var\n|</code> into just <code> 1 var\n</code>. Symbols that are not
+   * quoted are unaffected.
+   */
+  private String removeQuotes(String symbol) {
+    return (symbol.startsWith("|") && symbol.endsWith("|"))
+        ? symbol.substring(1, symbol.length() - 1)
+        : symbol;
+  }
+
+  /**
+   * Stores Bitwuzla terms for all defined symbols.
+   *
+   * <p>The cache maps from <code>String x Sort</code> to <code>Term</code>. Here the first argument
+   * is the name of the symbol, and we allow polymorphic symbols where the same name can have more
+   * than one sort. If the symbol can be printed as a simple symbol or a quoted symbol (like <code>
+   * var1</code> and <code>|var1|</code>) in SMTLIB we identify both version as they refer to the
+   * same variable.
+   */
+  private final Table<String, Sort, Term> formulaCache =
+      TreeBasedTable.create(
+          (String symA, String symB) -> removeQuotes(symA).compareTo(removeQuotes(symB)),
+          Comparator.comparing(Sort::toString));
 
   /**
    * This mapping stores symbols and their constraints, such as from fp-to-bv casts with their

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

@@ -74,10 +74,6 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException {
         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);
-        }
         Sort sort = parsed.sort();
 
         // Check if the symbol is already defined in the variable cache
@@ -138,9 +134,6 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     Map_TermTerm subst = new Map_TermTerm();
     for (Term term : declared) {
       String symbol = term.symbol();
-      if (symbol.startsWith("|") && symbol.endsWith("|")) {
-        symbol = symbol.substring(1, symbol.length() - 1);
-      }
       if (cache.containsRow(symbol)) {
         // Symbol is from the context: add the original term to the substitution map
         subst.put(term, cache.get(symbol, term.sort()));