conversion from and to Z3 sorts of maps and sets should be complete now

src/purescala/FairZ3Solver.scala

@@ -139,6 +139,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
         case Int32Type => RegularSort(intSort)
         case AbstractClassType(d) => RegularSort(adtSorts(d))
         case CaseClassType(d) => RegularSort(adtSorts(d))
+        case SetType(d) => RegularSort(setSorts(d))
+        case mt @ MapType(d,r) => RegularSort(mapSorts(mt))
         case _ => throw UntranslatableTypeException("Can't handle type " + tt)
       }
 
@@ -1083,7 +1085,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
             }
             // case OpAsArray => {
             //   assert(argsSize == 0)
-            //   
+            //   throw new Exception()
             // }
             case other => {
               System.err.println("Don't know what to do with this declKind : " + other)

src/purescala/Z3ModelReconstruction.scala

@@ -21,37 +21,49 @@ trait Z3ModelReconstruction {
     if(exprToZ3Id.isDefinedAt(id.toVariable)) {
       val z3ID : Z3AST = exprToZ3Id(id.toVariable)
 
-      expectedType match {
-        case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral(_))
-        case Int32Type => model.evalAs[Int](z3ID).map(IntLiteral(_))
-        case MapType(kt,vt) => model.eval(z3ID) match {
+      def rec(ast: Z3AST, expTpe: TypeTree): Option[Expr] = expTpe match {
+        case BooleanType => model.evalAs[Boolean](ast).map(BooleanLiteral(_))
+        case Int32Type => model.evalAs[Int](ast).map(IntLiteral(_))
+        case MapType(kt,vt) => model.eval(ast) match {
           case None => None
           case Some(t) => model.getArrayValue(t) match {
             case None => None
             case Some((map, elseValue)) => 
               val singletons = map.map(e => (e, z3.getASTKind(e._2))).collect {
-                case ((index, value), Z3AppAST(someCons, arg :: Nil)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(fromZ3Formula(index), fromZ3Formula(arg))
+                case ((index, value), Z3AppAST(someCons, arg :: Nil)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(rec(index, kt).get, rec(arg, vt).get)
               }
-              (if (singletons.isEmpty) Some(EmptyMap(kt, vt)) else Some(FiniteMap(singletons.toSeq))).map(_.setType(expectedType))
+              (if (singletons.isEmpty) Some(EmptyMap(kt, vt)) else Some(FiniteMap(singletons.toSeq))).map(_.setType(expTpe))
           }
         }
-        case funType @ FunctionType(fts, tt) => model.eval(z3ID) match {
+        case funType @ FunctionType(fts, tt) => model.eval(ast) match {
           case None => None
           case Some(t) => model.getArrayValue(t) match {
             case None => None
             case Some((es, ev)) =>
               val entries: Seq[(Seq[Expr], Expr)] = es.toSeq.map(e => (e, z3.getASTKind(e._1))).collect {
-                case ((key, value), Z3AppAST(cons, args)) if cons == funDomainConstructors(funType) => (args map fromZ3Formula, fromZ3Formula(value))
+                case ((key, value), Z3AppAST(cons, args)) if cons == funDomainConstructors(funType) => ((args zip fts) map (p => rec(p._1, p._2).get), rec(value, tt).get)
               }
-              val elseValue = fromZ3Formula(ev)
-              Some(AnonymousFunction(entries, elseValue).setType(expectedType))
+              val elseValue = rec(ev, tt).get
+              Some(AnonymousFunction(entries, elseValue).setType(expTpe))
           }
         }
-        case other => model.eval(z3ID) match {
+        case SetType(dt) => model.eval(ast) match {
+          case None => None
+          case Some(t) => model.getSetValue(t) match {
+            case None => None
+            case Some(set) => {
+              val elems = set.map(e => rec(e, dt).get)
+              (if (elems.isEmpty) Some(EmptySet(dt)) else Some(FiniteSet(elems.toSeq))).map(_.setType(expTpe))
+            }
+          }
+        }
+        case other => model.eval(ast) match {
           case None => None
           case Some(t) => softFromZ3Formula(t)
         }
       }
+
+      rec(z3ID, expectedType)
     } else None
   }