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/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) { 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..d0061596d8 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,15 @@ 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) { + IExpression simplified = creator.getEnv().simplify(formula); + if (formula instanceof ITerm) { + return model.evalToTerm((ITerm) simplified).getOrElse(() -> null); + } else if (formula instanceof IFormula) { + return model.evalExpression(simplified).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(); // unreachable } } } diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 40213bd4e0..afd17cae4b 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() { @@ -1147,16 +1147,15 @@ 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(); 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)) 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();