uuverifiers / princess Goto Github PK

The Princess Theorem Prover

License: Other

Makefile 0.21% Scala 69.68% QMake 16.65% SMT 9.97% TeX 0.32% Shell 0.78% Batchfile 0.01% Awk 0.01% OpenEdge ABL 2.38%

logic smt smt-lib smt-solver theorem-prover

princess's Introduction

The Princess Theorem Prover

Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted predicates, written entirely in Scala. Princess can reason about problems in integer arithmetic, augmented with predicates that can be axiomatised arbitrarily. Such problems can contain arbitrary quantifiers to express that some formula is supposed to hold for all or for some integers. Princess also contains theory modules for, among others, non-linear arithmetic, rationals, bit-vectors, arrays, heaps, algebraic data-types, strings.

More information about Princess can be found on the main webpage, https://philipp.ruemmer.org/princess.shtml

princess's People

Contributors

Stargazers

Watchers

Forkers

mario-bucev alan23273850 amandasystems oskarsoderberg jesper-amilon

princess's Issues

Inconsistant cast

The bug is occured when I try to solve LIA in ostrich.

The bug is caused by trying to cast the leadingTerm of LinearCombination0 to ConstanTerm. But the leadingTerm of LinearCombination0 is OneTerm, see:

princess/src/ap/terfor/linearcombination/LinearCombination.scala

Line 1432 in 24fe0ec

def leadingTerm : Term = OneTerm

Bug code:

princess/src/ap/proof/goal/FactsNormalisationTask.scala

Line 349 in 24fe0ec

logger.columnReduce(lc.leadingTerm.asInstanceOf[ConstantTerm], smallConst,

My exception stack trace is as below:

Caused by: java.lang.ClassCastException: class ap.terfor.OneTerm$ cannot be cast to class ap.terfor.ConstantTerm (ap.terfor.OneTerm$ and ap.terfor.ConstantTerm are in unnamed module of loader 'app')
	at ap.proof.goal.GoalColumnSolver.reduceWithLeadingCoeff(FactsNormalisationTask.scala:349)
	at ap.proof.goal.GoalColumnSolver.isSolvableEq(FactsNormalisationTask.scala:253)
	at ap.terfor.equations.ColumnSolver.$anonfun$result$1(ColumnSolver.scala:65)
	at scala.collection.Iterator$$anon$9.next(Iterator.scala:577)
	at ap.util.Seqs$.some(Seqs.scala:633)
	at ap.terfor.equations.ColumnSolver.result$lzycompute(ColumnSolver.scala:65)
	at ap.terfor.equations.ColumnSolver.result(ColumnSolver.scala:62)
	at ap.proof.goal.FactsNormalisationTask$.solvePositiveEqs$1(FactsNormalisationTask.scala:90)
	at ap.proof.goal.FactsNormalisationTask$.apply(FactsNormalisationTask.scala:101)
	at ap.proof.goal.Goal.step(Goal.scala:421)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:486)
	at ap.proof.ModelSearchProver$$anon$2.next(ModelSearchProver.scala:580)
	at ap.proof.certificates.PartialCombCertificate.dfExplore(Certificate.scala:524)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:600)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	at ap.proof.ModelSearchProver$$anon$2.next(ModelSearchProver.scala:580)
	at ap.proof.certificates.PartialCombCertificate.dfExplore(Certificate.scala:524)
	at ap.proof.certificates.PartialCompositionCertificate$$anon$2.next(Certificate.scala:357)
	at ap.proof.certificates.PartialInferenceCertificate.dfExplore(Certificate.scala:464)
	at ap.proof.certificates.PartialCompositionCertificate.dfExplore(Certificate.scala:363)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:600)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	at ap.proof.ModelSearchProver$$anon$2.next(ModelSearchProver.scala:580)
	at ap.proof.certificates.PartialCombCertificate.dfExplore(Certificate.scala:524)
	at ap.proof.certificates.PartialCompositionCertificate$$anon$2.next(Certificate.scala:357)
	at ap.proof.certificates.PartialInferenceCertificate.dfExplore(Certificate.scala:464)
	at ap.proof.certificates.PartialCompositionCertificate.dfExplore(Certificate.scala:363)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:600)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	at ap.proof.ModelSearchProver$$anon$2.next(ModelSearchProver.scala:580)
	at ap.proof.certificates.PartialCombCertificate.dfExplore(Certificate.scala:524)
	at ap.proof.certificates.PartialCompositionCertificate$$anon$2.next(Certificate.scala:357)
	at ap.proof.certificates.PartialInferenceCertificate.dfExplore(Certificate.scala:464)
	at ap.proof.certificates.PartialCompositionCertificate.dfExplore(Certificate.scala:363)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:600)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	at ap.proof.ModelSearchProver$$anon$2.next(ModelSearchProver.scala:580)
	at ap.proof.certificates.PartialCombCertificate.dfExplore(Certificate.scala:524)
	at ap.proof.certificates.PartialCompositionCertificate$$anon$2.next(Certificate.scala:357)
	at ap.proof.certificates.PartialInferenceCertificate.dfExplore(Certificate.scala:464)
	at ap.proof.certificates.PartialCompositionCertificate.dfExplore(Certificate.scala:363)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:600)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
	... 11 more

