Some fixes in recursive evaluator + new regression

src/it/resources/regression/tip/SAT/LanguagesBadForall.scala-0.tip

@@ -0,0 +1,21 @@
+(declare-datatypes (A!27) ((Lang!2 (Lang!3 (oo!1 Bool) (dd!1 (=> A!27 (Lang!2 A!27)))))))
+
+(declare-datatypes (T!0) ((List!3 (Cons!2 (h!46 T!0) (t!56 (List!3 T!0))) (Nil!2))))
+
+(define-fun-rec (par (A!32) (contains!1 ((thiss!56 (Lang!2 A!32)) (w!1 (List!3 A!32))) Bool (ite (is-Nil!2 w!1) (assume (is-Lang!3 thiss!56) (oo!1 thiss!56)) (contains!1 (@ (assume (is-Lang!3 thiss!56) (dd!1 thiss!56)) (h!46 w!1)) (t!56 w!1))))))
+
+(define-fun (par (A!30) (===!0 ((thiss!15 (Lang!2 A!30)) (that!16 (Lang!2 A!30))) Bool (forall ((w!0 (List!3 A!30))) (= (contains!1 thiss!15 w!0) (contains!1 that!16 w!0))))))
+
+(define-fun-rec (par (A!31) (+!1 ((thiss!23 (Lang!2 A!31)) (that!17 (Lang!2 A!31))) (Lang!2 A!31) (Lang!3 (or (assume (is-Lang!3 thiss!23) (oo!1 thiss!23)) (assume (is-Lang!3 that!17) (oo!1 that!17))) (lambda ((a!4 A!31)) (+!1 (@ (assume (is-Lang!3 thiss!23) (dd!1 thiss!23)) a!4) (@ (assume (is-Lang!3 that!17) (dd!1 that!17)) a!4)))))))
+
+(define-fun-rec (par (A!28) (zero!0 () (Lang!2 A!28) (Lang!3 false (lambda ((x$1!4 A!28)) (as zero!0 (Lang!2 A!28)))))))
+
+(define-fun (par (A!29) (one!0 () (Lang!2 A!29) (Lang!3 true (lambda ((x$2!4 A!29)) (as zero!0 (Lang!2 A!29)))))))
+
+(declare-datatypes () ((Object!2 (Object!3 (ptr!1 Int)))))
+
+(assert (not (===!0 (+!1 (as one!0 (Lang!2 Object!2)) (as zero!0 (Lang!2 Object!2))) (as zero!0 (Lang!2 Object!2)))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard

src/it/scala/inox/solvers/SolvingTestSuite.scala

@@ -10,7 +10,7 @@ trait SolvingTestSuite extends TestSuite {
     checkModels       <- Seq(false, true)
     feelingLucky      <- Seq(false, true)
     unrollAssumptions <- Seq(false, true)
-    assumeChecked     <- Seq(PurityOptions.Unchecked, PurityOptions.AssumeChecked)
+    assumeChecked     <- Seq(false, true)
     modelFinding      <- Seq(0, 1)
   } yield Seq(
     optSelectedSolvers(Set(solverName)),
@@ -25,7 +25,7 @@ trait SolvingTestSuite extends TestSuite {
 
   override protected def optionsString(options: Options): String = {
     super.optionsString(options) +
-    " assck=" + options.findOptionOrDefault(optAssumeChecked).assumeChecked +
+    " assck=" + options.findOptionOrDefault(optAssumeChecked) +
     " model=" + options.findOptionOrDefault(unrolling.optModelFinding)
   }
 }

src/it/scala/inox/tip/TipTestSuite.scala

@@ -13,12 +13,12 @@ class TipTestSuite extends TestSuite with ResourceUtils {
     Seq(optSelectedSolvers(Set("nativez3")), optCheckModels(true)),
     Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true)),
     Seq(optSelectedSolvers(Set("smt-cvc4")), optCheckModels(true)),
-    Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true), optAssumeChecked(PurityOptions.AssumeChecked))
+    Seq(optSelectedSolvers(Set("smt-z3")),   optCheckModels(true), optAssumeChecked(true))
   )
 
   override protected def optionsString(options: Options): String = {
     "solver=" + options.findOptionOrDefault(optSelectedSolvers).head +
-    (if (options.findOptionOrDefault(optAssumeChecked).assumeChecked) " assumechecked" else "")
+    (if (options.findOptionOrDefault(optAssumeChecked)) " assumechecked" else "")
   }
 
   private def ignoreSAT(ctx: Context, file: java.io.File): FilterStatus = 
