diff --git a/lib/ivy.xml b/lib/ivy.xml index ec89566edb..5cc7b4144e 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -169,7 +169,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java index 8c19b42bae..777251950f 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.FluentIterable; import de.uni_freiburg.informatik.ultimate.logic.Annotation; import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; import de.uni_freiburg.informatik.ultimate.logic.Assignments; @@ -28,6 +29,7 @@ import java.math.BigDecimal; import java.math.BigInteger; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.List; import java.util.Map; @@ -70,14 +72,18 @@ public LBool assertTerm(Term pTerm) throws SMTLIBException { @Override public void declareFun(String fun, Sort[] paramSorts, Sort resultSort) throws SMTLIBException { - FunctionSymbol fsym = theory.getFunction(fun, paramSorts); - - if (fsym == null) { + var functions = theory.getDeclaredFunctions(); + if (!functions.containsKey(fun)) { + // There is no function with that name yet: create a new symbol script.declareFun(fun, paramSorts, resultSort); } else { - if (!fsym.getReturnSort().equals(resultSort)) { + // A symbol with the same name already exists: Check if the signature matches and throw an + // exception otherwise + var decl = functions.get(fun); + if (!Arrays.equals(decl.getParameterSorts(), paramSorts) + || !decl.getReturnSort().equals(resultSort)) { throw new SMTLIBException( - "Function " + fun + " is already declared with different definition"); + "Function '%s' already declared with a different sort".formatted(fun)); } } } @@ -85,18 +91,21 @@ public void declareFun(String fun, Sort[] paramSorts, Sort resultSort) throws SM @Override public void defineFun(String fun, TermVariable[] params, Sort resultSort, Term definition) throws SMTLIBException { - Sort[] paramSorts = new Sort[params.length]; - for (int i = 0; i < paramSorts.length; i++) { - paramSorts[i] = params[i].getSort(); - } - FunctionSymbol fsym = theory.getFunction(fun, paramSorts); - - if (fsym == null) { + var functions = theory.getDeclaredFunctions(); + if (!functions.containsKey(fun)) { + // There is no function with that name yet: create a new symbol script.defineFun(fun, params, resultSort, definition); } else { - if (!fsym.getDefinition().equals(definition) || !fsym.getReturnSort().equals(resultSort)) { + // A symbol with the same name already exists: Check if the signature and the definition + // match and throw an exception otherwise + var decl = functions.get(fun); + if (!Arrays.equals( + decl.getParameterSorts(), + FluentIterable.from(params).transform(TermVariable::getSort).toArray(Sort.class)) + || !decl.getReturnSort().equals(resultSort) + || !decl.getDefinition().equals(definition)) { throw new SMTLIBException( - "Function " + fun + " is already defined with different definition"); + "Function '%s' already declared with a different sort".formatted(fun)); } } } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java index 2fe42faf15..12a7437fd0 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -90,7 +90,7 @@ public R allSat(AllSatCallback callback, List predicates) } @Override - protected boolean isUnsatImpl() throws InterruptedException { + protected boolean isUnsatImpl() throws InterruptedException, SolverException { out.print("(check-sat)"); boolean isUnsat = super.isUnsatImpl(); out.println(" ; " + (isUnsat ? "UNSAT" : "SAT")); diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java index 44ea0f5e1d..3a28ae8868 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -106,7 +106,7 @@ protected String addConstraint0(BooleanFormula constraint) { } @Override - protected boolean isUnsatImpl() throws InterruptedException { + protected boolean isUnsatImpl() throws InterruptedException, SolverException { // We actually terminate SmtInterpol during the analysis // by using a shutdown listener. However, SmtInterpol resets the // mStopEngine flag in DPLLEngine before starting to solve, @@ -118,21 +118,13 @@ protected boolean isUnsatImpl() throws InterruptedException { case SAT -> false; case UNSAT -> true; case UNKNOWN -> { - Object reason = env.getInfo(":reason-unknown"); - if (!(reason instanceof ReasonUnknown unknown)) { - throw new SMTLIBException("checkSat returned UNKNOWN with unknown reason " + reason); - } - switch (unknown) { - case MEMOUT -> - // SMTInterpol catches OOM, but we want to have it thrown. - throw new OutOfMemoryError("Out of memory during SMTInterpol operation"); - case CANCELLED -> { - shutdownNotifier.shutdownIfNecessary(); // expected if we requested termination - throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason); - } - default -> - throw new SMTLIBException( - "checkSat returned UNKNOWN with unexpected reason " + reason); + var reason = (ReasonUnknown) env.getInfo(":reason-unknown"); + switch (reason) { + case MEMOUT -> throw new OutOfMemoryError(); + case INCOMPLETE -> + throw new SolverException("Incomplete theory, could not decide satisfiability"); + case CANCELLED -> throw new InterruptedException(); + default -> throw new RuntimeException("Unknown solver error"); } } }; diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolBitvectorFormulaManager.java new file mode 100644 index 0000000000..3282acdfe8 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolBitvectorFormulaManager.java @@ -0,0 +1,197 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.smtinterpol; + +import static com.google.common.base.Preconditions.checkArgument; + +import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Sort; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import java.math.BigInteger; +import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; +import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; + +public class SmtInterpolBitvectorFormulaManager + extends AbstractBitvectorFormulaManager { + protected SmtInterpolBitvectorFormulaManager( + FormulaCreator pCreator, + AbstractBooleanFormulaManager pBmgr) { + super(pCreator, pBmgr); + } + + @Override + protected Term makeBitvectorImpl(int length, Term pParam1) { + return getFormulaCreator() + .getEnv() + .term("int_to_bv", new String[] {String.valueOf(length)}, null, pParam1); + } + + @Override + protected Term toIntegerFormulaImpl(Term pI, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "sbv_to_int" : "ubv_to_int", pI); + } + + @Override + protected Term negate(Term pParam1) { + return getFormulaCreator().getEnv().term("bvneg", pParam1); + } + + @Override + protected Term add(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvadd", pParam1, pParam2); + } + + @Override + protected Term subtract(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvsub", pParam1, pParam2); + } + + @Override + protected Term divide(Term pParam1, Term pParam2, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvsdiv" : "bvudiv", pParam1, pParam2); + } + + @Override + protected Term remainder(Term pParam1, Term pParam2, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvsrem" : "bvurem", pParam1, pParam2); + } + + @Override + protected Term smodulo(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvsmod", pParam1, pParam2); + } + + @Override + protected Term multiply(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvmul", pParam1, pParam2); + } + + @Override + protected Term equal(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("=", pParam1, pParam2); + } + + @Override + protected Term greaterThan(Term pParam1, Term pParam2, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvsgt" : "bvugt", pParam1, pParam2); + } + + @Override + protected Term greaterOrEquals(Term pParam1, Term pParam2, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvsge" : "bvuge", pParam1, pParam2); + } + + @Override + protected Term lessThan(Term pParam1, Term pParam2, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvslt" : "bvult", pParam1, pParam2); + } + + @Override + protected Term lessOrEquals(Term pParam1, Term pParam2, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvsle" : "bvule", pParam1, pParam2); + } + + @Override + protected Term not(Term pParam1) { + return getFormulaCreator().getEnv().term("bvnot", pParam1); + } + + @Override + protected Term and(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvand", pParam1, pParam2); + } + + @Override + protected Term or(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvor", pParam1, pParam2); + } + + @Override + protected Term xor(Term pParam1, Term pParam2) { + return getFormulaCreator().getEnv().term("bvxor", pParam1, pParam2); + } + + @Override + protected Term makeBitvectorImpl(int pLength, BigInteger pI) { + var raw = pI; + if (pI.signum() < 0) { + var positive = pI.negate(); + var value = BigInteger.ZERO; + for (var p = 0; p < Math.max(pLength, pI.bitLength() + 1); p++) { + if (p < positive.bitLength()) { + value = !positive.testBit(p) ? value.setBit(p) : value; + } else { + value = value.setBit(p); + } + } + raw = value.add(BigInteger.ONE); + } + checkArgument(raw.bitLength() <= pLength); + return getFormulaCreator() + .getEnv() + .getTheory() + .constant(raw, formulaCreator.getBitvectorType(pLength)); + } + + @Override + protected Term makeVariableImpl(int pLength, String pVar) { + return getFormulaCreator().makeVariable(getFormulaCreator().getBitvectorType(pLength), pVar); + } + + @Override + protected Term shiftRight(Term pNumber, Term toShift, boolean signed) { + return getFormulaCreator().getEnv().term(signed ? "bvashr" : "bvlshr", pNumber, toShift); + } + + @Override + protected Term shiftLeft(Term pNumber, Term pToShift) { + return getFormulaCreator().getEnv().term("bvshl", pNumber, pToShift); + } + + @Override + protected Term rotateRightByConstant(Term pNumber, int pToRotate) { + return getFormulaCreator() + .getEnv() + .term("rotate_right", new String[] {String.valueOf(pToRotate)}, null, pNumber); + } + + @Override + protected Term rotateLeftByConstant(Term pNumber, int pToRotate) { + return getFormulaCreator() + .getEnv() + .term("rotate_left", new String[] {String.valueOf(pToRotate)}, null, pNumber); + } + + @Override + protected Term concat(Term number, Term pAppend) { + return getFormulaCreator().getEnv().term("concat", number, pAppend); + } + + @Override + protected Term extract(Term pNumber, int pMsb, int pLsb) { + return getFormulaCreator() + .getEnv() + .term("extract", new String[] {String.valueOf(pMsb), String.valueOf(pLsb)}, null, pNumber); + } + + @Override + protected Term extend(Term pNumber, int pExtensionBits, boolean pSigned) { + return getFormulaCreator() + .getEnv() + .term( + pSigned ? "sign_extend" : "zero_extend", + new String[] {String.valueOf(pExtensionBits)}, + null, + pNumber); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java index bdc2f94c87..ea12d068d5 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -11,25 +11,38 @@ import static com.google.common.base.Preconditions.checkArgument; import static org.sosy_lab.common.collect.Collections3.transformedImmutableListCopy; +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import com.google.errorprone.annotations.CanIgnoreReturnValue; +import de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm; import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm; import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; +import de.uni_freiburg.informatik.ultimate.logic.LambdaTerm; +import de.uni_freiburg.informatik.ultimate.logic.LetTerm; +import de.uni_freiburg.informatik.ultimate.logic.MatchTerm; import de.uni_freiburg.informatik.ultimate.logic.NoopScript; +import de.uni_freiburg.informatik.ultimate.logic.QuantifiedFormula; import de.uni_freiburg.informatik.ultimate.logic.Rational; import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException; import de.uni_freiburg.informatik.ultimate.logic.Script; import de.uni_freiburg.informatik.ultimate.logic.Sort; import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.TermVariable; import de.uni_freiburg.informatik.ultimate.logic.Theory; +import java.math.BigDecimal; import java.math.BigInteger; import java.util.ArrayList; +import java.util.Arrays; import java.util.List; +import java.util.Map; import org.sosy_lab.java_smt.api.ArrayFormula; +import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FunctionDeclarationKind; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; @@ -39,7 +52,7 @@ class SmtInterpolFormulaCreator extends FormulaCreator UNSUPPORTED_IDENTIFIERS = - ImmutableSet.of("true", "false", "select", "store", "or", "and", "xor", "distinct"); + ImmutableSet.of("true", "false", "select", "store", "or", "and", "xor", "distinct", "_"); SmtInterpolFormulaCreator(final Script env) { super( @@ -63,6 +76,8 @@ private FormulaType getFormulaTypeOfSort(final Sort pSort) { return FormulaType.RationalType; } else if (pSort == getBoolType()) { return FormulaType.BooleanType; + } else if (pSort.isBitVecSort()) { + return FormulaType.getBitvectorTypeWithSize(Integer.parseInt(pSort.getIndices()[0])); } else if (pSort.isArraySort()) { return FormulaType.getArrayType( getFormulaTypeOfSort(pSort.getArguments()[0]), @@ -81,8 +96,7 @@ public FormulaType getFormulaType(final T pFormula) { getArrayFormulaElementType((ArrayFormula) pFormula); return (FormulaType) FormulaType.getArrayType(arrayIndexType, arrayElementType); } - - return super.getFormulaType(pFormula); + return (FormulaType) getFormulaTypeOfSort(extractInfo(pFormula).getSort()); } @Override @@ -99,26 +113,21 @@ public Term makeVariable(final Sort type, final String varName) { @CanIgnoreReturnValue private FunctionSymbol declareFun(String fun, Sort[] paramSorts, Sort resultSort) { checkSymbol(fun); - FunctionSymbol fsym = environment.getTheory().getFunction(fun, paramSorts); - - if (fsym == null) { - try { - environment.declareFun(fun, paramSorts, resultSort); - } catch (SMTLIBException e) { - // can fail, if function is already declared with a different sort - throw new IllegalArgumentException("Cannot declare function '" + fun + "'", e); - } - return environment.getTheory().getFunction(fun, paramSorts); + var functions = environment.getTheory().getDeclaredFunctions(); + if (!functions.containsKey(fun)) { + // There is no function with that name yet: create a new symbol + environment.declareFun(fun, paramSorts, resultSort); } else { - if (!fsym.getReturnSort().equals(resultSort)) { + // A symbol with the same name already exists: Check if the signature matches and throw an + // exception otherwise + var decl = functions.get(fun); + if (!Arrays.equals(decl.getParameterSorts(), paramSorts) + || !decl.getReturnSort().equals(resultSort)) { throw new IllegalArgumentException( - "Function " + fun + " is already declared with different definition"); - } - if (fun.equals("true") || fun.equals("false")) { - throw new IllegalArgumentException("Cannot declare a variable named " + fun); + "Function '%s' already declared with a different sort".formatted(fun)); } - return fsym; } + return functions.get(fun); } /** @@ -131,8 +140,6 @@ private FunctionSymbol declareFun(String fun, Sort[] paramSorts, Sort resultSort * @throws IllegalArgumentException if symbol contains | or \. */ private void checkSymbol(String symbol) throws SMTLIBException { - checkArgument( - symbol.indexOf('|') == -1 && symbol.indexOf('\\') == -1, "Symbol must not contain | or \\"); checkArgument( !UNSUPPORTED_IDENTIFIERS.contains(symbol), "SMTInterpol does not support %s as identifier.", @@ -141,8 +148,7 @@ private void checkSymbol(String symbol) throws SMTLIBException { @Override public Sort getBitvectorType(final int pBitwidth) { - throw new UnsupportedOperationException( - "Bitvector theory is not supported " + "by SmtInterpol"); + return environment.getTheory().getSort("BitVec", new String[] {String.valueOf(pBitwidth)}); } @Override @@ -164,16 +170,35 @@ public Object convertValue(Term value) { return value.getTheory().mTrue == value; } else if (value instanceof ConstantTerm constantTerm && constantTerm.getValue() instanceof Rational rationalValue) { - /* * From SmtInterpol documentation (see {@link ConstantTerm#getValue}), - * the output is SmtInterpol's Rational unless it is a bitvector, - * and currently we do not support bitvectors for SmtInterpol. + * the output is SmtInterpol's Rational unless it is a bitvector, even if the formula has + * Integer type */ org.sosy_lab.common.rationals.Rational ratValue = org.sosy_lab.common.rationals.Rational.of( rationalValue.numerator(), rationalValue.denominator()); return ratValue.isIntegral() ? ratValue.getNum() : ratValue; + } else if (value instanceof ConstantTerm constantTerm + && constantTerm.getValue() instanceof BigDecimal decimalValue) { + // Reals can be either rational or decimal values + return org.sosy_lab.common.rationals.Rational.ofBigDecimal(decimalValue); + + } else if (value instanceof ConstantTerm constantTerm + && constantTerm.getValue() instanceof BigInteger bitvectorValue) { + // Bitvector term (_ bv0 32) + return bitvectorValue; + } else if (value instanceof ConstantTerm constantTerm + && constantTerm.getValue() instanceof String bitvectorValue) { + // Bitvector term #b1001 or #xffe + var prefix = bitvectorValue.substring(0, 2); + var base = + switch (prefix) { + case "#b" -> 2; + case "#x" -> 16; + default -> throw new IllegalStateException("Unexpected value: " + bitvectorValue); + }; + return new BigInteger(bitvectorValue.substring(2), base); } else { throw new IllegalArgumentException("Unexpected value: " + value); } @@ -181,25 +206,9 @@ public Object convertValue(Term value) { @Override public R visit(FormulaVisitor visitor, Formula f, final Term input) { - checkArgument( - input.getTheory().equals(environment.getTheory()), - "Given term belongs to a different instance of SMTInterpol: %s", - input); - if (input instanceof ConstantTerm constantTerm) { - Object outValue; - Object interpolValue = constantTerm.getValue(); - if (interpolValue instanceof Rational rat) { - if ((input.getSort().getName().equals("Int") && rat.isIntegral()) - || BigInteger.ONE.equals(rat.denominator())) { - outValue = rat.numerator(); - } else { - outValue = org.sosy_lab.common.rationals.Rational.of(rat.numerator(), rat.denominator()); - } - } else { - outValue = constantTerm.getValue(); - } - return visitor.visitConstant(f, outValue); + return visitor.visitConstant(f, convertValue(constantTerm)); + } else if (input instanceof ApplicationTerm app) { final int arity = app.getParameters().length; final FunctionSymbol func = app.getFunction(); @@ -237,15 +246,76 @@ public R visit(FormulaVisitor visitor, Formula f, final Term input) { name, getDeclarationKind(app), argTypes, getFormulaType(f), app.getFunction())); } - } else { - // TODO: support for quantifiers and bound variables + } else if (input instanceof QuantifiedFormula quantified) { + var quantifier = + switch (quantified.getQuantifier()) { + case QuantifiedFormula.EXISTS -> Quantifier.EXISTS; + case QuantifiedFormula.FORALL -> Quantifier.FORALL; + default -> throw new AssertionError(); + }; + + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (TermVariable var : quantified.getVariables()) { + builder.put(var, makeVariable(var.getSort(), var.getName())); + } + + var newVars = builder.buildOrThrow(); + var newBody = substBoundVariables(newVars, quantified.getSubformula()); + + return visitor.visitQuantifier( + (BooleanFormula) f, + quantifier, + transformedImmutableListCopy(newVars.values(), this::encapsulateWithTypeOf), + encapsulateBoolean(newBody)); + } else { throw new UnsupportedOperationException( "Unexpected SMTInterpol formula of type %s: %s" .formatted(input.getClass().getSimpleName(), input)); } } + /** Substitute bound variables with free variables. */ + private Term substBoundVariables(Map pSubst, Term pTerm) { + if (pTerm instanceof ApplicationTerm application) { + var args = application.getParameters(); + if (args.length == 0) { + return pTerm; + } else { + return callFunctionImpl( + application.getFunction(), + FluentIterable.from(args).transform(p -> substBoundVariables(pSubst, p)).toList()); + } + } else if (pTerm instanceof ConstantTerm constant) { + return constant; + } else if (pTerm instanceof TermVariable variable) { + return pSubst.getOrDefault(variable, variable); + } else if (pTerm instanceof AnnotatedTerm annotated) { + throw new IllegalArgumentException("Unexpected 'annotated' term: %s".formatted(annotated)); + } else if (pTerm instanceof LambdaTerm lambda) { + throw new IllegalArgumentException("Unexpected 'lambda' term: %s".formatted(lambda)); + } else if (pTerm instanceof LetTerm let) { + throw new IllegalArgumentException("Unexpected 'let' term: %s".formatted(let)); + } else if (pTerm instanceof MatchTerm match) { + throw new IllegalArgumentException("Unexpected 'match' term: %s".formatted(match)); + } else if (pTerm instanceof QuantifiedFormula quantified) { + var bound = FluentIterable.from(quantified.getVariables()).toList(); + ImmutableMap.Builder newSubst = ImmutableMap.builder(); + for (var entry : pSubst.entrySet()) { + if (!bound.contains(entry.getKey())) { + newSubst.put(entry.getKey(), entry.getValue()); + } + } + return getEnv() + .quantifier( + quantified.getQuantifier(), + quantified.getVariables(), + substBoundVariables(newSubst.buildOrThrow(), quantified.getSubformula())); + } else { + throw new AssertionError(); + } + } + String getName(Term t) { if (t instanceof ApplicationTerm app && isUF(app)) { return app.getFunction().getName(); @@ -313,6 +383,54 @@ private FunctionDeclarationKind getDeclarationKind(ApplicationTerm input) { case ">=" -> FunctionDeclarationKind.GTE; case "to_int" -> FunctionDeclarationKind.FLOOR; case "to_real" -> FunctionDeclarationKind.TO_REAL; + + case "concat" -> FunctionDeclarationKind.BV_CONCAT; + case "extract" -> FunctionDeclarationKind.BV_EXTRACT; + case "bvnot" -> FunctionDeclarationKind.BV_NOT; + case "bvand" -> FunctionDeclarationKind.BV_AND; + case "bvor" -> FunctionDeclarationKind.BV_OR; + case "bvneg" -> FunctionDeclarationKind.BV_NEG; + case "bvadd" -> FunctionDeclarationKind.BV_ADD; + case "bvmul" -> FunctionDeclarationKind.BV_MUL; + case "bvudiv" -> FunctionDeclarationKind.BV_UDIV; + case "bvurem" -> FunctionDeclarationKind.BV_UREM; + case "bvshl" -> FunctionDeclarationKind.BV_SHL; + case "bvlshr" -> FunctionDeclarationKind.BV_LSHR; + case "bvnand" -> FunctionDeclarationKind.OTHER; + case "bvnor" -> FunctionDeclarationKind.OTHER; + case "bvxor" -> FunctionDeclarationKind.BV_XOR; + case "bvxnor" -> FunctionDeclarationKind.OTHER; + case "bvcomp" -> FunctionDeclarationKind.OTHER; + case "bvsub" -> FunctionDeclarationKind.BV_SUB; + case "bvsdiv" -> FunctionDeclarationKind.BV_SDIV; + case "bvsrem" -> FunctionDeclarationKind.BV_SREM; + case "bvsmod" -> FunctionDeclarationKind.BV_SMOD; + case "bvashr" -> FunctionDeclarationKind.BV_ASHR; + case "repeat" -> FunctionDeclarationKind.OTHER; + case "zero_extend" -> FunctionDeclarationKind.BV_ZERO_EXTENSION; + case "sign_extend" -> FunctionDeclarationKind.BV_SIGN_EXTENSION; + case "rotate_left" -> FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT; + case "rotate_right" -> FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT; + case "bvult" -> FunctionDeclarationKind.BV_ULT; + case "bvule" -> FunctionDeclarationKind.BV_ULE; + case "bvugt" -> FunctionDeclarationKind.BV_UGT; + case "bvuge" -> FunctionDeclarationKind.BV_UGE; + case "bvslt" -> FunctionDeclarationKind.BV_SLT; + case "bvsle" -> FunctionDeclarationKind.BV_SLE; + case "bvsgt" -> FunctionDeclarationKind.BV_SGT; + case "bvsge" -> FunctionDeclarationKind.BV_SGE; + case "ubv_to_int" -> FunctionDeclarationKind.UBV_TO_INT; + case "sbv_to_int" -> FunctionDeclarationKind.SBV_TO_INT; + case "int_to_bv" -> FunctionDeclarationKind.INT_TO_BV; + case "bvnego" -> FunctionDeclarationKind.OTHER; + case "bvuaddo" -> FunctionDeclarationKind.OTHER; + case "bvsaddo" -> FunctionDeclarationKind.OTHER; + case "bvumulo" -> FunctionDeclarationKind.OTHER; + case "bvsmulo" -> FunctionDeclarationKind.OTHER; + case "bvusubo" -> FunctionDeclarationKind.OTHER; + case "bvssubo" -> FunctionDeclarationKind.OTHER; + case "bvsdivo" -> FunctionDeclarationKind.OTHER; + default -> // TODO: other declaration kinds! FunctionDeclarationKind.OTHER; @@ -341,8 +459,8 @@ public Term callFunctionImpl(FunctionSymbol declaration, List args) { } castedArgs.add(arg); } - - return environment.term(declaration.getName(), castedArgs.toArray(new Term[0])); + return environment.term( + declaration.getName(), declaration.getIndices(), null, castedArgs.toArray(new Term[0])); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java index f91e8def43..2ec4436463 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java @@ -40,13 +40,16 @@ class SmtInterpolFormulaManager extends AbstractFormulaManager + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.smtinterpol; + +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableMap; +import de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm; +import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; +import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm; +import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; +import de.uni_freiburg.informatik.ultimate.logic.LambdaTerm; +import de.uni_freiburg.informatik.ultimate.logic.LetTerm; +import de.uni_freiburg.informatik.ultimate.logic.MatchTerm; +import de.uni_freiburg.informatik.ultimate.logic.QuantifiedFormula; +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Sort; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.TermVariable; +import java.util.List; +import java.util.Map; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; + +public class SmtInterpolQuantifiedFormulaManager + extends AbstractQuantifiedFormulaManager { + protected SmtInterpolQuantifiedFormulaManager( + FormulaCreator pCreator) { + super(pCreator); + } + + @Override + protected Term eliminateQuantifiers(Term pExtractInfo) + throws SolverException, InterruptedException { + throw new UnsupportedOperationException(); + } + + /** Replace free variables with bound variables. */ + private Term substFreeVariables(Map pSubst, Term pTerm) { + if (pTerm instanceof ApplicationTerm application) { + var args = application.getParameters(); + if (args.length == 0) { + return pSubst.containsKey(pTerm) ? pSubst.get(pTerm) : pTerm; + } else { + return formulaCreator.callFunctionImpl( + application.getFunction(), + FluentIterable.from(args).transform(p -> substFreeVariables(pSubst, p)).toList()); + } + } else if (pTerm instanceof ConstantTerm constant) { + return constant; + } else if (pTerm instanceof TermVariable variable) { + return variable; + } else if (pTerm instanceof AnnotatedTerm annotated) { + throw new IllegalArgumentException("Unexpected 'annotated' term: %s".formatted(annotated)); + } else if (pTerm instanceof LambdaTerm lambda) { + throw new IllegalArgumentException("Unexpected 'lambda' term: %s".formatted(lambda)); + } else if (pTerm instanceof LetTerm let) { + throw new IllegalArgumentException("Unexpected 'let' term: %s".formatted(let)); + } else if (pTerm instanceof MatchTerm match) { + throw new IllegalArgumentException("Unexpected 'match' term: %s".formatted(match)); + } else if (pTerm instanceof QuantifiedFormula quantified) { + formulaCreator + .getEnv() + .quantifier( + quantified.getQuantifier(), + quantified.getVariables(), + substFreeVariables(pSubst, quantified.getSubformula())); + } else { + throw new AssertionError(); + } + return pTerm; + } + + @Override + public Term mkQuantifier(Quantifier q, List vars, Term body) { + var quantifier = + switch (q) { + case FORALL -> QuantifiedFormula.FORALL; + case EXISTS -> QuantifiedFormula.EXISTS; + }; + + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (Term var : vars) { + builder.put( + var, + formulaCreator + .getEnv() + .variable(((ApplicationTerm) var).getFunction().getName(), var.getSort())); + } + + var newVars = builder.buildOrThrow(); + var newBody = substFreeVariables(newVars, body); + + return formulaCreator + .getEnv() + .quantifier(quantifier, newVars.values().toArray(new TermVariable[0]), newBody); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java index 278b878b3d..7687544bbd 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -124,7 +124,11 @@ public static SmtInterpolSolverContext create( new SmtInterpolIntegerFormulaManager(creator, pNonLinearArithmetic); SmtInterpolRationalFormulaManager rationalTheory = new SmtInterpolRationalFormulaManager(creator, pNonLinearArithmetic); + SmtInterpolBitvectorFormulaManager bitvectorTheory = + new SmtInterpolBitvectorFormulaManager(creator, booleanTheory); SmtInterpolArrayFormulaManager arrayTheory = new SmtInterpolArrayFormulaManager(creator); + SmtInterpolQuantifiedFormulaManager quantifiedTheory = + new SmtInterpolQuantifiedFormulaManager(creator); SmtInterpolFormulaManager manager = new SmtInterpolFormulaManager( creator, @@ -132,7 +136,9 @@ public static SmtInterpolSolverContext create( booleanTheory, integerTheory, rationalTheory, + bitvectorTheory, arrayTheory, + quantifiedTheory, logger); return new SmtInterpolSolverContext(manager, pShutdownNotifier, settings); } @@ -140,7 +146,7 @@ public static SmtInterpolSolverContext create( /** instantiate the central SMTInterpol script from where all others are copied. */ private static Script getSmtInterpolScript( ShutdownNotifier pShutdownNotifier, - @javax.annotation.Nullable PathCounterTemplate smtLogfile, + @Nullable PathCounterTemplate smtLogfile, SmtInterpolSettings settings, LogManager logger) throws InvalidConfigurationException { @@ -160,11 +166,7 @@ private static Script getSmtInterpolScript( e); } } - // TODO: We would like to use Logics.ALL here and let the solver decide which logics are needed. - // But ... SMTInterpol eagerly checks logics for model generation, - // so we limit the available theories here to a large set of logics, - // including Arrays, UFs, and non-linear arithmetics over Ints and Rationals. - script.setLogic(Logics.AUFNIRA); + script.setLogic(Logics.ALL); return script; } diff --git a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java index 40564d9150..9824398310 100644 --- a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java @@ -221,6 +221,10 @@ public void testArrayConstBvWithDefault() throws SolverException, InterruptedExc .withMessage("Solver %s does not yet support array initialization", solverToUse()) .that(solverToUse()) .isNotEqualTo(Solvers.BOOLECTOR); + assume() + .withMessage("SmtInterpol does not support constant arrays over bitvectors") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); final int size = 8; diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index 6d74474e72..408200fb87 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java @@ -166,6 +166,7 @@ public void bvModelValue32bit() throws SolverException, InterruptedException { public void bvToInt() throws SolverException, InterruptedException { requireBitvectorToInt(); requireIntegers(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); for (int size : new int[] {1, 2, 4, 8}) { int max = 1 << size; @@ -192,6 +193,7 @@ public void bvToInt() throws SolverException, InterruptedException { public void bvToIntEquality() throws SolverException, InterruptedException { requireBitvectorToInt(); requireIntegers(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); for (int size : new int[] {10, 16, 20, 32, 64}) { for (int i : new int[] {1, 2, 4, 32, 64, 100}) { @@ -217,6 +219,7 @@ public void bvToIntEquality() throws SolverException, InterruptedException { public void bvToIntEqualityWithOverflow() throws SolverException, InterruptedException { requireBitvectorToInt(); requireIntegers(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); for (int size : SOME_SIZES) { for (int i : SOME_NUMBERS) { @@ -241,6 +244,7 @@ public void bvToIntEqualityWithOverflow() throws SolverException, InterruptedExc public void bvToIntEqualityWithOverflowNegative() throws SolverException, InterruptedException { requireBitvectorToInt(); requireIntegers(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); for (int size : SOME_SIZES) { for (int i : SOME_NUMBERS) { @@ -266,6 +270,7 @@ public void bvToIntEqualityWithOverflowNegative() throws SolverException, Interr public void bvToIntEqualityWithSymbols() throws SolverException, InterruptedException { requireBitvectorToInt(); requireIntegers(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); for (int size : new int[] {1, 2, 4}) { IntegerFormula var = imgr.makeVariable("x_" + size); @@ -428,6 +433,8 @@ public void bvIsZeroAfterShiftLeft() throws SolverException, InterruptedExceptio @Test public void bvRotateByConstant() throws SolverException, InterruptedException { + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); + for (int bitsize : new int[] {8, 13, 25, 31}) { BitvectorFormula zero = bvmgr.makeBitvector(bitsize, 0); BitvectorFormula a = bvmgr.makeVariable(bitsize, "a" + bitsize); @@ -468,6 +475,7 @@ public void bvRotateByBV() throws SolverException, InterruptedException { switch (solverToUse()) { case YICES2 -> new int[] {2, 3, 4, 8}; case PRINCESS -> new int[] {2, 3}; // Princess is too slow for larger bitvectors + case SMTINTERPOL -> new int[] {1}; // SmtInterpol is very slow in this test default -> new int[] {2, 3, 4, 8, 13, 25, 31}; }; @@ -584,6 +592,8 @@ public void bvITETest() { @Test public void bvModulo() throws SolverException, InterruptedException { + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); + BitvectorFormula ten = bvmgr.makeBitvector(8, 10); BitvectorFormula five = bvmgr.makeBitvector(8, 5); BitvectorFormula three = bvmgr.makeBitvector(8, 3); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 2c48cb6396..da2f5fed02 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1319,6 +1319,10 @@ public void testGetArrays3BitvectorNoParsing() throws SolverException, Interrupt + "but reports only default 123") .that(solverToUse()) .isNotEqualTo(Solvers.YICES2); + assume() + .withMessage("SmtInterpol uses default values for the array") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); // (= (select (select (select arr 5) 3) 1) x) // (= x 123)" @@ -2514,7 +2518,12 @@ public void arrayTest5() assume() .withMessage("Solver is quite slow for this example") .that(solverToUse()) - .isNoneOf(Solvers.CVC5, Solvers.MATHSAT5, Solvers.PRINCESS, Solvers.BITWUZLA); + .isNoneOf( + Solvers.CVC5, + Solvers.MATHSAT5, + Solvers.PRINCESS, + Solvers.BITWUZLA, + Solvers.SMTINTERPOL); checkModelIteration(formula, false); } @@ -2657,6 +2666,14 @@ public void testArray2BvBv() { assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); // Doesn't support multiple indices + // SmtInterpol returns the following model: + // array[5,_]=20 + // array[3,2]=5 <- Only index without wildcards + // array[3,_]=20 + // array[_,7]=10 + // array[_,_]=20 + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); + // Test for 2d bitvector arrays with formula like: // array[1][7] = 10 and array[3][2] = 5 and array[5][4] = 20 // We have no default value, so the solver can choose any value for other indices, @@ -2705,6 +2722,10 @@ public void testArrayStore1BvBvBv() { .withMessage("Yices does not support constant arrays when mcsat is used") .that(solver) .isNotEqualTo(Solvers.YICES2); + assume() + .withMessage("SmtInterpol does not support constant arrays over bitvectors") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); var scalarType = FormulaType.getBitvectorTypeWithSize(8); @@ -2750,6 +2771,10 @@ public void testArrayStore2BvBvBv() { .withMessage("Yices does not support constant arrays when mcsat is used") .that(solver) .isNotEqualTo(Solvers.YICES2); + assume() + .withMessage("SmtInterpol does not support constant arrays over bitvectors") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); // FIXME CVC4 array model is sometimes broken in JavaSMT. Unfixable in CVC4, fixed in CVC5. assume().that(solver).isNotEqualTo(Solvers.CVC4); diff --git a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java index 1e20511714..723a47e56c 100644 --- a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java @@ -552,12 +552,14 @@ public void testBVEquality() throws SolverException, InterruptedException { @Test public void testBVEquality2() throws SolverException, InterruptedException { requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); assume() .withMessage("Yices2 quantifier support is very limited at the moment") .that(solverToUse()) .isNotEqualTo(Solvers.YICES2); + assume() + .withMessage("Quantifier support in SmtInterpol is incomplete") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z"); BitvectorFormula y = bvmgr.makeVariable(bvWidth, "y"); @@ -570,12 +572,14 @@ public void testBVEquality3() throws SolverException, InterruptedException { // exists z . (forall y . z = y && z + 2 > z) // UNSAT because of bv behaviour requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); assume() .withMessage("Yices2 quantifier support is very limited at the moment") .that(solverToUse()) .isNotEqualTo(Solvers.YICES2); + assume() + .withMessage("Quantifier support in SmtInterpol is incomplete") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z"); BitvectorFormula zPlusTwo = diff --git a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java index 07b65a7a05..c7b33b5531 100644 --- a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java @@ -116,6 +116,10 @@ public void forallFloorIsLessThanValueTest() throws SolverException, Interrupted .withMessage("Princees does not support universal quantification over rationals") .that(solverToUse()) .isNotEqualTo(Solvers.PRINCESS); + assume() + .withMessage("Quantifier support in SmtInterpol is incomplete") + .that(solverToUse()) + .isNotEqualTo(Solvers.SMTINTERPOL); RationalFormula v = rmgr.makeVariable("v"); // counterexample: all integers diff --git a/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java b/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java index 64e963b7df..f646b2b7b8 100644 --- a/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java @@ -55,7 +55,7 @@ public void rotateLeftTest() { FunctionDeclarationKind.BV_UREM, FunctionDeclarationKind.BV_LSHR, FunctionDeclarationKind.BV_SUB); - case CVC5, PRINCESS -> + case CVC5, PRINCESS, SMTINTERPOL -> assertThat(functions) .containsExactly( FunctionDeclarationKind.BV_OR, @@ -112,7 +112,7 @@ public void rotateRightTest() { FunctionDeclarationKind.BV_UREM, FunctionDeclarationKind.BV_SHL, FunctionDeclarationKind.BV_SUB); - case CVC5, PRINCESS -> + case CVC5, PRINCESS, SMTINTERPOL -> assertThat(functions) .containsExactly( FunctionDeclarationKind.BV_OR, diff --git a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java index fa6528f32d..7a0e87df0e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java @@ -231,6 +231,9 @@ public void allSatTest_withQuantifier() throws SolverException, InterruptedExcep requireBitvectors(); requireQuantifiers(); + // FIXME SmtInterpol crashes here, report to the developers + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); + assume() .withMessage("solver does only partially support quantifiers") .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 67de75af49..ab564e845b 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -325,7 +325,7 @@ protected final void requireQuantifierElimination() { assume() .withMessage("Solver %s does not support quantifier elimination", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.BOOLECTOR, Solvers.MATHSAT5, Solvers.YICES2, Solvers.BITWUZLA); + .isNoneOf(Solvers.MATHSAT5, Solvers.YICES2, Solvers.BITWUZLA, Solvers.SMTINTERPOL); } /** Skip test if the solver does not support arrays. */ diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java index 30a62ac6d4..9b405e8b18 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIODeclarationsTest.java @@ -185,7 +185,8 @@ 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, Solvers.CVC5).contains(solverToUse())) { + if (EnumSet.of(Solvers.MATHSAT5, Solvers.BITWUZLA, Solvers.CVC5, Solvers.SMTINTERPOL) + .contains(solverToUse())) { BooleanFormula formula = mgr.parse(query); Truth.assertThat(mgr.extractVariables(formula).values()).containsExactly(var); } else { diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index 4c78d4b7c2..246ea679e0 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -362,6 +362,10 @@ public void intTest3_DivModNonLinear() throws SolverException, InterruptedExcept @Test public void intTestBV_DivMod() throws SolverException, InterruptedException { requireBitvectors(); + assume() + .withMessage("SmtInterpol only has limited support for bitvectors") + .that(solver) + .isNotEqualTo(Solvers.SMTINTERPOL); final int bitsize = 8; BitvectorFormula a = bvmgr.makeVariable(bitsize, "int_a"); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index b1b205d3db..43650e4c84 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -320,6 +320,7 @@ public void integerDivisionVisit() { public void integerToBitvectorConversionVisit() { requireIntegers(); requireBitvectors(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); // Yices does not support integer to bitvector conversions assume().that(solver).isNotEqualTo(Solvers.YICES2); @@ -335,6 +336,7 @@ public void integerToBitvectorConversionVisit() { public void bitvectorToIntegerConversionVisit() { requireIntegers(); requireBitvectors(); + assume().that(solver).isNotEqualTo(Solvers.SMTINTERPOL); // Yices does not support integer to bitvector conversions assume().that(solver).isNotEqualTo(Solvers.YICES2); diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 6d1f718fcb..a7e4d6fc7d 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.test; import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.api.FormulaType.BooleanType; import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; @@ -22,6 +23,7 @@ import java.util.function.BiFunction; import java.util.function.Function; import org.junit.Test; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.Formula; @@ -174,6 +176,8 @@ boolean allowInvalidNames() { @CanIgnoreReturnValue private T createVariableWith(Function creator, String name) { + assume().that(!(solver == Solvers.SMTINTERPOL && name.equals("_"))).isTrue(); + if (allowInvalidNames() && !mgr.isValidName(name)) { assertThrows(IllegalArgumentException.class, () -> creator.apply(name)); return null;