Skip to content

Commit

Permalink
Bitwuzla: Move code to remove quotes from SMTLIB names to BitwuzlaFor…
Browse files Browse the repository at this point in the history
…mulaCreator
  • Loading branch information
daniel-raffler committed Jan 1, 2025
1 parent 3e21163 commit 4f69f14
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 11 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -56,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.
Expand Down Expand Up @@ -401,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);
Expand All @@ -419,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;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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()));
Expand Down

0 comments on commit 4f69f14

Please sign in to comment.