From fc74781bff799dc40195f9c1879ea1d2e1c3836a Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 27 Oct 2025 19:24:38 +0100 Subject: [PATCH 01/47] Add incomplete (crude) implementation for CVC5 parser --- .../solvers/cvc5/CVC5FormulaCreator.java | 4 +- .../solvers/cvc5/CVC5FormulaManager.java | 72 ++++++++++++++++++- 2 files changed, 73 insertions(+), 3 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 946b6be069..bb2e4a10e1 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -76,8 +76,8 @@ public class CVC5FormulaCreator extends FormulaCreator 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<>(); + protected final Table variablesCache = HashBasedTable.create(); + protected final Map functionsCache = new HashMap<>(); private final TermManager termManager; private final Solver solver; 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 e77d109188..514c70008c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -8,14 +8,22 @@ package org.sosy_lab.java_smt.solvers.cvc5; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; + import com.google.common.base.Joiner; import com.google.common.collect.Iterables; 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.LinkedHashMap; import java.util.Map; import org.sosy_lab.java_smt.api.Formula; @@ -66,7 +74,69 @@ static Term getCVC5Term(Formula pT) { @Override public Term parseImpl(String formulaStr) throws IllegalArgumentException { - throw new UnsupportedOperationException(); + TermManager env = creator.getEnv(); + Solver parseSolver = new Solver(env); + SymbolManager sm = new SymbolManager(env); + if (!parseSolver.isLogicSet()) { + try { + parseSolver.setLogic("ALL"); + } catch (CVC5ApiException e) { + throw new AssertionError("Unexpected exception", e); + } + } + String expectedSuccessMsg = "success\n"; + parseSolver.setOption("print-success", "true"); + InputParser parser = new InputParser(parseSolver, sm); + parser.setStringInput(InputLanguage.SMT_LIB_2_6, formulaStr, ""); + + Command command = parser.nextCommand(); + while (!command.isNull()) { + // This WILL read in asserts, and they are no longer available for getTerm(), but on the + // solver as assertions + // TODO: pushs and pops? + String invokeReturn = command.invoke(parseSolver, sm); + if (!invokeReturn.equals(expectedSuccessMsg)) { + throw new AssertionError("Unknown error when parsing using CVC5: " + invokeReturn); + } + command = parser.nextCommand(); + } + + parser.deletePointer(); + + // Register new terms in our caches + for (Term declaredTerm : sm.getDeclaredTerms()) { + Sort declaredSort = declaredTerm.getSort(); + // TODO: is isFunction() correct? + if (!declaredSort.isFunction()) { + Term termCacheHit = + creator.variablesCache.get(declaredTerm.toString(), declaredSort.toString()); + if (termCacheHit == null) { + checkState(!creator.variablesCache.containsRow(declaredTerm.toString())); + creator.variablesCache.put( + declaredTerm.toString(), declaredSort.toString(), declaredTerm); + continue; + } else { + continue; + } + } + + Term funCacheHit = creator.functionsCache.get(declaredTerm.toString()); + // TODO: + if (funCacheHit == null) {} + } + + // Get the assertions out of the solver + if (parseSolver.getAssertions().length != 1) { + // If failing, conjugate the input and return + throw new AssertionError( + "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 " + "input"); + } + Term parsedTerm = parseSolver.getAssertions()[0]; + + checkState(!checkNotNull(parsedTerm).isNull()); + parseSolver.deletePointer(); + + return parsedTerm; } @Override From 2fa2ea62a8d1d2b5f1415c4d8dabce0e164c4ffd Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 27 Oct 2025 19:24:48 +0100 Subject: [PATCH 02/47] Enable CVC5 parser tests --- src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 2a975a3b24..735933b695 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -345,7 +345,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() { From a5a90b78393958fdff2603fa050d8628198dcc64 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 27 Oct 2025 19:25:12 +0100 Subject: [PATCH 03/47] Disable a slow test for CVC5 --- 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 40213bd4e0..30ebdf9a87 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2243,7 +2243,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 844b362675c76b6fc1ca855d8401ebee06753fd6 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 10:38:41 +0100 Subject: [PATCH 04/47] CVC5 parser: add substitution to known (cached) terms for the final term, as it creates new distinct terms when parsing --- .../solvers/cvc5/CVC5FormulaManager.java | 34 ++++++++++++++----- 1 file changed, 26 insertions(+), 8 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 514c70008c..d4c7faba24 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -12,6 +12,7 @@ import static com.google.common.base.Preconditions.checkState; import com.google.common.base.Joiner; +import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import de.uni_freiburg.informatik.ultimate.logic.PrintTerm; import io.github.cvc5.CVC5ApiException; @@ -89,11 +90,19 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { InputParser parser = new InputParser(parseSolver, sm); parser.setStringInput(InputLanguage.SMT_LIB_2_6, formulaStr, ""); + ImmutableSet.Builder substituteFrom = ImmutableSet.builder(); + ImmutableSet.Builder substituteTo = ImmutableSet.builder(); + Command command = parser.nextCommand(); while (!command.isNull()) { + if (command.toString().contains("push") || command.toString().contains("pop")) { + // TODO: push and pop? + throw new IllegalArgumentException( + "Parsing SMTLIB2 with CVC5 in JavaSMT does not support" + " push or pop currently."); + } + // This WILL read in asserts, and they are no longer available for getTerm(), but on the // solver as assertions - // TODO: pushs and pops? String invokeReturn = command.invoke(parseSolver, sm); if (!invokeReturn.equals(expectedSuccessMsg)) { throw new AssertionError("Unknown error when parsing using CVC5: " + invokeReturn); @@ -114,25 +123,34 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { checkState(!creator.variablesCache.containsRow(declaredTerm.toString())); creator.variablesCache.put( declaredTerm.toString(), declaredSort.toString(), declaredTerm); - continue; + } else { - continue; + substituteFrom.add(declaredTerm); + substituteTo.add(termCacheHit); } - } + } else { - Term funCacheHit = creator.functionsCache.get(declaredTerm.toString()); - // TODO: - if (funCacheHit == null) {} + Term funCacheHit = creator.functionsCache.get(declaredTerm.toString()); + // TODO: + if (funCacheHit == null) {} + throw new IllegalArgumentException("implement me"); + } } // Get the assertions out of the solver if (parseSolver.getAssertions().length != 1) { // If failing, conjugate the input and return throw new AssertionError( - "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 " + "input"); + "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 input"); } Term parsedTerm = parseSolver.getAssertions()[0]; + // If the symbols used in the term were already declared before parsing, the term uses new + // ones with the same name, so we need to substitute them! + parsedTerm = + parsedTerm.substitute( + substituteFrom.build().toArray(new Term[0]), substituteTo.build().toArray(new Term[0])); + checkState(!checkNotNull(parsedTerm).isNull()); parseSolver.deletePointer(); From 3b58ca2f8ca6f297fcaf399d606c120352b2122f Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 10:44:18 +0100 Subject: [PATCH 05/47] CVC5 parser: add some assertions before substituting terms at the end --- .../solvers/cvc5/CVC5FormulaManager.java | 23 ++++++++++++++----- 1 file changed, 17 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 d4c7faba24..cc337007d1 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -90,8 +90,8 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { InputParser parser = new InputParser(parseSolver, sm); parser.setStringInput(InputLanguage.SMT_LIB_2_6, formulaStr, ""); - ImmutableSet.Builder substituteFrom = ImmutableSet.builder(); - ImmutableSet.Builder substituteTo = ImmutableSet.builder(); + ImmutableSet.Builder substituteFromBuilder = ImmutableSet.builder(); + ImmutableSet.Builder substituteToBuilder = ImmutableSet.builder(); Command command = parser.nextCommand(); while (!command.isNull()) { @@ -125,14 +125,19 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { declaredTerm.toString(), declaredSort.toString(), declaredTerm); } else { - substituteFrom.add(declaredTerm); - substituteTo.add(termCacheHit); + substituteFromBuilder.add(declaredTerm); + substituteToBuilder.add(termCacheHit); } } else { Term funCacheHit = creator.functionsCache.get(declaredTerm.toString()); // TODO: - if (funCacheHit == null) {} + if (funCacheHit == null) { + + } else { + substituteFromBuilder.add(declaredTerm); + substituteToBuilder.add(funCacheHit); + } throw new IllegalArgumentException("implement me"); } } @@ -147,9 +152,15 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // If the symbols used in the term were already declared before parsing, the term uses new // ones with the same name, so we need to substitute them! + ImmutableSet substituteFrom = substituteFromBuilder.build(); + ImmutableSet substituteTo = substituteToBuilder.build(); + checkState(substituteFrom.size() == substituteTo.size()); + assert substituteFrom.stream() + .map(Term::toString) + .allMatch(from -> substituteTo.stream().map(Term::toString).anyMatch(from::equals)); parsedTerm = parsedTerm.substitute( - substituteFrom.build().toArray(new Term[0]), substituteTo.build().toArray(new Term[0])); + substituteFrom.toArray(new Term[0]), substituteTo.toArray(new Term[0])); checkState(!checkNotNull(parsedTerm).isNull()); parseSolver.deletePointer(); From 025f97ad2c04e8e88198d8f93c7a3afc645b9c18 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 10:56:08 +0100 Subject: [PATCH 06/47] CVC5 parser: add UF parsing with additional assertions (TODO: Quantifier parsing) --- .../solvers/cvc5/CVC5FormulaManager.java | 34 +++++++++++-------- 1 file changed, 19 insertions(+), 15 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 cc337007d1..6654407736 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -113,32 +113,36 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { parser.deletePointer(); // Register new terms in our caches - for (Term declaredTerm : sm.getDeclaredTerms()) { - Sort declaredSort = declaredTerm.getSort(); - // TODO: is isFunction() correct? - if (!declaredSort.isFunction()) { - Term termCacheHit = - creator.variablesCache.get(declaredTerm.toString(), declaredSort.toString()); + for (Term parsedTerm : sm.getDeclaredTerms()) { + String parsedTermString = parsedTerm.toString(); + Sort parsedSort = parsedTerm.getSort(); + String parsedSortString = parsedSort.toString(); + + // TODO: quantifiers and their bounds seems to be handled distinctly + + if (!parsedSort.isFunction()) { + Term termCacheHit = creator.variablesCache.get(parsedTermString, parsedSortString); if (termCacheHit == null) { - checkState(!creator.variablesCache.containsRow(declaredTerm.toString())); - creator.variablesCache.put( - declaredTerm.toString(), declaredSort.toString(), declaredTerm); + assert !creator.functionsCache.containsKey(parsedTermString); + checkState(!creator.variablesCache.containsRow(parsedTermString)); + creator.variablesCache.put(parsedTermString, parsedSortString, parsedTerm); } else { - substituteFromBuilder.add(declaredTerm); + substituteFromBuilder.add(parsedTerm); substituteToBuilder.add(termCacheHit); } - } else { - Term funCacheHit = creator.functionsCache.get(declaredTerm.toString()); - // TODO: + } else { + // UFs + Term funCacheHit = creator.functionsCache.get(parsedTermString); if (funCacheHit == null) { + assert !creator.variablesCache.contains(parsedTermString, parsedSortString); + creator.functionsCache.put(parsedTermString, parsedTerm); } else { - substituteFromBuilder.add(declaredTerm); + substituteFromBuilder.add(parsedTerm); substituteToBuilder.add(funCacheHit); } - throw new IllegalArgumentException("implement me"); } } From 71dee39eadc3efb515ff30964261f811c7b0da54 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 11:18:25 +0100 Subject: [PATCH 07/47] CVC5 parser: add info about quantifier/bound variable handling and add precondition about named terms (as they are currently not handled) --- .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 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 6654407736..84daa98d6e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -118,8 +118,6 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { Sort parsedSort = parsedTerm.getSort(); String parsedSortString = parsedSort.toString(); - // TODO: quantifiers and their bounds seems to be handled distinctly - if (!parsedSort.isFunction()) { Term termCacheHit = creator.variablesCache.get(parsedTermString, parsedSortString); if (termCacheHit == null) { @@ -146,6 +144,9 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { } } + // TODO: Which terms can end up here? + checkState(sm.getNamedTerms().isEmpty()); + // Get the assertions out of the solver if (parseSolver.getAssertions().length != 1) { // If failing, conjugate the input and return @@ -166,6 +167,10 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { parsedTerm.substitute( substituteFrom.toArray(new Term[0]), substituteTo.toArray(new Term[0])); + // Quantified formulas do not give us the bound variables in getDeclaredTerms() above. + // Find them and register a free equivalent + // TODO: + checkState(!checkNotNull(parsedTerm).isNull()); parseSolver.deletePointer(); From 13e130d09c429b9778e3de7932027f99ab25d3ba Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 11:36:09 +0100 Subject: [PATCH 08/47] CVC5 parser: refactor UF handling and unpack applied UFs before caching --- .../solvers/cvc5/CVC5FormulaManager.java | 56 ++++++++++++------- 1 file changed, 35 insertions(+), 21 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 84daa98d6e..379583072c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -114,33 +114,47 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Register new terms in our caches for (Term parsedTerm : sm.getDeclaredTerms()) { - String parsedTermString = parsedTerm.toString(); - Sort parsedSort = parsedTerm.getSort(); - String parsedSortString = parsedSort.toString(); + try { + Kind kind = parsedTerm.getKind(); + if (kind == Kind.APPLY_UF) { + parsedTerm = parsedTerm.getChild(0); + } - if (!parsedSort.isFunction()) { - Term termCacheHit = creator.variablesCache.get(parsedTermString, parsedSortString); - if (termCacheHit == null) { - assert !creator.functionsCache.containsKey(parsedTermString); - checkState(!creator.variablesCache.containsRow(parsedTermString)); - creator.variablesCache.put(parsedTermString, parsedSortString, parsedTerm); + String parsedTermString = parsedTerm.toString(); + Sort parsedSort = parsedTerm.getSort(); + String parsedSortString = parsedSort.toString(); - } else { - substituteFromBuilder.add(parsedTerm); - substituteToBuilder.add(termCacheHit); - } + if (parsedSort.isFunction()) { + // UFs + Term funCacheHit = creator.functionsCache.get(parsedTermString); + if (funCacheHit == null) { + assert !creator.variablesCache.contains(parsedTermString, parsedSortString); + creator.functionsCache.put(parsedTermString, parsedTerm); - } else { - // UFs - Term funCacheHit = creator.functionsCache.get(parsedTermString); - if (funCacheHit == null) { - assert !creator.variablesCache.contains(parsedTermString, parsedSortString); - creator.functionsCache.put(parsedTermString, parsedTerm); + } else { + substituteFromBuilder.add(parsedTerm); + substituteToBuilder.add(funCacheHit); + } } else { - substituteFromBuilder.add(parsedTerm); - substituteToBuilder.add(funCacheHit); + Term termCacheHit = creator.variablesCache.get(parsedTermString, parsedSortString); + if (termCacheHit == null) { + assert !creator.functionsCache.containsKey(parsedTermString); + checkState(!creator.variablesCache.containsRow(parsedTermString)); + creator.variablesCache.put(parsedTermString, parsedSortString, parsedTerm); + + } else { + substituteFromBuilder.add(parsedTerm); + substituteToBuilder.add(termCacheHit); + } } + } catch (CVC5ApiException apiException) { + throw new IllegalArgumentException( + "You tried reading a bool variable potentially in a UF application that failed. Checked" + + " term: " + + parsedTerm + + ".", + apiException); } } From 69cafaf0654e5c17d04977cebdd7be8e380e0c23 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 11:51:17 +0100 Subject: [PATCH 09/47] CVC5: improve retrieval method for free vars from cache for bound vars --- .../solvers/cvc5/CVC5FormulaCreator.java | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 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 bb2e4a10e1..0a0dc5846f 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -417,7 +417,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { // 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); + Term originalVar = getFreeVariableFromCache(formula.toString(), sort); return visitor.visitBoundVariable(encapsulate(originalVar), 0); } else if (f.getKind() == Kind.FORALL || f.getKind() == Kind.EXISTS) { @@ -427,7 +427,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 = getFreeVariableFromCache(name, boundVar.getSort()); body = body.substitute(boundVar, freeVar); freeVars.add(encapsulate(freeVar)); } @@ -845,14 +845,20 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep return FloatingPointNumber.of(bits, expWidth, mantWidth); } - private Term accessVariablesCache(String name, Sort sort) { + /** + * Returns the free variable for the given name and sort of a bound variable from the variables + * cache. Will throw a {@link NullPointerException} if no variable is known for the input! + */ + private Term getFreeVariableFromCache(String name, Sort sort) { Term existingVar = variablesCache.get(name, sort.toString()); Preconditions.checkNotNull( existingVar, - "Symbol %s requested with type %s, but already used with type %s", + "Symbol %s requested with type %s, but %s", name, sort, - variablesCache.row(name).keySet()); + variablesCache.containsRow(name) + ? "the used symbol is already registered with type " + variablesCache.row(name).keySet() + : "the used symbol is unknown to the variables cache"); return existingVar; } } From 95d1de55f7aa1e1f83b133f6d0ca0a8592d1adc1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 11:52:41 +0100 Subject: [PATCH 10/47] CVC5: only use static imports for the 3 precondition methods to make code more readable --- .../java_smt/solvers/cvc5/CVC5FormulaCreator.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 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 0a0dc5846f..13899ea3b6 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -9,9 +9,9 @@ package org.sosy_lab.java_smt.solvers.cvc5; import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; -import com.google.common.base.Preconditions; import com.google.common.base.Splitter; import com.google.common.collect.FluentIterable; import com.google.common.collect.HashBasedTable; @@ -103,7 +103,7 @@ public Term makeVariable(Sort sort, String name) { if (existingVar != null) { return existingVar; } - Preconditions.checkArgument( + checkArgument( !variablesCache.containsRow(name), "Symbol %s requested with type %s, but already used with type %s", name, @@ -439,7 +439,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { return visitor.visitFreeVariable(formula, dequote(f.toString())); } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) { - Preconditions.checkState( + checkState( f.getNumChildren() == 1, "Unexpected formula '%s' with sort '%s'", f, f.getSort()); return visitor.visitConstant(formula, f.getChild(0).getSymbol()); @@ -765,7 +765,7 @@ public Term declareUFImpl(String pName, Sort pReturnType, List pArgTypes) functionsCache.put(pName, exp); } else { - Preconditions.checkArgument( + checkArgument( exp.getSort().equals(exp.getSort()), "Symbol %s already in use for different return type %s", exp, @@ -773,7 +773,7 @@ public Term declareUFImpl(String pName, Sort pReturnType, List pArgTypes) for (int i = 1; i < exp.getNumChildren(); i++) { // CVC5s first argument in a function/Uf is the declaration, we don't need that here try { - Preconditions.checkArgument( + checkArgument( pArgTypes.get(i).equals(exp.getChild(i).getSort()), "Argument %s with type %s does not match expected type %s", i - 1, @@ -840,7 +840,7 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep final var expWidth = Ints.checkedCast(fpValue.first); final var mantWidth = Ints.checkedCast(fpValue.second - 1); // without sign bit final var bvValue = fpValue.third; - Preconditions.checkState(bvValue.isBitVectorValue()); + checkState(bvValue.isBitVectorValue()); final var bits = bvValue.getBitVectorValue(); return FloatingPointNumber.of(bits, expWidth, mantWidth); } @@ -851,7 +851,7 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep */ private Term getFreeVariableFromCache(String name, Sort sort) { Term existingVar = variablesCache.get(name, sort.toString()); - Preconditions.checkNotNull( + checkNotNull( existingVar, "Symbol %s requested with type %s, but %s", name, From da723000218c23ae454eb573fc300b55f0138fe2 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 11:53:12 +0100 Subject: [PATCH 11/47] CVC5: refactor return in creator method getFreeVariableFromCache() --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java | 3 +-- 1 file changed, 1 insertion(+), 2 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 13899ea3b6..ea4f79d657 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -851,7 +851,7 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep */ private Term getFreeVariableFromCache(String name, Sort sort) { Term existingVar = variablesCache.get(name, sort.toString()); - checkNotNull( + return checkNotNull( existingVar, "Symbol %s requested with type %s, but %s", name, @@ -859,6 +859,5 @@ private Term getFreeVariableFromCache(String name, Sort sort) { variablesCache.containsRow(name) ? "the used symbol is already registered with type " + variablesCache.row(name).keySet() : "the used symbol is unknown to the variables cache"); - return existingVar; } } From 4900b2fab9ee615c964dd10507fbf2927ab1ce63 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 13:14:36 +0100 Subject: [PATCH 12/47] CVC5: use a custom visitor to visit all bound variables after parsing to register their free counterparts --- .../solvers/cvc5/CVC5FormulaCreator.java | 100 +++++++++++++++++- .../solvers/cvc5/CVC5FormulaManager.java | 10 +- 2 files changed, 101 insertions(+), 9 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 ea4f79d657..ffcb3f9537 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -32,10 +32,14 @@ import io.github.cvc5.Term; import io.github.cvc5.TermManager; import java.math.BigInteger; +import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Deque; import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.ArrayFormula; @@ -48,11 +52,13 @@ import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.RegexFormula; import org.sosy_lab.java_smt.api.StringFormula; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5ArrayFormula; @@ -78,6 +84,7 @@ public class CVC5FormulaCreator extends FormulaCreator variablesCache = HashBasedTable.create(); protected final Map functionsCache = new HashMap<>(); + protected boolean registerUnknownBoundVariables = false; private final TermManager termManager; private final Solver solver; @@ -417,7 +424,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { // 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 = getFreeVariableFromCache(formula.toString(), sort); + Term originalVar = getFreeVariableFromCache(formula.toString(), sort, visitor); return visitor.visitBoundVariable(encapsulate(originalVar), 0); } else if (f.getKind() == Kind.FORALL || f.getKind() == Kind.EXISTS) { @@ -427,7 +434,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 = getFreeVariableFromCache(name, boundVar.getSort()); + Term freeVar = getFreeVariableFromCache(name, boundVar.getSort(), visitor); body = body.substitute(boundVar, freeVar); freeVars.add(encapsulate(freeVar)); } @@ -849,7 +856,10 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep * Returns the free variable for the given name and sort of a bound variable from the variables * cache. Will throw a {@link NullPointerException} if no variable is known for the input! */ - private Term getFreeVariableFromCache(String name, Sort sort) { + private Term getFreeVariableFromCache(String name, Sort sort, FormulaVisitor visitor) { + if (visitor instanceof BoundVariablesRegisteringRecursiveVisitor) { + ((BoundVariablesRegisteringRecursiveVisitor) visitor).registerBoundVariable(name, sort); + } Term existingVar = variablesCache.get(name, sort.toString()); return checkNotNull( existingVar, @@ -860,4 +870,88 @@ private Term getFreeVariableFromCache(String name, Sort sort) { ? "the used symbol is already registered with type " + variablesCache.row(name).keySet() : "the used symbol is unknown to the variables cache"); } + + /** + * Caches all bound variables nested in the boolean input term that are unknown to the variable + * cache with a free variable copy in it. + */ + protected void registerBoundVariablesWithVisitor(Term input) { + checkArgument( + input.getSort().isBoolean(), + "Only boolean terms can be used to register " + "bound variables as free variables!"); + + BoundVariablesRegisteringRecursiveVisitor boundVariablesRegisteringRecursiveVisitor = + new BoundVariablesRegisteringRecursiveVisitor(this); + + boundVariablesRegisteringRecursiveVisitor.addToQueue(encapsulateBoolean(input)); + while (!boundVariablesRegisteringRecursiveVisitor.isQueueEmpty()) { + Formula tt = boundVariablesRegisteringRecursiveVisitor.pop(); + TraversalProcess process = visit(tt, boundVariablesRegisteringRecursiveVisitor); + if (process == TraversalProcess.ABORT) { + return; + } + } + } + + private static final class BoundVariablesRegisteringRecursiveVisitor + implements FormulaVisitor { + + private final Set seen = new HashSet<>(); + private final Deque toVisit = new ArrayDeque<>(); + + private final CVC5FormulaCreator usedCreator; + + BoundVariablesRegisteringRecursiveVisitor(CVC5FormulaCreator pCreator) { + usedCreator = checkNotNull(pCreator); + } + + private void registerBoundVariable(String boundVariableName, Sort boundVarSort) { + String boundSort = boundVarSort.toString(); + Term existingVar = usedCreator.variablesCache.get(boundVariableName, boundSort); + if (existingVar == null) { + existingVar = usedCreator.makeVariable(boundVarSort, boundVariableName); + usedCreator.variablesCache.put(boundVariableName, boundSort, existingVar); + } + } + + void addToQueue(Formula f) { + if (seen.add(f)) { + toVisit.push(f); + } + } + + boolean isQueueEmpty() { + return toVisit.isEmpty(); + } + + Formula pop() { + return toVisit.pop(); + } + + @Override + public TraversalProcess visitFreeVariable(Formula pF, String pName) { + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitConstant(Formula pF, Object pValue) { + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitFunction( + Formula pF, List pArgs, FunctionDeclaration pFunctionDeclaration) { + for (Formula f : pArgs) { + addToQueue(f); + } + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitQuantifier( + BooleanFormula pF, Quantifier pQuantifier, List boundVars, BooleanFormula pBody) { + addToQueue(pBody); + return TraversalProcess.CONTINUE; + } + } } 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 379583072c..a3f6ec4179 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -110,7 +110,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { command = parser.nextCommand(); } - parser.deletePointer(); + parser.deletePointer(); // Clean up parser // Register new terms in our caches for (Term parsedTerm : sm.getDeclaredTerms()) { @@ -168,6 +168,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 input"); } Term parsedTerm = parseSolver.getAssertions()[0]; + checkState(!checkNotNull(parsedTerm).isNull()); // If the symbols used in the term were already declared before parsing, the term uses new // ones with the same name, so we need to substitute them! @@ -183,11 +184,8 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Quantified formulas do not give us the bound variables in getDeclaredTerms() above. // Find them and register a free equivalent - // TODO: - - checkState(!checkNotNull(parsedTerm).isNull()); - parseSolver.deletePointer(); - + creator.registerBoundVariablesWithVisitor(parsedTerm); + parseSolver.deletePointer(); // Clean up parse solver return parsedTerm; } From 55e572eb16dbb1bcb48704ce14c24c78a976efa9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 16:29:43 +0100 Subject: [PATCH 13/47] Add tests for multi-dimensional arrays not based on parsing SMTLIB2 (as not every solver can do that!) for int and bv arrays --- src/org/sosy_lab/java_smt/test/ModelTest.java | 121 ++++++++++++++++++ 1 file changed, 121 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 40213bd4e0..09ff827066 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -14,6 +14,7 @@ import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; +import static org.sosy_lab.java_smt.api.FormulaType.getBitvectorTypeWithSize; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.collect.ImmutableList; @@ -79,6 +80,8 @@ public class ModelTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { private static final ArrayFormulaType ARRAY_TYPE_INT_INT = FormulaType.getArrayType(IntegerType, IntegerType); + private static final ArrayFormulaType ARRAY_TYPE_BV32_BV32 = + FormulaType.getArrayType(getBitvectorTypeWithSize(32), getBitvectorTypeWithSize(32)); private static final ImmutableList SOLVERS_WITH_PARTIAL_MODEL = ImmutableList.of(Solvers.Z3); @@ -1145,6 +1148,124 @@ public void testGetArrays6() throws SolverException, InterruptedException { testModelIterator(f); } + @Test + public void testGetArrays3IntegerNoParsing() throws SolverException, InterruptedException { + requireIntegers(); + requireArrays(); + requireArrayModel(); + + assume() + .withMessage("Solvers have problems with multi-dimensional arrays") + .that(solverToUse()) + .isNoneOf(Solvers.PRINCESS, Solvers.CVC4, Solvers.YICES2); + + // (= (select (select (select arr 5) 3) 1) x) + // (= x 123)" + ArrayFormulaType innerType = + FormulaType.getArrayType(IntegerType, IntegerType); + ArrayFormulaType> middleType = + FormulaType.getArrayType(IntegerType, innerType); + ArrayFormulaType< + IntegerFormula, + ArrayFormula>> + type = FormulaType.getArrayType(IntegerType, middleType); + + IntegerFormula num1 = imgr.makeNumber(1); + IntegerFormula num3 = imgr.makeNumber(3); + IntegerFormula num5 = imgr.makeNumber(5); + IntegerFormula num123 = imgr.makeNumber(123); + IntegerFormula x = imgr.makeVariable("x"); + ArrayFormula< + IntegerFormula, + ArrayFormula>> + arr = amgr.makeArray("arr", type); + + BooleanFormula f = + bmgr.and( + imgr.equal(x, amgr.select(amgr.select(amgr.select(arr, num5), num3), num1)), + imgr.equal(x, num123)); + + testModelIterator(f); + testModelGetters(f, imgr.makeVariable("x"), BigInteger.valueOf(123), "x"); + ArrayFormulaType< + IntegerFormula, + ArrayFormula>> + arrType = + FormulaType.getArrayType( + IntegerType, FormulaType.getArrayType(IntegerType, ARRAY_TYPE_INT_INT)); + testModelGetters( + f, + amgr.select( + amgr.select( + amgr.select(amgr.makeArray("arr", arrType), imgr.makeNumber(5)), + imgr.makeNumber(3)), + imgr.makeNumber(1)), + BigInteger.valueOf(123), + "arr", + true, + ImmutableList.of(BigInteger.valueOf(5), BigInteger.valueOf(3), BigInteger.ONE)); + } + + @Test + public void testGetArrays3BitvectorNoParsing() throws SolverException, InterruptedException { + requireBitvectors(); + requireArrays(); + requireArrayModel(); + + assume() + .withMessage("Solvers have problems with multi-dimensional arrays") + .that(solverToUse()) + .isNoneOf( + Solvers.PRINCESS, Solvers.CVC4, Solvers.YICES2, Solvers.BOOLECTOR, Solvers.BITWUZLA); + + // (= (select (select (select arr 5) 3) 1) x) + // (= x 123)" + BitvectorType bvType = getBitvectorTypeWithSize(32); + ArrayFormulaType innerType = + FormulaType.getArrayType(bvType, bvType); + ArrayFormulaType> + middleType = FormulaType.getArrayType(bvType, innerType); + ArrayFormulaType< + BitvectorFormula, + ArrayFormula>> + type = FormulaType.getArrayType(bvType, middleType); + + BitvectorFormula num1 = bvmgr.makeBitvector(32, 1); + BitvectorFormula num3 = bvmgr.makeBitvector(32, 3); + BitvectorFormula num5 = bvmgr.makeBitvector(32, 5); + BitvectorFormula num123 = bvmgr.makeBitvector(32, 123); + BitvectorFormula x = bvmgr.makeVariable(32, "x"); + ArrayFormula< + BitvectorFormula, + ArrayFormula>> + arr = amgr.makeArray("arr", type); + + BooleanFormula f = + bmgr.and( + bvmgr.equal(x, amgr.select(amgr.select(amgr.select(arr, num5), num3), num1)), + bvmgr.equal(x, num123)); + + testModelIterator(f); + testModelGetters(f, bvmgr.makeVariable(32, "x"), BigInteger.valueOf(123), "x"); + ArrayFormulaType< + BitvectorFormula, + ArrayFormula>> + arrType = + FormulaType.getArrayType( + bvType, FormulaType.getArrayType(bvType, ARRAY_TYPE_BV32_BV32)); + testModelGetters( + f, + amgr.select( + amgr.select( + amgr.select(amgr.makeArray("arr", arrType), bvmgr.makeBitvector(32, 5)), + bvmgr.makeBitvector(32, 3)), + bvmgr.makeBitvector(32, 1)), + BigInteger.valueOf(123), + "arr", + true, + ImmutableList.of(BigInteger.valueOf(5), BigInteger.valueOf(3), BigInteger.ONE)); + } + @Test public void testGetArrays3() throws SolverException, InterruptedException { requireParser(); From d13c807d494da2f1966240b5ee785f99594c235e Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 16:31:24 +0100 Subject: [PATCH 14/47] CVC5 parser: apply checkstyle suggestion --- .../solvers/cvc5/CVC5FormulaManager.java | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 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 a3f6ec4179..fc9e499662 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -114,14 +114,15 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Register new terms in our caches for (Term parsedTerm : sm.getDeclaredTerms()) { + Term termToRegister = parsedTerm; try { - Kind kind = parsedTerm.getKind(); + Kind kind = termToRegister.getKind(); if (kind == Kind.APPLY_UF) { - parsedTerm = parsedTerm.getChild(0); + termToRegister = termToRegister.getChild(0); } - String parsedTermString = parsedTerm.toString(); - Sort parsedSort = parsedTerm.getSort(); + String parsedTermString = termToRegister.toString(); + Sort parsedSort = termToRegister.getSort(); String parsedSortString = parsedSort.toString(); if (parsedSort.isFunction()) { @@ -129,10 +130,10 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { Term funCacheHit = creator.functionsCache.get(parsedTermString); if (funCacheHit == null) { assert !creator.variablesCache.contains(parsedTermString, parsedSortString); - creator.functionsCache.put(parsedTermString, parsedTerm); + creator.functionsCache.put(parsedTermString, termToRegister); } else { - substituteFromBuilder.add(parsedTerm); + substituteFromBuilder.add(termToRegister); substituteToBuilder.add(funCacheHit); } @@ -141,10 +142,10 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { if (termCacheHit == null) { assert !creator.functionsCache.containsKey(parsedTermString); checkState(!creator.variablesCache.containsRow(parsedTermString)); - creator.variablesCache.put(parsedTermString, parsedSortString, parsedTerm); + creator.variablesCache.put(parsedTermString, parsedSortString, termToRegister); } else { - substituteFromBuilder.add(parsedTerm); + substituteFromBuilder.add(termToRegister); substituteToBuilder.add(termCacheHit); } } From df00d8d40d572d0517a5d7983008993b3715baca Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 16:52:25 +0100 Subject: [PATCH 15/47] CVC5 Model: add improved array evaluation from Daniel Raffler with minor modifications from 0d463c83410a332ed81ff4f7628d25ae729b3782 --- .../java_smt/solvers/cvc5/CVC5Model.java | 120 ++++++++++++++++-- 1 file changed, 111 insertions(+), 9 deletions(-) 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 dc57d3c5cf..af5ae12f06 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; @@ -21,6 +22,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.basicimpl.AbstractEvaluator; import org.sosy_lab.java_smt.basicimpl.AbstractModel; public class CVC5Model extends AbstractModel { @@ -81,7 +83,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 +171,97 @@ 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(this::evaluateImpl) + .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 +285,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 From c7f8be35615ec37a04d94769359b82003e4dc0b9 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 17:07:25 +0100 Subject: [PATCH 16/47] CVC5 Parser: clean up error messages and add more doc for them --- .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 12 +++++------- 1 file changed, 5 insertions(+), 7 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 fc9e499662..034b51ac7e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -82,6 +82,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { try { parseSolver.setLogic("ALL"); } catch (CVC5ApiException e) { + // Should never happen in this configuration throw new AssertionError("Unexpected exception", e); } } @@ -103,6 +104,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // This WILL read in asserts, and they are no longer available for getTerm(), but on the // solver as assertions + // invoke() throws CVC5ParserException for errors String invokeReturn = command.invoke(parseSolver, sm); if (!invokeReturn.equals(expectedSuccessMsg)) { throw new AssertionError("Unknown error when parsing using CVC5: " + invokeReturn); @@ -151,21 +153,17 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { } } catch (CVC5ApiException apiException) { throw new IllegalArgumentException( - "You tried reading a bool variable potentially in a UF application that failed. Checked" - + " term: " - + parsedTerm - + ".", - apiException); + "Error parsing the following term in CVC5: " + parsedTerm, apiException); } } - // TODO: Which terms can end up here? + // TODO: Which terms can end up here? Seems like this is always empty checkState(sm.getNamedTerms().isEmpty()); // Get the assertions out of the solver if (parseSolver.getAssertions().length != 1) { // If failing, conjugate the input and return - throw new AssertionError( + throw new IllegalArgumentException( "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 input"); } Term parsedTerm = parseSolver.getAssertions()[0]; From fd562b35fb4f75089250a6dbd1238d6db0e673ce Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 17:07:54 +0100 Subject: [PATCH 17/47] CVC5 Model: format --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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 af5ae12f06..8622407852 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java @@ -22,7 +22,6 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; -import org.sosy_lab.java_smt.basicimpl.AbstractEvaluator; import org.sosy_lab.java_smt.basicimpl.AbstractModel; public class CVC5Model extends AbstractModel { @@ -240,9 +239,7 @@ private Iterable buildArrayAssignment(Term expr, Term value) { creator.encapsulateBoolean(equation), getVar(expr), creator.convertValue(element, element), - FluentIterable.from(getArgs(select)) - .transform(this::evaluateImpl) - .toList())); + FluentIterable.from(getArgs(select)).transform(this::evaluateImpl).toList())); } return FluentIterable.concat(current, buildArrayAssignment(expr, value.getChild(0))); From 8cbd003c0f7fdb182807f3b1c33f4a2dbacf9df8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 17:09:21 +0100 Subject: [PATCH 18/47] CVC5 parser: improve doc location and text for an error --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 034b51ac7e..28ddd718ee 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -104,11 +104,11 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // This WILL read in asserts, and they are no longer available for getTerm(), but on the // solver as assertions - // invoke() throws CVC5ParserException for errors String invokeReturn = command.invoke(parseSolver, sm); if (!invokeReturn.equals(expectedSuccessMsg)) { throw new AssertionError("Unknown error when parsing using CVC5: " + invokeReturn); } + // nextCommand() throws CVC5ParserException for errors command = parser.nextCommand(); } From d56b3e95ddecaca342878f9948df9e5d66113a60 Mon Sep 17 00:00:00 2001 From: BaierD Date: Tue, 28 Oct 2025 21:58:09 +0100 Subject: [PATCH 19/47] CVC5 parser: replace all expressions using dot (e.g .def_ ) as first char when defining expressions and re-substitute the terms later on (only works for Mathsat most likely, but no other solver returns something like this!) --- .../solvers/cvc5/CVC5FormulaManager.java | 64 +++++++++++++++++-- 1 file changed, 59 insertions(+), 5 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 28ddd718ee..caa856fa25 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -12,6 +12,7 @@ import static com.google.common.base.Preconditions.checkState; import com.google.common.base.Joiner; +import com.google.common.collect.ImmutableBiMap; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import de.uni_freiburg.informatik.ultimate.logic.PrintTerm; @@ -27,6 +28,9 @@ import io.github.cvc5.modes.InputLanguage; import java.util.LinkedHashMap; import java.util.Map; +import java.util.Map.Entry; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -89,7 +93,35 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { String expectedSuccessMsg = "success\n"; parseSolver.setOption("print-success", "true"); InputParser parser = new InputParser(parseSolver, sm); - parser.setStringInput(InputLanguage.SMT_LIB_2_6, formulaStr, ""); + + // Sanitize input String for CVC5 (it disallows . and @ without quotes) + String sanitizedInputFormula = formulaStr; + ImmutableBiMap replacementMap = null; + if (sanitizedInputFormula.contains("define-fun .def_")) { + // MathSAT5 output, resubstitute + ImmutableBiMap.Builder replacementMapBuilder = ImmutableBiMap.builder(); + // Since no quotes are used, we can assume that there are no spaces in the defined name + String pattern = "(define-fun \\.)[^\\s]+"; + Pattern r = Pattern.compile(pattern); + Matcher m = r.matcher(sanitizedInputFormula); + + while (m.find()) { + String match = m.group(); + String bare = match.replace("define-fun ", ""); // to replace + String replacement = "|" + bare.substring(1, bare.length()) + "|"; + checkState(!sanitizedInputFormula.contains(replacement)); + replacementMapBuilder.put(bare, replacement); + } + + replacementMap = replacementMapBuilder.buildOrThrow(); + for (Entry replacementEntry : replacementMap.entrySet()) { + sanitizedInputFormula = + sanitizedInputFormula.replace(replacementEntry.getKey(), replacementEntry.getValue()); + } + checkState(!sanitizedInputFormula.contains("define-fun .")); + } + + parser.setStringInput(InputLanguage.SMT_LIB_2_6, sanitizedInputFormula, ""); ImmutableSet.Builder substituteFromBuilder = ImmutableSet.builder(); ImmutableSet.Builder substituteToBuilder = ImmutableSet.builder(); @@ -99,7 +131,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { if (command.toString().contains("push") || command.toString().contains("pop")) { // TODO: push and pop? throw new IllegalArgumentException( - "Parsing SMTLIB2 with CVC5 in JavaSMT does not support" + " push or pop currently."); + "Parsing SMTLIB2 with CVC5 in JavaSMT does not support push or pop currently."); } // This WILL read in asserts, and they are no longer available for getTerm(), but on the @@ -161,13 +193,35 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { checkState(sm.getNamedTerms().isEmpty()); // Get the assertions out of the solver - if (parseSolver.getAssertions().length != 1) { + Term[] assertions = parseSolver.getAssertions(); + checkState(assertions.length > 0); + Term parsedTerm = assertions[assertions.length - 1]; + checkState(!checkNotNull(parsedTerm).isNull()); + if (assertions.length > 1 && replacementMap != null) { + // re-substitute MathSAT5 input + try { + for (int i = assertions.length - 2; i >= 0; i--) { + Term equation = assertions[i]; + + if (equation.getKind() != Kind.EQUAL) { + // Original problem we try to solve + throw new IllegalArgumentException( + "Error when parsing using CVC5, no expressions may use a . or " + + "@ as first character in a symbol."); + } + + parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); + } + } catch (CVC5ApiException apiException) { + throw new IllegalArgumentException( + "Error parsing the following term in CVC5: " + parsedTerm, apiException); + } + + } else if (assertions.length != 1) { // If failing, conjugate the input and return throw new IllegalArgumentException( "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 input"); } - Term parsedTerm = parseSolver.getAssertions()[0]; - checkState(!checkNotNull(parsedTerm).isNull()); // If the symbols used in the term were already declared before parsing, the term uses new // ones with the same name, so we need to substitute them! From de7bddde465227b8b1473d8d6458ab3589926032 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 09:17:26 +0100 Subject: [PATCH 20/47] CVC5 parser: use substring method with less arguments --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 caa856fa25..576e01182c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -108,7 +108,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { while (m.find()) { String match = m.group(); String bare = match.replace("define-fun ", ""); // to replace - String replacement = "|" + bare.substring(1, bare.length()) + "|"; + String replacement = "|" + bare.substring(1) + "|"; checkState(!sanitizedInputFormula.contains(replacement)); replacementMapBuilder.put(bare, replacement); } From 81add689485ecf31f2ff71c250109ad0a75cf1ba Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 09:21:22 +0100 Subject: [PATCH 21/47] CVC5 parser: throw IllegalArgumentException instead of AssertionError for an error --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 576e01182c..661aa18bbf 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -138,7 +138,8 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // solver as assertions String invokeReturn = command.invoke(parseSolver, sm); if (!invokeReturn.equals(expectedSuccessMsg)) { - throw new AssertionError("Unknown error when parsing using CVC5: " + invokeReturn); + throw new IllegalArgumentException( + "Unknown error when parsing using CVC5: " + invokeReturn); } // nextCommand() throws CVC5ParserException for errors command = parser.nextCommand(); From baf545825f829bf4cd6983de59d4f2a63a9226a2 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 09:40:40 +0100 Subject: [PATCH 22/47] CVC5 parser: catch CVC5ParseExeception and rethrow as IllegalArgumentException instead --- .../solvers/cvc5/CVC5FormulaManager.java | 32 +++++++++++++++---- 1 file changed, 26 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 661aa18bbf..9c64686497 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -126,7 +126,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { ImmutableSet.Builder substituteFromBuilder = ImmutableSet.builder(); ImmutableSet.Builder substituteToBuilder = ImmutableSet.builder(); - Command command = parser.nextCommand(); + Command command = getNextCommand(parser); while (!command.isNull()) { if (command.toString().contains("push") || command.toString().contains("pop")) { // TODO: push and pop? @@ -136,13 +136,13 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // This WILL read in asserts, and they are no longer available for getTerm(), but on the // solver as assertions - String invokeReturn = command.invoke(parseSolver, sm); + String invokeReturn = invokeCommand(command, parseSolver, sm); + if (!invokeReturn.equals(expectedSuccessMsg)) { - throw new IllegalArgumentException( - "Unknown error when parsing using CVC5: " + invokeReturn); + throw new IllegalArgumentException("Error when parsing using CVC5: " + invokeReturn); } - // nextCommand() throws CVC5ParserException for errors - command = parser.nextCommand(); + + command = getNextCommand(parser); } parser.deletePointer(); // Clean up parser @@ -298,4 +298,24 @@ public T substitute( FormulaType type = getFormulaType(f); return getFormulaCreator().encapsulate(type, input.substitute(changeFrom, changeTo)); } + + private Command getNextCommand(InputParser parser) { + try { + // throws CVC5ParserException for errors + return parser.nextCommand(); + } catch (Exception parseException) { + throw new IllegalArgumentException( + "Error parsing with CVC5: " + parseException.getMessage(), parseException); + } + } + + private String invokeCommand(Command command, Solver parseSolver, SymbolManager sm) { + try { + // throws CVC5ParserException for errors + return command.invoke(parseSolver, sm); + } catch (Exception parseException) { + throw new IllegalArgumentException( + "Error parsing with CVC5 " + parseException.getMessage(), parseException); + } + } } From 3d2d434e1f818037f092ae4757acf7bd7e0a47af Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 09:56:56 +0100 Subject: [PATCH 23/47] CVC5 parser: disallow multiple sorts for the same term name --- .../solvers/cvc5/CVC5FormulaManager.java | 27 +++++++++++++++---- 1 file changed, 22 insertions(+), 5 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 9c64686497..479e652e53 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -160,11 +160,31 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { Sort parsedSort = termToRegister.getSort(); String parsedSortString = parsedSort.toString(); + Term funCacheHit = creator.functionsCache.get(parsedTermString); + Map termRowHit = creator.variablesCache.row(parsedTermString); + Term termCacheHit = termRowHit.get(parsedSortString); + + if (funCacheHit != null && termCacheHit != null) { + throw new IllegalArgumentException( + "Error parsing with CVC5: the parsed term " + + parsedTermString + + " is parsed with the 2 distinct sorts " + + parsedSortString + + " and " + + funCacheHit.getSort()); + } else if (!termRowHit.isEmpty() && !termRowHit.containsKey(parsedSortString)) { + throw new IllegalArgumentException( + "Error parsing with CVC5: the parsed term " + + parsedTermString + + " is parsed with the 2 distinct sorts " + + parsedSortString + + " and " + + termRowHit.keySet()); + } + if (parsedSort.isFunction()) { // UFs - Term funCacheHit = creator.functionsCache.get(parsedTermString); if (funCacheHit == null) { - assert !creator.variablesCache.contains(parsedTermString, parsedSortString); creator.functionsCache.put(parsedTermString, termToRegister); } else { @@ -173,10 +193,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { } } else { - Term termCacheHit = creator.variablesCache.get(parsedTermString, parsedSortString); if (termCacheHit == null) { - assert !creator.functionsCache.containsKey(parsedTermString); - checkState(!creator.variablesCache.containsRow(parsedTermString)); creator.variablesCache.put(parsedTermString, parsedSortString, termToRegister); } else { From f6fd8eaa108f77a043b2847f203ee7fad58fa95f Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 13:16:27 +0100 Subject: [PATCH 24/47] CVC5 parser: properly track number of actually parsed assertions + re-substitute function-definitions that are added as assertions into the assertion --- .../solvers/cvc5/CVC5FormulaManager.java | 52 +++++++++++++++---- 1 file changed, 41 insertions(+), 11 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 479e652e53..368df7acc2 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.solvers.cvc5; +import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; @@ -126,6 +127,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { ImmutableSet.Builder substituteFromBuilder = ImmutableSet.builder(); ImmutableSet.Builder substituteToBuilder = ImmutableSet.builder(); + int numberOfAssertions = 0; Command command = getNextCommand(parser); while (!command.isNull()) { if (command.toString().contains("push") || command.toString().contains("pop")) { @@ -134,6 +136,10 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { "Parsing SMTLIB2 with CVC5 in JavaSMT does not support push or pop currently."); } + if (command.toString().startsWith("(assert ")) { + numberOfAssertions++; + } + // This WILL read in asserts, and they are no longer available for getTerm(), but on the // solver as assertions String invokeReturn = invokeCommand(command, parseSolver, sm); @@ -212,12 +218,26 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Get the assertions out of the solver Term[] assertions = parseSolver.getAssertions(); - checkState(assertions.length > 0); + checkArgument( + numberOfAssertions > 0, + "Error when parsing using CVC5: at least one assert " + + "statement needs to be part of the input"); + + // If failing, conjugate the input and return + // (We disallow push and pop currently, so this is fine!) + // TODO: this can be improved, but we need to be able to discern the non-assertion terms to + // re-substitute (we can just remember them before invoking the commands above) + checkArgument( + numberOfAssertions == 1, + "Error when parsing using CVC5: at most one assert " + + "statement is currently allowed to be part of the input"); + checkArgument(assertions.length > 0, "Error when parsing using CVC5: no term found to return"); Term parsedTerm = assertions[assertions.length - 1]; checkState(!checkNotNull(parsedTerm).isNull()); - if (assertions.length > 1 && replacementMap != null) { - // re-substitute MathSAT5 input - try { + + try { + if (assertions.length > 1 && replacementMap != null) { + // re-substitute MathSAT5 input for (int i = assertions.length - 2; i >= 0; i--) { Term equation = assertions[i]; @@ -230,15 +250,25 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); } - } catch (CVC5ApiException apiException) { - throw new IllegalArgumentException( - "Error parsing the following term in CVC5: " + parsedTerm, apiException); - } - } else if (assertions.length != 1) { - // If failing, conjugate the input and return + } else if (assertions.length != 1) { + // Sometimes terms are added as assertions without them being sources by an assertion, but + // a fun-def. We re-substitute these! + for (int i = assertions.length - 2; i >= 0; i--) { + Term equation = assertions[i]; + + if (equation.getKind() != Kind.EQUAL) { + // Original problem description we try to solve + throw new IllegalArgumentException( + "Error when parsing using CVC5: re-substitution of function-definitions into " + + "assertions failed"); + } + parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); + } + } + } catch (CVC5ApiException apiException) { throw new IllegalArgumentException( - "Error when parsing using CVC5: more than 1 assertion in SMTLIB2 input"); + "Error parsing the following term in CVC5: " + parsedTerm, apiException); } // If the symbols used in the term were already declared before parsing, the term uses new From 06800de085646037e29c80a045233091ea917215 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 13:34:54 +0100 Subject: [PATCH 25/47] CVC5 dump: refactor collecting and transformation of variables and UFs to SMTLIB2 --- .../solvers/cvc5/CVC5FormulaManager.java | 28 +++++++++++-------- 1 file changed, 17 insertions(+), 11 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 368df7acc2..5f5b953636 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -14,6 +14,7 @@ import com.google.common.base.Joiner; import com.google.common.collect.ImmutableBiMap; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import de.uni_freiburg.informatik.ultimate.logic.PrintTerm; @@ -295,18 +296,26 @@ public String dumpFormulaImpl(Term f) { assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType : "Only BooleanFormulas may be dumped"; - StringBuilder out = new StringBuilder(); + StringBuilder variablesAndUFsAsSMTLIB2 = getAllDeclaredVariablesAndUFsAsSMTLIB2(f); + + // now add the final assert + variablesAndUFsAsSMTLIB2.append("(assert ").append(f).append(')'); + return variablesAndUFsAsSMTLIB2.toString(); + } + + private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { + StringBuilder variablesAndUFsAsSMTLIB2 = new StringBuilder(); // get all symbols - final Map allVars = new LinkedHashMap<>(); - creator.extractVariablesAndUFs(f, true, allVars::put); + ImmutableMap.Builder allKnownVarsAndUFsBuilder = ImmutableMap.builder(); + creator.extractVariablesAndUFs(f, true, allKnownVarsAndUFsBuilder::put); // print all symbols - for (Map.Entry entry : allVars.entrySet()) { + for (Entry entry : allKnownVarsAndUFsBuilder.buildOrThrow().entrySet()) { String name = entry.getKey(); Term var = entry.getValue(); // escaping is stolen from SMTInterpol, lets hope this remains consistent - out.append("(declare-fun ").append(PrintTerm.quoteIdentifier(name)).append(" ("); + variablesAndUFsAsSMTLIB2.append("(declare-fun ").append(PrintTerm.quoteIdentifier(name)).append(" ("); // add function parameters Iterable childrenTypes; @@ -319,15 +328,12 @@ assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType } catch (CVC5ApiException e) { childrenTypes = Iterables.transform(var, Term::getSort); } - out.append(Joiner.on(" ").join(childrenTypes)); + variablesAndUFsAsSMTLIB2.append(Joiner.on(" ").join(childrenTypes)); // and return type - out.append(") ").append(var.getSort().toString()).append(")\n"); + variablesAndUFsAsSMTLIB2.append(") ").append(var.getSort().toString()).append(")\n"); } - - // now add the final assert - out.append("(assert ").append(f).append(')'); - return out.toString(); + return variablesAndUFsAsSMTLIB2; } @Override From 0591f8e3153721294051411500de7ec731878723 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:01:56 +0100 Subject: [PATCH 26/47] CVC5: add creator method to get all cached variables and UFs --- .../solvers/cvc5/CVC5FormulaCreator.java | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) 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 df70574d22..eca1e326c7 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -20,6 +20,7 @@ import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import com.google.common.collect.Table; +import com.google.common.collect.Table.Cell; import com.google.common.primitives.Ints; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Datatype; @@ -39,6 +40,7 @@ import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Map.Entry; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.rationals.Rational; @@ -957,4 +959,28 @@ public TraversalProcess visitQuantifier( return TraversalProcess.CONTINUE; } } + + private static final Set INTERNAL_UF_NAMES = + ImmutableSet.of( + "Rational_*_", "Rational_/_", "Rational_%_", "Integer_*_", "Integer_/_", "Integer_%_"); + + protected Map getAllCachedVariablesAndUFs( + boolean includeUFs, boolean excludeInternalArithmeticUFs) { + ImmutableMap.Builder knownVariablesAndUFsMap = ImmutableMap.builder(); + for (Cell cell : variablesCache.cellSet()) { + knownVariablesAndUFsMap.put(cell.getRowKey(), cell.getValue()); + } + if (includeUFs) { + for (Entry fun : functionsCache.entrySet()) { + if (excludeInternalArithmeticUFs) { + if (!INTERNAL_UF_NAMES.contains(fun.getKey())) { + knownVariablesAndUFsMap.put(fun); + } + } else { + knownVariablesAndUFsMap.put(fun); + } + } + } + return knownVariablesAndUFsMap.buildOrThrow(); + } } From 3db56cf33e86985001ec4690d4f1258c5ee36c19 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:02:52 +0100 Subject: [PATCH 27/47] CVC5: allow parsing to skip double declarations and add constants to check this error + improve dumping by properly using function return and input types for our smtlib2 output --- .../solvers/cvc5/CVC5FormulaManager.java | 83 +++++++++++++++---- 1 file changed, 65 insertions(+), 18 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 5f5b953636..46472b5201 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -28,7 +28,7 @@ import io.github.cvc5.Term; import io.github.cvc5.TermManager; import io.github.cvc5.modes.InputLanguage; -import java.util.LinkedHashMap; +import java.util.Arrays; import java.util.Map; import java.util.Map.Entry; import java.util.regex.Matcher; @@ -41,6 +41,11 @@ class CVC5FormulaManager extends AbstractFormulaManagerbuilder() + .putAll(creator.getAllCachedVariablesAndUFs(true, true)) + .buildOrThrow()); + String sanitizedInputFormula = knownVarsAndUfs.append(formulaStr).toString(); ImmutableBiMap replacementMap = null; + // Sanitize input String for CVC5 (it disallows . and @ without quotes) if (sanitizedInputFormula.contains("define-fun .def_")) { // MathSAT5 output, resubstitute ImmutableBiMap.Builder replacementMapBuilder = ImmutableBiMap.builder(); @@ -145,7 +157,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // solver as assertions String invokeReturn = invokeCommand(command, parseSolver, sm); - if (!invokeReturn.equals(expectedSuccessMsg)) { + if (isDisallowedInvokeError(invokeReturn)) { throw new IllegalArgumentException("Error when parsing using CVC5: " + invokeReturn); } @@ -304,34 +316,53 @@ assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType } private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { - StringBuilder variablesAndUFsAsSMTLIB2 = new StringBuilder(); // get all symbols ImmutableMap.Builder allKnownVarsAndUFsBuilder = ImmutableMap.builder(); creator.extractVariablesAndUFs(f, true, allKnownVarsAndUFsBuilder::put); - // print all symbols - for (Entry entry : allKnownVarsAndUFsBuilder.buildOrThrow().entrySet()) { + // return all symbols relevant for the input term as SMTLIB2 + return getSMTLIB2For(allKnownVarsAndUFsBuilder.buildOrThrow()); + } + + private static StringBuilder getSMTLIB2For(Map varsAndUFs) { + StringBuilder variablesAndUFsAsSMTLIB2 = new StringBuilder(); + for (Entry entry : varsAndUFs.entrySet()) { String name = entry.getKey(); - Term var = entry.getValue(); + Term varOrUf = entry.getValue(); // escaping is stolen from SMTInterpol, lets hope this remains consistent - variablesAndUFsAsSMTLIB2.append("(declare-fun ").append(PrintTerm.quoteIdentifier(name)).append(" ("); + variablesAndUFsAsSMTLIB2 + .append("(declare-fun ") + .append(PrintTerm.quoteIdentifier(name)) + .append(" ("); // add function parameters Iterable childrenTypes; try { - if (var.getSort().isFunction() || var.getKind() == Kind.APPLY_UF) { - childrenTypes = Iterables.skip(Iterables.transform(var, Term::getSort), 1); - } else { - childrenTypes = Iterables.transform(var, Term::getSort); + if (varOrUf.getKind() == Kind.APPLY_UF) { + // Unpack the def of the UF to get to the declaration which has the types + varOrUf = varOrUf.getChild(0); } - } catch (CVC5ApiException e) { - childrenTypes = Iterables.transform(var, Term::getSort); + } catch (CVC5ApiException apiEx) { + // Does not happen anyway + throw new IllegalArgumentException("CVC5 internal error: " + apiEx.getMessage(), apiEx); + } + + Sort sort = varOrUf.getSort(); + if (sort.isFunction()) { + childrenTypes = Arrays.asList(sort.getFunctionDomainSorts()); + } else { + childrenTypes = Iterables.transform(varOrUf, Term::getSort); } + variablesAndUFsAsSMTLIB2.append(Joiner.on(" ").join(childrenTypes)); - // and return type - variablesAndUFsAsSMTLIB2.append(") ").append(var.getSort().toString()).append(")\n"); + // Return type + String returnTypeString = sort.toString(); + if (sort.isFunction()) { + returnTypeString = sort.getFunctionCodomainSort().toString(); + } + variablesAndUFsAsSMTLIB2.append(") ").append(returnTypeString).append(")\n"); } return variablesAndUFsAsSMTLIB2; } @@ -371,4 +402,20 @@ private String invokeCommand(Command command, Solver parseSolver, SymbolManager "Error parsing with CVC5 " + parseException.getMessage(), parseException); } } + + /** + * We allow invoke() to succeed with the expected string, but also to fail for multiple + * definitions of the same variable for example. + */ + private boolean isDisallowedInvokeError(String pInvokeReturn) { + // We allow skipping of variables that are declared twice + if (pInvokeReturn.equals(INVOKE_SUCCESS)) { + return false; + } else if (pInvokeReturn.startsWith(INVOKE_MULTI_DEF_ERROR_PREFIX) + && pInvokeReturn.endsWith(INVOKE_MULTI_DEF_ERROR_SUFFIX)) { + return false; + } + // Extend as needed + return true; + } } From 37cab0dde2d85d2d1e692ebcbaa67c2e44f23e88 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:20:18 +0100 Subject: [PATCH 28/47] CVC5 parser: only add declarations from the cache if they are really needed (UFs fail for double declaration, variables actually work) and only declare UFs once, even if used multiple times, when dumping --- .../solvers/cvc5/CVC5FormulaManager.java | 43 +++++++++++++------ 1 file changed, 29 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 46472b5201..c57b998462 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -31,6 +31,7 @@ import java.util.Arrays; import java.util.Map; import java.util.Map.Entry; +import java.util.Set; import java.util.regex.Matcher; import java.util.regex.Pattern; import org.sosy_lab.java_smt.api.Formula; @@ -102,13 +103,19 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { InputParser parser = new InputParser(parseSolver, sm); // Add all already known (cached) variables and UFs - // (double parsing is no problem and is ignored below, but the internal UFs cause problems) - StringBuilder knownVarsAndUfs = - getSMTLIB2For( + // (double parsing is a problem for UFs it seems, and the internal UFs cause problems) + Set declarationsForAllVarsAndUfs = + getSMTLIB2DeclarationsFor( ImmutableMap.builder() .putAll(creator.getAllCachedVariablesAndUFs(true, true)) .buildOrThrow()); - String sanitizedInputFormula = knownVarsAndUfs.append(formulaStr).toString(); + StringBuilder extraDefs = new StringBuilder(); + for (String declaration : declarationsForAllVarsAndUfs) { + if (!formulaStr.contains(declaration.replace("\n", ""))) { + extraDefs.append(declaration); + } + } + String sanitizedInputFormula = extraDefs.append(formulaStr).toString(); ImmutableBiMap replacementMap = null; // Sanitize input String for CVC5 (it disallows . and @ without quotes) if (sanitizedInputFormula.contains("define-fun .def_")) { @@ -321,20 +328,27 @@ private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { creator.extractVariablesAndUFs(f, true, allKnownVarsAndUFsBuilder::put); // return all symbols relevant for the input term as SMTLIB2 - return getSMTLIB2For(allKnownVarsAndUFsBuilder.buildOrThrow()); + StringBuilder builder = new StringBuilder(); + // buildKeepingLast due to UFs; 1 UF might be applied multiple times. But the names and the + // types are consistent. + getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()).stream() + .forEach(builder::append); + return builder; } - private static StringBuilder getSMTLIB2For(Map varsAndUFs) { - StringBuilder variablesAndUFsAsSMTLIB2 = new StringBuilder(); + /** + * Returns the SMTLIB2 declarations for the input, line by line with one declaration per line, + * with a line-break at the end of all lines. + */ + private static Set getSMTLIB2DeclarationsFor(Map varsAndUFs) { + ImmutableSet.Builder variablesAndUFsAsSMTLIB2 = ImmutableSet.builder(); for (Entry entry : varsAndUFs.entrySet()) { String name = entry.getKey(); Term varOrUf = entry.getValue(); + StringBuilder line = new StringBuilder(); // escaping is stolen from SMTInterpol, lets hope this remains consistent - variablesAndUFsAsSMTLIB2 - .append("(declare-fun ") - .append(PrintTerm.quoteIdentifier(name)) - .append(" ("); + line.append("(declare-fun ").append(PrintTerm.quoteIdentifier(name)).append(" ("); // add function parameters Iterable childrenTypes; @@ -355,16 +369,17 @@ private static StringBuilder getSMTLIB2For(Map varsAndUFs) { childrenTypes = Iterables.transform(varOrUf, Term::getSort); } - variablesAndUFsAsSMTLIB2.append(Joiner.on(" ").join(childrenTypes)); + line.append(Joiner.on(" ").join(childrenTypes)); // Return type String returnTypeString = sort.toString(); if (sort.isFunction()) { returnTypeString = sort.getFunctionCodomainSort().toString(); } - variablesAndUFsAsSMTLIB2.append(") ").append(returnTypeString).append(")\n"); + line.append(") ").append(returnTypeString).append(")\n"); + variablesAndUFsAsSMTLIB2.add(line.toString()); } - return variablesAndUFsAsSMTLIB2; + return variablesAndUFsAsSMTLIB2.build(); } @Override From 3b3b1e7ab8dfe5d50911391014a05ad2fadf90de Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:26:09 +0100 Subject: [PATCH 29/47] CVC5: add CVC5 to more strict test category for parsing test --- .../sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index 5701551726..e4e6663168 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -136,7 +136,7 @@ public void parseDeclareRedundantTest1() { requireIntegers(); IntegerFormula var = imgr.makeVariable("x"); String query = "(declare-fun x () Int)(declare-fun x () Int)(assert (= 0 x))"; - if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3).contains(solverToUse())) { + if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3, Solvers.CVC5).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); } else { // some solvers are more tolerant for identical symbols. From 26894047b95be4f5e27de3da0e2f038f5ff088fc Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:26:39 +0100 Subject: [PATCH 30/47] CVC5: move newly added set of internal UF names and add doc --- .../java_smt/solvers/cvc5/CVC5FormulaCreator.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 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 eca1e326c7..47f63ca7c2 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -76,6 +76,11 @@ public class CVC5FormulaCreator extends FormulaCreator { + // Used to determine the internal UFs not to use when parsing + private static final Set INTERNAL_UF_NAMES = + ImmutableSet.of( + "Rational_*_", "Rational_/_", "Rational_%_", "Integer_*_", "Integer_/_", "Integer_%_"); + /** CVC5 does not allow using some key-functions from SMTLIB2 as identifiers. */ private static final ImmutableSet UNSUPPORTED_IDENTIFIERS = ImmutableSet.of("let"); @@ -960,10 +965,6 @@ public TraversalProcess visitQuantifier( } } - private static final Set INTERNAL_UF_NAMES = - ImmutableSet.of( - "Rational_*_", "Rational_/_", "Rational_%_", "Integer_*_", "Integer_/_", "Integer_%_"); - protected Map getAllCachedVariablesAndUFs( boolean includeUFs, boolean excludeInternalArithmeticUFs) { ImmutableMap.Builder knownVariablesAndUFsMap = ImmutableMap.builder(); From 686ef7f26009a34f8ff67f21281dbd01848c1166 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:51:08 +0100 Subject: [PATCH 31/47] CVC5: refactor parsing to be more readable and understandable --- .../solvers/cvc5/CVC5FormulaManager.java | 252 ++++++++++-------- 1 file changed, 139 insertions(+), 113 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 c57b998462..c9af4c4460 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -13,7 +13,6 @@ import static com.google.common.base.Preconditions.checkState; import com.google.common.base.Joiner; -import com.google.common.collect.ImmutableBiMap; import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; @@ -104,42 +103,12 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Add all already known (cached) variables and UFs // (double parsing is a problem for UFs it seems, and the internal UFs cause problems) - Set declarationsForAllVarsAndUfs = - getSMTLIB2DeclarationsFor( - ImmutableMap.builder() - .putAll(creator.getAllCachedVariablesAndUFs(true, true)) - .buildOrThrow()); - StringBuilder extraDefs = new StringBuilder(); - for (String declaration : declarationsForAllVarsAndUfs) { - if (!formulaStr.contains(declaration.replace("\n", ""))) { - extraDefs.append(declaration); - } - } - String sanitizedInputFormula = extraDefs.append(formulaStr).toString(); - ImmutableBiMap replacementMap = null; + String sanitizedInputFormula = addCachedDeclarationsTo(formulaStr); + boolean mathsatReplacement = false; // Sanitize input String for CVC5 (it disallows . and @ without quotes) if (sanitizedInputFormula.contains("define-fun .def_")) { - // MathSAT5 output, resubstitute - ImmutableBiMap.Builder replacementMapBuilder = ImmutableBiMap.builder(); - // Since no quotes are used, we can assume that there are no spaces in the defined name - String pattern = "(define-fun \\.)[^\\s]+"; - Pattern r = Pattern.compile(pattern); - Matcher m = r.matcher(sanitizedInputFormula); - - while (m.find()) { - String match = m.group(); - String bare = match.replace("define-fun ", ""); // to replace - String replacement = "|" + bare.substring(1) + "|"; - checkState(!sanitizedInputFormula.contains(replacement)); - replacementMapBuilder.put(bare, replacement); - } - - replacementMap = replacementMapBuilder.buildOrThrow(); - for (Entry replacementEntry : replacementMap.entrySet()) { - sanitizedInputFormula = - sanitizedInputFormula.replace(replacementEntry.getKey(), replacementEntry.getValue()); - } - checkState(!sanitizedInputFormula.contains("define-fun .")); + mathsatReplacement = true; + sanitizedInputFormula = sanitizeInputForMathsat(sanitizedInputFormula); } parser.setStringInput(InputLanguage.SMT_LIB_2_6, sanitizedInputFormula, ""); @@ -171,9 +140,79 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { command = getNextCommand(parser); } + // Register new terms in our caches or throw for errors + registerNewTermsInCache(sm, substituteFromBuilder, substituteToBuilder); + + // TODO: Which terms can end up here? Seems like this is always empty + checkState(sm.getNamedTerms().isEmpty()); + + // Get the assertions out of the solver and re-substitute additional definitions outside of + // assertions + Term parsedTerm = getAssertedTerm(parseSolver, numberOfAssertions, mathsatReplacement); + + // If the symbols used in the term were already declared before parsing, the term uses new + // ones with the same name, so we need to substitute them! + parsedTerm = + resubstituteCachedVariables( + substituteFromBuilder.build(), substituteToBuilder.build(), parsedTerm); + + // Quantified formulas do not give us the bound variables in getDeclaredTerms() above. + // Find them and register a free equivalent + creator.registerBoundVariablesWithVisitor(parsedTerm); + parser.deletePointer(); // Clean up parser + parseSolver.deletePointer(); // Clean up parse solver + return parsedTerm; + } + + private String addCachedDeclarationsTo(String formulaStr) { + // Add all already known (cached) variables and UFs + // (double parsing is a problem for UFs it seems, and the internal UFs cause problems) + Set declarationsForAllVarsAndUfs = + getSMTLIB2DeclarationsFor( + ImmutableMap.builder() + .putAll(creator.getAllCachedVariablesAndUFs(true, true)) + .buildOrThrow()); + + StringBuilder extraDefs = new StringBuilder(); + for (String declaration : declarationsForAllVarsAndUfs) { + if (!formulaStr.contains(declaration.replace("\n", ""))) { + extraDefs.append(declaration); + } + } + return extraDefs.append(formulaStr).toString(); + } - // Register new terms in our caches + private String sanitizeInputForMathsat(String inputString) { + // MathSAT5 output, resubstitute the illegal input. + // Since no quotes are used, we can assume that there are no spaces in the defined name. + ImmutableMap.Builder replacementMapBuilder = ImmutableMap.builder(); + String sanitizedInputFormula = inputString; + String pattern = "(define-fun \\.)[^\\s]+"; + Pattern r = Pattern.compile(pattern); + Matcher m = r.matcher(sanitizedInputFormula); + + while (m.find()) { + String match = m.group(); + String bare = match.replace("define-fun ", ""); // to replace + String replacement = "|" + bare.substring(1) + "|"; + checkState(!sanitizedInputFormula.contains(replacement)); + replacementMapBuilder.put(bare, replacement); + // TODO: can we modify the string while we match? + } + + for (Entry replacementEntry : replacementMapBuilder.buildOrThrow().entrySet()) { + sanitizedInputFormula = + sanitizedInputFormula.replace(replacementEntry.getKey(), replacementEntry.getValue()); + } + checkState(!sanitizedInputFormula.contains("define-fun .")); + return sanitizedInputFormula; + } + + private void registerNewTermsInCache( + SymbolManager sm, + ImmutableSet.Builder substituteFromBuilder, + ImmutableSet.Builder substituteToBuilder) { for (Term parsedTerm : sm.getDeclaredTerms()) { Term termToRegister = parsedTerm; try { @@ -232,82 +271,6 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { "Error parsing the following term in CVC5: " + parsedTerm, apiException); } } - - // TODO: Which terms can end up here? Seems like this is always empty - checkState(sm.getNamedTerms().isEmpty()); - - // Get the assertions out of the solver - Term[] assertions = parseSolver.getAssertions(); - checkArgument( - numberOfAssertions > 0, - "Error when parsing using CVC5: at least one assert " - + "statement needs to be part of the input"); - - // If failing, conjugate the input and return - // (We disallow push and pop currently, so this is fine!) - // TODO: this can be improved, but we need to be able to discern the non-assertion terms to - // re-substitute (we can just remember them before invoking the commands above) - checkArgument( - numberOfAssertions == 1, - "Error when parsing using CVC5: at most one assert " - + "statement is currently allowed to be part of the input"); - checkArgument(assertions.length > 0, "Error when parsing using CVC5: no term found to return"); - Term parsedTerm = assertions[assertions.length - 1]; - checkState(!checkNotNull(parsedTerm).isNull()); - - try { - if (assertions.length > 1 && replacementMap != null) { - // re-substitute MathSAT5 input - for (int i = assertions.length - 2; i >= 0; i--) { - Term equation = assertions[i]; - - if (equation.getKind() != Kind.EQUAL) { - // Original problem we try to solve - throw new IllegalArgumentException( - "Error when parsing using CVC5, no expressions may use a . or " - + "@ as first character in a symbol."); - } - - parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); - } - - } else if (assertions.length != 1) { - // Sometimes terms are added as assertions without them being sources by an assertion, but - // a fun-def. We re-substitute these! - for (int i = assertions.length - 2; i >= 0; i--) { - Term equation = assertions[i]; - - if (equation.getKind() != Kind.EQUAL) { - // Original problem description we try to solve - throw new IllegalArgumentException( - "Error when parsing using CVC5: re-substitution of function-definitions into " - + "assertions failed"); - } - parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); - } - } - } catch (CVC5ApiException apiException) { - throw new IllegalArgumentException( - "Error parsing the following term in CVC5: " + parsedTerm, apiException); - } - - // If the symbols used in the term were already declared before parsing, the term uses new - // ones with the same name, so we need to substitute them! - ImmutableSet substituteFrom = substituteFromBuilder.build(); - ImmutableSet substituteTo = substituteToBuilder.build(); - checkState(substituteFrom.size() == substituteTo.size()); - assert substituteFrom.stream() - .map(Term::toString) - .allMatch(from -> substituteTo.stream().map(Term::toString).anyMatch(from::equals)); - parsedTerm = - parsedTerm.substitute( - substituteFrom.toArray(new Term[0]), substituteTo.toArray(new Term[0])); - - // Quantified formulas do not give us the bound variables in getDeclaredTerms() above. - // Find them and register a free equivalent - creator.registerBoundVariablesWithVisitor(parsedTerm); - parseSolver.deletePointer(); // Clean up parse solver - return parsedTerm; } @Override @@ -317,7 +280,7 @@ assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType StringBuilder variablesAndUFsAsSMTLIB2 = getAllDeclaredVariablesAndUFsAsSMTLIB2(f); - // now add the final assert + // Add the final assert after the declarations variablesAndUFsAsSMTLIB2.append("(assert ").append(f).append(')'); return variablesAndUFsAsSMTLIB2.toString(); } @@ -433,4 +396,67 @@ private boolean isDisallowedInvokeError(String pInvokeReturn) { // Extend as needed return true; } + + private static Term resubstituteCachedVariables( + Set substituteFrom, Set substituteTo, Term parsedTerm) { + checkState(substituteFrom.size() == substituteTo.size()); + assert substituteFrom.stream() + .map(Term::toString) + .allMatch(from -> substituteTo.stream().map(Term::toString).anyMatch(from::equals)); + parsedTerm = + parsedTerm.substitute( + substituteFrom.toArray(new Term[0]), substituteTo.toArray(new Term[0])); + return parsedTerm; + } + + private static Term getAssertedTerm( + Solver parseSolver, int numberOfAssertions, boolean mathsatReplacementUsed) { + Term[] assertions = parseSolver.getAssertions(); + checkArgument( + numberOfAssertions > 0, + "Error when parsing using CVC5: at least one assert " + + "statement needs to be part of the input"); + + // If failing, conjugate the input and return + // (We disallow push and pop currently, so this is fine!) + // TODO: this can be improved, but we need to be able to discern the non-assertion terms to + // re-substitute (we can just remember them before invoking the commands above) + checkArgument( + numberOfAssertions == 1, + "Error when parsing using CVC5: at most one assert " + + "statement is currently allowed to be part of the input"); + checkArgument(assertions.length > 0, "Error when parsing using CVC5: no term found to return"); + Term parsedTerm = assertions[assertions.length - 1]; + checkState(!checkNotNull(parsedTerm).isNull()); + + if (assertions.length > 1) { + // Sometimes terms are added as assertions without them being sources by an assertion, but + // a fun-def. We re-substitute these! (E.g. MathSAT5 input) + for (int i = assertions.length - 2; i >= 0; i--) { + Term equation = assertions[i]; + + try { + if (equation.getKind() != Kind.EQUAL) { + // Original problem we try to solve + if (mathsatReplacementUsed) { + throw new IllegalArgumentException( + "Error when parsing using CVC5, no expressions may use a . or " + + "@ as first character in a symbol."); + } else { + throw new IllegalArgumentException( + "Error when parsing using CVC5: re-substitution of function-definitions into " + + "assertions failed"); + } + } + + parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); + } catch (CVC5ApiException apiException) { + // getKind() will not throw here, but getChild() might for unexpected input + throw new IllegalArgumentException( + "Error parsing in CVC5: " + apiException.getMessage(), apiException); + } + } + } + return parsedTerm; + } } From ad5ab639ba1b80a1d6d8a9f89b312b7463d8053d Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 17:55:32 +0100 Subject: [PATCH 32/47] CVC5 parser: remove allowed invoke error msg, as it fails later (variables and UFs are not allowed to be defined twice) --- .../solvers/cvc5/CVC5FormulaManager.java | 21 +------------------ 1 file changed, 1 insertion(+), 20 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 c9af4c4460..8625b80652 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -42,9 +42,6 @@ class CVC5FormulaManager extends AbstractFormulaManager substituteFrom, Set substituteTo, Term parsedTerm) { checkState(substituteFrom.size() == substituteTo.size()); From 3ae018b847c3d113061d3bd4e9da67f498c450a7 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 18:05:20 +0100 Subject: [PATCH 33/47] CVC5 parser: also check for present declarations present with declare-const before adding them to the input if known already --- .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 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 8625b80652..fb03d9eb08 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -173,8 +173,15 @@ private String addCachedDeclarationsTo(String formulaStr) { StringBuilder extraDefs = new StringBuilder(); for (String declaration : declarationsForAllVarsAndUfs) { - if (!formulaStr.contains(declaration.replace("\n", ""))) { - extraDefs.append(declaration); + String declWoNewline = declaration.replace("\n", ""); + if (!formulaStr.contains(declWoNewline)) { + if (!declWoNewline.contains("()")) { + extraDefs.append(declaration); + } else if (!formulaStr.contains( + declWoNewline.replace("(declare-fun ", "(declare-const ").replace(" ()", ""))) { + // No "input" value; may be a variable, which can be defined using declare-const as well + extraDefs.append(declaration); + } } } return extraDefs.append(formulaStr).toString(); From 93c5582ab954c3415800280a7aafefbb3b68e418 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 18:08:11 +0100 Subject: [PATCH 34/47] CVC5 parser: add to more strict test branch in SolverFormulaIODeclarationsTest.java --- .../sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index e4e6663168..c854e2e32d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -152,7 +152,7 @@ public void parseDeclareRedundantTest2() { fmgr.declareAndCallUF("foo", IntegerType, imgr.makeNumber(1), imgr.makeNumber(2)); String query = "(declare-fun foo (Int Int) Int)(declare-fun foo (Int Int) Int)(assert (= 0 (foo 1 2)))"; - if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3).contains(solverToUse())) { + if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3, Solvers.CVC5).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); } else { // some solvers are more tolerant for identical symbols. From c7b57bdef85515c0a35e7c96672484bc36115d45 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 18:32:53 +0100 Subject: [PATCH 35/47] Use (_.getKey(), _.getValue()) when building new map instead of the entry as checkstyle thinks WRONGLY that we use only the keys --- .../sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java | 4 ++-- 1 file changed, 2 insertions(+), 2 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 47f63ca7c2..152321fe0a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -975,10 +975,10 @@ protected Map getAllCachedVariablesAndUFs( for (Entry fun : functionsCache.entrySet()) { if (excludeInternalArithmeticUFs) { if (!INTERNAL_UF_NAMES.contains(fun.getKey())) { - knownVariablesAndUFsMap.put(fun); + knownVariablesAndUFsMap.put(fun.getKey(), fun.getValue()); } } else { - knownVariablesAndUFsMap.put(fun); + knownVariablesAndUFsMap.put(fun.getKey(), fun.getValue()); } } } From 3d0c1e5503f9500b43f41d80d68f35636c328fa0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 29 Oct 2025 18:33:07 +0100 Subject: [PATCH 36/47] Simplify usage of stream in CVC5FormulaManager.java --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 3 +-- 1 file changed, 1 insertion(+), 2 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 fb03d9eb08..8bba812232 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -298,8 +298,7 @@ private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { StringBuilder builder = new StringBuilder(); // buildKeepingLast due to UFs; 1 UF might be applied multiple times. But the names and the // types are consistent. - getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()).stream() - .forEach(builder::append); + getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()).forEach(builder::append); return builder; } From 0e114e35e99ec9b051ec2f0c38cf0554681d093d Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 31 Oct 2025 20:56:14 +0100 Subject: [PATCH 37/47] CVC5 Parser: don't use replace(), but substring() to remove newline from internal output before adding to the input --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 8bba812232..505306ff30 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -173,7 +173,8 @@ private String addCachedDeclarationsTo(String formulaStr) { StringBuilder extraDefs = new StringBuilder(); for (String declaration : declarationsForAllVarsAndUfs) { - String declWoNewline = declaration.replace("\n", ""); + // Remove newline from the end + String declWoNewline = declaration.substring(0, declaration.length() - 1); if (!formulaStr.contains(declWoNewline)) { if (!declWoNewline.contains("()")) { extraDefs.append(declaration); From 3651299636e7518a388d5076eee569408d3a4b93 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 31 Oct 2025 21:01:02 +0100 Subject: [PATCH 38/47] CVC5 Parser: improve named term TODO w infos from Daniel Raffler --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 505306ff30..1100f9eead 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -140,7 +140,8 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { // Register new terms in our caches or throw for errors registerNewTermsInCache(sm, substituteFromBuilder, substituteToBuilder); - // TODO: Which terms can end up here? Seems like this is always empty + // For named definitions like (=> (! (> x y) : named p1) (! (= x z) : named p2)) + // TODO: how to handle this in CVC5 in JavaSMT? checkState(sm.getNamedTerms().isEmpty()); // Get the assertions out of the solver and re-substitute additional definitions outside of From 7ec916276cc70076b490d15a6ba8fe9cc80220b6 Mon Sep 17 00:00:00 2001 From: BaierD Date: Fri, 31 Oct 2025 21:03:33 +0100 Subject: [PATCH 39/47] CVC5 Parser: remove unneeded check for push/pop and add a note instead --- .../sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 6 +----- 1 file changed, 1 insertion(+), 5 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 1100f9eead..f86763a998 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -116,11 +116,7 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { int numberOfAssertions = 0; Command command = getNextCommand(parser); while (!command.isNull()) { - if (command.toString().contains("push") || command.toString().contains("pop")) { - // TODO: push and pop? - throw new IllegalArgumentException( - "Parsing SMTLIB2 with CVC5 in JavaSMT does not support push or pop currently."); - } + // Note: push and pop are not handled as we disallow SMTLIB2 input including it! if (command.toString().startsWith("(assert ")) { numberOfAssertions++; From 0e1e9573d6d3a2504ea4b72be65645b59bd5ef75 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 1 Nov 2025 13:29:42 +0100 Subject: [PATCH 40/47] CVC5 Parser: switch parser tests for CVC5 into lenient category that allows symbols to be parsed multiple times --- .../java_smt/test/SolverFormulaIODeclarationsTest.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index c854e2e32d..2df3f08aa0 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -136,7 +136,7 @@ public void parseDeclareRedundantTest1() { requireIntegers(); IntegerFormula var = imgr.makeVariable("x"); String query = "(declare-fun x () Int)(declare-fun x () Int)(assert (= 0 x))"; - if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3, Solvers.CVC5).contains(solverToUse())) { + if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); } else { // some solvers are more tolerant for identical symbols. @@ -152,7 +152,7 @@ public void parseDeclareRedundantTest2() { fmgr.declareAndCallUF("foo", IntegerType, imgr.makeNumber(1), imgr.makeNumber(2)); String query = "(declare-fun foo (Int Int) Int)(declare-fun foo (Int Int) Int)(assert (= 0 (foo 1 2)))"; - if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3, Solvers.CVC5).contains(solverToUse())) { + if (EnumSet.of(Solvers.PRINCESS, Solvers.Z3).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> mgr.parse(query)); } else { // some solvers are more tolerant for identical symbols. @@ -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 { From d77198f2d874a073be3ea1d3f44fb81aff2b0bdf Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 1 Nov 2025 13:52:13 +0100 Subject: [PATCH 41/47] CVC5 Parser: rework implementation by using CVC5s options to allow more lenient parsing, reuse symbols etc. and remove all imprecise SMTLIB2 insertions and now unneeded methods --- .../solvers/cvc5/CVC5FormulaCreator.java | 2 +- .../solvers/cvc5/CVC5FormulaManager.java | 257 +++++++++--------- 2 files changed, 124 insertions(+), 135 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 152321fe0a..a8e9a208af 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -965,7 +965,7 @@ public TraversalProcess visitQuantifier( } } - protected Map getAllCachedVariablesAndUFs( + protected ImmutableMap getAllCachedVariablesAndUFs( boolean includeUFs, boolean excludeInternalArithmeticUFs) { ImmutableMap.Builder knownVariablesAndUFsMap = ImmutableMap.builder(); for (Cell cell : variablesCache.cellSet()) { 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 f86763a998..76833ebab8 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -31,8 +31,6 @@ import java.util.Map; import java.util.Map.Entry; import java.util.Set; -import java.util.regex.Matcher; -import java.util.regex.Pattern; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -42,6 +40,9 @@ class CVC5FormulaManager extends AbstractFormulaManager substituteFromBuilder = ImmutableSet.builder(); ImmutableSet.Builder substituteToBuilder = ImmutableSet.builder(); - int numberOfAssertions = 0; - Command command = getNextCommand(parser); - while (!command.isNull()) { - // Note: push and pop are not handled as we disallow SMTLIB2 input including it! + // "Commands" represent 1 definition or assertion from the input string + Command command; + try { + // throws CVC5ParserException for errors, which can only be caught with Exception + command = parser.nextCommand(); + while (!command.isNull()) { + // Note: push and pop are not handled as we disallow SMTLIB2 input including it! - if (command.toString().startsWith("(assert ")) { - numberOfAssertions++; - } + // This WILL read in asserts, and they are no longer available for getTerm(), but on the + // solver as assertions + String invokeReturn = invokeCommand(command, parseSolver, symbolManager); + + if (!invokeReturn.equals(INVOKE_SUCCESS)) { + throw new IllegalArgumentException("Error when parsing using CVC5: " + invokeReturn); + } - // This WILL read in asserts, and they are no longer available for getTerm(), but on the - // solver as assertions - String invokeReturn = invokeCommand(command, parseSolver, sm); + command = parser.nextCommand(); + } + } catch (Exception parseException) { + // nextCommand(); throws CVC5ParserException for errors, which can only be caught with + // Exception + if (parseException instanceof IllegalArgumentException) { + throw (IllegalArgumentException) parseException; + } - if (!invokeReturn.equals(INVOKE_SUCCESS)) { - throw new IllegalArgumentException("Error when parsing using CVC5: " + invokeReturn); + String message = parseException.getMessage(); + if (message.startsWith(PARSING_MISSING_SYMBOL_START) + && message.endsWith(PARSING_MISSING_SYMBOL_END)) { + // This case seems to happen only very rarely (maybe just boolean variables or assertions + // with 1 symbol in them?)! CVC5 seems to recognize most declared symbols just fine. + + // Strip the error message until only the symbol is left + String symbolNotDeclared = message.substring(8, message.length() - 28); + + Term knownTerm = creator.functionsCache.get(symbolNotDeclared); + if (knownTerm == null) { + Map variableRow = creator.variablesCache.row(symbolNotDeclared); + if (variableRow.size() == 1) { + knownTerm = variableRow.values().iterator().next(); + return parseWithAddedSymbol(formulaStr, symbolNotDeclared, knownTerm); + } + } else { + return parseWithAddedSymbol(formulaStr, symbolNotDeclared, knownTerm); + } } - command = getNextCommand(parser); + throw new IllegalArgumentException( + "Error parsing with CVC5: " + parseException.getMessage(), parseException); } // Register new terms in our caches or throw for errors - registerNewTermsInCache(sm, substituteFromBuilder, substituteToBuilder); + registerNewTermsInCache(symbolManager, substituteFromBuilder, substituteToBuilder); // For named definitions like (=> (! (> x y) : named p1) (! (= x z) : named p2)) // TODO: how to handle this in CVC5 in JavaSMT? - checkState(sm.getNamedTerms().isEmpty()); + checkState(symbolManager.getNamedTerms().isEmpty()); // Get the assertions out of the solver and re-substitute additional definitions outside of // assertions - Term parsedTerm = getAssertedTerm(parseSolver, numberOfAssertions, mathsatReplacement); + Term parsedTerm = getAssertedTerm(parseSolver); // If the symbols used in the term were already declared before parsing, the term uses new // ones with the same name, so we need to substitute them! @@ -159,56 +178,42 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { return parsedTerm; } - private String addCachedDeclarationsTo(String formulaStr) { - // Add all already known (cached) variables and UFs - // (double parsing is a problem for UFs it seems, and the internal UFs cause problems) + private Term parseWithAddedSymbol(String formulaStr, String symbolNotDeclared, Term knownTerm) { Set declarationsForAllVarsAndUfs = - getSMTLIB2DeclarationsFor( - ImmutableMap.builder() - .putAll(creator.getAllCachedVariablesAndUFs(true, true)) - .buildOrThrow()); - - StringBuilder extraDefs = new StringBuilder(); - for (String declaration : declarationsForAllVarsAndUfs) { - // Remove newline from the end - String declWoNewline = declaration.substring(0, declaration.length() - 1); - if (!formulaStr.contains(declWoNewline)) { - if (!declWoNewline.contains("()")) { - extraDefs.append(declaration); - } else if (!formulaStr.contains( - declWoNewline.replace("(declare-fun ", "(declare-const ").replace(" ()", ""))) { - // No "input" value; may be a variable, which can be defined using declare-const as well - extraDefs.append(declaration); - } - } - } - return extraDefs.append(formulaStr).toString(); + getSMTLIB2DeclarationsFor(ImmutableMap.of(symbolNotDeclared, knownTerm)); + checkState(declarationsForAllVarsAndUfs.size() == 1); + // TODO: insert after options if options present? + String inputWithAddedVariable = declarationsForAllVarsAndUfs.iterator().next() + formulaStr; + return parseCVC5(inputWithAddedVariable); } - private String sanitizeInputForMathsat(String inputString) { - // MathSAT5 output, resubstitute the illegal input. - // Since no quotes are used, we can assume that there are no spaces in the defined name. - ImmutableMap.Builder replacementMapBuilder = ImmutableMap.builder(); - String sanitizedInputFormula = inputString; - String pattern = "(define-fun \\.)[^\\s]+"; - Pattern r = Pattern.compile(pattern); - Matcher m = r.matcher(sanitizedInputFormula); - - while (m.find()) { - String match = m.group(); - String bare = match.replace("define-fun ", ""); // to replace - String replacement = "|" + bare.substring(1) + "|"; - checkState(!sanitizedInputFormula.contains(replacement)); - replacementMapBuilder.put(bare, replacement); - // TODO: can we modify the string while we match? - } - - for (Entry replacementEntry : replacementMapBuilder.buildOrThrow().entrySet()) { - sanitizedInputFormula = - sanitizedInputFormula.replace(replacementEntry.getKey(), replacementEntry.getValue()); + /** + * Builds the parser from the given {@link Solver} and the {@link SymbolManager}. The {@link + * SymbolManager} needs to be persistent to remember terms already parsed/created. + */ + private InputParser getParser(Solver parseSolver) { + if (!parseSolver.isLogicSet()) { + try { + parseSolver.setLogic("ALL"); + } catch (CVC5ApiException e) { + // Should never happen in this configuration + throw new AssertionError("Unexpected exception", e); + } } - checkState(!sanitizedInputFormula.contains("define-fun .")); - return sanitizedInputFormula; + // Expected success string due to option set: "success\n" + parseSolver.setOption("print-success", "true"); + // more tolerant of non-conforming inputs, default: default + parseSolver.setOption("parsing-mode", "lenient"); + // force all declarations and definitions to be global when parsing, default: false + parseSolver.setOption("global-declarations", "true"); + // use API interface for fresh constants when parsing declarations and definitions, default: + // true + parseSolver.setOption("fresh-declarations", "false"); + // allows overloading of terms and sorts if true, default: true + parseSolver.setOption("term-sort-overload", "false"); + + InputParser parser = new InputParser(parseSolver, symbolManager); + return parser; } private void registerNewTermsInCache( @@ -296,15 +301,18 @@ private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { StringBuilder builder = new StringBuilder(); // buildKeepingLast due to UFs; 1 UF might be applied multiple times. But the names and the // types are consistent. - getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()).forEach(builder::append); + getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()) + .forEach(builder::append); return builder; } /** - * Returns the SMTLIB2 declarations for the input, line by line with one declaration per line, - * with a line-break at the end of all lines. + * Returns the SMTLIB2 declarations for the input (Entry) line by line with one + * declaration per line, with a line-break at the end of all lines. The output order will match + * the order of the input map. */ - private static Set getSMTLIB2DeclarationsFor(Map varsAndUFs) { + private static ImmutableSet getSMTLIB2DeclarationsFor( + ImmutableMap varsAndUFs) { ImmutableSet.Builder variablesAndUFsAsSMTLIB2 = ImmutableSet.builder(); for (Entry entry : varsAndUFs.entrySet()) { String name = entry.getKey(); @@ -362,16 +370,6 @@ public T substitute( return getFormulaCreator().encapsulate(type, input.substitute(changeFrom, changeTo)); } - private Command getNextCommand(InputParser parser) { - try { - // throws CVC5ParserException for errors - return parser.nextCommand(); - } catch (Exception parseException) { - throw new IllegalArgumentException( - "Error parsing with CVC5: " + parseException.getMessage(), parseException); - } - } - private String invokeCommand(Command command, Solver parseSolver, SymbolManager sm) { try { // throws CVC5ParserException for errors @@ -394,47 +392,38 @@ private static Term resubstituteCachedVariables( return parsedTerm; } - private static Term getAssertedTerm( - Solver parseSolver, int numberOfAssertions, boolean mathsatReplacementUsed) { + // Assumes that there is only one assertion at index 0 in the parsers assertions array + // Additional definitions are ordered from index 1 to length - 1 REVERSED! + private static Term getAssertedTerm(Solver parseSolver) { Term[] assertions = parseSolver.getAssertions(); + checkArgument( - numberOfAssertions > 0, - "Error when parsing using CVC5: at least one assert " - + "statement needs to be part of the input"); - - // If failing, conjugate the input and return - // (We disallow push and pop currently, so this is fine!) - // TODO: this can be improved, but we need to be able to discern the non-assertion terms to - // re-substitute (we can just remember them before invoking the commands above) - checkArgument( - numberOfAssertions == 1, - "Error when parsing using CVC5: at most one assert " - + "statement is currently allowed to be part of the input"); - checkArgument(assertions.length > 0, "Error when parsing using CVC5: no term found to return"); - Term parsedTerm = assertions[assertions.length - 1]; + assertions.length > 0, + "Error when parsing using CVC5: no term found to return." + + " Did the input string contain assertions?"); + Term parsedTerm = assertions[0]; checkState(!checkNotNull(parsedTerm).isNull()); if (assertions.length > 1) { // Sometimes terms are added as assertions without them being sources by an assertion, but - // a fun-def. We re-substitute these! (E.g. MathSAT5 input) - for (int i = assertions.length - 2; i >= 0; i--) { - Term equation = assertions[i]; + // as function-def. We re-substitute these into the assertion. + for (int i = assertions.length - 1; i >= 1; i--) { + Term parsedDefinition = assertions[i]; try { - if (equation.getKind() != Kind.EQUAL) { - // Original problem we try to solve - if (mathsatReplacementUsed) { - throw new IllegalArgumentException( - "Error when parsing using CVC5, no expressions may use a . or " - + "@ as first character in a symbol."); - } else { - throw new IllegalArgumentException( - "Error when parsing using CVC5: re-substitution of function-definitions into " - + "assertions failed"); - } + Kind kind = parsedDefinition.getKind(); + if (kind == Kind.EQUAL) { + parsedTerm = + parsedTerm.substitute(parsedDefinition.getChild(0), parsedDefinition.getChild(1)); + } else { + throw new IllegalArgumentException( + "Error when parsing using CVC5: re-substitution of function-definitions into " + + "assertions failed due to unexpected term " + + parsedDefinition + + " kind " + + parsedDefinition.getKind()); } - parsedTerm = parsedTerm.substitute(equation.getChild(0), equation.getChild(1)); } catch (CVC5ApiException apiException) { // getKind() will not throw here, but getChild() might for unexpected input throw new IllegalArgumentException( From bb419397a5cf715b8fc0b117c29ba70848b30149 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 1 Nov 2025 13:54:32 +0100 Subject: [PATCH 42/47] CVC5FormulaManager reorder methods --- .../solvers/cvc5/CVC5FormulaManager.java | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 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 76833ebab8..ab481497ae 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,18 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException { return parseCVC5(formulaStr); } + @Override + public String dumpFormulaImpl(Term f) { + assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType + : "Only BooleanFormulas may be dumped"; + + StringBuilder variablesAndUFsAsSMTLIB2 = getAllDeclaredVariablesAndUFsAsSMTLIB2(f); + + // Add the final assert after the declarations + variablesAndUFsAsSMTLIB2.append("(assert ").append(f).append(')'); + return variablesAndUFsAsSMTLIB2.toString(); + } + // Collect all actually parsed symbols as far as possible, then restart with cached // symbols included if needed (this way we can use the correct symbols from the input string // easily to not include them from the cache and reduce possible mistakes with symbols that @@ -280,18 +292,6 @@ private void registerNewTermsInCache( } } - @Override - public String dumpFormulaImpl(Term f) { - assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType - : "Only BooleanFormulas may be dumped"; - - StringBuilder variablesAndUFsAsSMTLIB2 = getAllDeclaredVariablesAndUFsAsSMTLIB2(f); - - // Add the final assert after the declarations - variablesAndUFsAsSMTLIB2.append("(assert ").append(f).append(')'); - return variablesAndUFsAsSMTLIB2.toString(); - } - private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { // get all symbols ImmutableMap.Builder allKnownVarsAndUFsBuilder = ImmutableMap.builder(); From 98ff665c85cc04f033c8d95412f7bd3e9821e3b3 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 1 Nov 2025 14:02:14 +0100 Subject: [PATCH 43/47] CVC5FormulaCreator clean up unused methods and consts --- .../solvers/cvc5/CVC5FormulaCreator.java | 27 ------------------- 1 file changed, 27 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 a8e9a208af..df70574d22 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -20,7 +20,6 @@ import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import com.google.common.collect.Table; -import com.google.common.collect.Table.Cell; import com.google.common.primitives.Ints; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Datatype; @@ -40,7 +39,6 @@ import java.util.HashSet; import java.util.List; import java.util.Map; -import java.util.Map.Entry; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.rationals.Rational; @@ -76,11 +74,6 @@ public class CVC5FormulaCreator extends FormulaCreator { - // Used to determine the internal UFs not to use when parsing - private static final Set INTERNAL_UF_NAMES = - ImmutableSet.of( - "Rational_*_", "Rational_/_", "Rational_%_", "Integer_*_", "Integer_/_", "Integer_%_"); - /** CVC5 does not allow using some key-functions from SMTLIB2 as identifiers. */ private static final ImmutableSet UNSUPPORTED_IDENTIFIERS = ImmutableSet.of("let"); @@ -964,24 +957,4 @@ public TraversalProcess visitQuantifier( return TraversalProcess.CONTINUE; } } - - protected ImmutableMap getAllCachedVariablesAndUFs( - boolean includeUFs, boolean excludeInternalArithmeticUFs) { - ImmutableMap.Builder knownVariablesAndUFsMap = ImmutableMap.builder(); - for (Cell cell : variablesCache.cellSet()) { - knownVariablesAndUFsMap.put(cell.getRowKey(), cell.getValue()); - } - if (includeUFs) { - for (Entry fun : functionsCache.entrySet()) { - if (excludeInternalArithmeticUFs) { - if (!INTERNAL_UF_NAMES.contains(fun.getKey())) { - knownVariablesAndUFsMap.put(fun.getKey(), fun.getValue()); - } - } else { - knownVariablesAndUFsMap.put(fun.getKey(), fun.getValue()); - } - } - } - return knownVariablesAndUFsMap.buildOrThrow(); - } } From a94d6133e58731acc396fa2b1675b56e12d31744 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 1 Nov 2025 14:02:40 +0100 Subject: [PATCH 44/47] CVC5FormulaManager simplify used methods and doc --- .../solvers/cvc5/CVC5FormulaManager.java | 25 +++++++------------ 1 file changed, 9 insertions(+), 16 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 ab481497ae..7ef39f004f 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -191,12 +191,10 @@ private Term parseCVC5(final String formulaStr) { } private Term parseWithAddedSymbol(String formulaStr, String symbolNotDeclared, Term knownTerm) { - Set declarationsForAllVarsAndUfs = + StringBuilder declaration = getSMTLIB2DeclarationsFor(ImmutableMap.of(symbolNotDeclared, knownTerm)); - checkState(declarationsForAllVarsAndUfs.size() == 1); // TODO: insert after options if options present? - String inputWithAddedVariable = declarationsForAllVarsAndUfs.iterator().next() + formulaStr; - return parseCVC5(inputWithAddedVariable); + return parseCVC5(declaration.append(formulaStr).toString()); } /** @@ -293,27 +291,22 @@ private void registerNewTermsInCache( } private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { - // get all symbols ImmutableMap.Builder allKnownVarsAndUFsBuilder = ImmutableMap.builder(); + // Get all symbols relevant for the input term creator.extractVariablesAndUFs(f, true, allKnownVarsAndUFsBuilder::put); - // return all symbols relevant for the input term as SMTLIB2 - StringBuilder builder = new StringBuilder(); // buildKeepingLast due to UFs; 1 UF might be applied multiple times. But the names and the // types are consistent. - getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()) - .forEach(builder::append); - return builder; + return getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()); } /** - * Returns the SMTLIB2 declarations for the input (Entry) line by line with one + * Returns the SMTLIB2 declarations for the input Map line by line with one * declaration per line, with a line-break at the end of all lines. The output order will match * the order of the input map. */ - private static ImmutableSet getSMTLIB2DeclarationsFor( - ImmutableMap varsAndUFs) { - ImmutableSet.Builder variablesAndUFsAsSMTLIB2 = ImmutableSet.builder(); + private static StringBuilder getSMTLIB2DeclarationsFor(ImmutableMap varsAndUFs) { + StringBuilder declarations = new StringBuilder(); for (Entry entry : varsAndUFs.entrySet()) { String name = entry.getKey(); Term varOrUf = entry.getValue(); @@ -349,9 +342,9 @@ private static ImmutableSet getSMTLIB2DeclarationsFor( returnTypeString = sort.getFunctionCodomainSort().toString(); } line.append(") ").append(returnTypeString).append(")\n"); - variablesAndUFsAsSMTLIB2.add(line.toString()); + declarations.append(line); } - return variablesAndUFsAsSMTLIB2.build(); + return declarations; } @Override From 43a2413ff96732f62ad869d2f32d992e297b8947 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sat, 1 Nov 2025 14:30:33 +0100 Subject: [PATCH 45/47] CVC5FormulaManager improve JavaDoc for generation of declarations from terms --- .../sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 6 +++--- 1 file changed, 3 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 7ef39f004f..6f7984d690 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -301,9 +301,9 @@ private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { } /** - * Returns the SMTLIB2 declarations for the input Map line by line with one - * declaration per line, with a line-break at the end of all lines. The output order will match - * the order of the input map. + * Returns the SMTLIB2 declarations for the input Map with key=symbol for the value=term, line by + * line with one declaration per line, with a line-break at the end of all lines. The output order + * will match the order of the input map. */ private static StringBuilder getSMTLIB2DeclarationsFor(ImmutableMap varsAndUFs) { StringBuilder declarations = new StringBuilder(); From 55de80f6051dc751f58b9bb1d9e33198e0259bb1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 2 Nov 2025 13:26:40 +0100 Subject: [PATCH 46/47] CVC5 parser: add more doc for options used --- .../solvers/cvc5/CVC5FormulaManager.java | 20 ++++++++++++++----- 1 file changed, 15 insertions(+), 5 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 6f7984d690..66862b7c88 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -210,16 +210,26 @@ private InputParser getParser(Solver parseSolver) { throw new AssertionError("Unexpected exception", e); } } - // Expected success string due to option set: "success\n" + // Expected success string due to option set is "success\n" (as sanity check when invoking + // parsing commands, which might also return errors!) parseSolver.setOption("print-success", "true"); - // more tolerant of non-conforming inputs, default: default + + // More tolerant of non-conforming inputs, default: default + // Allows e.g. parsing of Mathsat output with . in front of the definition names. parseSolver.setOption("parsing-mode", "lenient"); - // force all declarations and definitions to be global when parsing, default: false + + // Force all declarations and definitions to be global when parsing, default: false + // I.e. remembers declarations and definitions and helps to re-use them when parsed before etc. parseSolver.setOption("global-declarations", "true"); - // use API interface for fresh constants when parsing declarations and definitions, default: + + // Use API interface for fresh constants when parsing declarations and definitions, default: // true + // Parser re-uses existing declarations and definitions. parseSolver.setOption("fresh-declarations", "false"); - // allows overloading of terms and sorts if true, default: true + + // Allows overloading of terms and sorts if true, default: true + // Technically we want this to happen. But disabling this allows us to do it with our cache + // safely and get better error messaged. parseSolver.setOption("term-sort-overload", "false"); InputParser parser = new InputParser(parseSolver, symbolManager); From b8b6483bda535c48889e5115e8d946ec6f2eb6d8 Mon Sep 17 00:00:00 2001 From: BaierD Date: Sun, 2 Nov 2025 14:07:48 +0100 Subject: [PATCH 47/47] CVC5 parser: make JavaDoc of parser creation more descriptive --- .../sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java | 4 ++-- 1 file changed, 2 insertions(+), 2 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 66862b7c88..b375d09e7e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -198,8 +198,8 @@ private Term parseWithAddedSymbol(String formulaStr, String symbolNotDeclared, T } /** - * Builds the parser from the given {@link Solver} and the {@link SymbolManager}. The {@link - * SymbolManager} needs to be persistent to remember terms already parsed/created. + * Builds the parser from the given {@link Solver} and the {@link SymbolManager} of this class. + * The {@link SymbolManager} needs to be persistent to remember terms already parsed/created. */ private InputParser getParser(Solver parseSolver) { if (!parseSolver.isLogicSet()) {