bug fix and support for set membership in evaluator

src/purescala/DefaultTactic.scala

@@ -33,6 +33,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
         val theExpr = { 
           val resFresh = FreshIdentifier("result", true).setType(body.getType)
           val bodyAndPost = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(post.get)))
+
           val withPrec = if(prec.isEmpty) {
             bodyAndPost
           } else {
@@ -83,7 +84,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
   
     def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
       val toRet = if(function.hasBody) {
-        val cleanBody = matchToIfThenElse(function.body.get)
+        val cleanBody = expandLets(matchToIfThenElse(function.body.get))
 
         val allPathConds = collectWithPathCondition((t => t match {
           case FunctionInvocation(fd, _) if(fd.hasPrecondition) => true

src/purescala/Evaluator.scala

@@ -217,6 +217,11 @@ object Evaluator {
           }
           case (le,re) => throw TypeErrorEx(TypeError(le, s1.getType))
         }
+        case ElementOfSet(el,s) => (rec(ctx,el), rec(ctx,s)) match {
+          case (_, EmptySet(_)) => BooleanLiteral(false)
+          case (e, f @ FiniteSet(els)) => BooleanLiteral(els.contains(e))
+          case (l,r) => throw TypeErrorEx(TypeError(r, SetType(l.getType)))
+        }
 
         case f @ FiniteSet(els) => FiniteSet(els.map(rec(ctx,_)).distinct).setType(f.getType)
         case e @ EmptySet(_) => e

src/purescala/Z3ModelReconstruction.scala

@@ -13,7 +13,7 @@ trait Z3ModelReconstruction {
   // exprToZ3Id, softFromZ3Formula, reporter
 
   private final val AUTOCOMPLETEMODELS : Boolean = true
-  private final val SIMPLESTCOMPLETION : Boolean = false // if true, use 0, Nil(), etc., else random
+  private final val SIMPLESTCOMPLETION : Boolean = true // if true, use 0, Nil(), etc., else random
 
   def modelValue(model: Z3Model, id: Identifier, tpe: TypeTree = null) : Option[Expr] = {
     val expectedType = if(tpe == null) id.getType else tpe
@@ -34,25 +34,21 @@ trait Z3ModelReconstruction {
 
   def modelToMap(model: Z3Model, ids: Iterable[Identifier]) : Map[Identifier,Expr] = {
     var asMap = Map.empty[Identifier,Expr]
+
+    def completeID(id : Identifier) : Unit = if (SIMPLESTCOMPLETION) {
+      asMap = asMap + ((id -> simplestValue(id.toVariable)))
+      reporter.info("Completing variable '" + id + "' to simplest value")
+    } else {
+      asMap = asMap + ((id -> randomValue(id.toVariable)))
+      reporter.info("Completing variable '" + id + "' to random value")
+    }
+
     for(id <- ids) {
       modelValue(model, id) match {
-        case None => ; // can't do much here
-        case Some(ex) =>
-          if (AUTOCOMPLETEMODELS) {
-            ex match {
-              case v @ Variable(exprId) if exprId == id =>
-                if (SIMPLESTCOMPLETION) {
-                  asMap = asMap + ((id -> simplestValue(id.toVariable)))
-                  reporter.info("Completing variable '" + id + "' to simplest value")
-                } else {
-                  asMap = asMap + ((id -> randomValue(id.toVariable)))
-                  reporter.info("Completing variable '" + id + "' to random value")
-                }
-              case _ => asMap = asMap + ((id -> ex))
-            }
-          } else {
-            asMap = asMap + ((id -> ex))
-          }
+        case None if (AUTOCOMPLETEMODELS) => completeID(id)
+        case None => ;
+        case Some(v @ Variable(exprId)) if (AUTOCOMPLETEMODELS && exprId == id) => completeID(id)
+        case Some(ex) => asMap = asMap + ((id -> ex))
       }
     }
     asMap