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