[Ostrich] String theory crashes when solving query with STR_LESS_EQUAL

❗ Maybe the following is a bug for Ostrich. Then please move this issue to a better place.

The JavaSMT developers are currently trying to improve their support for String/Regex theory with the SMT solver Princess (see sosy-lab/java-smt#257). There are some smaller issues in Princess (version 2023-06-19) that block us from a good integration.

The following issue appeared when solving a smaller formula for String theory:

Description:

We want to solve the query "a" <= var && var <= "c" && len(var) == 1 and want to proove that var is one of ["a", "b", "c"]. (The original query uses STR_LESS_THAN rather than STR_LESS_EQUAL, which limits the result to var:="b".)

Code / Junit test:

Please note that the interaction between Java and Scala is not nice to read 😄 .

  private StringTheory stringTheory;
  private SimpleAPI api;

  @Before
  public void init() {
    api = SimpleAPI.apply(
            SimpleAPI.apply$default$1(),
            SimpleAPI.apply$default$2(),
            SimpleAPI.apply$default$3(),
            SimpleAPI.apply$default$4(),
            SimpleAPI.apply$default$5(),
            SimpleAPI.apply$default$6(),
            SimpleAPI.apply$default$7(),
            SimpleAPI.apply$default$8(),
            SimpleAPI.apply$default$9(),
            SimpleAPI.apply$default$10(),
            SimpleAPI.apply$default$11());
    stringTheory = new OstrichStringTheory(
        collectionAsScalaIterableConverter(new ArrayList<Tuple2<String, Transducer>>()).asScala().toSeq(),
        new OFlags(
            OFlags.$lessinit$greater$default$1(),
            OFlags.$lessinit$greater$default$2(),
            OFlags.$lessinit$greater$default$3(),
            OFlags.$lessinit$greater$default$4(),
            OFlags.$lessinit$greater$default$5(),
            OFlags.$lessinit$greater$default$6(),
            OFlags.$lessinit$greater$default$7(),
            OFlags.$lessinit$greater$default$8(),
            OFlags.$lessinit$greater$default$9(),
            OFlags.$lessinit$greater$default$10(),
            OFlags.$lessinit$greater$default$11(),
            OFlags.$lessinit$greater$default$12()));
  }

  @Test
  public void testStringTheory() {
    ITerm a = stringTheory.string2Term("a");
    ITerm c = stringTheory.string2Term("c");
    ITerm var = api.createConstant("var", stringTheory.StringSort());
    ITerm num1 = new IIntLit(IdealInt.apply(1));

    IFormula a_le_var = new IAtom(stringTheory.str_$less$eq(), collectionAsScalaIterableConverter(List.of(a, var)).asScala().toSeq());
    IFormula var_le_c = new IAtom(stringTheory.str_$less$eq(), collectionAsScalaIterableConverter(List.of(var, c)).asScala().toSeq());
    IFormula var_of_len_one = num1.$eq$eq$eq(new IFunApp(stringTheory.str_len(), collectionAsScalaIterableConverter(List.of(var)).asScala().toSeq()));

    api.addAssertion(a_le_var);
    api.addAssertion(var_le_c);
    api.addAssertion(var_of_len_one);
    Value result = api.checkSat(true); // --> CRASH instead of SAT
  }
}

