diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index d231b49305..e1a6b005c0 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/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 { private final TermManager termManager; + /** + * Variable cache, contains terms for all declared symbols + * + *

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. + * + *

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 formulaCache = HashBasedTable.create(); + /** + * Remove SMTLIB quotes from a symbol name. + * + *

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 visit(FormulaVisitor 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 visit(FormulaVisitor 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 getCache() { + Table 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 getFormulaFromCache(String variable) { - Iterator> 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); diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index 9c66dfdac8..cbf4c44b64 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/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); } } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaNativeApiTest.java index 63bb7fc1e7..29857857d0 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaNativeApiTest.java +++ b/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,89 @@ 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 + 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|"); + } }