Bound unfolding in Inox rather than rely on timeouts in PartialEvaluator

.larabot.conf

@@ -1,6 +1,5 @@
 commands = [
-    "sbt -batch -Dparallel=5 test"
-    "sbt -batch -Dparallel=5 it:test"
+    "sbt -batch -Dparallel=1 it:testOnly *SMTZ3Unroll*"
 ]
 
 nightly {

build.sbt

@@ -14,7 +14,7 @@ val isMac     = osInf.indexOf("Mac") >= 0
 val osName = if (isWindows) "win" else if (isMac) "mac" else "unix"
 val osArch = System.getProperty("sun.arch.data.model")
 
-val inoxVersion = "1.1.0-332-ga6cbf8e"
+val inoxVersion = "1.1.0-341-gb70895c"
 val dottyLibrary = "dotty-compiler_2.12"
 val dottyVersion = "0.12.0-RC1-nonbootstrapped"
 val circeVersion = "0.10.0-M2"

core/src/main/scala/stainless/transformers/PartialEvaluator.scala

@@ -10,7 +10,17 @@ trait PartialEvaluator extends SimplifierWithPC { self =>
   import symbols._
   import exprOps._
 
+  protected def strictlyPositive(tpe: Type, e: Expr): Expr = (tpe match {
+    case IntegerType() => GreaterThan(e, IntegerLiteral(0))
+    case BVType(signed, size) => GreaterThan(e, BVLiteral(signed, 0, size))
+    case TupleType(tps) => and((1 to tps.length).map(i => strictlyPositive(tps(i-1), TupleSelect(e,i))): _*)
+    case _ => sys.error(s"Type $tpe is not supported for measures")
+  }).setPos(e)
+
   override protected def simplify(e: Expr, path: Env): (Expr, Boolean) = e match {
+    // case Annotated(e, Seq(Unchecked)) =>
+    //   simplify(e, path)
+
     case fi @ FunctionInvocation(id, tps, args) =>
       val tfd = fi.tfd
       val (rargs, pargs) = args.map(simplify(_, path)).unzip
@@ -20,6 +30,14 @@ trait PartialEvaluator extends SimplifierWithPC { self =>
         case _ => false
       } (expr)
 
+      def validMeasure: Option[Boolean] = {
+        measureOf(tfd.fullBody) map { measure =>
+          val nextMeasure = exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, measure)
+          val query = strictlyPositive(nextMeasure.getType, nextMeasure)
+          path.implies(query)
+        }
+      }
+
       def isProductiveUnfolding(inlined: Expr): Boolean = {
         def isKnown(expr: Expr): Boolean = expr match {
           case BooleanLiteral(_) => true
@@ -74,7 +92,7 @@ trait PartialEvaluator extends SimplifierWithPC { self =>
 
       inlined
         .filterNot(containsChoose)
-        .filter(isProductiveUnfolding)
+        .filter(expr => validMeasure.getOrElse(isProductiveUnfolding(expr)))
         .map(unfold)
         .getOrElse((
           FunctionInvocation(id, tps, rargs).copiedFrom(fi),

core/src/main/scala/stainless/transformers/SimplifierWithSolver.scala

@@ -7,6 +7,7 @@ import scala.language.existentials
 import scala.concurrent.duration._
 
 import inox.solvers.optCheckModels
+import inox.solvers.unrolling.{optUnrollBound, optUnrollFactor}
 
 trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self =>
   import trees._
@@ -23,14 +24,15 @@ trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self =>
     val symbols: self.symbols.type
   } = inox.Program(trees)(symbols)
 
-  protected val solver =
+  protected val solver = {
+    val solverContext = context.withOpts(optCheckModels(false), optUnrollBound(1), optUnrollFactor(2))
     semantics.getSemantics(program)
-      .getSolver(context.withOpts(optCheckModels(false)))
-      .withTimeout(150.millis)
+      .getSolver(solverContext)
       .toAPI
       .asInstanceOf[inox.solvers.SimpleSolverAPI {
         val program: self.program.type
       }]
+  }
 
   class Env private (val path: Path) extends PathLike[Env] with SolvingPath {
     override def implies(cond: Expr): Boolean = {

core/src/main/scala/stainless/verification/PartialEvaluation.scala

@@ -31,14 +31,6 @@ trait PartialEvaluation
   protected class TransformerContext(val symbols: s.Symbols) { self0 =>
     import symbols._
 
-    private[this] val simpleSimplifier = new {
-      override val trees: s.type = s
-      override val symbols: self0.symbols.type = self0.symbols
-      override val opts = inox.solvers.PurityOptions.assumeChecked
-    } with transformers.PartialEvaluator with inox.transformers.SimplifierWithPath {
-      override val pp = Env
-    }
-
     private[this] val solvingSimplifier = new {
       override val trees: s.type = s
       override val symbols: self0.symbols.type = self0.symbols
@@ -61,11 +53,8 @@ trait PartialEvaluation
     def shouldPartialEval(fd: FunDef): Boolean =
       invocationsToEval(fd.id).nonEmpty && !(fd.flags contains Synthetic)
 
-    private[this] def partialEval(fi: FunctionInvocation, path: Path, simple: Boolean = false): Expr = {
-      if (simple)
-        simpleSimplifier.transform(fi, simpleSimplifier.Env(path))
-      else
-        solvingSimplifier.transform(fi, solvingSimplifier.Env(path))
+    private[this] def partialEval(fi: FunctionInvocation, path: Path): Expr = {
+      solvingSimplifier.transform(fi, solvingSimplifier.Env(path))
     }
 
     final def transform(fd: FunDef): FunDef = {
@@ -78,7 +67,7 @@ trait PartialEvaluation
           reporter.debug(s"   Before: $fi")
 
           val (elapsed, res) = timers.partialeval.runAndGetTime {
-            partialEval(fi, path, simple = isSynthetic(fi.id))
+            partialEval(fi, path)
           }
 
           reporter.debug(s"   After: ${res.get}")

frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala

@@ -11,8 +11,8 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp
 
   override def configurations: Seq[Seq[inox.OptionValue[_]]] = Seq(
     Seq(
-      inox.optSelectedSolvers(Set("smt-z3")),
       inox.optTimeout(300.seconds),
+      inox.optSelectedSolvers(Set("smt-z3")),
       verification.optStrictArithmetic(false),
     )
   )

frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala

@@ -64,6 +64,20 @@ class SMTZ3VerificationSuite extends VerificationSuite {
   }
 }
 
+class SMTZ3UnrollBoundVerificationSuite(unrollBound: Int, unrollFactor: Int) extends SMTZ3VerificationSuite {
+  override def configurations = super.configurations.map {
+    seq => Seq(
+      inox.solvers.unrolling.optUnrollBound(unrollBound),
+      inox.solvers.unrolling.optUnrollFactor(unrollFactor),
+    ) ++ seq
+  }
+}
+
+class SMTZ3UnrollBoundOneOneSuite extends SMTZ3UnrollBoundVerificationSuite(1, 1)
+class SMTZ3UnrollBoundOneTwoSuite extends SMTZ3UnrollBoundVerificationSuite(1, 2)
+class SMTZ3UnrollBoundTwoOneSuite extends SMTZ3UnrollBoundVerificationSuite(2, 1)
+class SMTZ3UnrollBoundTwoTwoSuite extends SMTZ3UnrollBoundVerificationSuite(2, 2)
+
 class CodeGenVerificationSuite extends SMTZ3VerificationSuite {
   override def configurations = super.configurations.map {
     seq => Seq(