Stacktrace:

ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.Exception: Cannot handle literal char_<=(var, 2)
	at ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2146)
	at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1(SimpleAPI.scala:2082)
	at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1$adapted(SimpleAPI.scala:2082)
	at scala.Option.foreach(Option.scala:437)
	at ap.api.SimpleAPI.getOrUpdateLastStatus(SimpleAPI.scala:2082)
	at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2088)
	at ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2062)
	at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:1985)
	at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1913)
	at ... <insert code position from above>
Caused by: java.lang.Exception: Cannot handle literal char_<=(var, 2)
	at ostrich.OstrichSolver.$anonfun$findStringModel$1(OstrichSolver.scala:189)
	at scala.collection.immutable.Vector.foreach(Vector.scala:1856)
	at ostrich.OstrichSolver.findStringModel(OstrichSolver.scala:162)
	at ostrich.OstrichStringTheory$$anon$1.$anonfun$callBackwardProp$1(OstrichStringTheory.scala:382)
	at ap.util.LRUCache.apply(LRUCache.scala:49)
	at ostrich.OstrichStringTheory$$anon$1.callBackwardProp(OstrichStringTheory.scala:382)
	at ostrich.OstrichStringTheory$$anon$1.$anonfun$handleGoal$6(OstrichStringTheory.scala:369)
	at ap.proof.theoryPlugins.TheoryProcedure$RichActionSeq.elseDo(Plugin.scala:197)
	at ostrich.OstrichStringTheory$$anon$1.handleGoal(OstrichStringTheory.scala:369)
	at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:275)
	at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:435)
	at ap.proof.goal.Goal.step(Goal.scala:421)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:487)
	at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1113)
	at ap.api.ProofThreadRunnable$$anonfun$1.$anonfun$applyOrElse$2(ProofThread.scala:157)
	at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
	at ap.api.ProofThreadRunnable$$anonfun$1.applyOrElse(ProofThread.scala:158)
	at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
	at ap.api.ProofThreadRunnable.$anonfun$run$2(ProofThread.scala:213)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Timeout$.withChecker(Timeout.scala:56)
	at ap.api.ProofThreadRunnable.run(ProofThread.scala:203)
	at java.base/java.lang.Thread.run(Thread.java:833)

Unexpected result of VALID

