From 42e4814a54be9af0c392f71e3587519b006d3bd8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 16 Sep 2025 15:08:40 +0200 Subject: [PATCH 1/5] Princess: Return to using the partial model --- .../princess/PrincessAbstractProver.java | 33 -------- .../solvers/princess/PrincessModel.java | 84 ++----------------- src/org/sosy_lab/java_smt/test/ModelTest.java | 7 +- .../java_smt/test/SolverAllSatTest.java | 7 -- 4 files changed, 7 insertions(+), 124 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 8c86a06b69..3380d4fde3 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -23,9 +23,7 @@ import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; -import java.util.Collections; import java.util.Deque; -import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; import java.util.Set; @@ -35,7 +33,6 @@ 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; @@ -50,15 +47,6 @@ abstract class PrincessAbstractProver extends AbstractProverWithAllSat { protected final PrincessFormulaManager mgr; protected final Deque trackingStack = new ArrayDeque<>(); // symbols on all levels - /** - * Values returned by {@link Model#evaluate(Formula)}. - * - *

We need to record these to make sure that the values returned by the evaluator are - * consistent. Calling {@link #isUnsat()} will reset this list as the underlying model has been - * updated. - */ - protected final Set evaluatedTerms = new LinkedHashSet<>(); - // assign a unique partition number for eah added constraint, for unsat-core and interpolation. protected final UniqueIdGenerator idGenerator = new UniqueIdGenerator(); protected final Deque> partitions = new ArrayDeque<>(); @@ -89,14 +77,9 @@ protected PrincessAbstractProver( public boolean isUnsat() throws SolverException { Preconditions.checkState(!closed); wasLastSatCheckSat = false; - evaluatedTerms.clear(); final Value result = api.checkSat(true); if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) { wasLastSatCheckSat = true; - if (this.generateModels || this.generateAllSat) { - // we only build the model if we have set the correct options - evaluatedTerms.add(callOrThrow(api::partialModelAsFormula)); - } return false; } else if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Unsat())) { return true; @@ -147,22 +130,6 @@ protected void popImpl() { partitions.pop(); } - /** - * Get all terms that have been evaluated in the current model. The formulas are assignments that - * extend the original model. - */ - Collection getEvaluatedTerms() { - Preconditions.checkState( - this.generateModels || this.generateAllSat, - "Model generation was not enabled, no evaluated terms available."); - return Collections.unmodifiableSet(evaluatedTerms); - } - - /** Track an assignment `term == value` for an evaluated term and its value. */ - void addEvaluatedTerm(IFormula pFormula) { - evaluatedTerms.add(pFormula); - } - @SuppressWarnings("resource") @Override public Model getModel() throws SolverException { 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..8e0f482c3d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -12,25 +12,19 @@ import ap.api.PartialModel; import ap.api.SimpleAPI; -import ap.basetypes.IdealInt; import ap.parser.IAtom; import ap.parser.IBinFormula; import ap.parser.IBinJunctor; -import ap.parser.IBoolLit$; import ap.parser.IConstant; import ap.parser.IExpression; import ap.parser.IFormula; import ap.parser.IFunApp; -import ap.parser.IIntLit; -import ap.parser.IPlus; import ap.parser.ITerm; -import ap.parser.ITimes; import ap.terfor.preds.Predicate; import ap.theories.arrays.ExtArray; import ap.theories.arrays.ExtArray.ArraySort; import ap.theories.arrays.ExtArray.Select$; import ap.theories.arrays.ExtArray.Store$; -import ap.theories.rationals.Rationals; import ap.types.Sort; import ap.types.Sort$; import com.google.common.collect.ArrayListMultimap; @@ -48,21 +42,15 @@ import org.sosy_lab.java_smt.basicimpl.FormulaCreator; class PrincessModel extends AbstractModel { - private final PrincessAbstractProver prover; - private final PartialModel model; private final SimpleAPI api; - // Keeps track of the temporary variables created for explicit term evaluations in the model. - private int counter = 0; - PrincessModel( PrincessAbstractProver pProver, PartialModel partialModel, FormulaCreator creator, SimpleAPI pApi) { super(pProver, creator); - this.prover = pProver; this.model = partialModel; this.api = pApi; } @@ -249,74 +237,14 @@ public String toString() { return model.toString(); } - /** Tries to determine the Sort of a Term. */ - private Sort getSort(IExpression pTerm) { - // Just using sortof() won't work as Princess may have simplified the original term - // FIXME: This may also affect other parts of the code that use sortof() - if (pTerm instanceof ITimes) { - ITimes times = (ITimes) pTerm; - return getSort(times.subterm()); - } else if (pTerm instanceof IPlus) { - IPlus plus = (IPlus) pTerm; - return getSort(plus.apply(0)); - } else if (pTerm instanceof IFormula) { - return creator.getBoolType(); - } else { - // TODO: Do we need more cases? - return Sort$.MODULE$.sortOf((ITerm) pTerm); - } - } - - /** - * Simplify rational values. - * - *

Rewrite a/1 as a, otherwise return the term unchanged - */ - private ITerm simplifyRational(ITerm pTerm) { - // TODO: Reduce the term further? - // TODO: Also do this for the values in the model? - if (Sort$.MODULE$.sortOf(pTerm).equals(creator.getRationalType()) - && pTerm instanceof IFunApp - && ((IFunApp) pTerm).fun().name().equals("Rat_frac") - && pTerm.apply(1).equals(new IIntLit(IdealInt.ONE()))) { - return Rationals.int2ring((ITerm) pTerm.apply(0)); - } - return pTerm; - } - @Override - protected @Nullable IExpression evalImpl(IExpression expr) { - // The utility variable only appears temporarily on the solver's stack. - // The user should never notice it. - // We might not even need an index/counter for the variable. - String newVariable = "__JAVASMT__MODEL_EVAL_" + counter++; - - // Extending the partial model does not seem to work in Princess if the formula uses rational - // variables. To work around this issue we (temporarily) add the formula to the assertion - // stack and then repeat the sat-check to get the value. - api.push(); - for (IFormula fixed : prover.getEvaluatedTerms()) { - api.addAssertion(fixed); - } - - if (expr instanceof ITerm) { - ITerm term = (ITerm) expr; - ITerm var = api.createConstant(newVariable, getSort(term)); - api.addAssertion(var.$eq$eq$eq(term)); - api.checkSat(true); - ITerm value = simplifyRational(api.evalToTerm(var)); - api.pop(); - prover.addEvaluatedTerm(value.$eq$eq$eq(term)); - return value; + protected @Nullable IExpression evalImpl(IExpression formula) { + if (formula instanceof ITerm) { + return model.evalToTerm((ITerm) formula).getOrElse(() -> null); + } else if (formula instanceof IFormula) { + return model.evalExpression(formula).getOrElse(() -> null); } else { - IFormula formula = (IFormula) expr; - IFormula var = api.createBooleanVariable(newVariable); - api.addAssertion(var.$less$eq$greater(formula)); - api.checkSat(true); - IFormula value = IBoolLit$.MODULE$.apply(api.eval(var)); - api.pop(); - prover.addEvaluatedTerm(value.$less$eq$greater(formula)); - return value; + throw new AssertionError("unexpected formula: " + formula); } } } diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 40213bd4e0..8e2e61024e 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -81,7 +81,7 @@ public class ModelTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { FormulaType.getArrayType(IntegerType, IntegerType); private static final ImmutableList SOLVERS_WITH_PARTIAL_MODEL = - ImmutableList.of(Solvers.Z3); + ImmutableList.of(Solvers.Z3, Solvers.PRINCESS); @Before public void setup() { @@ -1152,11 +1152,6 @@ public void testGetArrays3() throws SolverException, InterruptedException { requireArrays(); requireArrayModel(); - assume() - .withMessage("As of now, only Princess does not support multi-dimensional arrays") - .that(solver) - .isNotEqualTo(Solvers.PRINCESS); - // create formula for "arr[5][3][1]==x && x==123" BooleanFormula f = mgr.parse( diff --git a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java index 7775633373..c5db4da57e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java @@ -218,13 +218,6 @@ public void allSatTest_withQuantifier() throws SolverException, InterruptedExcep .isNotEqualTo(Solvers.PRINCESS); } - if ("normal".equals(proverEnv)) { - assume() - .withMessage("solver reports a partial model when using quantifiers") - .that(solverToUse()) - .isNotEqualTo(Solvers.PRINCESS); - } - // (y = 1) // & (PRED1 <-> (y = 1)) // & (PRED3 <-> ALL x_0. (3 * x_0 != y)) From d019061225d92c7517399d80ca42c10553dc77b5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 16 Sep 2025 15:24:25 +0200 Subject: [PATCH 2/5] Princess: Simplify code for getting the sort of a term in PrincessEnvironment --- .../solvers/princess/PrincessEnvironment.java | 50 +++---------------- 1 file changed, 6 insertions(+), 44 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 40aeaecb00..d4a6e1f03c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -22,10 +22,7 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; -import ap.parser.IPlus; import ap.parser.ITerm; -import ap.parser.ITermITE; -import ap.parser.ITimes; import ap.parser.Parser2InputAbsy.TranslationException; import ap.parser.PartialEvaluator; import ap.parser.SMTLineariser; @@ -563,26 +560,10 @@ private static String getName(IExpression var) { } static FormulaType getFormulaType(IExpression pFormula) { - // TODO: We could use Sort.sortof() here, but it sometimes returns `integer` even though the - // term is rational. We should figure out why and then open a new issue for this. if (pFormula instanceof IFormula) { return FormulaType.BooleanType; - } else if (pFormula instanceof ITimes) { - // coeff is always INT, lets check the subterm. - ITimes times = (ITimes) pFormula; - return getFormulaType(times.subterm()); - } else if (pFormula instanceof IPlus) { - IPlus plus = (IPlus) pFormula; - FormulaType t1 = getFormulaType(plus.t1()); - FormulaType t2 = getFormulaType(plus.t2()); - return mergeFormulaTypes(t1, t2); - } else if (pFormula instanceof ITermITE) { - ITermITE plus = (ITermITE) pFormula; - FormulaType t1 = getFormulaType(plus.left()); - FormulaType t2 = getFormulaType(plus.right()); - return mergeFormulaTypes(t1, t2); } else { - final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula); + final Sort sort = Sort.sortOf((ITerm) pFormula); try { return getFormulaTypeFromSort(sort); } catch (IllegalArgumentException e) { @@ -596,28 +577,6 @@ static FormulaType getFormulaType(IExpression pFormula) { } } - /** - * Merge INTEGER and RATIONAL type or INTEGER and BITVECTOR and return the more general type. The - * ordering is: RATIONAL > INTEGER > BITVECTOR. - * - * @throws IllegalArgumentException for any other type. - */ - private static FormulaType mergeFormulaTypes(FormulaType type1, FormulaType type2) { - if (type1.equals(type2)) { - return type1; - } - if ((type1.isIntegerType() || type1.isRationalType()) - && (type2.isIntegerType() || type2.isRationalType())) { - return type1.isRationalType() ? type1 : type2; - } - if ((type1.isIntegerType() || type1.isBitvectorType()) - && (type2.isIntegerType() || type2.isBitvectorType())) { - return type1.isIntegerType() ? type1 : type2; - } - throw new IllegalArgumentException( - String.format("Types %s and %s can not be merged.", type1, type2)); - } - private static FormulaType getFormulaTypeFromSort(final Sort sort) { if (sort == PrincessEnvironment.BOOL_SORT) { return FormulaType.BooleanType; @@ -640,13 +599,16 @@ private static FormulaType getFormulaTypeFromSort(final Sort sort) { } else if (sort instanceof MultipleValueBool$) { return FormulaType.BooleanType; } else { + // Check if it's a bitvector sort scala.Option bitWidth = getBitWidth(sort); if (bitWidth.isDefined()) { return FormulaType.getBitvectorTypeWithSize((Integer) bitWidth.get()); + } else { + // Otherwise, fail + throw new IllegalArgumentException( + String.format("Unknown formula type '%s' for sort '%s'.", sort.getClass(), sort)); } } - throw new IllegalArgumentException( - String.format("Unknown formula type '%s' for sort '%s'.", sort.getClass(), sort)); } static scala.Option getBitWidth(final Sort sort) { From 5231dee82d860fa69c43b109772c4890c546291c Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 19 Sep 2025 17:20:05 +0200 Subject: [PATCH 3/5] Princess: Simplify formulas before evaluation --- .../sosy_lab/java_smt/solvers/princess/PrincessModel.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 8e0f482c3d..d0061596d8 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -239,12 +239,13 @@ public String toString() { @Override protected @Nullable IExpression evalImpl(IExpression formula) { + IExpression simplified = creator.getEnv().simplify(formula); if (formula instanceof ITerm) { - return model.evalToTerm((ITerm) formula).getOrElse(() -> null); + return model.evalToTerm((ITerm) simplified).getOrElse(() -> null); } else if (formula instanceof IFormula) { - return model.evalExpression(formula).getOrElse(() -> null); + return model.evalExpression(simplified).getOrElse(() -> null); } else { - throw new AssertionError("unexpected formula: " + formula); + throw new AssertionError(); // unreachable } } } From 4ce0eb4a51432fecd3b3b59687dc9b576a0adfce Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 24 Sep 2025 09:10:38 +0200 Subject: [PATCH 4/5] Princess: Disable a test that requires evaluation of String formulas The partial model misses support for evaluating constant String formulas. The issue was reported and has already been fixed. We should remember to enable the test again in the next update https://github.com/uuverifiers/ostrich/issues/108 --- src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index 231394788c..426d475465 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -152,6 +152,11 @@ public void testInputEscape() throws SolverException, InterruptedException { @Test public void testOutputUnescape() throws SolverException, InterruptedException { + // Princess does not (fully) support evaluating String formulas when the partial model is + // used. This has already been fixed upstream + // TODO Enable this test once we update Princess to the next version + assume().that(solver).isNotEqualTo(Solvers.PRINCESS); + // Test if Unicode escape sequences get properly converted back when reading from the model. try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { assertThat(!prover.isUnsat()).isTrue(); From 6296a0220b4adaf5784b83f727fc2f97100a41a0 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 24 Sep 2025 09:29:40 +0200 Subject: [PATCH 5/5] Princess: Disable a test that requires model values for arrays with multiple indices This is an issue with our backend and will be addressed separately See https://github.com/sosy-lab/java-smt/issues/520 --- src/org/sosy_lab/java_smt/test/ModelTest.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 8e2e61024e..afd17cae4b 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1147,6 +1147,10 @@ public void testGetArrays6() throws SolverException, InterruptedException { @Test public void testGetArrays3() throws SolverException, InterruptedException { + // We're having some issues handling arrays with more than one index in our Princess backend + // TODO Enable this test once model generation is fixed + assume().that(solver).isNotEqualTo(Solvers.PRINCESS); + requireParser(); requireIntegers(); requireArrays();