search

uuverifiers / princess

The Princess Theorem Prover
Other
22 stars 4 forks source link

Abbrev causes crashes when used with rational numbers #12

Closed daniel-raffler closed 1 month ago

daniel-raffler commented 1 month ago

Hello, there seems to be something wrong when mixing abbreviations with rational numbers.

Here is an example program:

import ap.SimpleAPI
import ap.api.SimpleAPI.ProverStatus
import ap.parser.ITerm
import ap.theories.rationals.Rationals
import ap.util.Debug
import org.scalatest.funsuite.AnyFunSuite

class AbbrevTest extends AnyFunSuite {

  import ap.theories.rationals.Rationals._
  import ap.parser.IExpression.{Sort => _, _};

  val withAssertions = true;

  def makeLargeTerm(k: Int): ITerm = if (k == 1) int(1) else makeLargeTerm(k - 1) + frac(1, k)

  test("Abbrev") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      val f0 = makeLargeTerm(10) // 2.9289682539682539682539682539682539682539682539682539682539682539
      val f1 = Rationals.lt(f0, int(3)) & Rationals.lt(frac(29, 10), f0)
      val f2 = abbrevSharedExpressions(f1 & f1, 10)

      addAssertion(f2)

      assert(checkSat(true) == ProverStatus.Sat)
    }
  }

  test("NoAbbrev") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      val f0 = makeLargeTerm(10)
      val f1 = Rationals.lt(f0, int(3)) & Rationals.lt(frac(29, 10), f0)
      val f2 = abbrevSharedExpressions(f1 & f1, 100) // Cut-off too large

      addAssertion(f2)

      assert(checkSat(true) == ProverStatus.Sat)
    }
  }
}

The test with abbreviations crashes with an assertion error:


assertion failed
java.lang.AssertionError: assertion failed
    at scala.Predef$.assert(Predef.scala:264)
    at ap.util.Debug$.assertTrue(Debug.scala:142)
    at ap.util.Debug$.assertInt(Debug.scala:213)
    at ap.parser.FunctionEncoder.apply(FunctionEncoder.scala:342)
    at ap.parser.FunctionPreproc.encodeFunctions(FunctionPreprocessing.scala:63)
    at ap.parser.StdFunctionPreproc.$anonfun$newFors$2(FunctionPreprocessing.scala:118)
    at scala.collection.Iterator$$anon$9.next(Iterator.scala:584)
    at scala.collection.immutable.List.prependedAll(List.scala:153)
    at scala.collection.immutable.List$.from(List.scala:685)
    at scala.collection.immutable.List$.from(List.scala:682)
    at scala.collection.IterableOps$WithFilter.map(Iterable.scala:900)
    at ap.parser.StdFunctionPreproc.<init>(FunctionPreprocessing.scala:117)
    at ap.parser.Preprocessing$.apply(Preprocessing.scala:143)
    at ap.api.SimpleAPI.toInternal(SimpleAPI.scala:4220)
    at ap.api.SimpleAPI.flushTodo(SimpleAPI.scala:4003)
    at ap.api.SimpleAPI.setPartitionNumberHelp(SimpleAPI.scala:2273)
    at ap.api.SimpleAPI.withPartitionNumber(SimpleAPI.scala:2287)
    at ap.api.SimpleAPI.abbrevHelp(SimpleAPI.scala:1489)
    at ap.api.SimpleAPI.abbrev(SimpleAPI.scala:1473)
    at ap.api.SimpleAPI.abbrev(SimpleAPI.scala:1449)
    at ap.api.SimpleAPI.$anonfun$abbrevSharedExpressions$1(SimpleAPI.scala:1547)
    at ap.parser.SubExprAbbreviator$Abbreviator.postVisit(InputAbsyVisitor.scala:1603)
    at ap.parser.SubExprAbbreviator$Abbreviator.postVisit(InputAbsyVisitor.scala:1585)
    at ap.parser.CollectingVisitor.visit(InputAbsyVisitor.scala:126)
    at ap.parser.SubExprAbbreviator$.apply(InputAbsyVisitor.scala:1564)
    at ap.api.SimpleAPI.abbrevSharedExpressions(SimpleAPI.scala:1543)
    at ap.api.SimpleAPI.abbrevSharedExpressions(SimpleAPI.scala:1611)
    at AbbrevTest.$anonfun$new$2(AbbrevTest.scala:25)
    at ap.api.SimpleAPI$.withProver(SimpleAPI.scala:178)
    at AbbrevTest.$anonfun$new$1(AbbrevTest.scala:19)
    ...

We've first noticed this issue in CPAchecker while working on adding rational numbers to the Princess backend for JavaSMT. There some of the example programs would crash due to Match errors:

Exception in thread "main" ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: scala.MatchError: _13 (of class ap.terfor.VariableTerm)
    at ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2150)
    at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1(SimpleAPI.scala:2086)
    at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1$adapted(SimpleAPI.scala:2086)
    at scala.Option.foreach(Option.scala:437)
    at ap.api.SimpleAPI.getOrUpdateLastStatus(SimpleAPI.scala:2086)
    at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2092)
    at ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2066)
    at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:1989)
    at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1917)
    at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsat(PrincessAbstractProver.java:79)
    at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.isUnsat(BasicProverWithAssumptionsWrapper.java:65)
    at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.isUnsat(BasicProverEnvironmentView.java:61)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:710)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.boundedModelCheck(AbstractBMCAlgorithm.java:686)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.boundedModelCheck(BMCAlgorithm.java:158)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:454)
    at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
    at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:489)
    at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:357)
    at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:171)
Caused by: scala.MatchError: _13 (of class ap.terfor.VariableTerm)
    at ap.theories.nia.Polynomial$.$anonfun$fromLinearCombinationGen$2(Polynomial.scala:568)
    at ap.theories.nia.Polynomial$.$anonfun$fromLinearCombinationGen$2$adapted(Polynomial.scala:566)
    at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
    at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
    at scala.collection.AbstractIterable.foreach(Iterable.scala:926)
    at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:896)
    at ap.theories.nia.Polynomial$.fromLinearCombinationGen(Polynomial.scala:566)
    at ap.theories.nia.Polynomial$.fromMulAtomGen(Polynomial.scala:583)
    at ap.theories.nia.GroebnerMultiplication$$anon$1.$anonfun$handleGoalAux$4(GroebnerMultiplication.scala:372)
    at ap.theories.nia.GroebnerMultiplication$$anon$1.$anonfun$handleGoalAux$4$adapted(GroebnerMultiplication.scala:371)
    at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
    at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
    at scala.collection.AbstractIterator.foreach(Iterator.scala:1293)
    at ap.theories.nia.GroebnerMultiplication$$anon$1.$anonfun$handleGoalAux$2(GroebnerMultiplication.scala:371)
    at ap.util.LRUCache.apply(LRUCache.scala:49)
    at ap.theories.nia.GroebnerMultiplication$$anon$1.ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux(GroebnerMultiplication.scala:364)
    at ap.theories.nia.GroebnerMultiplication$$anon$1.handleGoal(GroebnerMultiplication.scala:230)
    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:423)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:489)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
    ...

Enabling assertions will give the same error as in the test above. And the whole issue can be resolved by simply not using abbrevSharedExpressions.

Does anybody know what could be going on here?

pruemmer commented 1 month ago

That's another great catch, thanks! Fixed in the latest version.

daniel-raffler commented 1 month ago

I just ran some tests and it's working now. Thanks for your help!