I am not expecting this formula (http://logicrunch.it.uu.se:4096/~wv/princess/?ex=perma%2F1681311035_1997373393) to be valid since its basically A & !A for me:

\existentialConstants {
  int a;
}

\problem {
  \exists int v0; (a=(-2*v0)) & ! \exists int v0; (a=(-2*v0))
}

But the Princess Web Interface returns:

VALID

Equivalent constraint:
\forall int v0; a != -2*v0 & \exists int v0; a = -2*v0

Concrete witness:
false

VALID means for me that the formula is true in all interpretations. I don't see how this can be true for this formula.

If I only toggle on +incremental and +model but not +mostGeneralConstraint then the answer is:

VALID

Under the assignment:
sc_5_0_0 = 0

but I cannot interpret this answer and haven't found something similar in the examples.

I would really appreciate if someone could explain the results of Princess to me.

Model evaluation for rational theory is incomplete and does not simplify terms

The JavaSMT developers are currently trying to improve their support for Rational theory with the SMT solver Princess (see sosy-lab/java-smt#257). There are some smaller issues in Princess (version 2023-06-19) that block us from a good integration.

The following issue appeared in model evaluation:

Description:

(declare-fun x () Real)
(assert (= x 2))
(check-sat) // --> SAT
(evaluate-model (+ 2 x)) // --> no result available 😢 , expected result would be 4

Code / Junit test:

Comparing Integer and Rational theory shows that the model evaluation for Integer theory is more advanced than Rational theory.

  private SimpleAPI api;

  @Before
  public void init() {
    api = SimpleAPI.apply(
        SimpleAPI.apply$default$1(),
        SimpleAPI.apply$default$2(),
        SimpleAPI.apply$default$3(),
        SimpleAPI.apply$default$4(),
        SimpleAPI.apply$default$5(),
        SimpleAPI.apply$default$6(),
        SimpleAPI.apply$default$7(),
        SimpleAPI.apply$default$8(),
        SimpleAPI.apply$default$9(),
        SimpleAPI.apply$default$10(),
        SimpleAPI.apply$default$11()
    );
  }

  @Test
  public void testIntegerEvaluation() {
    ITerm num2 = new IIntLit(IdealInt.apply(2));
    ITerm x = api.createConstant("x", Sort.Integer$.MODULE$);
    IFormula eq = num2.$eq$eq$eq(x);
    api.addAssertion(eq);
    Value result = api.checkSat(true); // --> SAT
    PartialModel model = api.partialModel();
    Option<IExpression> eval = model.evalExpression(num2.$plus(x));
    System.out.println(eval); // -> Some(4) :-) GOOD BEHAVIOUR
  }

  @Test
  public void testRationalEvaluation() {
    ITerm num2 = Rationals$.MODULE$.int2ring(new IIntLit(IdealInt.apply(2)));
    ITerm x = api.createConstant("x", Rationals$.MODULE$.dom());
    IFormula eq = num2.$eq$eq$eq(x);
    api.addAssertion(eq);
    Value result = api.checkSat(true); // --> SAT
    PartialModel model = api.partialModel();
    Option<IExpression> eval = model.evalExpression(num2.$plus(x));
    System.out.println(eval); // -> None :-( BAD BEHAVIOUR
  }

Wanted behaviour:

Princess should also provide a model evaluation and term simplification for Rational theory, such that the result from above is available.

No model despite +model

Hi, princess does not return a concrete model/witness for me despite providing +model.

I omitted the formula from the request because I don't know if I am allowed to provide it.
Hope it's straightforward to see in the princess code why there could potentially be missing the concrete model, otherwise I can ask if the formula is safe to share.

{
"options" : ["-inputFormat=pri", "-quiet", "+model"],
"formula" : "\\existentialConstants { nat x_0, x_1, x_2; }\\problem { [omitted] }"
}

The result is:

{
    "result": "VALID\n\nUnder the constraint:\nx_2 = 2*x_0 & x_1 = 0\n"
}

Interestingly enough I get a concrete model when providing -clausifier=simple in some cases. Then I get:

{
    "result": "VALID\n\nUnder the constraint:\n(x_2 = 2*x_0 & x_1 = 0 & x_0 >= 3) | (x_2 = 2*x_0 & x_1 = 0 & x_0 >= 2) | (x_2 = 2 & x_1 = 0 & x_0 = 1) | (x_2 = 0 & x_1 = 0 & x_0 = 0)\n\nConcrete witness:\nx_2 = 6 & x_1 = 0 & x_0 = 3\n"
}

I also cannot access the maven repository:

<repositories>
    <repository>
        <id>uuverifiers</id>
        <name>uuverifiers</name>
        <url>http://logicrunch.research.it.uu.se/maven/</url>
    </repository>
</repositories>

Is it currently offline? I tried with https as well but then its redirecting me to another page.

Model evaluation for rational theory crashes in MatchError

The following issue appeared in model evaluation:

Description:

We want to evaluate a rational division in a model, completely unrelated to any pushed assertions.

(declare-fun x () Real)
(assert (true))
(check-sat) // --> SAT
(evaluate-model (/ x 2))

The division in the last line is a rational division, not the integer-based one.
The result is not relevant for us and can be any arbitrary value, except a crashing program :-)

Code / Junit test:

  private SimpleAPI api;

  @Before
  public void init() {
    Debug.enableAllAssertions(true);
    api = SimpleAPI.apply(
        SimpleAPI.apply$default$1(),
        SimpleAPI.apply$default$2(),
        SimpleAPI.apply$default$3(),
        SimpleAPI.apply$default$4(),
        SimpleAPI.apply$default$5(),
        SimpleAPI.apply$default$6(),
        SimpleAPI.apply$default$7(),
        SimpleAPI.apply$default$8(),
        SimpleAPI.apply$default$9(),
        SimpleAPI.apply$default$10(),
        SimpleAPI.apply$default$11()
    );
  }

  @Test
  public void testRationalEvaluation2() {
    ITerm num2 = Rationals$.MODULE$.int2ring(new IIntLit(IdealInt.apply(2)));
    ITerm x = api.createConstant("x", Rationals$.MODULE$.dom());
    Value result = api.checkSat(true); // --> we have not added any constraints, so this is SAT
    PartialModel model = api.partialModel();
    Option<IExpression> eval = model.evalExpression(Rationals$.MODULE$.div(x, num2)); // --> CRASH
    System.out.println(eval); // -> Some(0) would be nice to receive
  }
}

