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 54761f9a1e..df70574d22 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; @@ -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; @@ -76,8 +82,9 @@ 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<>(); + protected boolean registerUnknownBoundVariables = false; private final TermManager termManager; private final Solver solver; @@ -103,7 +110,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, @@ -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 = accessVariablesCache(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 = Preconditions.checkNotNull(accessVariablesCache(name, boundVar.getSort())); + Term freeVar = getFreeVariableFromCache(name, boundVar.getSort(), visitor); body = body.substitute(boundVar, freeVar); freeVars.add(encapsulate(freeVar)); } @@ -439,7 +446,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()); @@ -768,7 +775,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, @@ -776,7 +783,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, @@ -843,19 +850,111 @@ 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); } - 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, FormulaVisitor visitor) { + if (visitor instanceof BoundVariablesRegisteringRecursiveVisitor) { + ((BoundVariablesRegisteringRecursiveVisitor) visitor).registerBoundVariable(name, sort); + } Term existingVar = variablesCache.get(name, sort.toString()); - Preconditions.checkNotNull( + return 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()); - return existingVar; + variablesCache.containsRow(name) + ? "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 e77d109188..b375d09e7e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -8,16 +8,29 @@ 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.Joiner; +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; 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 java.util.LinkedHashMap; +import io.github.cvc5.modes.InputLanguage; +import java.util.Arrays; import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -26,6 +39,11 @@ class CVC5FormulaManager extends AbstractFormulaManager allVars = new LinkedHashMap<>(); - creator.extractVariablesAndUFs(f, true, allVars::put); + 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 + // need to be included from the cache) + private Term parseCVC5(final String formulaStr) { + // checkState(definitionsInInput.isEmpty()); // TODO: remove or use + final Solver parseSolver = new Solver(creator.getEnv()); + final InputParser parser = getParser(parseSolver); + + parser.setStringInput(InputLanguage.SMT_LIB_2_6, formulaStr, ""); + + ImmutableSet.Builder substituteFromBuilder = ImmutableSet.builder(); + ImmutableSet.Builder substituteToBuilder = ImmutableSet.builder(); + + // "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! + + // 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); + } + + 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; + } + + 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); + } + } + + throw new IllegalArgumentException( + "Error parsing with CVC5: " + parseException.getMessage(), parseException); + } + + // Register new terms in our caches or throw for errors + 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(symbolManager.getNamedTerms().isEmpty()); + + // Get the assertions out of the solver and re-substitute additional definitions outside of + // assertions + 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! + 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 Term parseWithAddedSymbol(String formulaStr, String symbolNotDeclared, Term knownTerm) { + StringBuilder declaration = + getSMTLIB2DeclarationsFor(ImmutableMap.of(symbolNotDeclared, knownTerm)); + // TODO: insert after options if options present? + return parseCVC5(declaration.append(formulaStr).toString()); + } + + /** + * 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()) { + try { + parseSolver.setLogic("ALL"); + } catch (CVC5ApiException e) { + // Should never happen in this configuration + throw new AssertionError("Unexpected exception", e); + } + } + // 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 + // 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 + // 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: + // true + // Parser re-uses existing declarations and definitions. + parseSolver.setOption("fresh-declarations", "false"); + + // 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); + return parser; + } + + private void registerNewTermsInCache( + SymbolManager sm, + ImmutableSet.Builder substituteFromBuilder, + ImmutableSet.Builder substituteToBuilder) { + for (Term parsedTerm : sm.getDeclaredTerms()) { + Term termToRegister = parsedTerm; + try { + Kind kind = termToRegister.getKind(); + if (kind == Kind.APPLY_UF) { + termToRegister = termToRegister.getChild(0); + } + + String parsedTermString = termToRegister.toString(); + 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); - // print all symbols - for (Map.Entry entry : allVars.entrySet()) { + 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 + if (funCacheHit == null) { + creator.functionsCache.put(parsedTermString, termToRegister); + + } else { + substituteFromBuilder.add(termToRegister); + substituteToBuilder.add(funCacheHit); + } + + } else { + if (termCacheHit == null) { + creator.variablesCache.put(parsedTermString, parsedSortString, termToRegister); + + } else { + substituteFromBuilder.add(termToRegister); + substituteToBuilder.add(termCacheHit); + } + } + } catch (CVC5ApiException apiException) { + throw new IllegalArgumentException( + "Error parsing the following term in CVC5: " + parsedTerm, apiException); + } + } + } + + private StringBuilder getAllDeclaredVariablesAndUFsAsSMTLIB2(Term f) { + ImmutableMap.Builder allKnownVarsAndUFsBuilder = ImmutableMap.builder(); + // Get all symbols relevant for the input term + creator.extractVariablesAndUFs(f, true, allKnownVarsAndUFsBuilder::put); + + // buildKeepingLast due to UFs; 1 UF might be applied multiple times. But the names and the + // types are consistent. + return getSMTLIB2DeclarationsFor(allKnownVarsAndUFsBuilder.buildKeepingLast()); + } + + /** + * 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(); + for (Entry entry : varsAndUFs.entrySet()) { String name = entry.getKey(); - Term var = entry.getValue(); + Term varOrUf = entry.getValue(); + StringBuilder line = new StringBuilder(); // escaping is stolen from SMTInterpol, lets hope this remains consistent - out.append("(declare-fun ").append(PrintTerm.quoteIdentifier(name)).append(" ("); + line.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); } - out.append(Joiner.on(" ").join(childrenTypes)); - // and return type - out.append(") ").append(var.getSort().toString()).append(")\n"); - } + Sort sort = varOrUf.getSort(); + if (sort.isFunction()) { + childrenTypes = Arrays.asList(sort.getFunctionDomainSorts()); + } else { + childrenTypes = Iterables.transform(varOrUf, Term::getSort); + } - // now add the final assert - out.append("(assert ").append(f).append(')'); - return out.toString(); + line.append(Joiner.on(" ").join(childrenTypes)); + + // Return type + String returnTypeString = sort.toString(); + if (sort.isFunction()) { + returnTypeString = sort.getFunctionCodomainSort().toString(); + } + line.append(") ").append(returnTypeString).append(")\n"); + declarations.append(line); + } + return declarations; } @Override @@ -124,4 +372,68 @@ public T substitute( FormulaType type = getFormulaType(f); return getFormulaCreator().encapsulate(type, input.substitute(changeFrom, changeTo)); } + + 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); + } + } + + 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; + } + + // 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( + 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 + // as function-def. We re-substitute these into the assertion. + for (int i = assertions.length - 1; i >= 1; i--) { + Term parsedDefinition = assertions[i]; + + try { + 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()); + } + + } 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; + } } 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..8622407852 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,95 @@ 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 +282,23 @@ private ValueAssignment getAssignment(Term pKeyTerm) { } Term valueTerm = solver.getValue(pKeyTerm); - Formula keyFormula = creator.encapsulateWithTypeOf(pKeyTerm); - Formula valueFormula = creator.encapsulateWithTypeOf(valueTerm); - BooleanFormula equation = - creator.encapsulateBoolean(termManager.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); - Object value = creator.convertValue(pKeyTerm, valueTerm); - return new ValueAssignment( - keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build()); + if (valueTerm.getSort().isArray()) { + return buildArrayAssignment(pKeyTerm, valueTerm); + } else { + Formula keyFormula = creator.encapsulateWithTypeOf(pKeyTerm); + Formula valueFormula = creator.encapsulateWithTypeOf(valueTerm); + BooleanFormula equation = + creator.encapsulateBoolean(termManager.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); + Object value = creator.convertValue(pKeyTerm, valueTerm); + return ImmutableList.of( + new ValueAssignment( + keyFormula, + valueFormula, + equation, + nameStr, + value, + argumentInterpretationBuilder.build())); + } } @Override diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 40213bd4e0..e0c736944f 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(); @@ -2243,7 +2364,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 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() { diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index 5701551726..2df3f08aa0 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 {