From 50e62584d9f1f5e16d7fccdde80a74461c149c6e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 16 Dec 2024 22:20:59 +0100 Subject: [PATCH 1/6] Bitwuzla: Fix handling of quoted symbol names while parsing SMTLIB formulas --- .../solvers/bitwuzla/BitwuzlaFormulaManager.java | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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..794b1977e4 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -137,12 +137,16 @@ 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 = 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(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); } } From 19b393e65112175bfd4ee12e97e78965a18916e9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Dec 2024 18:45:19 +0100 Subject: [PATCH 2/6] Bitwuzla: Make the code less error prone by identifying `|var|` and `var` directly in the variable cache --- .../bitwuzla/BitwuzlaFormulaCreator.java | 29 +++++++++++++++++-- .../bitwuzla/BitwuzlaFormulaManager.java | 7 ----- 2 files changed, 27 insertions(+), 9 deletions(-) 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..7259ce2ad3 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/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 { private final TermManager termManager; - private final Table formulaCache = HashBasedTable.create(); + /** + * Returns the symbol name without any SMTLIB quotes. + * + *

Will turn | 1var\n| into just 1 var\n. 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. + * + *

The cache maps from String x Sort to Term. 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 + * var1 and |var1|) in SMTLIB we identify both version as they refer to the + * same variable. + */ + private final Table 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 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 794b1977e4..89052e1c2f 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/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())); From 8eaaf7f51fcaeda922ea6d556210a865fb2af366 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Dec 2024 18:47:25 +0100 Subject: [PATCH 3/6] Bitwuzla: Remove dead code --- .../bitwuzla/BitwuzlaFormulaCreator.java | 21 +------------------ 1 file changed, 1 insertion(+), 20 deletions(-) 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 7259ce2ad3..ef34a3c80e 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -22,12 +22,9 @@ import java.util.Comparator; 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; @@ -580,26 +577,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); From 3e21163c61f961ce6a0394984d3677193e1de4fe Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 28 Dec 2024 13:26:43 +0100 Subject: [PATCH 4/6] Revert "Bitwuzla: Make the code less error prone by identifying `|var|` and `var` directly in the variable cache" This reverts commit ce2688ee5dfd2356821f4c468b392dbb001b7d4d. --- .../bitwuzla/BitwuzlaFormulaCreator.java | 29 ++----------------- .../bitwuzla/BitwuzlaFormulaManager.java | 7 +++++ 2 files changed, 9 insertions(+), 27 deletions(-) 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 ef34a3c80e..3807f332fc 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -12,14 +12,13 @@ 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.LinkedHashSet; @@ -57,31 +56,7 @@ public class BitwuzlaFormulaCreator extends FormulaCreator { private final TermManager termManager; - /** - * Returns the symbol name without any SMTLIB quotes. - * - *

Will turn | 1var\n| into just 1 var\n. 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. - * - *

The cache maps from String x Sort to Term. 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 - * var1 and |var1|) in SMTLIB we identify both version as they refer to the - * same variable. - */ - private final Table formulaCache = - TreeBasedTable.create( - (String symA, String symB) -> removeQuotes(symA).compareTo(removeQuotes(symB)), - Comparator.comparing(Sort::toString)); + private final Table formulaCache = HashBasedTable.create(); /** * This mapping stores symbols and their constraints, such as from fp-to-bv casts with their 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 89052e1c2f..794b1977e4 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -74,6 +74,10 @@ 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 @@ -134,6 +138,9 @@ 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())); From 4f69f14788a06b2cdd885a6e2180a4677e621022 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 28 Dec 2024 13:53:50 +0100 Subject: [PATCH 5/6] Bitwuzla: Move code to remove quotes from SMTLIB names to BitwuzlaFormulaCreator --- .../bitwuzla/BitwuzlaFormulaCreator.java | 28 +++++++++++++++++-- .../bitwuzla/BitwuzlaFormulaManager.java | 11 ++------ 2 files changed, 28 insertions(+), 11 deletions(-) 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 3807f332fc..e1a6b005c0 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -56,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. @@ -401,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); @@ -419,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; 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 794b1977e4..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,10 +133,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Process the symbols from the parser 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); - } + 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(symbol, term.sort())); From 3c0c20a79469760a67f931100c4e2b55abd2aded Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 13 Jan 2025 12:48:15 +0100 Subject: [PATCH 6/6] Bitwuzla: Add native tests for quoted symbols --- .../bitwuzla/BitwuzlaNativeApiTest.java | 95 +++++++++++++++++++ 1 file changed, 95 insertions(+) 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|"); + } }