Stacktrace:

scala.MatchError: _0 (of class ap.parser.ISortedVariable)
	at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:134)
	at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:114)
	at ap.parser.CollectingVisitor.visit(InputAbsyVisitor.scala:169)
	at ap.api.PartialModel$Evaluator$.apply(PartialModel.scala:116)
	at ap.api.PartialModel.evalExpression(PartialModel.scala:59)
	at ... <insert code position from above>

The term (/ x 2) that is used for the model evaluation can be printed as EPS Rat. EX (((Rat_denom = _0) & ((_0 + -1) >= 0)) & (mul(_0, _1[Rat]) = mul(x, Rat_frac(1, 2)))). I assume that the symbol _0 comes from this notation.

@pruemmer Could you take a look?

Unsoundness with quantifiers and ADTs

Result should be unsat but is sat:

(set-logic ALL)
(declare-sort a 0)
(declare-datatypes ((prod 0)) (((Pair (gx a) (gy a)))))
(declare-fun p () prod)
(assert (forall ((x a) (y a)) (not (= p (Pair x y)))))
(check-sat)

Effect of option [+-]dnfConstraints

I am unsure about what [+-]dnfConstraints exactly does.
In the manual it states that this option turns ground constraints into DNF (for me ground constraints are formulae without any (free) variables).

The following shows an example output of Princess where I cannot follow what the option does (I am using it together with +mostGeneralConstraint):

((((x₁-x₀) ≠ 1 ∨ 1 ≤ x₀ ≤ 2) ∧ (x₁ ≠ 0 ∨ 0 ≥ x₀)) ∧ ((x₁-x₀) = 1 ∨ 0 ≥ x₁)) (+dnfConstraints)
(((x₁-x₀) = 1 ∧ 1 ≤ x₀ ≤ 2) ∨ (x₁ = 0 ∧ x₀ = 0)) (-dnfConstraints)

Both of the mostGeneralConstraints do not contain any ground constraints so I would not expect [+-]dnfConstraints to change the result.

Can someone maybe explain to me what [+-]dnfConstraints exactly does?
We are aiming for a DNF as seen in example 2.
When dnfConstraints is disabled Princess seems to be tending more towards our desired result.
Maybe there is another option for some kind of DNF not just designed to consider ground terms?

uuverifiers / princess Goto Github PK

princess's Introduction

The Princess Theorem Prover

princess's People

Contributors

Stargazers

Watchers

Forkers

princess's Issues

Description:

Code / Junit test:

Stacktrace:

Description:

Code / Junit test:

Wanted behaviour:

Description:

Code / Junit test:

Stacktrace:

Recommend Projects

Recommend Topics

Recommend Org