From d8e3e3f6b30e5a254474cd729f230ae50e748bee Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 7 Sep 2025 01:14:33 +0200 Subject: [PATCH 01/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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);