From 509567133a56731d994f5afe938cea38f38b01a6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Apr 2026 16:39:37 +0200 Subject: [PATCH 1/9] SmtInterpol: Update to version 2.5-1465 --- lib/ivy.xml | 2 +- .../smtinterpol/FormulaCollectionScript.java | 21 ++++++++--- ...LoggingSmtInterpolInterpolatingProver.java | 2 +- .../SmtInterpolFormulaCreator.java | 36 +++++-------------- .../smtinterpol/SmtInterpolSolverContext.java | 8 ++--- .../java_smt/test/VariableNamesTest.java | 4 +++ 6 files changed, 34 insertions(+), 39 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 03061a6c08..e75fd26ead 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -165,7 +165,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..4a415b9319 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java @@ -70,8 +70,12 @@ 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); - + FunctionSymbol fsym = null; + try { + fsym = theory.getFunction(fun, paramSorts); + } catch (SMTLIBException e) { + // fsym = null + } if (fsym == null) { script.declareFun(fun, paramSorts, resultSort); } else { @@ -89,8 +93,12 @@ public void defineFun(String fun, TermVariable[] params, Sort resultSort, Term d for (int i = 0; i < paramSorts.length; i++) { paramSorts[i] = params[i].getSort(); } - FunctionSymbol fsym = theory.getFunction(fun, paramSorts); - + FunctionSymbol fsym = null; + try { + fsym = theory.getFunction(fun, paramSorts); + } catch (SMTLIBException e) { + // fsym = null + } if (fsym == null) { script.defineFun(fun, params, resultSort, definition); } else { @@ -168,6 +176,11 @@ public Term quantifier(int quantor, TermVariable[] vars, Term body, Term[]... pa return script.quantifier(quantor, vars, body, patterns); } + @Override + public Term lambda(TermVariable[] pTermVariables, Term pTerm) throws SMTLIBException { + return script.lambda(pTermVariables, pTerm); + } + @Override public Term let(TermVariable[] vars, Term[] values, Term body) throws SMTLIBException { return script.let(vars, values, body); 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..44f57fc635 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -55,7 +55,7 @@ private PrintWriter initializeLoggerForInterpolation( for (Map.Entry entry : globalOptions.entrySet()) { writer.println("(set-option %s %s)".formatted(entry.getKey(), entry.getValue())); } - writer.println("(set-logic " + env.getTheory().getLogic().name() + ")"); + writer.println("(set-logic " + env.getTheory().getLogic().getName() + ")"); return writer; } 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..45b31c72b1 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -23,7 +23,6 @@ import de.uni_freiburg.informatik.ultimate.logic.Sort; import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.logic.Theory; -import java.math.BigInteger; import java.util.ArrayList; import java.util.List; import org.sosy_lab.java_smt.api.ArrayFormula; @@ -39,7 +38,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( @@ -99,8 +98,12 @@ 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); - + FunctionSymbol fsym = null; + try { + fsym = environment.getTheory().getFunction(fun, paramSorts); + } catch (SMTLIBException e) { + // fsym = null + } if (fsym == null) { try { environment.declareFun(fun, paramSorts, resultSort); @@ -114,9 +117,6 @@ private FunctionSymbol declareFun(String fun, Sort[] paramSorts, Sort 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); - } return fsym; } } @@ -131,8 +131,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.", @@ -181,25 +179,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(); 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..3526fdbb51 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -140,7 +140,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 +160,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/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; From 764dafe85df7e86eaff429415b5a29914807f58f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Apr 2026 16:48:32 +0200 Subject: [PATCH 2/9] SmtInterpol: Add bitvector theory --- .../SmtInterpolBitvectorFormulaManager.java | 197 ++++++++++++++++++ .../SmtInterpolFormulaCreator.java | 81 ++++++- .../SmtInterpolFormulaManager.java | 3 +- .../smtinterpol/SmtInterpolSolverContext.java | 3 + .../test/ArrayFormulaManagerTest.java | 4 + .../test/BitvectorFormulaManagerTest.java | 1 + src/org/sosy_lab/java_smt/test/ModelTest.java | 27 ++- .../java_smt/test/RotationVisitorTest.java | 4 +- .../test/SolverFormulaIODeclarationsTest.java | 3 +- .../java_smt/test/SolverTheoriesTest.java | 4 + 10 files changed, 313 insertions(+), 14 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolBitvectorFormulaManager.java 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 45b31c72b1..b83c115b9e 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -23,6 +23,7 @@ import de.uni_freiburg.informatik.ultimate.logic.Sort; import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.logic.Theory; +import java.math.BigInteger; import java.util.ArrayList; import java.util.List; import org.sosy_lab.java_smt.api.ArrayFormula; @@ -62,6 +63,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]), @@ -80,8 +83,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 @@ -139,8 +141,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 @@ -162,16 +163,30 @@ 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 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); } @@ -295,6 +310,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; @@ -323,8 +386,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..f553058e4e 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java @@ -46,6 +46,7 @@ class SmtInterpolFormulaManager extends AbstractFormulaManager 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}; }; 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/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/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"); From 646c88b40e9d5650bb35e807f0a8cee138a6b949 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Apr 2026 16:53:43 +0200 Subject: [PATCH 3/9] SmtInterpol: Add quantifier theory --- .../SmtInterpolFormulaCreator.java | 76 ++++++++++++- .../SmtInterpolFormulaManager.java | 3 +- .../SmtInterpolQuantifiedFormulaManager.java | 106 ++++++++++++++++++ .../smtinterpol/SmtInterpolSolverContext.java | 3 + .../java_smt/test/QuantifierManagerTest.java | 12 +- .../test/RationalFormulaManagerTest.java | 4 + .../java_smt/test/SolverAllSatTest.java | 3 + .../java_smt/test/SolverBasedTest0.java | 2 +- 8 files changed, 201 insertions(+), 8 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolQuantifiedFormulaManager.java 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 b83c115b9e..af01dfce3b 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,36 @@ 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.BigInteger; import java.util.ArrayList; 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; @@ -234,15 +245,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.build(); + var newBody = substBoundVariables(newVars, quantified.getSubformula()); + + return visitor.visitQuantifier( + (BooleanFormula) f, + quantifier, + FluentIterable.from(newVars.values()).transform(this::encapsulateWithTypeOf).toList(), + 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.build(), quantified.getSubformula())); + } else { + throw new AssertionError(); + } + } + String getName(Term t) { if (t instanceof ApplicationTerm app && isUF(app)) { return app.getFunction().getName(); 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 f553058e4e..4758185ea2 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java @@ -48,6 +48,7 @@ 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.build(); + 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 bbe48d28ac..7687544bbd 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -127,6 +127,8 @@ public static SmtInterpolSolverContext create( SmtInterpolBitvectorFormulaManager bitvectorTheory = new SmtInterpolBitvectorFormulaManager(creator, booleanTheory); SmtInterpolArrayFormulaManager arrayTheory = new SmtInterpolArrayFormulaManager(creator); + SmtInterpolQuantifiedFormulaManager quantifiedTheory = + new SmtInterpolQuantifiedFormulaManager(creator); SmtInterpolFormulaManager manager = new SmtInterpolFormulaManager( creator, @@ -136,6 +138,7 @@ public static SmtInterpolSolverContext create( rationalTheory, bitvectorTheory, arrayTheory, + quantifiedTheory, logger); return new SmtInterpolSolverContext(manager, pShutdownNotifier, settings); } 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/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. */ From 73954e3d2d7230f8325a3fcb325a9a3fb3701c67 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Apr 2026 16:57:39 +0200 Subject: [PATCH 4/9] SmtInterpol: Better error handling for incomplete theories --- ...LoggingSmtInterpolInterpolatingProver.java | 2 +- .../SmtInterpolAbstractProver.java | 24 +++++++------------ 2 files changed, 9 insertions(+), 17 deletions(-) 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 44f57fc635..e532b7a913 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"); } } }; From 4ae6510bfbb2049ac04d8bfb876f96fbd07adeba Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 9 Apr 2026 10:46:06 +0200 Subject: [PATCH 5/9] SmtInterpol: Fix handling of decimals in the visitor --- .../solvers/smtinterpol/SmtInterpolFormulaCreator.java | 6 ++++++ 1 file changed, 6 insertions(+) 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 af01dfce3b..763f9d5bb4 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -31,6 +31,7 @@ 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.List; @@ -183,6 +184,11 @@ public Object convertValue(Term value) { 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) From 3b0c23a122cd51586386746733f4b60891e99963 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 12 Apr 2026 17:09:18 +0200 Subject: [PATCH 6/9] SmtInterpol: Downgrade to 2.5-1388-ga5a4ab0c Disable tests that use integer/bv conversions from Smtlib 2.7. Support has been added in recently, but 2.5-1388-ga5a4ab0c is too old --- lib/ivy.xml | 2 +- .../solvers/smtinterpol/FormulaCollectionScript.java | 5 ----- .../LoggingSmtInterpolInterpolatingProver.java | 2 +- .../java_smt/test/BitvectorFormulaManagerTest.java | 9 +++++++++ src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 2 ++ 5 files changed, 13 insertions(+), 7 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index e75fd26ead..17fea987d0 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -165,7 +165,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 4a415b9319..5e6a66ecac 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java @@ -176,11 +176,6 @@ public Term quantifier(int quantor, TermVariable[] vars, Term body, Term[]... pa return script.quantifier(quantor, vars, body, patterns); } - @Override - public Term lambda(TermVariable[] pTermVariables, Term pTerm) throws SMTLIBException { - return script.lambda(pTermVariables, pTerm); - } - @Override public Term let(TermVariable[] vars, Term[] values, Term body) throws SMTLIBException { return script.let(vars, values, body); 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 e532b7a913..12a7437fd0 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java @@ -55,7 +55,7 @@ private PrintWriter initializeLoggerForInterpolation( for (Map.Entry entry : globalOptions.entrySet()) { writer.println("(set-option %s %s)".formatted(entry.getKey(), entry.getValue())); } - writer.println("(set-logic " + env.getTheory().getLogic().getName() + ")"); + writer.println("(set-logic " + env.getTheory().getLogic().name() + ")"); return writer; } diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index b3641f7657..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); @@ -585,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/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); From 8f3f43ded796b3f6efea2beb624e6be0f1fd2a9a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 12 Apr 2026 18:58:57 +0200 Subject: [PATCH 7/9] Errorprone --- .../solvers/smtinterpol/SmtInterpolFormulaCreator.java | 6 +++--- .../smtinterpol/SmtInterpolQuantifiedFormulaManager.java | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) 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 763f9d5bb4..502a9f7dca 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -264,13 +264,13 @@ public R visit(FormulaVisitor visitor, Formula f, final Term input) { builder.put(var, makeVariable(var.getSort(), var.getName())); } - var newVars = builder.build(); + var newVars = builder.buildOrThrow(); var newBody = substBoundVariables(newVars, quantified.getSubformula()); return visitor.visitQuantifier( (BooleanFormula) f, quantifier, - FluentIterable.from(newVars.values()).transform(this::encapsulateWithTypeOf).toList(), + transformedImmutableListCopy(newVars.values(), this::encapsulateWithTypeOf), encapsulateBoolean(newBody)); } else { @@ -315,7 +315,7 @@ private Term substBoundVariables(Map pSubst, Term pTerm) { .quantifier( quantified.getQuantifier(), quantified.getVariables(), - substBoundVariables(newSubst.build(), quantified.getSubformula())); + substBoundVariables(newSubst.buildOrThrow(), quantified.getSubformula())); } else { throw new AssertionError(); } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolQuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolQuantifiedFormulaManager.java index 4178eeb2af..371e5a6446 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolQuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolQuantifiedFormulaManager.java @@ -96,7 +96,7 @@ public Term mkQuantifier(Quantifier q, List vars, Term body) { .variable(((ApplicationTerm) var).getFunction().getName(), var.getSort())); } - var newVars = builder.build(); + var newVars = builder.buildOrThrow(); var newBody = substFreeVariables(newVars, body); return formulaCreator From 29da9d44d234adb3f050d8a54a6523ed813bb1a4 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 12 Apr 2026 19:00:39 +0200 Subject: [PATCH 8/9] Checkstyle --- .../java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java | 1 + 1 file changed, 1 insertion(+) 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 4758185ea2..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,6 +40,7 @@ class SmtInterpolFormulaManager extends AbstractFormulaManager Date: Mon, 13 Apr 2026 19:56:56 +0200 Subject: [PATCH 9/9] SmtInterpol: Check for collisions before declaring new function symbols --- .../smtinterpol/FormulaCollectionScript.java | 45 ++++++++++--------- .../SmtInterpolFormulaCreator.java | 29 +++++------- 2 files changed, 35 insertions(+), 39 deletions(-) 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 5e6a66ecac..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,18 +72,18 @@ public LBool assertTerm(Term pTerm) throws SMTLIBException { @Override public void declareFun(String fun, Sort[] paramSorts, Sort resultSort) throws SMTLIBException { - FunctionSymbol fsym = null; - try { - fsym = theory.getFunction(fun, paramSorts); - } catch (SMTLIBException e) { - // fsym = null - } - 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)); } } } @@ -89,22 +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 = null; - try { - fsym = theory.getFunction(fun, paramSorts); - } catch (SMTLIBException e) { - // fsym = null - } - 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/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java index 502a9f7dca..ea12d068d5 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -34,6 +34,7 @@ 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; @@ -112,27 +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 = null; - try { - fsym = environment.getTheory().getFunction(fun, paramSorts); - } catch (SMTLIBException e) { - // fsym = null - } - 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"); + "Function '%s' already declared with a different sort".formatted(fun)); } - return fsym; } + return functions.get(fun); } /**