Take measures into account when unfolding in partial evaluator

Author: romac

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,23 @@ trait PartialEvaluator extends SimplifierWithPC { self =>
         case _ => false
       } (expr)
 
+      def validMeasure: Boolean = {
+        println("measure: " + measureOf(tfd.fullBody))
+        measureOf(tfd.fullBody) match {
+          case Some(measure) =>
+            val nextMeasure = exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, measure)
+            println("next: " + nextMeasure)
+            val query = strictlyPositive(nextMeasure.getType, nextMeasure)
+            println("query: " + query)
+            val result = path.implies(query)
+
+            println("result: " + result)
+            result
+
+          case None => false
+        }
+      }
+
       def isProductiveUnfolding(inlined: Expr): Boolean = {
         def isKnown(expr: Expr): Boolean = expr match {
           case BooleanLiteral(_) => true
@@ -74,7 +101,7 @@ trait PartialEvaluator extends SimplifierWithPC { self =>
 
       inlined
         .filterNot(containsChoose)
-        .filter(isProductiveUnfolding)
+        .filter(expr => validMeasure || isProductiveUnfolding(expr))
         .map(unfold)
         .getOrElse((
           FunctionInvocation(id, tps, rargs).copiedFrom(fi),

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

@@ -7,7 +7,7 @@ import scala.language.existentials
 import scala.concurrent.duration._
 
 import inox.solvers.optCheckModels
-import inox.solvers.unrolling.optMaxUnfoldSteps
+import inox.solvers.unrolling.{optUnrollBound, optUnrollFactor}
 
 trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self =>
   import trees._
@@ -25,7 +25,7 @@ trait SimplifierWithSolver extends inox.transformers.SimplifierWithPC { self =>
   } = inox.Program(trees)(symbols)
 
   protected val solver = {
-    val solverContext = context.withOpts(optCheckModels(false), optMaxUnfoldSteps(1))
+    val solverContext = context.withOpts(optCheckModels(false), optUnrollBound(1), optUnrollFactor(2))
     semantics.getSemantics(program)
       .getSolver(solverContext)
       .toAPI