@@ -32,7 +32,7 @@ class TipTestSuite extends TestSuite with ResourceUtils {
         case ("smt-cvc4", "BinarySearchTreeQuant.scala-2.tip") => Ignore
         // this test only holds when assumeChecked=false
         case (_, "LambdaEquality2.scala-1.tip")
-        if ctx.options.findOptionOrDefault(optAssumeChecked).assumeChecked => Skip
+        if ctx.options.findOptionOrDefault(optAssumeChecked) => Skip
         case _ => Test
       }
 

src/main/scala/inox/ast/SymbolOps.scala

@@ -104,7 +104,7 @@ trait SymbolOps { self: TypeOps =>
   /** Returns 'true' iff the evaluation of expression `expr` cannot lead to a crash. */
   def isPure(expr: Expr)(implicit opts: PurityOptions): Boolean = isPureIn(expr, Path.empty)
 
-  def isAlwaysPure(expr: Expr) = isPure(expr)(PurityOptions.Unchecked)
+  def isAlwaysPure(expr: Expr) = isPure(expr)(PurityOptions.unchecked)
 
   /** Returns 'true' iff the evaluation of expression `expr` cannot lead to a crash under the provided path. */
   def isPureIn(e: Expr, path: Path)(implicit opts: PurityOptions): Boolean = {
@@ -158,8 +158,8 @@ trait SymbolOps { self: TypeOps =>
           if (reportErrors) ctx.reporter.error(SimplifyGroundError(e, evaluated))
           evalChildren(e)
         }
-      case l: Lambda if !opts.totalFunctions =>
-        evalChildren(l)(PurityOptions.Unchecked)
+      case l: Lambda =>
+        evalChildren(l)(PurityOptions.unchecked)
       case e =>
         evalChildren(e)
     }
@@ -263,6 +263,19 @@ trait SymbolOps { self: TypeOps =>
         (tvars & tvs).isEmpty && (pathVars & tvs).isEmpty
       }
 
+      def containsChoose(e: Expr): Boolean =
+        exists { case c: Choose => true case _ => false } (e)
+
+      def containsRecursive(e: Expr): Boolean =
+        exists { case fi: FunctionInvocation => fi.tfd.fd.isRecursive case _ => false } (e)
+
+      def isLiftable(e: Expr, path: Path): Boolean = {
+        isLocal(e, path) &&
+        (isSimple(e) || !onlySimple) &&
+        !containsChoose(e) &&
+        ((isAlwaysPure(e) && !containsRecursive(e)) || (!inFunction && (isPure(e) || path.conditions.isEmpty)))
+      }
+
       transformWithPC(body)((e, env, op) => e match {
         case v @ Variable(id, tpe, flags) =>
           Variable(
@@ -279,25 +292,11 @@ trait SymbolOps { self: TypeOps =>
           val newEs = es.map(op.rec(_, env))
           recons(newEs)
 
-        case Let(vd, e, b) if (
-          isLocal(e, env) &&
-          (isSimple(e) || !onlySimple) &&
-          !exists { case c: Choose => true case _ => false } (e) && (
-            isAlwaysPure(e) ||
-            ((!inFunction || opts.totalFunctions) && (isPure(e) || env.conditions.isEmpty))
-          )
-        ) =>
+        case Let(vd, e, b) if isLiftable(e, env) =>
           subst += vd.toVariable -> e
           op.rec(b, env)
 
-        case expr if (
-          isLocal(expr, env) &&
-          (isSimple(expr) || !onlySimple) &&
-          !exists { case c: Choose => true case _ => false } (expr) && (
-            isAlwaysPure(expr) ||
-            ((!inFunction || opts.totalFunctions) && (isPure(expr) || env.conditions.isEmpty))
-          )
-        ) =>
+        case expr if isLiftable(expr, env) =>
           Variable(getId(expr), expr.getType, Set.empty)
 
         case f: Forall =>
@@ -463,7 +462,7 @@ trait SymbolOps { self: TypeOps =>
 
     case FunctionType(from, to) =>
       val l = Lambda(from.map(tpe => ValDef(FreshIdentifier("x", true), tpe)), constructExpr(0, to))
-      uniquateClosure(i, l)(PurityOptions.Unchecked)
+      uniquateClosure(i, l)(PurityOptions.unchecked)
   }
 
   /* Inline lambda lets that appear in forall bodies. For example,
@@ -1198,7 +1197,7 @@ trait SymbolOps { self: TypeOps =>
     * @see [[SymbolOps.isPure isPure]]
     */
   def let(vd: ValDef, e: Expr, bd: Expr) = {
-    if ((variablesOf(bd) contains vd.toVariable) || !isPure(e)(PurityOptions.Unchecked))
+    if ((variablesOf(bd) contains vd.toVariable) || !isPure(e)(PurityOptions.unchecked))
       Let(vd, e, bd).setPos(Position.between(vd.getPos, bd.getPos))
     else bd
   }
@@ -1207,7 +1206,7 @@ trait SymbolOps { self: TypeOps =>
     * @see [[Expressions.IfExpr IfExpr]]
     */
   def ifExpr(c: Expr, t: Expr, e: Expr): Expr = (t, e) match {
-    case (_, `t`) if isPure(c)(PurityOptions.Unchecked) => t
+    case (_, `t`) if isPure(c)(PurityOptions.unchecked) => t
     case (IfExpr(c2, thenn, `e`), _) => ifExpr(and(c, c2), thenn, e)
     case (_, IfExpr(c2, `t`, e2)) => ifExpr(or(c, c2), t, e2)
     case (BooleanLiteral(true), BooleanLiteral(false)) => c

src/main/scala/inox/solvers/package.scala

@@ -8,29 +8,16 @@ import scala.concurrent.duration._
 package object solvers {
   import combinators._
 
-  sealed abstract class PurityOptions {
-    def assumeChecked = this != PurityOptions.Unchecked
-    def totalFunctions = this == PurityOptions.TotalFunctions
-  }
+  object optAssumeChecked extends FlagOptionDef("assume-checked", false)
 
-  object PurityOptions {
-    case object Unchecked extends PurityOptions
-    case object AssumeChecked extends PurityOptions
-    case object TotalFunctions extends PurityOptions
+  class PurityOptions(val assumeChecked: Boolean)
 
-    def apply(ctx: Context) = ctx.options.findOptionOrDefault(optAssumeChecked)
-  }
+  object PurityOptions {
+    def apply(ctx: Context) =
+      new PurityOptions(ctx.options.findOptionOrDefault(optAssumeChecked))
 
-  object optAssumeChecked extends OptionDef[PurityOptions] {
-    val name = "assume-checked"
-    val default = PurityOptions.Unchecked
-    val parser = (str: String) => str match {
-      case "false" => Some(PurityOptions.Unchecked)
-      case "" | "checked" => Some(PurityOptions.AssumeChecked)
-      case "total" => Some(PurityOptions.TotalFunctions)
-      case _ => None
-    }
-    val usageRhs = s"--$name=(false|checked|total)"
+    def assumeChecked = new PurityOptions(true)
+    def unchecked = new PurityOptions(false)
   }
 
   object optNoSimplifications extends FlagOptionDef("no-simplifications", false)

src/main/scala/inox/transformers/SimplifierWithPC.scala

@@ -374,12 +374,11 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
           lazy val inLambda = exists { case l: Lambda => variablesOf(l) contains v case _ => false }(rb)
           lazy val immediateCall = existsWithPC(rb) { case (`v`, path) => path.isEmpty case _ => false }
           lazy val containsLambda = exists { case l: Lambda => true case _ => false }(re)
-          lazy val realPE = opts match {
-            case solvers.PurityOptions.Unchecked => pe
-            case solvers.PurityOptions.TotalFunctions => pe
-            case _ =>
-              val simp = simplifier(solvers.PurityOptions.Unchecked)
-              simp.isPure(e, path.asInstanceOf[simp.CNFPath])
+          lazy val realPE = if (opts.assumeChecked) {
+            val simp = simplifier(solvers.PurityOptions.unchecked)
+            simp.isPure(e, path.asInstanceOf[simp.CNFPath])
+          } else {
+            pe
           }
 
           val (lete, letp) = if (