From 0d463c83410a332ed81ff4f7628d25ae729b3782 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 31 Mar 2025 12:41:15 +0200 Subject: [PATCH 1/8] CVC5: Add parsing support --- .../solvers/cvc5/CVC5FormulaCreator.java | 77 +++------- .../solvers/cvc5/CVC5FormulaManager.java | 142 +++++++++++++++++- .../java_smt/solvers/cvc5/CVC5Model.java | 118 +++++++++++++-- src/org/sosy_lab/java_smt/test/ModelTest.java | 1 - .../java_smt/test/SolverBasedTest0.java | 2 +- .../test/SolverFormulaIODeclarationsTest.java | 21 ++- .../java_smt/test/SolverFormulaIOTest.java | 10 ++ 7 files changed, 303 insertions(+), 68 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index ebde92e4e4..45763315df 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -34,9 +34,7 @@ import java.lang.reflect.Array; import java.math.BigInteger; import java.util.ArrayList; -import java.util.HashMap; import java.util.List; -import java.util.Map; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.ArrayFormula; @@ -72,13 +70,9 @@ public class CVC5FormulaCreator extends FormulaCreator UNSUPPORTED_IDENTIFIERS = ImmutableSet.of("let"); - // private static final Pattern FLOATING_POINT_PATTERN = Pattern.compile("^\\(fp #b(?\\d) - // #b(?\\d+) #b(?\\d+)$"); + /** We use a variable cache to keep track of variables/Ufs that have already been defined. */ + private final Table variablesCache = HashBasedTable.create(); - // because CVC5 returns distinct pointers for types, while the - // String representation is equal (and they are equal) - private final Table variablesCache = HashBasedTable.create(); - private final Map functionsCache = new HashMap<>(); private final TermManager termManager; private final Solver solver; @@ -98,9 +92,13 @@ public Solver getSolver() { return solver; } + Table getDeclaredVariables() { + return variablesCache; + } + @Override public Term makeVariable(Sort sort, String name) { - Term existingVar = variablesCache.get(name, sort.toString()); + Term existingVar = variablesCache.get(name, sort); if (existingVar != null) { return existingVar; } @@ -124,7 +122,7 @@ public Term makeVariable(Sort sort, String name) { .getKey()); } Term newVar = termManager.mkConst(sort, name); - variablesCache.put(name, sort.toString(), newVar); + variablesCache.put(name, sort, newVar); return newVar; } @@ -426,13 +424,6 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { getFormulaType(f), f.getKind())); - } else if (f.getKind() == Kind.VARIABLE) { - // BOUND vars are used for all vars that are bound to a quantifier in CVC5. - // We resubstitute them back to the original free. - // CVC5 doesn't give you the de-brujin index - Term originalVar = accessVariablesCache(formula.toString(), sort); - return visitor.visitBoundVariable(encapsulate(originalVar), 0); - } else if (f.getKind() == Kind.FORALL || f.getKind() == Kind.EXISTS) { // QUANTIFIER: replace bound variable with free variable for visitation assert f.getNumChildren() == 2; @@ -440,7 +431,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { List freeVars = new ArrayList<>(); for (Term boundVar : f.getChild(0)) { // unpack grand-children of f. String name = getName(boundVar); - Term freeVar = Preconditions.checkNotNull(accessVariablesCache(name, boundVar.getSort())); + Term freeVar = makeVariable(boundVar.getSort(), name); body = body.substitute(boundVar, freeVar); freeVars.add(encapsulate(freeVar)); } @@ -520,7 +511,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { * back to a common one. */ private Term normalize(Term operator) { - Term function = functionsCache.get(getName(operator)); + Term function = variablesCache.get(getName(operator), operator.getSort()); if (function != null) { checkState( function.getId() == operator.getId(), @@ -766,20 +757,19 @@ private void checkSymbol(String symbol) { public Term declareUFImpl(String pName, Sort pReturnType, List pArgTypes) { checkSymbol(pName); - Term exp = functionsCache.get(pName); + // Ufs in CVC5 can't have 0 arity. We just use a variable as a workaround. + Sort termSort = + pArgTypes.isEmpty() + ? pReturnType + : environment.mkFunctionSort(pArgTypes.toArray(new Sort[0]), pReturnType); + Term exp = variablesCache.get(pName, termSort); if (exp == null) { - // Ufs in CVC5 can't have 0 arity. We just use a variable as a workaround. - Sort sort = - pArgTypes.isEmpty() - ? pReturnType - : termManager.mkFunctionSort(pArgTypes.toArray(new Sort[0]), pReturnType); - exp = termManager.mkConst(sort, pName); - functionsCache.put(pName, exp); - + exp = termManager.mkConst(termSort, pName); + variablesCache.put(pName, exp.getSort(), exp); } else { Preconditions.checkArgument( - exp.getSort().equals(exp.getSort()), + pReturnType.equals(exp.getSort().getFunctionCodomainSort()), "Symbol %s already in use for different return type %s", exp, exp.getSort()); @@ -801,6 +791,11 @@ public Term declareUFImpl(String pName, Sort pReturnType, List pArgTypes) return exp; } + @Override + public Object convertValue(Term pValue) { + return convertValue(pValue, pValue); + } + @Override public Object convertValue(Term expForType, Term value) { final Sort type = expForType.getSort(); @@ -857,28 +852,4 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep final var bits = bvValue.getBitVectorValue(); return FloatingPointNumber.of(bits, expWidth, mantWidth); } - - private Term accessVariablesCache(String name, Sort sort) { - Term existingVar = variablesCache.get(name, sort.toString()); - if (existingVar == null) { - throw new IllegalArgumentException( - "Symbol " - + name - + " requested with type " - + sort - + ", but " - + "already " - + "used " - + "with " - + "type" - + variablesCache - .rowMap() - .get(name) - .entrySet() - .toArray((java.util.Map.Entry[]) Array.newInstance(java.util.Map.Entry.class, 0))[ - 0] - .getKey()); - } - return existingVar; - } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index d7fb51e845..f95ec8a921 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -9,18 +9,34 @@ package org.sosy_lab.java_smt.solvers.cvc5; import com.google.common.base.Joiner; +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; import com.google.common.collect.Iterables; +import com.google.common.collect.Table; +import com.google.common.collect.Table.Cell; import de.uni_freiburg.informatik.ultimate.logic.PrintTerm; import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.Command; +import io.github.cvc5.InputParser; import io.github.cvc5.Kind; +import io.github.cvc5.Solver; import io.github.cvc5.Sort; +import io.github.cvc5.SymbolManager; import io.github.cvc5.Term; import io.github.cvc5.TermManager; +import io.github.cvc5.modes.InputLanguage; +import java.util.Arrays; +import java.util.HashMap; import java.util.LinkedHashMap; +import java.util.List; import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; +import java.util.stream.Collectors; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; class CVC5FormulaManager extends AbstractFormulaManager { @@ -66,7 +82,131 @@ static Term getCVC5Term(Formula pT) { @Override public Term parseImpl(String formulaStr) throws IllegalArgumentException { - throw new UnsupportedOperationException(); + // Split the input string into a list of SMT-LIB2 commands + List tokens = Tokenizer.tokenize(formulaStr); + + Table cache = creator.getDeclaredVariables(); + + // Process the declarations + ImmutableList.Builder processed = ImmutableList.builder(); + for (String token : tokens) { + if (Tokenizer.isDeclarationToken(token)) { + // Parse the variable/UF declaration to get a name + TermManager tm = new TermManager(); + Solver solver = new Solver(tm); + InputParser parser = new InputParser(solver); + SymbolManager symbolManager = new SymbolManager(tm); + parser.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)" + token, ""); + parser.nextCommand().invoke(solver, symbolManager); + parser.nextCommand().invoke(solver, symbolManager); + + Term parsed = symbolManager.getDeclaredTerms()[0]; + + String symbol = parsed.getSymbol(); + Sort sort = parsed.getSort(); + + // Check if the symbol is already defined in the variable cache + if (cache.containsRow(symbol)) { + if (!cache.contains(symbol, sort)) { + // Sort of the definition that we parsed does not match the sort from the variable + // cache. + throw new IllegalArgumentException(); + } + // Skip if it's just a redefinition + continue; + } + } + // Otherwise, keep the command + processed.add(token); + } + + // Build SMT-LIB2 declarations for all variables in the cache + ImmutableList.Builder builder = ImmutableList.builder(); + for (Cell c : cache.cellSet()) { + String symbol = c.getValue().toString(); + List args = ImmutableList.of(); + Sort sort = c.getValue().getSort(); + + if (sort.isFunction()) { + args = List.of(sort.getFunctionDomainSorts()); + sort = sort.getFunctionCodomainSort(); + } + StringBuilder decl = new StringBuilder(); + decl.append("(declare-fun").append(" "); + decl.append(symbol).append(" "); + decl.append("("); + for (Sort p : args) { + decl.append(p).append(" "); + } + decl.append(")").append(" "); + decl.append(sort); + decl.append(")"); + + builder.add(decl.toString()); + } + + String decls = String.join("\n", builder.build()); + String input = String.join("\n", processed.build()); + + // Add the declarations to the input and parse everything + TermManager termManager = new TermManager(); + Solver solver = new Solver(termManager); + InputParser parser = new InputParser(solver); + SymbolManager symbolManager = parser.getSymbolManager(); + parser.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)" + decls + input, ""); + + Command cmd = parser.nextCommand(); + while (!cmd.isNull()) { + try { + Preconditions.checkArgument( + ImmutableList.of("set-logic", "declare-fun", "declare-const", "define-fun", "assert") + .contains(cmd.getCommandName()), + "Command %s is not supported", + cmd.getCommandName()); + cmd.invoke(solver, symbolManager); + cmd = parser.nextCommand(); + } catch (Throwable e) { + throw new IllegalArgumentException(e); + } + } + + // Get the assertions from the input + Term[] asserted = solver.getAssertions(); + Term result = asserted.length == 1 ? asserted[0] : termManager.mkTerm(Kind.AND, asserted); + + // Now get all declared symbols + Term[] declared = symbolManager.getDeclaredTerms(); + + // Check that all variables/UF have a single type signature + // The CVC5 parser allows polymorphic types, but we don't support them in JavaSMT + Set duplicates = + Arrays.stream(declared) + .collect(Collectors.groupingBy(Term::getSymbol, Collectors.counting())) + .entrySet() + .stream() + .filter(m -> m.getValue() > 1) + .map(Entry::getKey) + .collect(Collectors.toSet()); + Preconditions.checkArgument( + duplicates.isEmpty(), + "Parsing failed as there were multiple conflicting definitions for the symbol(s) '%s'", + duplicates); + + // Process the symbols from the parser + Map subst = new HashMap<>(); + for (Term term : declared) { + if (cache.containsRow(term.getSymbol())) { + // Symbol is from the context: add the original term to the substitution map + subst.put(term, cache.get(term.getSymbol(), term.getSort())); + } else { + // Symbol is new, add it to the context + cache.put(term.getSymbol(), term.getSort(), term); + } + } + + // Substitute all symbols from the context with their original terms + return result.substitute( + subst.keySet().toArray(new Term[0]), subst.values().toArray(new Term[0])); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java index cba98c1d85..cc90890cf9 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.cvc5; import com.google.common.base.Preconditions; +import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import io.github.cvc5.CVC5ApiException; @@ -81,7 +82,7 @@ private void recursiveAssignmentFinder(ImmutableSet.Builder bui // Vars and UFs, as well as bound vars in UFs! // In CVC5 consts are variables! Free variables (in CVC5s notation, we call them bound // variables, created with mkVar() can never have a value!) - builder.add(getAssignment(expr)); + builder.addAll(getAssignment(expr)); } else if (kind == Kind.FORALL || kind == Kind.EXISTS) { // Body of the quantifier, with bound vars! Term body = expr.getChild(1); @@ -169,7 +170,96 @@ private ValueAssignment getAssignmentForUf(Term pKeyTerm) { keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build()); } - private ValueAssignment getAssignment(Term pKeyTerm) { + /** Takes a (nested) select statement and returns its indices. */ + private Iterable getArgs(Term array) throws CVC5ApiException { + if (array.getKind().equals(Kind.SELECT)) { + return FluentIterable.concat(getArgs(array.getChild(0)), ImmutableList.of(array.getChild(1))); + } else { + return ImmutableList.of(); + } + } + + /** Takes a select statement with multiple indices and returns the variable name at the bottom. */ + private String getVar(Term array) throws CVC5ApiException { + if (array.getKind().equals(Kind.SELECT)) { + return getVar(array.getChild(0)); + } else { + return array.getSymbol(); + } + } + + /** Build assignment for an array value. */ + private Iterable buildArrayAssignment(Term expr, Term value) { + // CVC5 returns values such as "(Store (Store ... i1,1 e1,1) i1,0 e1,0)" where the i1,x match + // the first index of the array and the elements e1,Y can again be arrays (if there is more + // than one index). We need "pattern match" this values to extract assignments from it. + // Initially we have: + // arr = (Store (Store ... i1,1 e1,1) i1,0 e1,0) + // where 'arr' is the name of the variable. By applying (Select i1,0 ...) to both side we get: + // (Select i1,0 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) + // The right side simplifies to e1,0 as the index matches. We need to continue with this for + // all other matches to the first index, that is + // (Select i1,1 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) + // = (Select i1,0 (Store ... i1,1 e1,1)) + // = e1,1 + // until all matches are explored and the bottom of the Store chain is reached. If the array + // has more than one dimension we also have to descend into the elements to apply the next + // index there. For instance, let's consider a 2-dimensional array with type (Array Int -> + // (Array Int -> Int)). After matching the first index just as in the above example we might + // have: + // (Select i1,0 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) = e1,0 + // In this case e1,0 is again a Store chain, let's say e1,0 := (Store (Store ... i2,1 e2,1) + // i2,0 e2,0), and we now continue with the second index: + // (Select i2,1 (Select i1,0 arr)) = (Select i2,1 (Store (Store ... i2,1 e2,1) i2,0 e2,0)) = + // = e2,1 + // This again has to be done for all possible matches. + // Once we've reached the last index, the successor element will be a non-array value. We + // then create the final assignments and return: + // (Select iK,mK ... (Select i2,1 (Select i1,0 arr)) = eik,mK + try { + if (value.getKind().equals(Kind.STORE)) { + // This is a Store node for the current index. We need to follow the chain downwards to + // match this index, while also exploring the successor for the other indices + Term index = value.getChild(1); + Term element = value.getChild(2); + + Term select = creator.getEnv().mkTerm(Kind.SELECT, expr, index); + + Iterable current; + if (expr.getSort().getArrayElementSort().isArray()) { + current = buildArrayAssignment(select, element); + } else { + Term equation = creator.getEnv().mkTerm(Kind.EQUAL, select, element); + current = + FluentIterable.of( + new ValueAssignment( + creator.encapsulate(creator.getFormulaType(element), select), + creator.encapsulate(creator.getFormulaType(element), element), + creator.encapsulateBoolean(equation), + getVar(expr), + creator.convertValue(element, element), + FluentIterable.from(getArgs(select)) + .transform(creator::convertValue) + .toList())); + } + return FluentIterable.concat(current, buildArrayAssignment(expr, value.getChild(0))); + + } else if (value.getKind().equals(Kind.CONST_ARRAY)) { + // We've reached the end of the Store chain + return ImmutableList.of(); + + } else { + // Should be unreachable + // We assume that array values are made up of "const" and "store" nodes with non-array + // constants as leaves + throw new IllegalArgumentException(); + } + } catch (CVC5ApiException e) { + throw new RuntimeException(e); + } + } + + private Iterable getAssignment(Term pKeyTerm) { ImmutableList.Builder argumentInterpretationBuilder = ImmutableList.builder(); for (int i = 0; i < pKeyTerm.getNumChildren(); i++) { try { @@ -193,13 +283,23 @@ private ValueAssignment getAssignment(Term pKeyTerm) { } Term valueTerm = solver.getValue(pKeyTerm); - Formula keyFormula = creator.encapsulateWithTypeOf(pKeyTerm); - Formula valueFormula = creator.encapsulateWithTypeOf(valueTerm); - BooleanFormula equation = - creator.encapsulateBoolean(termManager.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); - Object value = creator.convertValue(pKeyTerm, valueTerm); - return new ValueAssignment( - keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build()); + if (valueTerm.getSort().isArray()) { + return buildArrayAssignment(pKeyTerm, valueTerm); + } else { + Formula keyFormula = creator.encapsulateWithTypeOf(pKeyTerm); + Formula valueFormula = creator.encapsulateWithTypeOf(valueTerm); + BooleanFormula equation = + creator.encapsulateBoolean(termManager.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); + Object value = creator.convertValue(pKeyTerm, valueTerm); + return ImmutableList.of( + new ValueAssignment( + keyFormula, + valueFormula, + equation, + nameStr, + value, + argumentInterpretationBuilder.build())); + } } @Override diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 34db34585b..e3565e1c86 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1724,7 +1724,6 @@ private void checkModelAssignmentsValid( // supported yet // TODO: only filter out UF formulas here, not all if (solver != Solvers.BOOLECTOR) { - // CVC5 crashes here assertThatFormula(bmgr.and(pModelAssignments)).implies(constraint); } } diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index de2715e3f2..e331eead8c 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -324,7 +324,7 @@ protected void requireParser() { assume() .withMessage("Solver %s does not support parsing formulae", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5); + .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2); } protected void requireArrayModel() { diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index 5701551726..a193ee39bd 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -167,7 +167,7 @@ public void parseDeclareRedundantBvTest() { BitvectorFormula var = bvmgr.makeVariable(8, "x"); String query = "(declare-fun x () (_ BitVec 8))(declare-fun x () (_ BitVec 8))(assert (= x #b00000000))"; - if (EnumSet.of(Solvers.MATHSAT5, Solvers.BITWUZLA).contains(solverToUse())) { + if (EnumSet.of(Solvers.MATHSAT5, Solvers.BITWUZLA, Solvers.CVC5).contains(solverToUse())) { BooleanFormula formula = mgr.parse(query); Truth.assertThat(mgr.extractVariables(formula).values()).containsExactly(var); } else { @@ -194,6 +194,13 @@ public void parseDeclareConflictInQueryTest2() { @Test public void parseDeclareConflictInQueryTest3() { requireIntegers(); + // CVC5 allows multiple definitions of the same symbol with different types. This is causing + // some issues with JavaSMT where UF functions must have a single type. + // In the test above we were able to work around the issue by checking if the list of + // declared symbols that is returned by the parser contains any duplicates. However, this + // does not seem to work here as the two definitions only differ in their return type and + // CVC5 reports only one if the declaration. + // TODO Report this to the developers String query = "(declare-fun x (Int) Bool)(declare-fun x (Int) Int)(assert (x 0))"; if (Solvers.Z3 != solverToUse()) { assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); @@ -318,7 +325,15 @@ public void parseAbbreviation() throws SolverException, InterruptedException { + " (not (= |f::v@2| (_ bv1 32)))))"; BooleanFormula parsedQuery = mgr.parse(query); assertThatFormula(parsedQuery).isUnsatisfiable(); - assert_().that(mgr.extractVariables(parsedQuery)).hasSize(9); - assert_().that(mgr.extractVariablesAndUFs(parsedQuery)).hasSize(9); + if (solver == Solvers.CVC5) { + // CVC5 does not substitute "abbrev_9", but adds the definition to the assertions and then + // counts it as another variable + assert_().that(mgr.extractVariables(parsedQuery)).hasSize(10); + assert_().that(mgr.extractVariablesAndUFs(parsedQuery)).hasSize(10); + + } else { + assert_().that(mgr.extractVariables(parsedQuery)).hasSize(9); + assert_().that(mgr.extractVariablesAndUFs(parsedQuery)).hasSize(9); + } } } diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index f59932d77e..69ee5bd43d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java @@ -277,12 +277,16 @@ public void funcsDumpTest() { @Test public void parseMathSatTestParseFirst1() throws SolverException, InterruptedException { + // MathSat prints reserved symbols starting with . or @ that CVC5 can't parse + assume().that(solver).isNotEqualTo(Solvers.CVC5); requireParser(); compareParseWithOrgParseFirst(MATHSAT_DUMP1, this::genBoolExpr); } @Test public void parseMathSatTestExprFirst1() throws SolverException, InterruptedException { + // MathSat prints reserved symbols starting with . or @ that CVC5 can't parse + assume().that(solver).isNotEqualTo(Solvers.CVC5); requireParser(); compareParseWithOrgExprFirst(MATHSAT_DUMP1, this::genBoolExpr); } @@ -313,6 +317,8 @@ public void parseZ3TestExprFirst1() throws SolverException, InterruptedException @Test public void parseMathSatTestParseFirst2() throws SolverException, InterruptedException { + // MathSat prints reserved symbols starting with . or @ that CVC5 can't parse + assume().that(solver).isNotEqualTo(Solvers.CVC5); requireParser(); requireIntegers(); compareParseWithOrgParseFirst(MATHSAT_DUMP2, this::redundancyExprGen); @@ -320,6 +326,8 @@ public void parseMathSatTestParseFirst2() throws SolverException, InterruptedExc @Test public void parseMathSatTestExprFirst2() throws SolverException, InterruptedException { + // MathSat prints reserved symbols starting with . or @ that CVC5 can't parse + assume().that(solver).isNotEqualTo(Solvers.CVC5); requireParser(); compareParseWithOrgExprFirst(MATHSAT_DUMP2, this::redundancyExprGen); } @@ -352,6 +360,8 @@ public void parseZ3SatTestExprFirst2() throws SolverException, InterruptedExcept @Test public void parseMathSatTestExprFirst3() throws SolverException, InterruptedException { + // MathSat prints reserved symbols starting with . or @ that CVC5 can't parse + assume().that(solver).isNotEqualTo(Solvers.CVC5); requireParser(); requireIntegers(); compareParseWithOrgExprFirst(MATHSAT_DUMP3, this::functionExprGen); From 323a1ef318d0f209738a652c6197e0ec47a56ef0 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 31 Mar 2025 16:27:01 +0200 Subject: [PATCH 2/8] CVC5: Throw an exception when the parser finds conflicting definitions for the same symbol CVC5 seems to not always throw exceptions when there is a parse error. An error message is printed to the screen in C++, but this seems to get lost in the Java bindings. --- .../solvers/cvc5/CVC5FormulaManager.java | 22 +++++++++++++------ .../test/SolverFormulaIODeclarationsTest.java | 7 ------ 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index f95ec8a921..0622b18f7a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -88,6 +88,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { Table cache = creator.getDeclaredVariables(); // Process the declarations + Map localSymbols = new HashMap<>(); ImmutableList.Builder processed = ImmutableList.builder(); for (String token : tokens) { if (Tokenizer.isDeclarationToken(token)) { @@ -107,14 +108,21 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Check if the symbol is already defined in the variable cache if (cache.containsRow(symbol)) { - if (!cache.contains(symbol, sort)) { - // Sort of the definition that we parsed does not match the sort from the variable - // cache. - throw new IllegalArgumentException(); - } - // Skip if it's just a redefinition - continue; + Preconditions.checkArgument( + cache.contains(symbol, sort), + "Symbol %s is already used by the solver with a different typ", + symbol); + continue; // Skip if it's a redefinition } + + // Check if it collides with a definition that was parsed earlier + Preconditions.checkArgument( + !localSymbols.containsKey(symbol) || localSymbols.get(symbol).equals(sort), + "Symbol %s has already been defined by this script with a different type", + sort); + + // Add the symbol to the local definitions for this parse + localSymbols.put(symbol, sort); } // Otherwise, keep the command processed.add(token); diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index a193ee39bd..9a49e91b62 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -194,13 +194,6 @@ public void parseDeclareConflictInQueryTest2() { @Test public void parseDeclareConflictInQueryTest3() { requireIntegers(); - // CVC5 allows multiple definitions of the same symbol with different types. This is causing - // some issues with JavaSMT where UF functions must have a single type. - // In the test above we were able to work around the issue by checking if the list of - // declared symbols that is returned by the parser contains any duplicates. However, this - // does not seem to work here as the two definitions only differ in their return type and - // CVC5 reports only one if the declaration. - // TODO Report this to the developers String query = "(declare-fun x (Int) Bool)(declare-fun x (Int) Int)(assert (x 0))"; if (Solvers.Z3 != solverToUse()) { assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); From 5aee81785c9b18b547305935eaa781d733f2e081 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 31 Mar 2025 16:27:56 +0200 Subject: [PATCH 3/8] CVC5: Disable a test where CVC5 is too slow --- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index e3565e1c86..3583a51eb8 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2240,7 +2240,7 @@ public void arrayTest5() assume() .withMessage("Solver is quite slow for this example") .that(solverToUse()) - .isNotEqualTo(Solvers.PRINCESS); + .isNoneOf(Solvers.PRINCESS, Solvers.CVC5); BooleanFormula formula = context From 0804d3304f05c05ba94d702709abccb9a2f48fa6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 4 Apr 2025 07:57:27 +0200 Subject: [PATCH 4/8] CVC5: Create parsed symbols on the same TermManager --- .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index 0622b18f7a..fb2c37498e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -93,10 +93,9 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { for (String token : tokens) { if (Tokenizer.isDeclarationToken(token)) { // Parse the variable/UF declaration to get a name - TermManager tm = new TermManager(); - Solver solver = new Solver(tm); + Solver solver = new Solver(getEnvironment()); InputParser parser = new InputParser(solver); - SymbolManager symbolManager = new SymbolManager(tm); + SymbolManager symbolManager = new SymbolManager(getEnvironment()); parser.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)" + token, ""); parser.nextCommand().invoke(solver, symbolManager); parser.nextCommand().invoke(solver, symbolManager); @@ -157,8 +156,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { String input = String.join("\n", processed.build()); // Add the declarations to the input and parse everything - TermManager termManager = new TermManager(); - Solver solver = new Solver(termManager); + Solver solver = new Solver(getEnvironment()); InputParser parser = new InputParser(solver); SymbolManager symbolManager = parser.getSymbolManager(); parser.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)" + decls + input, ""); @@ -180,7 +178,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Get the assertions from the input Term[] asserted = solver.getAssertions(); - Term result = asserted.length == 1 ? asserted[0] : termManager.mkTerm(Kind.AND, asserted); + Term result = asserted.length == 1 ? asserted[0] : getEnvironment().mkTerm(Kind.AND, asserted); // Now get all declared symbols Term[] declared = symbolManager.getDeclaredTerms(); From 7f3d7272a10b2dff5ab943c619dc36b8e6d85f35 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 4 Apr 2025 07:57:45 +0200 Subject: [PATCH 5/8] CVC5: Ignore quotes when looking up symbols --- .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index fb2c37498e..363fc5929c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -103,6 +103,10 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { Term parsed = symbolManager.getDeclaredTerms()[0]; String symbol = parsed.getSymbol(); + if (symbol.startsWith("|") && symbol.endsWith("|")) { + // Strip quotes from the name + symbol = symbol.substring(1, symbol.length() - 1); + } Sort sort = parsed.getSort(); // Check if the symbol is already defined in the variable cache @@ -201,12 +205,17 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Process the symbols from the parser Map subst = new HashMap<>(); for (Term term : declared) { - if (cache.containsRow(term.getSymbol())) { + String symbol = term.getSymbol(); + if (symbol.startsWith("|") && symbol.endsWith("|")) { + // Strip quotes from the name + 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.getSymbol(), term.getSort())); + subst.put(term, cache.get(symbol, term.getSort())); } else { // Symbol is new, add it to the context - cache.put(term.getSymbol(), term.getSort(), term); + cache.put(symbol, term.getSort(), term); } } From 57e4356ee0199476795752b213583bc96ed1edbe Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 5 Apr 2025 00:48:14 +0200 Subject: [PATCH 6/8] CVC5: Add a native test for the parser --- .../solvers/cvc5/CVC5NativeAPITest.java | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java index e15fdec270..a7194ef287 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java @@ -13,6 +13,8 @@ import com.google.common.base.Preconditions; import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.Command; +import io.github.cvc5.InputParser; import io.github.cvc5.Kind; import io.github.cvc5.Op; import io.github.cvc5.Proof; @@ -21,8 +23,10 @@ import io.github.cvc5.RoundingMode; import io.github.cvc5.Solver; import io.github.cvc5.Sort; +import io.github.cvc5.SymbolManager; import io.github.cvc5.Term; import io.github.cvc5.TermManager; +import io.github.cvc5.modes.InputLanguage; import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; @@ -1378,6 +1382,29 @@ public void testBitvectorSortinVariableCache() throws CVC5ApiException { exp); } + @Test + public void parseTest() { + InputParser parser = new InputParser(solver); + SymbolManager symbolManager = parser.getSymbolManager(); + parser.setStringInput( + InputLanguage.SMT_LIB_2_6, "(declare-const a Int)(assert (= a 3))", "parseTest"); + + Command cmd = parser.nextCommand(); + while (!cmd.isNull()) { + try { + cmd.invoke(solver, symbolManager); + cmd = parser.nextCommand(); + } catch (Throwable e) { + throw new IllegalArgumentException(e); + } + } + assertThat(symbolManager.getDeclaredTerms()).hasLength(1); + assertThat(symbolManager.getDeclaredTerms()[0].getSymbol()).isEqualTo("a"); + + assertThat(solver.getAssertions()).hasLength(1); + assertThat(solver.getAssertions()[0].toString()).isEqualTo("(= a 3)"); + } + @Test public void testProofMethods() throws CVC5ApiException { solver.setOption("produce-proofs", "true"); From 0586c3010fe594c943dc087694d95ce9fbd055eb Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 5 Apr 2025 09:49:41 +0200 Subject: [PATCH 7/8] CVC5: Add more info to the error message when parsing fails --- .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index 363fc5929c..dc04ce9282 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -111,18 +111,25 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Check if the symbol is already defined in the variable cache if (cache.containsRow(symbol)) { + Sort typeDefinition = cache.row(symbol).keySet().toArray(new Sort[0])[0]; Preconditions.checkArgument( cache.contains(symbol, sort), - "Symbol %s is already used by the solver with a different typ", - symbol); + "Symbol '%s' is already used by the solver with a different type. The new type is " + + "%s, but we already have a definition with type %s.", + symbol, + sort, + typeDefinition); continue; // Skip if it's a redefinition } // Check if it collides with a definition that was parsed earlier Preconditions.checkArgument( !localSymbols.containsKey(symbol) || localSymbols.get(symbol).equals(sort), - "Symbol %s has already been defined by this script with a different type", - sort); + "Symbol '%s' has already been defined by this script with a different type. The new " + + "type is %s, but we have already a definition with type %s.", + symbol, + sort, + localSymbols.get(symbol)); // Add the symbol to the local definitions for this parse localSymbols.put(symbol, sort); From 6d974bb49da4704f3211e1b31bc2b983f470f2f4 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 5 Apr 2025 12:25:27 +0200 Subject: [PATCH 8/8] CVC5: Remove a redundant check for duplicate definitions while parsing --- .../solvers/cvc5/CVC5FormulaManager.java | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index dc04ce9282..b15359555e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -25,14 +25,10 @@ import io.github.cvc5.Term; import io.github.cvc5.TermManager; import io.github.cvc5.modes.InputLanguage; -import java.util.Arrays; import java.util.HashMap; import java.util.LinkedHashMap; import java.util.List; import java.util.Map; -import java.util.Map.Entry; -import java.util.Set; -import java.util.stream.Collectors; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -194,21 +190,6 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Now get all declared symbols Term[] declared = symbolManager.getDeclaredTerms(); - // Check that all variables/UF have a single type signature - // The CVC5 parser allows polymorphic types, but we don't support them in JavaSMT - Set duplicates = - Arrays.stream(declared) - .collect(Collectors.groupingBy(Term::getSymbol, Collectors.counting())) - .entrySet() - .stream() - .filter(m -> m.getValue() > 1) - .map(Entry::getKey) - .collect(Collectors.toSet()); - Preconditions.checkArgument( - duplicates.isEmpty(), - "Parsing failed as there were multiple conflicting definitions for the symbol(s) '%s'", - duplicates); - // Process the symbols from the parser Map subst = new HashMap<>(); for (Term term : declared) {