Princess crashes while evaluating Epsilon terms in the partial model

[daniel-raffler]

Hello everyone,
Princess seems to have problems when evaluating Epsilon terms in a partial model. Unlike the other issues I've posted this one is not related to Rationals, but can happen for Integer formulas.

Here is a short example program:

import ap.SimpleAPI
import ap.parser.{ISortedEpsilon, ISortedVariable, ITerm}
import ap.types.Sort
import ap.util.Debug
import org.scalatest.funsuite.AnyFunSuite

class EpsilonBug extends AnyFunSuite {

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

  val withAssertions = false;

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

      val epsilonTerm = ISortedEpsilon(Sort.Integer,
        (10 + -1 * (10 * ISortedVariable(0, Sort.Integer)) >= 0) & (10 * ISortedVariable(0, Sort.Integer) + -1 >= 0))

      checkSat(true)
      assertResult(1 : ITerm)(evalToTerm(epsilonTerm))
    }
  }

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

      val epsilonTerm = ISortedEpsilon(Sort.Integer,
        (10 + -1 * (10 * ISortedVariable(0, Sort.Integer)) >= 0) & (10 * ISortedVariable(0, Sort.Integer) + -1 >= 0))

      checkSat(true)
      assertResult(1 : ITerm)(partialModel.evalToTerm(epsilonTerm))
    }
  }
}

The second test ("epsilon partial") crashes in the last line. This is the stacktrace:

_0 (of class ap.parser.ISortedVariable)
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 ap.api.PartialModel.evalToTerm(PartialModel.scala:72)
	at EpsilonBug.$anonfun$new$4(EpsilonBug.scala:35)
	at ap.api.SimpleAPI$.withProver(SimpleAPI.scala:178)
	at EpsilonBug.$anonfun$new$3(EpsilonBug.scala:28)
	at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
	at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
	at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
	at org.scalatest.Transformer.apply(Transformer.scala:22)
	at org.scalatest.Transformer.apply(Transformer.scala:20)
	at org.scalatest.funsuite.AnyFunSuiteLike$$anon$1.apply(AnyFunSuiteLike.scala:226)
	at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
	at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
	at org.scalatest.funsuite.AnyFunSuite.withFixture(AnyFunSuite.scala:1564)
	at org.scalatest.funsuite.AnyFunSuiteLike.invokeWithFixture$1(AnyFunSuiteLike.scala:224)
	at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$runTest$1(AnyFunSuiteLike.scala:236)
	at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTest(AnyFunSuiteLike.scala:236)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTest$(AnyFunSuiteLike.scala:218)
	at org.scalatest.funsuite.AnyFunSuite.runTest(AnyFunSuite.scala:1564)
	at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$runTests$1(AnyFunSuiteLike.scala:269)
	at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
	at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
	at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTests(AnyFunSuiteLike.scala:269)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTests$(AnyFunSuiteLike.scala:268)
	at org.scalatest.funsuite.AnyFunSuite.runTests(AnyFunSuite.scala:1564)
	at org.scalatest.Suite.run(Suite.scala:1114)
	at org.scalatest.Suite.run$(Suite.scala:1096)
	at org.scalatest.funsuite.AnyFunSuite.org$scalatest$funsuite$AnyFunSuiteLike$$super$run(AnyFunSuite.scala:1564)
	at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$run$1(AnyFunSuiteLike.scala:273)
	at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
	at org.scalatest.funsuite.AnyFunSuiteLike.run(AnyFunSuiteLike.scala:273)
	at org.scalatest.funsuite.AnyFunSuiteLike.run$(AnyFunSuiteLike.scala:272)
	at org.scalatest.funsuite.AnyFunSuite.run(AnyFunSuite.scala:1564)
	at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:47)
	at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1321)
	at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1315)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1315)
	at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:992)
	at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:970)
	at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1481)
	at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:970)
	at org.scalatest.tools.Runner$.run(Runner.scala:798)
	at org.scalatest.tools.Runner.run(Runner.scala)
	at org.jetbrains.plugins.scala.testingSupport.scalaTest.ScalaTestRunner.runScalaTest2or3(ScalaTestRunner.java:43)
	at org.jetbrains.plugins.scala.testingSupport.scalaTest.ScalaTestRunner.main(ScalaTestRunner.java:26)
``

[pruemmer]

This issue is related to #16, and should be fixed in the same way: we need explicit function representing the rational operations, instead of translating everything on the fly to a base logic.

[pruemmer]

Do you have any concrete use cases where you need this kind of evaluation to work? In general, we cannot evaluate epsilon terms, but probably you are not generating them yourself in the first place, they are introduced by one of the theories?

[daniel-raffler]

This bug was originally based on a CPAchecker crash (here) that occurred when using Princess as a solver backend in JavaSMT. We've since changed the JavaSMT code and are using a workaround for Princess that avoids the partial model entirely. Because of this the crash is currently not reproducible. However, I can look into what happens when I try to remove the workaround.