From d8e3e3f6b30e5a254474cd729f230ae50e748bee Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:14:33 +0200 Subject: [PATCH 01/22] Princess: Remove internal symbols from the model --- .../sosy_lab/java_smt/solvers/princess/PrincessModel.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java index a26011bdde..c1df5497aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -84,7 +84,12 @@ public ImmutableList asList() { // then iterate over the model and generate the assignments ImmutableSet.Builder assignments = ImmutableSet.builder(); for (Map.Entry entry : asJava(interpretation).entrySet()) { - if (!entry.getKey().toString().equals("Rat_denom") && !isAbbrev(abbrevs, entry.getKey())) { + if (!entry.getKey().toString().equals("Rat_denom") + && !isAbbrev(abbrevs, entry.getKey()) + && !(entry.getKey() instanceof IAtom + && ((IAtom) entry.getKey()).pred().name().equals("arrayConstant")) + && !(entry.getKey() instanceof IFunApp + && ((IFunApp) entry.getKey()).fun().name().equals("valueAlmostEverywhere"))) { assignments.addAll(getAssignments(entry.getKey(), entry.getValue(), arrays)); } } From 8f5fef70d32f574b3edd66f03802008c395191e8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:16:08 +0200 Subject: [PATCH 02/22] Princess: Check types when finding a variable in the cache --- .../java_smt/solvers/princess/PrincessEnvironment.java | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index f3f933793e..e6d19b2f75 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -670,7 +670,14 @@ public IExpression makeVariable(Sort type, String varname) { } } else { if (sortedVariablesCache.containsKey(varname)) { - return sortedVariablesCache.get(varname); + ITerm found = sortedVariablesCache.get(varname); + Preconditions.checkArgument( + getFormulaType(found).equals(getFormulaTypeFromSort(type)), + "Can't declare variable \"%s\" with type %s. It has already been declared with type %s", + varname, + getFormulaTypeFromSort(type), + getFormulaType(found)); + return found; } else { ITerm var = api.createConstant(varname, type); addSymbol(var); @@ -683,6 +690,7 @@ public IExpression makeVariable(Sort type, String varname) { /** This function declares a new functionSymbol with the given argument types and result. */ public IFunction declareFun(String name, Sort returnType, List args) { if (functionsCache.containsKey(name)) { + // FIXME Check that the old declaration has the right type return functionsCache.get(name); } else { IFunction funcDecl = From 6c1c55adc89f1917cc4d3e91a4e07cf492da1256 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:20:35 +0200 Subject: [PATCH 03/22] Princess: Use MultipleValueBool for boolean UFs --- .../solvers/princess/PrincessEnvironment.java | 10 ++++++++++ .../solvers/princess/PrincessFormulaCreator.java | 11 ++++++++--- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index e6d19b2f75..4dde88af6c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -22,6 +22,7 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; +import ap.parser.IIntRelation; import ap.parser.IPlus; import ap.parser.ITerm; import ap.parser.ITermITE; @@ -337,6 +338,15 @@ public List parseStringToTerms(String s, PrincessFormulaC IFunction fun = ((IFunApp) var).fun(); functionsCache.put(fun.name(), fun); addFunction(fun); + } else if (var instanceof IIntFormula + && ((IIntFormula) var).rel().equals(IIntRelation.EqZero()) + && ((IIntFormula) var).apply(0) instanceof IFunApp) { + // Functions with return type Bool are wrapped in a predicate as (=0 (uf ...)) + IFunction fun = ((IFunApp) var.apply(0)).fun(); + functionsCache.put(fun.name(), fun); + addFunction(fun); + } else { + throw new IllegalArgumentException(); } } return formulas; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 4dc57e5b38..2dfca5e15e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -639,8 +639,11 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { IIntFormula f = (IIntFormula) input; if (f.rel().equals(IIntRelation.EqZero())) { final Sort sort = Sort$.MODULE$.sortOf(((IIntFormula) input).t()); - if (sort == PrincessEnvironment.BOOL_SORT) { - // this is really a Boolean formula, it has to be UF + if (sort == Sort.MultipleValueBool$.MODULE$) { + // Princess does not allow UFs to have return sort 'Bool' + // Instead, the function returns 'MultiplyValueBool' which is really an integer. The + // predicate (=0 (uf ...)) is then wrapped around the function application to get a + // (boolean) formula return FunctionDeclarationKind.UF; } else if (sort == PrincessEnvironment.INTEGER_SORT) { return FunctionDeclarationKind.EQ_ZERO; @@ -667,7 +670,9 @@ private static boolean isBinaryFunction(IExpression t, Enumeration.Value val) { @Override public PrincessFunctionDeclaration declareUFImpl( String pName, Sort pReturnType, List args) { - return new PrincessIFunctionDeclaration(environment.declareFun(pName, pReturnType, args)); + return new PrincessIFunctionDeclaration( + environment.declareFun( + pName, pReturnType.equals(BOOL_SORT) ? MultipleValueBool$.MODULE$ : pReturnType, args)); } @Override From d347bb81fa67ecca6b91495a527e956a8760b390 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:22:55 +0200 Subject: [PATCH 04/22] Princess: Cache constant array terms --- .../solvers/princess/PrincessEnvironment.java | 43 ++++++++++++------- 1 file changed, 27 insertions(+), 16 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index 4dde88af6c..b764686863 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -34,7 +34,6 @@ import ap.parser.SMTTypes.SMTType; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; -import ap.theories.arrays.ExtArray; import ap.theories.arrays.ExtArray.ArraySort; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.rationals.Rationals$; @@ -54,8 +53,6 @@ import java.io.File; import java.io.IOException; import java.io.StringReader; -import java.lang.reflect.InvocationTargetException; -import java.lang.reflect.Method; import java.nio.file.Path; import java.util.ArrayDeque; import java.util.ArrayList; @@ -177,6 +174,8 @@ class PrincessEnvironment { private final Map functionsCache = new HashMap<>(); + private final Map, Map> constArrayCache = new HashMap<>(); + private final int randomSeed; private final @Nullable PathCounterTemplate basicLogfile; private final ShutdownNotifier shutdownNotifier; @@ -724,20 +723,32 @@ public ITerm makeStore(ITerm array, ITerm index, ITerm value) { return new IFunApp(arraySort.theory().store(), toSeq(args)); } - public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) { - // return new IFunApp(arraySort.theory().const(), elseTerm); // I love Scala! So simple! ;-) - - // Scala uses keywords that are illegal in Java. Thus, we use reflection to access the method. - // TODO we should contact the developers of Princess and ask for a renaming. - final IFunction constArrayOp; - try { - Method constMethod = ExtArray.class.getMethod("const"); - constArrayOp = (IFunction) constMethod.invoke(arraySort.theory()); - } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException exception) { - throw new RuntimeException(exception); - } + void cacheConstArray(ArraySort arraySort, ITerm elseTerm, ITerm constArray) { + constArrayCache.compute( + getFormulaTypeFromSort(arraySort), + (sort, maps) -> { + if (maps == null) { + maps = new HashMap<>(); + } + maps.putIfAbsent(elseTerm, constArray); + return maps; + }); + } - return new IFunApp(constArrayOp, toSeq(ImmutableList.of(elseTerm))); + public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) { + constArrayCache.compute( + getFormulaTypeFromSort(arraySort), + (sort, maps) -> { + if (maps == null) { + maps = new HashMap<>(); + } + maps.computeIfAbsent( + elseTerm, + term -> + new IFunApp(arraySort.theory().constArray(), toSeq(ImmutableList.of(elseTerm)))); + return maps; + }); + return constArrayCache.get(getFormulaTypeFromSort(arraySort)).get(elseTerm); } public boolean hasArrayType(IExpression exp) { From 475b22e9a51ef047e6743dc1353075e47189d8f1 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:25:36 +0200 Subject: [PATCH 05/22] Princess: Refactor formula visitor to better match complex terms Princess will rewrite multiplication/division by introducing epsilon terms, which are not supported by JavaSmt. We use pattern matching to undo the transformation and restore the original formula --- .../PrincessBitvectorFormulaManager.java | 41 +- .../princess/PrincessFormulaCreator.java | 359 +++++++++++++++++- .../princess/PrincessFunctionDeclaration.java | 307 ++++++++++++++- .../PrincessRationalFormulaManager.java | 8 +- 4 files changed, 661 insertions(+), 54 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index 4ea9cf3191..0477b3a32c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java @@ -13,11 +13,10 @@ import ap.parser.ITerm; import ap.theories.bitvectors.ModuloArithmetic$; import ap.types.Sort; -import ap.types.Sort$; -import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; import java.math.BigInteger; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; -import scala.Option; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToIntegerDeclaration; class PrincessBitvectorFormulaManager extends AbstractBitvectorFormulaManager< @@ -137,29 +136,11 @@ protected IExpression makeBitvectorImpl(int pLength, IExpression pIntegerFormula @Override protected IExpression toIntegerFormulaImpl(IExpression pBVFormula, boolean signed) { - final Sort sort = Sort$.MODULE$.sortOf((ITerm) pBVFormula); - final Option bitWidth = PrincessEnvironment.getBitWidth(sort); - Preconditions.checkArgument(bitWidth.isDefined()); - final int size = (Integer) bitWidth.get(); - - // compute range for integer value, - // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15] - final BigInteger min; - final BigInteger max; - if (signed) { - min = BigInteger.ONE.shiftLeft(size - 1).negate(); - max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); - } else { - min = BigInteger.ZERO; - max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE); - } - - ITerm bvInRange = - ModuloArithmetic$.MODULE$.cast2Interval( - IdealInt.apply(min), IdealInt.apply(max), (ITerm) pBVFormula); - - // Princess can not directly convert from BV to INT. However, adding zero helps. Ugly. - return IExpression.i(0).$plus(bvInRange); + var decl = + signed + ? PrincessBitvectorToIntegerDeclaration.SIGNED + : PrincessBitvectorToIntegerDeclaration.UNSIGNED; + return decl.makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pBVFormula)); } @Override @@ -194,10 +175,8 @@ protected IExpression extract(IExpression pNumber, int pMsb, int pLsb) { @Override protected IExpression extend(IExpression pNumber, int pExtensionBits, boolean pSigned) { - if (pSigned) { - return ModuloArithmetic$.MODULE$.sign_extend(pExtensionBits, (ITerm) pNumber); - } else { - return ModuloArithmetic$.MODULE$.zero_extend(pExtensionBits, (ITerm) pNumber); - } + return new PrincessFunctionDeclaration.PrincessBitvectorExtendDeclaration( + pExtensionBits, pSigned) + .makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pNumber)); } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 2dfca5e15e..b6c4cb954a 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -11,11 +11,15 @@ import static com.google.common.base.Preconditions.checkArgument; import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.EXISTS; import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.FORALL; +import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.BOOL_SORT; +import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.INTEGER_SORT; import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toSeq; import static scala.collection.JavaConverters.asJava; import static scala.collection.JavaConverters.asJavaCollection; import ap.basetypes.IdealInt; +import ap.parser.ConstantSubstVisitor; +import ap.parser.ExpressionReplacingVisitor; import ap.parser.IAtom; import ap.parser.IBinFormula; import ap.parser.IBinJunctor; @@ -38,22 +42,29 @@ import ap.parser.ITermITE; import ap.parser.ITimes; import ap.parser.IVariable; +import ap.parser.Rewriter; +import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; import ap.theories.arrays.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; +import ap.theories.nia.GroebnerMultiplication; import ap.theories.nia.GroebnerMultiplication$; import ap.theories.rationals.Rationals; import ap.types.Sort; import ap.types.Sort$; +import ap.types.Sort.MultipleValueBool$; import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Sets; import com.google.common.collect.Table; import java.util.HashMap; import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import java.util.Optional; import java.util.Set; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.ArrayFormula; @@ -70,10 +81,17 @@ import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToBitvectorDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToBooleanDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessByExampleDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessConstArrayDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessEquationDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessIFunctionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessIntegerDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessIntegerModuloDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessModularCongruenceDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessMultiplyDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; import scala.Enumeration; +import scala.collection.JavaConverters; class PrincessFormulaCreator extends FormulaCreator { @@ -82,8 +100,15 @@ class PrincessFormulaCreator // Java-SMT kind private static final Map theoryFunctionKind = new HashMap<>(); private static final Map theoryPredKind = new HashMap<>(); + private static final Set CONSTANT_UFS = ImmutableSet.of("str_cons", "str_empty"); + // Get the symbol for multiplication + private final IFunction symbolMul = GroebnerMultiplication.mul(); + + // We use a list of patterns to match complex operations like division in the visitor + private final List patterns = precompile(); + static { theoryFunctionKind.put(ModuloArithmetic.bv_concat(), FunctionDeclarationKind.BV_CONCAT); theoryFunctionKind.put(ModuloArithmetic.bv_extract(), FunctionDeclarationKind.BV_EXTRACT); @@ -376,34 +401,329 @@ private static boolean isValue(IFunApp pExpr) { return true; } + /** Cast integer terms to rational, if needed. */ + private ITerm toReal(ITerm number) { + return getFormulaType(number).isIntegerType() ? Rationals.int2ring(number) : number; + } + + private static class Pair { + private final A a; + private final B b; + + Pair(A pA, B pB) { + a = pA; + b = pB; + } + + public A getA() { + return a; + } + + public B getB() { + return b; + } + } + + /** Merge two substitutions, returns {@link Optional#empty()} when there is a conflict. */ + private Optional> merge( + Optional> maybeSubst1, Optional> maybeSubst2) { + if (maybeSubst1.isPresent() && maybeSubst2.isPresent()) { + var subst1 = maybeSubst1.get(); + var subst2 = maybeSubst2.get(); + + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (var k : Sets.union(subst1.keySet(), subst2.keySet())) { + if (subst1.containsKey(k)) { + if (subst2.containsKey(k) && !subst1.get(k).equals(subst2.get(k))) { + return Optional.empty(); + } + builder.put(k, subst1.get(k)); + } else { + builder.put(k, subst2.get(k)); + } + } + return Optional.of(builder.build()); + } else { + return Optional.empty(); + } + } + + /** + * Simple term unification. + * + *

Assumes that the left term is more general. Will return {@link Optional#empty()} if the + * terms can't be unified. Otherwise, returns a substitution for the constant symbols in the left + * term. + */ + private Pair>, IExpression> unify( + IExpression t1, IExpression t2) { + if (t1.equals(t2)) { + return new Pair<>(Optional.of(Map.of()), t1); + } else if (t1 instanceof IConstant) { + return new Pair<>(Optional.of(Map.of(((IConstant) t1).c(), t2)), t2); + } else if (t1.getClass().equals(t2.getClass()) && t1.length() == t2.length()) { + // Recursively check the subterms + Optional> subst = Optional.of(ImmutableMap.of()); + ImmutableList.Builder terms = ImmutableList.builder(); + for (var i = 0; i < t1.length(); i++) { + Pair>, IExpression> r = + unify(t1.apply(i), t2.apply(i)); + subst = merge(subst, r.getA()); + + if (subst.isEmpty()) { + return new Pair<>(Optional.empty(), t1); + } + terms.add(r.getB()); + } + + // Check if the left term is equal to the right after the subtrees were unified + IExpression t = t1.update(toSeq(terms.build())); + if (t.equals(t2)) { + return new Pair<>(subst, t2); + } + } + return new Pair<>(Optional.empty(), t1); + } + + /** + * Rewrite terms of the form ((_ ITimes k) b) as (multiply (Expression.i k) b) + * . + * + *

This will later allow us to replace the first argument with a variable + */ + private IExpression rewriteMult(IExpression t) { + return Rewriter.rewrite( + t, + v -> { + if (v instanceof ITimes) { + var times = (ITimes) v; + return new IFunApp( + symbolMul, toSeq(ImmutableList.of(IExpression.i(times.coeff()), times.subterm()))); + } else { + return v; + } + }); + } + + /** + * Rewrite negative integer literals as -1 * a. + * + *

Will skip -1 terms while rewriting + */ + private IExpression rewriteNegated(IExpression t) { + return Rewriter.rewrite( + t, + v -> { + if (v instanceof IIntLit) { + var lit = ((IIntLit) v); + if (!lit.value().isUnit() && lit.value().signum() < 0) { + return new ITimes(IdealInt.apply(-1), IExpression.abs(lit)); + } + } + return v; + }); + } + + /** + * A pattern, consisting of an operation, it's arguments, and the resulting Princess term. + * + *

The princess term will be generalized, and by matching it to a given formula one can invert + * the operation and derive the original arguments. + */ + private static class Pattern { + private final PrincessFunctionDeclaration decl; + private final List args; + private final IExpression term; + + Pattern(PrincessFunctionDeclaration pDecl, List pArgs, IExpression pTerm) { + decl = pDecl; + args = pArgs; + term = pTerm; + } + } + + private Pattern buildPattern(PrincessFunctionDeclaration pDeclaration, List pArgs) { + return buildPattern(pDeclaration, pArgs, false); + } + + /** + * Helper function to build patterns. + * + *

If the last argument is set to true, we will generalize any constant terms in + * the arguments. + */ + private Pattern buildPattern( + PrincessFunctionDeclaration pDeclaration, List pArgs, boolean pFinal) { + var term = rewriteNegated(rewriteMult(pDeclaration.makeApp(environment, pArgs))); + if (pFinal) { + ImmutableList.Builder builder = ImmutableList.builder(); + for (var c : pArgs) { + if (c instanceof IConstant) { + // If the argument is already a variable, just keep it + builder.add(c); + } else if (c instanceof ITimes) { + // If it's a term (c * t), where c is an integer coefficient, and t is another integer + // literal, we replace t in (c * t) with a new variable + // Specifically, this can be used to generalize negative integer constants by first + // shifting the minus sign outside, and then replacing the nested integer term + var times = (ITimes) c; + if (times.apply(0) instanceof IIntLit) { + var newVar = + (ITerm) makeVariable(INTEGER_SORT, "@" + Integer.toUnsignedString(c.hashCode())); + term = ExpressionReplacingVisitor.apply(term, times.apply(0), newVar); + builder.add(new ITimes(times.coeff(), newVar)); + } else { + throw new IllegalArgumentException(); + } + } else { + // If we have an integer constant as argument, replace it with a new variable and + // update the term + var newVar = + (ITerm) makeVariable(INTEGER_SORT, "@" + Integer.toUnsignedString(c.hashCode())); + term = ExpressionReplacingVisitor.apply(term, c, newVar); + builder.add(newVar); + } + } + return new Pattern(pDeclaration, builder.build(), term); + } else { + return new Pattern(pDeclaration, pArgs, term); + } + } + + private List precompile() { + // Define two variable to match integer arguments + ITerm symbolInt1 = (ITerm) makeVariable(PrincessEnvironment.INTEGER_SORT, "@1integer"); + ITerm symbolInt2 = (ITerm) makeVariable(PrincessEnvironment.INTEGER_SORT, "@2integer"); + + // Define two variables for real arguments + ITerm symbolReal1 = (ITerm) makeVariable(PrincessEnvironment.FRACTION_SORT, "@1real"); + ITerm symbolReal2 = (ITerm) makeVariable(PrincessEnvironment.FRACTION_SORT, "@2real"); + + return ImmutableList.of( + // Rational.divide + buildPattern( + PrincessRationalDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolReal1, toReal(symbolInt2)), + true), + buildPattern( + PrincessRationalDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolReal1, symbolReal2)), + // Integer.divide + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(IExpression.i(2), symbolInt2), + true), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2))), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2).unary_$minus())), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3)), + true), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()), + true), + // Integer.modulo + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, ImmutableList.of(symbolInt1, symbolInt2)), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2))), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2).unary_$minus()), + true), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3)), + true), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()), + true), + // Integer.modularCongruence + buildPattern( + PrincessModularCongruenceDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, symbolInt2, IExpression.i(3)), + true)); + } + @SuppressWarnings("deprecation") @Override public R visit(FormulaVisitor visitor, final Formula f, final IExpression input) { - if (input instanceof IIntLit) { + IExpression re = rewriteNegated(rewriteMult(input)); + + // Check if one of the patterns matches + for (Pattern p : patterns) { + Optional> subst = unify(p.term, re).getA(); + + if (subst.isPresent()) { + ImmutableList.Builder args = ImmutableList.builder(); + ImmutableList.Builder> sorts = ImmutableList.builder(); + + for (IExpression arg : p.args) { + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (var entry : subst.get().entrySet()) { + builder.put(entry.getKey(), (ITerm) entry.getValue()); + } + IExpression updated = + ConstantSubstVisitor.apply(arg, JavaConverters.asScala(builder.build())); + updated = + Rewriter.rewrite( + updated, + v -> { + if (v instanceof ITimes) { + var times = (ITimes) v; + if (times.apply(0) instanceof IIntLit) { + var lit = (IIntLit) times.apply(0); + return IExpression.i(times.coeff().$times(lit.value())); + } + } + return v; + }); + + args.add(encapsulateWithTypeOf(updated)); + sorts.add(getFormulaType(updated)); + } + + return visitor.visitFunction( + f, + args.build(), + FunctionDeclarationImpl.of( + p.decl.getName(), p.decl.getKind(), sorts.build(), getFormulaType(f), p.decl)); + } + } + + if (input instanceof IFunApp && isValue((IFunApp) input)) { + // Is it a rational value? + return visitor.visitConstant(f, convertValue(input)); + + } else if (input instanceof IIntLit) { + // Is it an integer value? IdealInt value = ((IIntLit) input).value(); return visitor.visitConstant(f, value.bigIntValue()); } else if (input instanceof IBoolLit) { + // Is it a boolean value? IBoolLit literal = (IBoolLit) input; return visitor.visitConstant(f, literal.value()); - } else if (input instanceof IFunApp && isValue((IFunApp) input)) { - return visitor.visitConstant(f, convertValue(input)); - } else if (input instanceof IQuantified) { + // Is it a quantifier? return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); - } else if (input instanceof IVariable) { - // variable bound by a quantifier - return visitor.visitBoundVariable(f, ((IVariable) input).index()); - } else if (((input instanceof IAtom) && asJavaCollection(((IAtom) input).args()).isEmpty()) || input instanceof IConstant) { // nullary atoms and constant are variables return visitor.visitFreeVariable(f, input.toString()); } else if (input instanceof ITimes) { - // Princess encodes multiplication as "linear coefficient and factor" with arity 1. + // Princess encodes nonlinear multiplication as (coefficient* t), where "coefficient" is + // an integer constant and "t" is the only subterm assert input.length() == 1; ITimes multiplication = (ITimes) input; @@ -498,7 +818,15 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression if (kind == FunctionDeclarationKind.UF) { solverDeclaration = new PrincessIFunctionDeclaration(((IFunApp) input).fun()); } else if (kind == FunctionDeclarationKind.MUL) { - solverDeclaration = PrincessMultiplyDeclaration.INSTANCE; + if (getFormulaType(input.apply(0)).isRationalType()) { + solverDeclaration = PrincessRationalMultiplyDeclaration.INSTANCE; + } else if (getFormulaType(input.apply(0)).isIntegerType()) { + solverDeclaration = PrincessMultiplyDeclaration.INSTANCE; + } else { + throw new IllegalArgumentException(); + } + } else if (kind == FunctionDeclarationKind.CONST) { + solverDeclaration = new PrincessConstArrayDeclaration(environment, (IFunApp) input); } else { solverDeclaration = new PrincessByExampleDeclaration(input); } @@ -607,19 +935,14 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { return FunctionDeclarationKind.CONST; } else if (fun == ModuloArithmetic.mod_cast()) { return FunctionDeclarationKind.OTHER; - } else if (fun == ModuloArithmetic.int_cast()) { - return FunctionDeclarationKind.OTHER; + } else if (((IFunApp) input).fun().equals(Rationals.fromRing())) { + return FunctionDeclarationKind.TO_REAL; } else { return FunctionDeclarationKind.UF; } } else if (input instanceof IAtom) { final Predicate pred = ((IAtom) input).pred(); - final FunctionDeclarationKind theoryKind = theoryPredKind.get(pred); - if (theoryKind != null) { - return theoryKind; - } else { - return FunctionDeclarationKind.UF; - } + return theoryPredKind.getOrDefault(pred, FunctionDeclarationKind.UF); } else if (isBinaryFunction(input, IBinJunctor.And())) { return FunctionDeclarationKind.AND; } else if (isBinaryFunction(input, IBinJunctor.Or())) { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index d7b470236d..14ef5689e7 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -24,14 +24,22 @@ import ap.parser.ITermITE; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; +import ap.theories.arrays.ExtArray.ArraySort; +import ap.theories.bitvectors.ModuloArithmetic$; import ap.theories.nia.GroebnerMultiplication; +import ap.theories.rationals.Rationals; import ap.types.MonoSortedIFunction; import ap.types.Sort; import ap.types.Sort$; +import ap.types.Sort.MultipleValueBool$; import ap.types.SortedConstantTerm; import ap.types.SortedIFunction$; +import com.google.common.base.Preconditions; +import java.math.BigInteger; import java.util.ArrayList; import java.util.List; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; +import scala.Option; import scala.collection.immutable.Seq; /** @@ -44,7 +52,11 @@ abstract class PrincessFunctionDeclaration { private PrincessFunctionDeclaration() {} - abstract IExpression makeApp(PrincessEnvironment environment, List args); + public abstract IExpression makeApp(PrincessEnvironment environment, List args); + + public abstract String getName(); + + public abstract FunctionDeclarationKind getKind(); private abstract static class AbstractDeclaration extends PrincessFunctionDeclaration { @@ -65,7 +77,7 @@ public boolean equals(Object o) { } @Override - abstract IExpression makeApp(PrincessEnvironment env, List args); + public abstract IExpression makeApp(PrincessEnvironment env, List args); @Override public int hashCode() { @@ -112,7 +124,7 @@ public IExpression makeApp(PrincessEnvironment env, List args) { Sort returnType = SortedIFunction$.MODULE$.iResultSort(declarationItem, returnFormula.args()); // boolean term, so we have to use the fun-applier instead of the function itself - if (returnType == PrincessEnvironment.BOOL_SORT) { + if (returnType == MultipleValueBool$.MODULE$) { BooleanFunApplier ap = new BooleanFunApplier(declarationItem); return ap.apply(argsBuf); } else { @@ -149,6 +161,16 @@ private boolean functionTakesRational(Integer index) { } return false; } + + @Override + public String getName() { + return declarationItem.name(); + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.UF; + } } static class PrincessByExampleDeclaration extends AbstractDeclaration { @@ -161,6 +183,40 @@ static class PrincessByExampleDeclaration extends AbstractDeclaration args) { return declarationItem.update(toSeq(args)); } + + @Override + public String getName() { + throw new UnsupportedOperationException(); + } + + @Override + public FunctionDeclarationKind getKind() { + throw new UnsupportedOperationException(); + } + } + + static class PrincessConstArrayDeclaration extends AbstractDeclaration { + + PrincessConstArrayDeclaration(PrincessEnvironment env, IFunApp pArray) { + super((ArraySort) Sort$.MODULE$.sortOf(pArray)); + env.cacheConstArray(declarationItem, pArray.apply(0), pArray); + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return env.makeConstArray(declarationItem, (ITerm) args.get(0)); + } + + @Override + public String getName() { + return "const"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.CONST; + } } static class PrincessBitvectorToBooleanDeclaration extends AbstractDeclaration { @@ -185,6 +241,16 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return new IAtom(declarationItem, toSeq(newArgs)); } + + @Override + public String getName() { + throw new UnsupportedOperationException(); + } + + @Override + public FunctionDeclarationKind getKind() { + throw new UnsupportedOperationException(); + } } static class PrincessBitvectorToBitvectorDeclaration extends AbstractDeclaration { @@ -209,6 +275,16 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return new IFunApp(declarationItem, toSeq(newArgs)); } + + @Override + public String getName() { + throw new UnsupportedOperationException(); + } + + @Override + public FunctionDeclarationKind getKind() { + throw new UnsupportedOperationException(); + } } static class PrincessEquationDeclaration extends PrincessFunctionDeclaration { @@ -222,6 +298,100 @@ public IExpression makeApp(PrincessEnvironment env, List args) { checkArgument(args.size() == 2); return ((ITerm) args.get(0)).$eq$eq$eq((ITerm) args.get(1)); } + + @Override + public String getName() { + return "="; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.EQ; + } + } + + static class PrincessBitvectorToIntegerDeclaration extends PrincessFunctionDeclaration { + static final PrincessBitvectorToIntegerDeclaration SIGNED = + new PrincessBitvectorToIntegerDeclaration(true) {}; + static final PrincessBitvectorToIntegerDeclaration UNSIGNED = + new PrincessBitvectorToIntegerDeclaration(false) {}; + + private final boolean signed; + + private PrincessBitvectorToIntegerDeclaration(boolean pSigned) { + signed = pSigned; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + ITerm bvFormula = (ITerm) args.get(0); + + final Sort sort = Sort$.MODULE$.sortOf(bvFormula); + final Option bitWidth = PrincessEnvironment.getBitWidth(sort); + Preconditions.checkArgument(bitWidth.isDefined()); + final int size = (Integer) bitWidth.get(); + + // compute range for integer value, + // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15] + final BigInteger min; + final BigInteger max; + if (signed) { + min = BigInteger.ONE.shiftLeft(size - 1).negate(); + max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); + } else { + min = BigInteger.ZERO; + max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE); + } + + ITerm bvInRange = + ModuloArithmetic$.MODULE$.cast2Interval( + IdealInt.apply(min), IdealInt.apply(max), bvFormula); + + return ModuloArithmetic$.MODULE$.cast2Int(bvInRange); + } + + @Override + public String getName() { + return signed ? "sbv_to_int" : "ubv_to_int"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.OTHER; + } + } + + static class PrincessBitvectorExtendDeclaration extends PrincessFunctionDeclaration { + private final int extensionBits; + private final boolean signed; + + PrincessBitvectorExtendDeclaration(int pExtensionBits, boolean pSigned) { + extensionBits = pExtensionBits; + signed = pSigned; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + if (signed) { + return ModuloArithmetic$.MODULE$.sign_extend(extensionBits, (ITerm) args.get(0)); + } else { + return ModuloArithmetic$.MODULE$.zero_extend(extensionBits, (ITerm) args.get(0)); + } + } + + @Override + public String getName() { + return signed ? "sign_extend" : "zero_extend"; + } + + @Override + public FunctionDeclarationKind getKind() { + return signed + ? FunctionDeclarationKind.BV_SIGN_EXTENSION + : FunctionDeclarationKind.BV_ZERO_EXTENSION; + } } static class PrincessMultiplyDeclaration extends PrincessFunctionDeclaration { @@ -235,5 +405,136 @@ public IExpression makeApp(PrincessEnvironment env, List args) { checkArgument(args.size() == 2); return GroebnerMultiplication.mult((ITerm) args.get(0), (ITerm) args.get(1)); } + + @Override + public String getName() { + return "mul"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.MUL; + } + } + + static class PrincessRationalMultiplyDeclaration extends PrincessFunctionDeclaration { + + static final PrincessRationalMultiplyDeclaration INSTANCE = + new PrincessRationalMultiplyDeclaration() {}; + + private PrincessRationalMultiplyDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return Rationals.mul((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "mul"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.MUL; + } + } + + static class PrincessRationalDivisionDeclaration extends PrincessFunctionDeclaration { + static final PrincessRationalDivisionDeclaration INSTANCE = + new PrincessRationalDivisionDeclaration() {}; + + private PrincessRationalDivisionDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return Rationals.divWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "div"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.DIV; + } + } + + static class PrincessIntegerDivisionDeclaration extends PrincessFunctionDeclaration { + static final PrincessIntegerDivisionDeclaration INSTANCE = + new PrincessIntegerDivisionDeclaration() {}; + + private PrincessIntegerDivisionDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return GroebnerMultiplication.eDivWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "div"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.DIV; + } + } + + static class PrincessIntegerModuloDeclaration extends PrincessFunctionDeclaration { + static final PrincessIntegerModuloDeclaration INSTANCE = + new PrincessIntegerModuloDeclaration() {}; + + private PrincessIntegerModuloDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return GroebnerMultiplication.eModWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "mod"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.MODULO; + } + } + + static class PrincessModularCongruenceDeclaration extends PrincessFunctionDeclaration { + static final PrincessModularCongruenceDeclaration INSTANCE = + new PrincessModularCongruenceDeclaration() {}; + + private PrincessModularCongruenceDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 3); + var t1 = (ITerm) args.get(0); + var t2 = (ITerm) args.get(1); + var t3 = (ITerm) args.get(2); + return IExpression.ex( + IExpression.eqZero( + t1.$minus(t2).$plus(GroebnerMultiplication.mult(IExpression.v(0), t3)))); + } + + @Override + public String getName() { + return "div"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.OTHER; + } } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java index ba2cbf851c..a16c1f2faa 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -22,6 +22,8 @@ import org.sosy_lab.java_smt.api.NumeralFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.RationalFormulaManager; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; public class PrincessRationalFormulaManager extends PrincessNumeralFormulaManager @@ -130,7 +132,8 @@ protected ITerm subtract(IExpression number1, IExpression number2) { @Override protected IExpression multiply(IExpression number1, IExpression number2) { - return Rationals.mul(toType(number1), toType(number2)); + return PrincessRationalMultiplyDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(toType(number1), toType(number2))); } @Override @@ -138,7 +141,8 @@ protected IExpression divide(IExpression number1, IExpression number2) { // SMT-LIB allows division by zero, so we use divWithSpecialZero here. // If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`, // otherwise it is the normal division - return Rationals.divWithSpecialZero(toType(number1), toType(number2)); + return PrincessRationalDivisionDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(toType(number1), toType(number2))); } @Override From 3f96f61f4ec3ca85ad6a489bda529ee3954ee915 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:59:17 +0200 Subject: [PATCH 06/22] Princess: Apply error-prone patch --- .../solvers/princess/PrincessFormulaCreator.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index b6c4cb954a..d72052c3bf 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -428,8 +428,8 @@ public B getB() { private Optional> merge( Optional> maybeSubst1, Optional> maybeSubst2) { if (maybeSubst1.isPresent() && maybeSubst2.isPresent()) { - var subst1 = maybeSubst1.get(); - var subst2 = maybeSubst2.get(); + var subst1 = maybeSubst1.orElseThrow(); + var subst2 = maybeSubst2.orElseThrow(); ImmutableMap.Builder builder = ImmutableMap.builder(); for (var k : Sets.union(subst1.keySet(), subst2.keySet())) { @@ -442,7 +442,7 @@ private Optional> merge( builder.put(k, subst2.get(k)); } } - return Optional.of(builder.build()); + return Optional.of(builder.buildOrThrow()); } else { return Optional.empty(); } @@ -458,9 +458,9 @@ private Optional> merge( private Pair>, IExpression> unify( IExpression t1, IExpression t2) { if (t1.equals(t2)) { - return new Pair<>(Optional.of(Map.of()), t1); + return new Pair<>(Optional.of(ImmutableMap.of()), t1); } else if (t1 instanceof IConstant) { - return new Pair<>(Optional.of(Map.of(((IConstant) t1).c(), t2)), t2); + return new Pair<>(Optional.of(ImmutableMap.of(((IConstant) t1).c(), t2)), t2); } else if (t1.getClass().equals(t2.getClass()) && t1.length() == t2.length()) { // Recursively check the subterms Optional> subst = Optional.of(ImmutableMap.of()); @@ -667,11 +667,11 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression for (IExpression arg : p.args) { ImmutableMap.Builder builder = ImmutableMap.builder(); - for (var entry : subst.get().entrySet()) { + for (var entry : subst.orElseThrow().entrySet()) { builder.put(entry.getKey(), (ITerm) entry.getValue()); } IExpression updated = - ConstantSubstVisitor.apply(arg, JavaConverters.asScala(builder.build())); + ConstantSubstVisitor.apply(arg, JavaConverters.asScala(builder.buildOrThrow())); updated = Rewriter.rewrite( updated, From a9ad4fbb45cd97cdc711688ee2d9dcf960b874e0 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:12:51 +0200 Subject: [PATCH 07/22] Princess: Add missing case for constant values in the visitor This seems to have gotten lost during the last merge --- .../java_smt/solvers/princess/PrincessFormulaCreator.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index e1f89957e1..0875f4f0fb 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -714,6 +714,9 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression } } + if (isValue(input)) { + return visitor.visitConstant(encapsulateWithTypeOf(input), convertValue(input)); + } if (input instanceof IQuantified) { // Is it a quantifier? return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); From 664842a54a32950b50996d7c172771e701bc7467 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:13:38 +0200 Subject: [PATCH 08/22] Princess: Make methods in Pair package private --- .../java_smt/solvers/princess/PrincessFormulaCreator.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 0875f4f0fb..3280114001 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -431,11 +431,11 @@ private static class Pair { b = pB; } - public A getA() { + A getA() { return a; } - public B getB() { + B getB() { return b; } } From 5c8e6c605ed68bf347f32afdeef7c8df3c63e897 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:14:28 +0200 Subject: [PATCH 09/22] Princess: Add some line breaks in the list of rewrite rules --- .../java_smt/solvers/princess/PrincessFormulaCreator.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 3280114001..561ccc74a7 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -624,6 +624,7 @@ private List precompile() { buildPattern( PrincessRationalDivisionDeclaration.INSTANCE, ImmutableList.of(symbolReal1, symbolReal2)), + // Integer.divide buildPattern( PrincessIntegerDivisionDeclaration.INSTANCE, @@ -643,6 +644,7 @@ private List precompile() { PrincessIntegerDivisionDeclaration.INSTANCE, ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()), true), + // Integer.modulo buildPattern( PrincessIntegerModuloDeclaration.INSTANCE, ImmutableList.of(symbolInt1, symbolInt2)), @@ -661,6 +663,7 @@ private List precompile() { PrincessIntegerModuloDeclaration.INSTANCE, ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()), true), + // Integer.modularCongruence buildPattern( PrincessModularCongruenceDeclaration.INSTANCE, From c72861bf3bd376de6b115c5b7137cd8485b99684 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:16:17 +0200 Subject: [PATCH 10/22] Princess: Add theory symbols < and <= for Rationals --- .../java_smt/solvers/princess/PrincessFormulaCreator.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 561ccc74a7..231f99b4bb 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -144,6 +144,8 @@ class PrincessFormulaCreator theoryPredKind.put(ModuloArithmetic.bv_ule(), FunctionDeclarationKind.BV_ULE); theoryPredKind.put(ModuloArithmetic.bv_slt(), FunctionDeclarationKind.BV_SLT); theoryPredKind.put(ModuloArithmetic.bv_sle(), FunctionDeclarationKind.BV_SLE); + theoryPredKind.put(Rationals.lessThan(), FunctionDeclarationKind.LT); + theoryPredKind.put(Rationals.lessThanOrEqual(), FunctionDeclarationKind.LTE); theoryFunctionKind.put(GroebnerMultiplication$.MODULE$.mul(), FunctionDeclarationKind.MUL); From 80d86c24c98d009994ab04cc04b4248b12ccaa32 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:18:36 +0200 Subject: [PATCH 11/22] Princess: Add special case treatment for bv_extract and bv_concat in getFormulaType() Both operations seem to be "abstract" in Princess and we need to manually calculate the bitsize of the resulting vector --- .../solvers/princess/PrincessEnvironment.java | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index b926c347b9..bc206851de 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -12,6 +12,7 @@ import static scala.collection.JavaConverters.collectionAsScalaIterableConverter; import ap.api.SimpleAPI; +import ap.basetypes.IdealInt; import ap.parameters.GlobalSettings; import ap.parser.BooleanCompactifier; import ap.parser.Environment.EnvironmentException; @@ -22,6 +23,7 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; +import ap.parser.IIntLit; import ap.parser.IIntRelation; import ap.parser.IPlus; import ap.parser.ITerm; @@ -590,6 +592,18 @@ static FormulaType getFormulaType(IExpression pFormula) { FormulaType t1 = getFormulaType(plus.left()); FormulaType t2 = getFormulaType(plus.right()); return mergeFormulaTypes(t1, t2); + } else if (pFormula instanceof IFunApp + && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_extract())) { + IIntLit upper = (IIntLit) pFormula.apply(0); + IIntLit lower = (IIntLit) pFormula.apply(1); + IdealInt bwResult = upper.value().$minus(lower.value()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); + } else if (pFormula instanceof IFunApp + && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) { + IIntLit upper = (IIntLit) pFormula.apply(0); + IIntLit lower = (IIntLit) pFormula.apply(1); + IdealInt bwResult = upper.value().$plus(lower.value()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); } else { final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula); try { From a667cb7d1a1e8166dcc5265baf88f1f334557612 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:19:32 +0200 Subject: [PATCH 12/22] Princess: Move a comment around --- .../java_smt/solvers/princess/PrincessFunctionDeclaration.java | 3 +++ .../solvers/princess/PrincessRationalFormulaManager.java | 3 --- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index 8e38f16a3a..457dccbb87 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -450,6 +450,9 @@ private PrincessRationalDivisionDeclaration() {} @Override public IExpression makeApp(PrincessEnvironment env, List args) { checkArgument(args.size() == 2); + // SMT-LIB allows division by zero, so we use divWithSpecialZero here. + // If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`, + // otherwise it is the normal division return Rationals.divWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java index d0ab624fbc..2f020bd195 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -138,9 +138,6 @@ protected IExpression multiply(IExpression number1, IExpression number2) { @Override protected IExpression divide(IExpression number1, IExpression number2) { - // SMT-LIB allows division by zero, so we use divWithSpecialZero here. - // If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`, - // otherwise it is the normal division return PrincessRationalDivisionDeclaration.INSTANCE.makeApp( getFormulaCreator().getEnv(), ImmutableList.of(toType(number1), toType(number2))); } From 4cfe72a88402557634ad9ff3cfbe34b7b57bdb59 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 14:20:00 +0200 Subject: [PATCH 13/22] Princess: Add a rewrite rule for 'floor' --- .../princess/PrincessFormulaCreator.java | 4 ++++ .../princess/PrincessFunctionDeclaration.java | 23 +++++++++++++++++++ .../PrincessRationalFormulaManager.java | 4 +++- 3 files changed, 30 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 231f99b4bb..02de968e1d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -89,6 +89,7 @@ import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessModularCongruenceDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessMultiplyDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalFloorDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; import scala.Enumeration; import scala.collection.JavaConverters; @@ -627,6 +628,9 @@ private List precompile() { PrincessRationalDivisionDeclaration.INSTANCE, ImmutableList.of(symbolReal1, symbolReal2)), + // Rational.floor + buildPattern(PrincessRationalFloorDeclaration.INSTANCE, ImmutableList.of(symbolReal1)), + // Integer.divide buildPattern( PrincessIntegerDivisionDeclaration.INSTANCE, diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index 457dccbb87..f1edd7cb49 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -467,6 +467,29 @@ public FunctionDeclarationKind getKind() { } } + static class PrincessRationalFloorDeclaration extends PrincessFunctionDeclaration { + static final PrincessRationalFloorDeclaration INSTANCE = + new PrincessRationalFloorDeclaration() {}; + + private PrincessRationalFloorDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return Rationals.ring2int((ITerm) args.get(0)); + } + + @Override + public String getName() { + return "floor"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.FLOOR; + } + } + static class PrincessIntegerDivisionDeclaration extends PrincessFunctionDeclaration { static final PrincessIntegerDivisionDeclaration INSTANCE = new PrincessIntegerDivisionDeclaration() {}; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java index 2f020bd195..33da542bce 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -23,6 +23,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalFloorDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; public class PrincessRationalFormulaManager @@ -112,7 +113,8 @@ protected ITerm toType(IExpression param) { @Override protected IExpression floor(IExpression number) { - return Rationals.ring2int((ITerm) number); + return PrincessRationalFloorDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(number)); } @Override From 0df66757fa6395219c9d2d677826c5ce4b80e981 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 15:32:14 +0200 Subject: [PATCH 14/22] Princess: Fix 80d86c24c98d009994ab04cc04b4248b12ccaa32 We need to add 1 to the bitvector size for bv_extract. The lower bit is included --- .../sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index bc206851de..c0409b99ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -597,7 +597,7 @@ static FormulaType getFormulaType(IExpression pFormula) { IIntLit upper = (IIntLit) pFormula.apply(0); IIntLit lower = (IIntLit) pFormula.apply(1); IdealInt bwResult = upper.value().$minus(lower.value()); - return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue() + 1); } else if (pFormula instanceof IFunApp && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) { IIntLit upper = (IIntLit) pFormula.apply(0); From 6fd1409fa737b024b5e4f06fef4d9c4ed4a220f6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:20:46 +0100 Subject: [PATCH 15/22] Princess: Avoid creating an extra "" term in str.concat --- .../solvers/princess/PrincessStringFormulaManager.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java index 1ebd1496bc..0e4f39b8f1 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java @@ -87,12 +87,12 @@ protected ITerm length(IExpression pParam) { @Override protected ITerm concatImpl(List parts) { - ITerm result = (ITerm) makeStringImpl(""); - for (IExpression expr : parts) { + ITerm result = (ITerm) parts.get(0); + for (int i = 1; i < parts.size(); i++) { result = new IFunApp( PrincessEnvironment.stringTheory.str_$plus$plus(), - PrincessEnvironment.toSeq(ImmutableList.of(result, (ITerm) expr))); + PrincessEnvironment.toSeq(ImmutableList.of(result, (ITerm) parts.get(i)))); } return result; } From edb292fbeb463abdeef925af51b7000016f7c605 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:24:47 +0100 Subject: [PATCH 16/22] Princess: Add a rewrite rule for str.range --- .../princess/PrincessFormulaCreator.java | 10 ++++- .../princess/PrincessFunctionDeclaration.java | 40 +++++++++++++++++++ .../PrincessStringFormulaManager.java | 19 ++------- 3 files changed, 52 insertions(+), 17 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 02de968e1d..2f1cd842c8 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -91,6 +91,7 @@ import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalFloorDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessStringRangeDeclaration; import scala.Enumeration; import scala.collection.JavaConverters; @@ -674,7 +675,14 @@ private List precompile() { buildPattern( PrincessModularCongruenceDeclaration.INSTANCE, ImmutableList.of(symbolInt1, symbolInt2, IExpression.i(3)), - true)); + true), + + // String.range + buildPattern( + PrincessStringRangeDeclaration.INSTANCE, + ImmutableList.of( + makeVariable(getStringType(), "@1Str"), makeVariable(getStringType(), "@2Str")), + false)); } @SuppressWarnings("deprecation") diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index f1edd7cb49..e384adce46 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -9,10 +9,13 @@ package org.sosy_lab.java_smt.solvers.princess; import static com.google.common.base.Preconditions.checkArgument; +import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq; import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toSeq; import ap.basetypes.IdealInt; import ap.parser.IAtom; +import ap.parser.IBinFormula; +import ap.parser.IBinJunctor; import ap.parser.IConstant; import ap.parser.IExpression; import ap.parser.IExpression.BooleanFunApplier; @@ -563,4 +566,41 @@ public FunctionDeclarationKind getKind() { return FunctionDeclarationKind.OTHER; } } + + static class PrincessStringRangeDeclaration extends PrincessFunctionDeclaration { + static final PrincessStringRangeDeclaration INSTANCE = new PrincessStringRangeDeclaration() {}; + + private PrincessStringRangeDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + // Precondition: Both bounds must be single character Strings + // Princess already checks that the lower bound is smaller than the upper bound and returns + // the empty language otherwise. + ITerm one = new IIntLit(IdealInt.apply(1)); + IFormula cond = + new IBinFormula( + IBinJunctor.And(), + new IFunApp(PrincessEnvironment.stringTheory.str_len(), toITermSeq(args.get(0))) + .$eq$eq$eq(one), + new IFunApp(PrincessEnvironment.stringTheory.str_len(), toITermSeq(args.get(1))) + .$eq$eq$eq(one)); + return new ITermITE( + cond, + new IFunApp( + PrincessEnvironment.stringTheory.re_range(), toITermSeq(args.get(0), args.get(1))), + new IFunApp(PrincessEnvironment.stringTheory.re_none(), toITermSeq())); + } + + @Override + public String getName() { + return "range"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.RE_RANGE; + } + } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java index 0e4f39b8f1..51cffbcfe7 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java @@ -11,16 +11,11 @@ import static com.google.common.base.Preconditions.checkArgument; import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq; -import ap.basetypes.IdealInt; import ap.parser.IAtom; -import ap.parser.IBinFormula; -import ap.parser.IBinJunctor; import ap.parser.IExpression; import ap.parser.IFormula; import ap.parser.IFunApp; -import ap.parser.IIntLit; import ap.parser.ITerm; -import ap.parser.ITermITE; import ap.types.Sort; import com.google.common.collect.ImmutableList; import java.util.List; @@ -170,17 +165,9 @@ protected IExpression allCharImpl() { @Override protected ITerm range(IExpression start, IExpression end) { - // Precondition: Both bounds must be single character Strings - // Princess already checks that the lower bound is smaller than the upper bound and returns the - // empty language otherwise. - ITerm one = new IIntLit(IdealInt.apply(1)); - IFormula cond = - new IBinFormula( - IBinJunctor.And(), length(start).$eq$eq$eq(one), length(end).$eq$eq$eq(one)); - return new ITermITE( - cond, - new IFunApp(PrincessEnvironment.stringTheory.re_range(), toITermSeq(start, end)), - noneImpl()); + return (ITerm) + PrincessFunctionDeclaration.PrincessStringRangeDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(start, end)); } @Override From 65a9af94c64bcca098bd415ee83736443bffd8a6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:25:40 +0100 Subject: [PATCH 17/22] Princess: Add abbrev symbols to the variable cache --- .../princess/PrincessAbstractProver.java | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index 431fddc86a..b5949f1eed 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -33,9 +33,11 @@ import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap; import org.sosy_lab.common.collect.PersistentMap; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; import org.sosy_lab.java_smt.basicimpl.CachingModel; import scala.Enumeration.Value; @@ -100,8 +102,20 @@ protected int addConstraint0(BooleanFormula constraint) { partitions.push(partitions.pop().putAndCopy(formulaId, constraint)); api.setPartitionNumber(formulaId); - final IFormula t = (IFormula) mgr.extractInfo(constraint); - api.addAssertion(api.abbrevSharedExpressions(t, creator.getEnv().getMinAtomsForAbbreviation())); + var abbrev = + api.abbrevSharedExpressions( + (IFormula) mgr.extractInfo(constraint), creator.getEnv().getMinAtomsForAbbreviation()); + var rebuild = + mgr.transformRecursively( + creator.encapsulateBoolean(abbrev), + new FormulaTransformationVisitor(mgr) { + @Override + public Formula visitFreeVariable(Formula f, String name) { + // Add abbrev symbols to variable cache + return mgr.makeVariable(creator.getFormulaType(f), name); + } + }); + api.addAssertion((IFormula) mgr.extractInfo(rebuild)); return formulaId; } From 158edbdc95dc2b42ed5052b3e47610757f097836 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:27:19 +0100 Subject: [PATCH 18/22] Princess: Undo "Times" to "Mul" rewrite while substituting patterns for the formula visitor --- .../java_smt/solvers/princess/PrincessFormulaCreator.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 2f1cd842c8..fadebfd6c7 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -709,6 +709,13 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression Rewriter.rewrite( updated, v -> { + if (v instanceof IFunApp) { + var app = (IFunApp) v; + if (app.fun().name().equals("mul") && app.apply(0) instanceof IIntLit) { + var factor = (IIntLit) app.apply(0); + return new ITimes(factor.value(), app.apply(1)); + } + } if (v instanceof ITimes) { var times = (ITimes) v; if (times.apply(0) instanceof IIntLit) { From f126120406f51d22586d9b79abdf1ac16b7f15f6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:31:20 +0100 Subject: [PATCH 19/22] Princess: Add special case handling for several BV terms with indices in the formula visitor --- .../PrincessBitvectorFormulaManager.java | 3 +- .../solvers/princess/PrincessEnvironment.java | 4 +- .../princess/PrincessFormulaCreator.java | 154 +++++++++++++++++- .../princess/PrincessFunctionDeclaration.java | 90 ++++++++-- 4 files changed, 228 insertions(+), 23 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index 0477b3a32c..e1b8031472 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java @@ -131,7 +131,8 @@ protected IExpression makeBitvectorImpl(int pLength, BigInteger pI) { @Override protected IExpression makeBitvectorImpl(int pLength, IExpression pIntegerFormula) { - return ModuloArithmetic$.MODULE$.cast2UnsignedBV(pLength, (ITerm) pIntegerFormula); + return new PrincessFunctionDeclaration.PrincessBitvectorFromIntegerDeclaration(pLength) + .makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pIntegerFormula)); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index cae4bf0926..db432c9af1 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -577,8 +577,8 @@ static FormulaType getFormulaType(IExpression pFormula) { && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_extract())) { IIntLit upper = (IIntLit) pFormula.apply(0); IIntLit lower = (IIntLit) pFormula.apply(1); - IdealInt bwResult = upper.value().$minus(lower.value()); - return FormulaType.getBitvectorTypeWithSize(bwResult.intValue() + 1); + IdealInt bwResult = upper.value().$minus(lower.value()).$plus(IdealInt.ONE()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); } else if (pFormula instanceof IFunApp && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) { IIntLit upper = (IIntLit) pFormula.apply(0); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index fadebfd6c7..50774ad92b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -47,6 +47,8 @@ import ap.terfor.preds.Predicate; import ap.theories.arrays.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; +import ap.theories.bitvectors.ModuloArithmetic$; +import ap.theories.bitvectors.ModuloArithmetic.ModSort; import ap.theories.nia.GroebnerMultiplication; import ap.theories.nia.GroebnerMultiplication$; import ap.theories.rationals.Rationals; @@ -78,8 +80,10 @@ 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; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorFromIntegerDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToBitvectorDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToBooleanDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToIntegerDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessByExampleDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessConstArrayDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessEquationDeclaration; @@ -739,9 +743,151 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression } if (isValue(input)) { - return visitor.visitConstant(encapsulateWithTypeOf(input), convertValue(input)); - } - if (input instanceof IQuantified) { + return visitor.visitConstant(f, convertValue(input)); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic$.MODULE$.int_cast())) { + // Is it a cast from bv to integer? + var arg = (ITerm) input.apply(0); + var sort = (ModSort) Sort.sortOf(arg); + var kind = + sort.lower().isZero() + ? FunctionDeclarationKind.UBV_TO_INT + : FunctionDeclarationKind.SBV_TO_INT; + if (kind == FunctionDeclarationKind.SBV_TO_INT) { + arg = (ITerm) arg.apply(2); + } + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(PrincessEnvironment.getFormulaType(arg)), + FormulaType.IntegerType, + kind == FunctionDeclarationKind.SBV_TO_INT + ? PrincessBitvectorToIntegerDeclaration.SIGNED + : PrincessBitvectorToIntegerDeclaration.UNSIGNED)); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic$.MODULE$.zero_extend())) { + // Is it zero_extend? + var kind = FunctionDeclarationKind.BV_ZERO_EXTENSION; + var p1 = (IIntLit) input.apply(0); + var p2 = (IIntLit) input.apply(1); + var arg = input.apply(2); + var extend = p2.value().intValue(); + var declaration = + new PrincessFunctionDeclaration.PrincessBitvectorExtendDeclaration(extend, false); + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(getFormulaType(arg)), + FormulaType.getBitvectorTypeWithSize(p1.value().$plus(p2.value()).intValue()), + declaration)); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.mod_cast()) + && input.apply(2) instanceof IFunApp + && ((IFunApp) input.apply(2)).fun().equals(ModuloArithmetic.mod_cast())) { + // Is it sign_extend? + var app1 = (IFunApp) input; + var lower1 = (IIntLit) app1.apply(0); + var upper1 = (IIntLit) app1.apply(1); + var arg1 = app1.apply(2); + if (!lower1.value().isZero()) { + throw new AssertionError(); + } + var size1 = upper1.value().getHighestSetBit() + 1; + + var app2 = (IFunApp) arg1; + var lower2 = (IIntLit) app2.apply(0); + var upper2 = (IIntLit) app2.apply(1); + var arg2 = app2.apply(2); + if (lower2.value().isZero()) { + throw new AssertionError(); + } + var size2 = upper2.value().$minus(lower2.value()).getHighestSetBit() + 1; + var size = size1 - size2; + var declaration = + new PrincessFunctionDeclaration.PrincessBitvectorExtendDeclaration(size, true); + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg2)), + FunctionDeclarationImpl.of( + declaration.getKind().toString(), + declaration.getKind(), + ImmutableList.of(FormulaType.getBitvectorTypeWithSize(size2)), + FormulaType.getBitvectorTypeWithSize(size1), + declaration)); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.mod_cast())) { + // Is it int_to_bv? + var kind = FunctionDeclarationKind.INT_TO_BV; + var app = (IFunApp) input; + var lower = (IIntLit) app.apply(0); + var upper = (IIntLit) app.apply(1); + var arg = app.apply(2); + if (!lower.value().isZero()) { + throw new AssertionError(); + } + var size = upper.value().getHighestSetBit() + 1; + var declaration = new PrincessBitvectorFromIntegerDeclaration(size); + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(FormulaType.IntegerType), + FormulaType.getBitvectorTypeWithSize(size), + declaration)); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.bv_extract())) { + // Is it extract? + var kind = FunctionDeclarationKind.BV_EXTRACT; + var upper = ((IIntLit) input.apply(0)).value().intValue(); + var lower = ((IIntLit) input.apply(1)).value().intValue(); + var arg = input.apply(2); + var argType = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg); + + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(argType), + FormulaType.getBitvectorTypeWithSize(upper - lower + 1), + new PrincessFunctionDeclaration.PrincessBitvectorExtractDeclaration(upper, lower))); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.bv_concat())) { + // Is it concat? + var kind = FunctionDeclarationKind.BV_CONCAT; + var size1 = ((IIntLit) input.apply(0)).value().intValue(); + var size2 = ((IIntLit) input.apply(1)).value().intValue(); + var arg1 = input.apply(2); + var arg2 = input.apply(3); + var arg1Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg1); + var arg2Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg2); + + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg1), encapsulateWithTypeOf(arg2)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(arg1Type, arg2Type), + FormulaType.getBitvectorTypeWithSize(size1 + size2), + new PrincessFunctionDeclaration.PrincessBitvectorConcatDeclaration())); + + } else if (input instanceof IQuantified) { // Is it a quantifier? return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); @@ -949,7 +1095,7 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { } else if (ExtArray.Const$.MODULE$.unapply(fun).isDefined()) { return FunctionDeclarationKind.CONST; } else if (fun == ModuloArithmetic.mod_cast()) { - return FunctionDeclarationKind.OTHER; + return FunctionDeclarationKind.INT_TO_BV; } else if (((IFunApp) input).fun().equals(Rationals.fromRing())) { return FunctionDeclarationKind.TO_REAL; } else { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index e384adce46..bb4d98db93 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -313,6 +313,30 @@ public FunctionDeclarationKind getKind() { } } + static class PrincessBitvectorFromIntegerDeclaration extends PrincessFunctionDeclaration { + private final int bitwidth; + + public PrincessBitvectorFromIntegerDeclaration(int pBitwidth) { + bitwidth = pBitwidth; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return ModuloArithmetic$.MODULE$.cast2UnsignedBV(bitwidth, (ITerm) args.get(0)); + } + + @Override + public String getName() { + return "int_to_bv"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.INT_TO_BV; + } + } + static class PrincessBitvectorToIntegerDeclaration extends PrincessFunctionDeclaration { static final PrincessBitvectorToIntegerDeclaration SIGNED = new PrincessBitvectorToIntegerDeclaration(true) {}; @@ -335,23 +359,10 @@ public IExpression makeApp(PrincessEnvironment env, List args) { Preconditions.checkArgument(bitWidth.isDefined()); final int size = (Integer) bitWidth.get(); - // compute range for integer value, - // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15] - final BigInteger min; - final BigInteger max; if (signed) { - min = BigInteger.ONE.shiftLeft(size - 1).negate(); - max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); - } else { - min = BigInteger.ZERO; - max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE); + bvFormula = ModuloArithmetic$.MODULE$.cast2SignedBV(size, bvFormula); } - - ITerm bvInRange = - ModuloArithmetic$.MODULE$.cast2Interval( - IdealInt.apply(min), IdealInt.apply(max), bvFormula); - - return ModuloArithmetic$.MODULE$.cast2Int(bvInRange); + return ModuloArithmetic$.MODULE$.cast2Int(bvFormula); } @Override @@ -361,7 +372,7 @@ public String getName() { @Override public FunctionDeclarationKind getKind() { - return FunctionDeclarationKind.OTHER; + return signed ? FunctionDeclarationKind.SBV_TO_INT : FunctionDeclarationKind.UBV_TO_INT; } } @@ -567,6 +578,53 @@ public FunctionDeclarationKind getKind() { } } + static class PrincessBitvectorExtractDeclaration extends PrincessFunctionDeclaration { + private final int upper; + private final int lower; + + PrincessBitvectorExtractDeclaration(int pUpper, int pLower) { + upper = pUpper; + lower = pLower; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return ModuloArithmetic$.MODULE$.extract(upper, lower, (ITerm) args.get(0)); + } + + @Override + public String getName() { + return "extract"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.BV_EXTRACT; + } + } + + static class PrincessBitvectorConcatDeclaration extends PrincessFunctionDeclaration { + + PrincessBitvectorConcatDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return ModuloArithmetic$.MODULE$.concat((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "concat"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.BV_CONCAT; + } + } + static class PrincessStringRangeDeclaration extends PrincessFunctionDeclaration { static final PrincessStringRangeDeclaration INSTANCE = new PrincessStringRangeDeclaration() {}; From 71e1dc0625696135531c9a18d82cbe94fe35ac3a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:41:02 +0100 Subject: [PATCH 20/22] Princess: Always rewrite (= intTerm 0) to (=0 intTerm) Princess will occasionally return terms like (= term 0), even thought this isn't the canonical representation. This causes problems later as "(= term 0)" != "(=0 term)", even though the two formulas represent the same term --- .../princess/PrincessFormulaCreator.java | 20 ++++++++++++--- .../princess/PrincessFormulaManager.java | 25 ++++++++++++++++--- .../princess/PrincessFunctionDeclaration.java | 9 +++++-- .../solvers/princess/PrincessModel.java | 23 +++++++++-------- .../PrincessNumeralFormulaManager.java | 6 ++++- 5 files changed, 63 insertions(+), 20 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 50774ad92b..ee9f3a206c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -957,6 +957,22 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression return visit(visitor, f, ((IIntFormula) input).t()); } + if (kind == FunctionDeclarationKind.EQ_ZERO) { + // Rewrite EQ_ZERO(num) as EQ(num,0) for the visitor + var term = (IIntFormula) input; + var decl = PrincessEquationDeclaration.INSTANCE; + return visitor.visitFunction( + f, + ImmutableList.of( + encapsulateWithTypeOf(term.apply(0)), encapsulateWithTypeOf(IExpression.i(0))), + FunctionDeclarationImpl.of( + decl.getName(), + decl.getKind(), + ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType), + FormulaType.BooleanType, + PrincessEquationDeclaration.INSTANCE)); + } + ImmutableList.Builder args = ImmutableList.builder(); ImmutableList.Builder> argTypes = ImmutableList.builder(); int arity = input.length(); @@ -1129,10 +1145,8 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { // predicate (=0 (uf ...)) is then wrapped around the function application to get a // (boolean) formula return FunctionDeclarationKind.UF; - } else if (sort == PrincessEnvironment.INTEGER_SORT) { - return FunctionDeclarationKind.EQ_ZERO; } else { - return FunctionDeclarationKind.EQ; + return FunctionDeclarationKind.EQ_ZERO; } } else if (f.rel().equals(IIntRelation.GeqZero())) { return FunctionDeclarationKind.GTE_ZERO; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java index 98f7f60f31..9686a15cb2 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java @@ -10,9 +10,12 @@ import ap.parser.IBinFormula; import ap.parser.IBinJunctor; +import ap.parser.IEquation; import ap.parser.IExpression; import ap.parser.IFormula; +import ap.parser.IIntLit; import ap.parser.ITerm; +import ap.parser.Rewriter; import ap.types.Sort; import com.google.common.base.Preconditions; import java.io.IOException; @@ -59,11 +62,13 @@ BooleanFormula encapsulateBooleanFormula(IExpression t) { } @Override - protected IExpression equalImpl(IExpression pArg1, IExpression pArgs) { + protected IExpression equalImpl(IExpression pArg1, IExpression pArg2) { if (pArg1 instanceof IFormula) { - return new IBinFormula(IBinJunctor.Eqv(), (IFormula) pArg1, (IFormula) pArgs); + return new IBinFormula(IBinJunctor.Eqv(), (IFormula) pArg1, (IFormula) pArg2); + } else if (pArg2 instanceof IIntLit && ((IIntLit) pArg2).value().isZero()) { + return IExpression.eqZero((ITerm) pArg1); } else { - return ((ITerm) pArg1).$eq$eq$eq((ITerm) pArgs); + return ((ITerm) pArg1).$eq$eq$eq((ITerm) pArg2); } } @@ -74,7 +79,19 @@ public IExpression parseImpl(String pS) throws IllegalArgumentException { formulas.size() == 1, "parsing expects exactly one asserted term, but got %s terms", formulas.size()); - return formulas.get(0); + // Rewrite (= term 0) to (=0 term) + return Rewriter.rewrite( + formulas.get(0), + term -> { + if (term instanceof IEquation) { + var equation = (IEquation) term; + if (equation.right() instanceof IIntLit + && ((IIntLit) equation.right()).value().isZero()) { + return IExpression.eqZero(equation.left()); + } + } + return term; + }); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index bb4d98db93..965f2048b4 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -38,7 +38,6 @@ import ap.types.SortedConstantTerm; import ap.types.SortedIFunction$; import com.google.common.base.Preconditions; -import java.math.BigInteger; import java.util.ArrayList; import java.util.List; import org.sosy_lab.java_smt.api.FunctionDeclarationKind; @@ -299,7 +298,13 @@ private PrincessEquationDeclaration() {} @Override public IExpression makeApp(PrincessEnvironment env, List args) { checkArgument(args.size() == 2); - return ((ITerm) args.get(0)).$eq$eq$eq((ITerm) args.get(1)); + var left = (ITerm) args.get(0); + var right = (ITerm) args.get(1); + if (right instanceof IIntLit && ((IIntLit) right).value().isZero()) { + return IExpression.eqZero(left); + } else { + return left.$eq$eq$eq(right); + } } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java index 3dddd50534..feb69a2a1f 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -22,6 +22,7 @@ import ap.parser.IFormula; import ap.parser.IFunApp; import ap.parser.IFunction; +import ap.parser.IIntLit; import ap.parser.ITerm; import ap.terfor.preds.Predicate; import ap.theories.arrays.ExtArray; @@ -68,12 +69,7 @@ public ImmutableList asList() { // then iterate over the model and generate the assignments ImmutableSet.Builder assignments = ImmutableSet.builder(); for (Map.Entry entry : asJava(interpretation).entrySet()) { - if (!entry.getKey().toString().equals("Rat_denom") - && !isAbbrev(abbrevs, entry.getKey()) - && !(entry.getKey() instanceof IAtom - && ((IAtom) entry.getKey()).pred().name().equals("arrayConstant")) - && !(entry.getKey() instanceof IFunApp - && ((IFunApp) entry.getKey()).fun().name().equals("valueAlmostEverywhere"))) { + if (!entry.getKey().toString().equals("Rat_denom") && !isAbbrev(abbrevs, entry.getKey())) { assignments.addAll(getAssignments(entry.getKey(), entry.getValue())); } } @@ -84,6 +80,14 @@ private boolean isAbbrev(Set abbrevs, IExpression var) { return var instanceof IAtom && abbrevs.contains(((IAtom) var).pred()); } + private IFormula makeEquality(ITerm key, ITerm value) { + if (value instanceof IIntLit && ((IIntLit) value).value().isZero()) { + return IExpression.eqZero(key); + } else { + return key.$eq$eq$eq(value); + } + } + private Collection getAssignments(IExpression key, IExpression value) { // first check array-access. @@ -112,7 +116,7 @@ private Collection getAssignments(IExpression key, IExpression } else if (key instanceof IConstant) { name = key.toString(); - fAssignment = ((IConstant) key).$eq$eq$eq((ITerm) value); + fAssignment = makeEquality((IConstant) key, (ITerm) value); } else if (key instanceof IFunApp) { IFunApp cKey = (IFunApp) key; @@ -125,7 +129,7 @@ private Collection getAssignments(IExpression key, IExpression argumentInterpretations.add(creator.convertValue(arg)); } name = cKey.fun().name(); - fAssignment = ((ITerm) key).$eq$eq$eq((ITerm) value); + fAssignment = makeEquality((ITerm) key, (ITerm) value); } else { throw new AssertionError( @@ -196,8 +200,7 @@ private Collection buildArrayAssignments(ITerm arraySymbol, IFu new ValueAssignment( creator.encapsulateWithTypeOf(select), creator.encapsulateWithTypeOf(element), - creator.encapsulateBoolean( - ap.parser.IExpression.Eq$.MODULE$.apply(select, element)), + creator.encapsulateBoolean(makeEquality(select, element)), getVar(arraySymbol), creator.convertValue(element), transformedImmutableListCopy(getArrayIndices(select), this::evaluateImpl))); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java index a73fbaee79..8201a97c66 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java @@ -37,7 +37,11 @@ abstract class PrincessNumeralFormulaManager< @Override protected IFormula equal(IExpression pNumber1, IExpression pNumber2) { - return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2); + if (pNumber2.equals(IExpression.i(0))) { + return IExpression.eqZero((ITerm) pNumber1); + } else { + return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2); + } } @Override From 6be1701627259d792f695b397abbc4cd8c72e26e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:44:00 +0100 Subject: [PATCH 21/22] Princess: If interpolation fails, repeat sat-check and then interpolate again Princess sometimes does not have a proof, even though the solver stack should not have changed. Repeating the sat-check generates a new proof, and interpolation may then succeed --- .../princess/PrincessInterpolatingProver.java | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java index f29354ae77..dd1a13243b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.princess; import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkState; import static scala.collection.JavaConverters.asJava; import static scala.collection.JavaConverters.asScala; @@ -91,7 +92,7 @@ public List getSeqInterpolants( } // do the hard work - final Seq itps; + Seq itps; try { itps = api.getInterpolants(args.toSeq(), api.getInterpolants$default$2()); } catch (StackOverflowError e) { @@ -100,6 +101,17 @@ public List getSeqInterpolants( // so we can do the same for getInterpolants(). throw new SolverException( "Princess ran out of stack memory, try increasing the stack size.", e); + } catch (NullPointerException npe) { + try { + checkState(isUnsat(), "Illegal solver state"); + itps = api.getInterpolants(args.toSeq(), api.getInterpolants$default$2()); + } catch (InterruptedException ie) { + Thread.currentThread().interrupt(); + throw new SolverException("Thread was interrupted", ie); + } catch (StackOverflowError e) { + throw new SolverException( + "Princess ran out of stack memory, try increasing the stack size.", e); + } } assert itps.length() == pPartitions.size() - 1 From 7262b51b6d60406e5db31bab2b6550474321e112 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 27 Dec 2025 12:50:13 +0100 Subject: [PATCH 22/22] Princess: Rewrite interpolants to work around some issues in Princess --- .../princess/PrincessInterpolatingProver.java | 123 +++++++++++++++++- 1 file changed, 121 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java index dd1a13243b..3fbd9ef5c1 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java @@ -14,9 +14,26 @@ import static scala.collection.JavaConverters.asScala; import ap.api.SimpleAPI; +import ap.basetypes.IdealInt; import ap.basetypes.Tree; +import ap.parser.BooleanCompactifier; import ap.parser.IBoolLit; +import ap.parser.IEquation; +import ap.parser.IExpression; import ap.parser.IFormula; +import ap.parser.IFunApp; +import ap.parser.IIntFormula; +import ap.parser.IIntLit; +import ap.parser.IIntRelation; +import ap.parser.IPlus; +import ap.parser.ISortedQuantified; +import ap.parser.ISortedVariable; +import ap.parser.ITimes; +import ap.parser.PartialEvaluator; +import ap.parser.Rewriter; +import ap.theories.bitvectors.ModuloArithmetic; +import ap.types.Sort; +import ap.types.Sort.Integer$; import com.google.common.base.Preconditions; import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; @@ -118,10 +135,112 @@ public List getSeqInterpolants( : "There should be (n-1) interpolants for n partitions"; // convert data-structure back - // TODO check that interpolants do not contain abbreviations we did not introduce ourselves final List result = new ArrayList<>(); for (final IFormula itp : asJava(itps)) { - result.add(mgr.encapsulateBooleanFormula(itp)); + var simplified = PartialEvaluator.apply(BooleanCompactifier.apply(itp)); + var unsigned = + Rewriter.rewrite( + simplified, + term -> { + if (term instanceof IFunApp) { + // Rewrite casts to signed bitvectors as casts to unsigned bitvectors + var app = (IFunApp) term; + if (app.fun().name().equals("mod_cast")) { + var par1 = (IIntLit) app.apply(0); + var par2 = (IIntLit) app.apply(1); + if (par1.value().$less(IdealInt.ZERO())) { + var diff = par2.value().$minus(par1.value()); + return new IFunApp( + app.fun(), + PrincessEnvironment.toITermSeq( + IExpression.i(0), IExpression.i(diff), app.apply(2))); + } + } + } + return term; + }); + var quantifiedVariableFix = + Rewriter.rewrite( + unsigned, + term -> { + // Rewrite quantifiers with missing variable sorts + if (term instanceof ISortedQuantified) { + var quantified = (ISortedQuantified) term; + if (quantified.sort().name().equals("any")) { + return new ISortedQuantified( + quantified.quan(), Integer$.MODULE$, quantified.subformula()); + } + } + if (term instanceof ISortedVariable) { + var variable = (ISortedVariable) term; + if (variable.sort().name().equals("any")) { + return new ISortedVariable(variable.index(), Integer$.MODULE$); + } + } + return term; + }); + var selectBugFixed = + Rewriter.rewrite( + quantifiedVariableFix, + term -> { + // Add missing conversions for select(arr, idx) if the arrays maps to bitvectors + if (term instanceof ITimes) { + var times = (ITimes) term; + if (!PrincessEnvironment.getFormulaType(times.subterm()).isIntegerType()) { + return new ITimes(times.coeff(), ModuloArithmetic.cast2Int(times.subterm())); + } + } + if (term instanceof IPlus) { + var plus = (IPlus) term; + var t1 = plus.t1(); + if (!PrincessEnvironment.getFormulaType(t1).isIntegerType()) { + t1 = ModuloArithmetic.cast2Int(t1); + } + var t2 = plus.t2(); + if (!PrincessEnvironment.getFormulaType(t2).isIntegerType()) { + t2 = ModuloArithmetic.cast2Int(t2); + } + if (t1 != plus.t1() || t2 != plus.t2()) { + return new IPlus(t1, t2); + } + } + if (term instanceof IEquation) { + var eq = (IEquation) term; + var sort1 = Sort.sortOf(eq.left()); + var sort2 = Sort.sortOf(eq.right()); + if (sort1.equals(Integer$.MODULE$) && !sort2.equals(Integer$.MODULE$)) { + return new IEquation(eq.left(), ModuloArithmetic.cast2Int(eq.right())); + } + if (!sort1.equals(Integer$.MODULE$) && sort2.equals(Integer$.MODULE$)) { + return new IEquation(ModuloArithmetic.cast2Int(eq.left()), eq.right()); + } + } + if (term instanceof IIntFormula) { + var formula = (IIntFormula) term; + if (formula.rel().equals(IIntRelation.GeqZero()) + || formula.rel().equals(IIntRelation.EqZero())) { + if (!Sort.sortOf(formula.t()).equals(Integer$.MODULE$)) { + return new IIntFormula(formula.rel(), ModuloArithmetic.cast2Int(formula.t())); + } + } + } + return term; + }); + var eqZero = + Rewriter.rewrite( + selectBugFixed, + term -> { + // Rewrite (= term 0) as (=0 term) + if (term instanceof IEquation) { + var equation = (IEquation) term; + if (equation.right() instanceof IIntLit + && ((IIntLit) equation.right()).value().isZero()) { + return IExpression.eqZero(equation.left()); + } + } + return term; + }); + result.add(mgr.encapsulateBooleanFormula(eqZero)); } return result; }