Implement and test everything for smt-z3

 - Partial support for CVC4

project/Build.scala

@@ -79,7 +79,7 @@ object Leon extends Build {
   object Github {
     lazy val bonsai = RootProject(uri("git://github.com/colder/bonsai.git#8f485605785bda98ac61885b0c8036133783290a"))
 
-    private val scalaSmtLibVersion = "90f66cf07aef34b05dc5585bb35aca773b3d0d43"
+    private val scalaSmtLibVersion = "4cc4cb1ce38fe62790b674666ab141d0430b0f00"
     lazy val scalaSmtLib = RootProject(uri("git://github.com/regb/scala-smtlib.git#%s".format(scalaSmtLibVersion)))
   }
 }

src/main/scala/leon/purescala/Trees.scala

@@ -576,10 +576,12 @@ object Trees {
   }
 
   /* Array operations */
+  @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
   case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr with FixedType {
     val fixedType = ArrayType(defaultValue.getType)
   }
 
+  @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
   case class ArrayMake(defaultValue: Expr) extends Expr with FixedType {
     val fixedType = ArrayType(defaultValue.getType)
   }
@@ -613,6 +615,8 @@ object Trees {
     val fixedType = Int32Type
   }
   case class FiniteArray(exprs: Seq[Expr]) extends Expr
+
+  @deprecated("Unsupported Array operation with most solvers", "Leon 2.3")
   case class ArrayClone(array: Expr) extends Expr {
     if(array.getType != Untyped)
       setType(array.getType)

src/main/scala/leon/purescala/TypeTrees.scala

@@ -49,7 +49,7 @@ object TypeTrees {
   }
     
 
-  sealed abstract class TypeTree extends Tree
+  abstract class TypeTree extends Tree
 
   case object Untyped extends TypeTree
   case object BooleanType extends TypeTree

src/main/scala/leon/solvers/SolverFactory.scala

@@ -34,10 +34,10 @@ object SolverFactory {
         SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
 
       case "smt" | "smt-z3" =>
-        SolverFactory(() => new UnrollingSolver(ctx, new SMTLIBSolver(ctx, program) with SMTLIBZ3Target) with TimeoutSolver)
+        SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBZ3Target) with TimeoutSolver)
 
       case "smt-cvc4" =>
-        SolverFactory(() => new UnrollingSolver(ctx, new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target) with TimeoutSolver)
+        SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target) with TimeoutSolver)
 
       case _ =>
         ctx.reporter.fatalError("Unknown solver "+name)

src/main/scala/leon/solvers/combinators/UnrollingSolver.scala

@@ -12,23 +12,42 @@ import purescala.TypeTrees._
 
 import solvers.templates._
 import utils.Interruptible
+import evaluators._
 
-import scala.collection.mutable.{Map=>MutableMap}
+class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver) extends Solver with Interruptible {
 
-class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
-        extends Solver with Interruptible {
+  val (feelingLucky, useCodeGen) = locally {
+    var lucky            = false
+    var codegen          = false
 
-  private var lastCheckResult: (Boolean, Option[Boolean], Option[Map[Identifier,Expr]]) = (false, None, None)
+    for(opt <- context.options) opt match {
+      case LeonFlagOption("feelinglucky", v)       => lucky   = v
+      case LeonFlagOption("codegen", v)            => codegen = v
+      case _ =>
+    }
 
-  val reporter = context.reporter
+    (lucky, codegen)
+  }
 
+  private val evaluator : Evaluator = {
+    if(useCodeGen) {
+      new CodeGenEvaluator(context, program)
+    } else {
+      new DefaultEvaluator(context, program)
+    }
+  }
+
+  private var lastCheckResult: (Boolean, Option[Boolean], Option[Map[Identifier,Expr]]) = (false, None, None)
+  private var varsInVC       = List[Set[Identifier]](Set())
+  private var constraints    = List[List[Expr]](Nil)
   private var interrupted: Boolean = false
 
+  val reporter = context.reporter
+
   def name = "U:"+underlying.name
 
   def free {}
 
-  var varsInVC    = List[Set[Identifier]](Set())
 
   val templateGenerator = new TemplateGenerator(new TemplateEncoder[Expr] {
     def encodeId(id: Identifier): Expr= {
@@ -65,6 +84,7 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
     }
 
     varsInVC    = (varsInVC.head ++ freeIds) :: varsInVC.tail
+    constraints = (constraints.head ++ newClauses) :: constraints.tail
   }
 
 
@@ -72,12 +92,14 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
     unrollingBank.push()
     solver.push()
     varsInVC = Set[Identifier]() :: varsInVC
+    constraints = Nil :: constraints
   }
 
   def pop(lvl: Int = 1) {
     unrollingBank.pop(lvl)
     solver.pop(lvl)
     varsInVC = varsInVC.drop(lvl)
+    constraints = constraints.drop(lvl)
   }
 
   def check: Option[Boolean] = {
@@ -90,6 +112,36 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
     lastCheckResult = (true, res, model)
   }
 
+  def isValidModel(model: Map[Identifier, Expr], silenceErrors: Boolean = false): Boolean = {
+    import EvaluationResults._
+
+    val expr = And(constraints.flatten)
+
+    val fullModel = variablesOf(expr).map(v => v -> model.getOrElse(v, simplestValue(v.getType))).toMap
+
+    evaluator.eval(expr, fullModel) match {
+      case Successful(BooleanLiteral(true)) =>
+        reporter.debug("- Model validated.")
+        true
+
+      case Successful(BooleanLiteral(false)) =>
+        reporter.debug("- Invalid model.")
+        false
+
+      case RuntimeError(msg) =>
+        reporter.debug("- Model leads to runtime error.")
+        false
+
+      case EvaluatorError(msg) => 
+        if (silenceErrors) {
+          reporter.debug("- Model leads to evaluator error: " + msg)
+        } else {
+          reporter.warning("- Model leads to evaluator error: " + msg)
+        }
+        false
+    }
+  }
+
   def genericCheck(assumptions: Set[Expr]): Option[Boolean] = {
     lastCheckResult = (false, None, None)
 
@@ -99,12 +151,13 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
       solver.push()
       solver.assertCnstr(And((assumptions ++ unrollingBank.currentBlockers).toSeq))
       val res = solver.check
-      solver.pop()
 
       reporter.debug(" - Finished search with blocked literals")
 
       res match {
         case None =>
+          solver.pop()
+
           reporter.ifDebug { debug =>
             reporter.debug("Solver returned unknown!?")
           }
@@ -112,23 +165,29 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
 
         case Some(true) => // SAT
           val model = solver.getModel
+          solver.pop()
 
           foundAnswer(Some(true), Some(model))
 
         case Some(false) if !unrollingBank.canUnroll =>
+          solver.pop()
           foundAnswer(Some(false))
 
         case Some(false) =>
           //debug("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n  AND  \n"))
           //debug("UNSAT BECAUSE: "+core.mkString("  AND  "))
+          solver.pop()
 
           if (!interrupted) {
-            reporter.debug(" - Running search without blocked literals (w/o lucky test)")
+            if (feelingLucky) {
+              reporter.debug(" - Running search without blocked literals (w/ lucky test)")
+            } else {
+              reporter.debug(" - Running search without blocked literals (w/o lucky test)")
+            }
 
             solver.push()
             solver.assertCnstr(And(assumptions.toSeq))
             val res2 = solver.check
-            solver.pop()
 
             res2 match {
               case Some(false) =>
@@ -136,10 +195,19 @@ class UnrollingSolver(val context: LeonContext, underlying: IncrementalSolver)
                 foundAnswer(Some(false))
 
               case Some(true) =>
+                if (feelingLucky && !interrupted) {
+                  val model = solver.getModel
+
+                  // we might have been lucky :D
+                  if (isValidModel(model, silenceErrors = true)) {
+                    foundAnswer(Some(true), Some(model))
+                  }
+                }
 
               case None =>
                 foundAnswer(None)
             }
+            solver.pop()
           }
 
           if(interrupted) {

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala

@@ -13,39 +13,91 @@ import TypeTrees._
 
 import _root_.smtlib.sexpr.SExprs._
 import _root_.smtlib.interpreters.CVC4Interpreter
+import _root_.smtlib.Commands.{Identifier => _, _}
 
 trait SMTLIBCVC4Target extends SMTLIBTarget {
   this: SMTLIBSolver =>
 
-  val targetName = "cvc4"
+  def targetName = "cvc4"
 
   def getNewInterpreter() = new CVC4Interpreter
 
-  val extSym = SSymbol("_")
+  override def declareSort(t: TypeTree): SExpr = {
+    val tpe = normalizeType(t)
+    sorts.cachedB(tpe) {
+      tpe match {
+        case TypeParameter(id) =>
+          val s = id2sym(id)
+          val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s, SInt(0)))
+          sendCommand(cmd)
+          s
+        case SetType(base) =>
+          SList(SSymbol("Set"), declareSort(base))
+        case _ =>
+          super[SMTLIBTarget].declareSort(t)
+      }
+    }
+  }
+
+  override def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
+    case (s: SSymbol, tp: TypeParameter) =>
+      val n = s.s.split("_").toList.last
+      GenericValue(tp, n.toInt)
+
+    case (SList(SSymbol("as") ::  SSymbol("emptyset") :: _), SetType(base)) =>
+      FiniteSet(Seq()).setType(tpe)
+
+    case (SList(SSymbol("setenum") :: elems), SetType(base)) =>
+      FiniteSet(elems.map(fromSMT(_, base))).setType(tpe)
+
+    case (SList(SSymbol("union") :: elems), SetType(base)) =>
+      FiniteSet(elems.map(fromSMT(_, tpe) match {
+        case FiniteSet(elems) => elems
+      }).flatten).setType(tpe)
+
+    case _ =>
+      super[SMTLIBTarget].fromSMT(s, tpe)
+  }
 
   override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
-      case fs @ FiniteSet(elems) =>
-        val ss = declareSort(fs.getType)
-        var res = SList(SSymbol("as"), SSymbol("const"), ss, toSMT(BooleanLiteral(false)))
+    case a @ FiniteArray(elems) =>
+      val tpe @ ArrayType(base) = normalizeType(a.getType)
+      declareSort(tpe)
+
+      var ar: SExpr = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
+
+      for ((e, i) <- elems.zipWithIndex) {
+        ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
+      }
+
+      SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
+
+    /**
+     * ===== Set operations =====
+     */
+    case fs @ FiniteSet(elems) =>
+      if (elems.isEmpty) {
+        SList(SSymbol("as"), SSymbol("emptyset"), declareSort(fs.getType))
+      } else {
+        SList(SSymbol("setenum") :: elems.map(toSMT).toList)
+      }
+
+    case SubsetOf(ss, s) =>
+      SList(SSymbol("subseteq"), toSMT(ss), toSMT(s))
 
-        for (e <- elems) {
-          res = SList(SSymbol("store"), res, toSMT(e), toSMT(BooleanLiteral(true)))
-        }
+    case ElementOfSet(e, s) =>
+      SList(SSymbol("in"), toSMT(e), toSMT(s))
 
-        res
+    case SetDifference(a, b) =>
+      SList(SSymbol("setminus"), toSMT(a), toSMT(b))
 
-      case sd @ SetDifference(a, b) =>
-        // a -- b
-        // becomes:
-        // a && not(b)
-        SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(a), SList(SList(extSym, SSymbol("map"), SSymbol("not")), toSMT(b)))
-      case SetUnion(l, r) =>
-        SList(SList(extSym, SSymbol("map"), SSymbol("or")), toSMT(l), toSMT(r))
+    case SetUnion(a, b) =>
+      SList(SSymbol("union"), toSMT(a), toSMT(b))
 
-      case SetIntersection(l, r) =>
-        SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
+    case SetIntersection(a, b) =>
+      SList(SSymbol("intersection"), toSMT(a), toSMT(b))
 
-      case _ =>
-        super.toSMT(e)
+    case _ =>
+      super[SMTLIBTarget].toSMT(e)
   }
 }

src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

@@ -49,7 +49,15 @@ trait SMTLIBTarget {
     case _ =>   t
   }
 
-  def unsupported(str: Any) = reporter.fatalError(s"Unsupported in $targetName: $str")
+  // Corresponds to a smt map, not a leon/scala array
+  // Should NEVER escape past SMT-world
+  case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree
+
+  // Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array)
+  // Should NEVER escape past SMT-world
+  case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr
+
+  def unsupported(str: Any) = reporter.fatalError(s"Unsupported in smt-$targetName: $str")
 
   def declareSort(t: TypeTree): SExpr = {
     val tpe = normalizeType(t)
@@ -57,17 +65,16 @@ trait SMTLIBTarget {
       tpe match {
         case BooleanType => SSymbol("Bool")
         case Int32Type => SSymbol("Int")
-        case UnitType =>
-          val s = SSymbol("Unit")
-          val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
-          sendCommand(cmd)
-          s
+
+        case RawArrayType(from, to) =>
+          SList(SSymbol("Array"), declareSort(from), declareSort(to))
+
         case TypeParameter(id) =>
           val s = id2sym(id)
           val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
           sendCommand(cmd)
           s
-        case _: ClassType | _: TupleType =>
+        case _: ClassType | _: TupleType | _: ArrayType | UnitType =>
           declareStructuralSort(tpe)
         case _ =>
           unsupported("Sort "+t)
@@ -115,7 +122,7 @@ trait SMTLIBTarget {
           for (ct <- root +: sub; f <- ct.fields) findDependencies(f.tpe)
         }
       case tt @ TupleType(bases) =>
-        if (!(datatypes contains tt) && !(sorts containsA tt)) {
+        if (!(datatypes contains t) && !(sorts containsA t)) {
           val sym = freshSym("tuple"+bases.size)
 
           val c = Constructor(freshSym(sym.s), tt, bases.zipWithIndex.map {
@@ -127,8 +134,27 @@ trait SMTLIBTarget {
           bases.foreach(findDependencies)
         }
 
-      case st @ SetType(base) =>
+      case UnitType =>
+        if (!(datatypes contains t) && !(sorts containsA t)) {
+
+          val sym = freshSym("Unit")
+
+          datatypes += t -> DataType(sym, Seq(Constructor(freshSym(sym.s), t, Nil)))
+        }
+
+      case at @ ArrayType(base) =>
+        if (!(datatypes contains t) && !(sorts containsA t)) {
+          val sym = freshSym("array")
+
+          val c = Constructor(freshSym(sym.s), at, List(
+            (freshSym("size"), Int32Type),
+            (freshSym("content"), RawArrayType(Int32Type, base))
+          ))
 
+          datatypes += at -> DataType(sym, Seq(c))
+
+          findDependencies(base)
+        }
 
       case _ =>
     }
@@ -193,7 +219,11 @@ trait SMTLIBTarget {
         declareSort(e.getType)
         bindings.getOrElse(id, variables.toB(id))
 
-      case IntLiteral(v) => SInt(v)
+      case UnitLiteral() =>
+        declareSort(UnitType)
+        declareVariable(FreshIdentifier("Unit").setType(UnitType))
+
+      case IntLiteral(i) => if (i > 0) SInt(i) else SList(SSymbol("-"), SInt(-i))
       case BooleanLiteral(v) => SSymbol(if (v) "true" else "false")
       case StringLiteral(s) => SString(s)
       case Let(b,d,e) =>
@@ -235,8 +265,26 @@ trait SMTLIBTarget {
 
       case ts @ TupleSelect(t, i) =>
         val tpe = normalizeType(t.getType)
+        declareSort(tpe)
         SList(selectors.toB((tpe, i-1)), toSMT(t))
 
+      case al @ ArrayLength(a) =>
+        val tpe = normalizeType(a.getType)
+        SList(selectors.toB((tpe, 0)), toSMT(a))
+
+      case as @ ArraySelect(a, i) =>
+        val tpe = normalizeType(a.getType)
+        SList(SSymbol("select"), SList(selectors.toB((tpe, 1)), toSMT(a)), toSMT(i))
+
+      case as @ ArrayUpdated(a, i, e) =>
+        val tpe = normalizeType(a.getType)
+
+        val ssize    = SList(selectors.toB((tpe, 0)), toSMT(a))
+        val scontent = SList(selectors.toB((tpe, 1)), toSMT(a))
+
+        SList(constructors.toB(tpe), ssize, SList(SSymbol("store"), scontent, toSMT(i), toSMT(e)))
+
+
       case e @ UnaryOperator(u, _) =>
         val op = e match {
           case _: Not => SSymbol("not")
@@ -281,15 +329,21 @@ trait SMTLIBTarget {
     }
   }
 
-  def extractSpecialSymbols(s: SSymbol): Option[Expr] = {
-    None
+  def fromSMT(pair: (SExpr, TypeTree))(implicit letDefs: Map[SSymbol, SExpr]): Expr = {
+    fromSMT(pair._1, pair._2)
   }
 
-  def fromSMT(s: SExpr)(implicit bindings: Map[SSymbol, Expr]): Expr = s match {
-    case SInt(n)          => IntLiteral(n.toInt)
-    case SSymbol("true")  => BooleanLiteral(true)
-    case SSymbol("false") => BooleanLiteral(false)
-    case s: SSymbol if constructors.containsB(s) =>
+  def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
+    case (_, UnitType) =>
+      UnitLiteral()
+
+    case (SInt(n), Int32Type) =>
+      IntLiteral(n.toInt)
+
+    case (SSymbol(s), BooleanType)  =>
+      BooleanLiteral(s == "true")
+
+    case (s: SSymbol, _: ClassType) if constructors.containsB(s) =>
       constructors.toA(s) match {
         case cct: CaseClassType =>
           CaseClass(cct, Nil)
@@ -297,42 +351,51 @@ trait SMTLIBTarget {
           unsupported("woot? for a single constructor for non-case-object: "+t)
       }
 
-    case s: SSymbol =>
-      (bindings.get(s) orElse variables.getA(s).map(_.toVariable)
-                       orElse extractSpecialSymbols(s)).getOrElse {
+    case (s: SSymbol, tpe) if letDefs contains s =>
+      fromSMT(letDefs(s), tpe)
+
+    case (s: SSymbol, _) =>
+      variables.getA(s).map(_.toVariable).getOrElse {
         unsupported("Unknown symbol: "+s)
       }
 
-    case SList((s: SSymbol) :: args) if(constructors.containsB(s)) => 
-      val rargs = args.map(fromSMT)
+    case (SList((s: SSymbol) :: args), tpe) if constructors.containsB(s) =>
       constructors.toA(s) match {
         case cct: CaseClassType =>
+          val rargs = args.zip(cct.fields.map(_.tpe)).map(fromSMT)
           CaseClass(cct, rargs)
         case tt: TupleType =>
+          val rargs = args.zip(tt.bases).map(fromSMT)
           Tuple(rargs)
+
+        case at: ArrayType =>
+          val IntLiteral(size)                 = fromSMT(args(0), Int32Type)
+          val RawArrayValue(_, elems, default) = fromSMT(args(1), RawArrayType(Int32Type, at.base))
+
+          val entries = for (i <- 0 to size-1) yield elems.getOrElse(IntLiteral(i), default)
+
+          FiniteArray(entries).setType(at)
+
         case t =>
           unsupported("Woot? structural type that is non-structural: "+t)
       }
 
-    case SList(List(SSymbol("let"), SList(defs), body)) =>
-      val leonDefs: Seq[(SSymbol, Identifier, Expr)] = defs.map {
+    // EK: Since we have no type information, we cannot do type-directed
+    // extraction of defs, instead, we expand them in smt-world
+    case (SList(List(SSymbol("let"), SList(defs), body)), tpe) =>
+      val defsMap: Map[SSymbol, SExpr] = defs.map {
         case SList(List(s : SSymbol, value)) =>
-          (s, FreshIdentifier(s.s), fromSMT(value))
-      }
+          (s, value)
+      }.toMap
 
-      val newBindings = bindings ++ leonDefs.map(d => d._1 -> d._3)
-      val newBody = fromSMT(body)(newBindings)
-
-      LetTuple(leonDefs.map(_._2), Tuple(leonDefs.map(_._3)), newBody)
-
-    case SList(SSymbol(app) :: args) => {
-      val recArgs = args.map(fromSMT)
+      fromSMT(body, tpe)(letDefs ++ defsMap)
 
+    case (SList(SSymbol(app) :: args), tpe) => {
       app match {
         case "-" =>
-          recArgs match {
-            case List(a) => UMinus(a)
-            case List(a, b) => Minus(a, b)
+          args match {
+            case List(a) => UMinus(fromSMT(a, Int32Type))
+            case List(a, b) => Minus(fromSMT(a, Int32Type), fromSMT(b, Int32Type))
           }
 
         case _ =>
@@ -350,9 +413,11 @@ trait SMTLIBTarget {
       out.flush
     }
 
-    val response = interpreter.eval(cmd)
-    assert(!response.isInstanceOf[Error])
-    response
+    interpreter.eval(cmd) match {
+      case ErrorResponse(msg) =>
+        reporter.fatalError("Unnexpected error from smt-"+targetName+" solver: "+msg)
+      case res => res
+    }
   }
 
   override def assertCnstr(expr: Expr): Unit = {
@@ -375,7 +440,9 @@ trait SMTLIBTarget {
 
     valuationPairs.collect {
       case (sym: SSymbol, value) if variables.containsB(sym) =>
-        (variables.toA(sym), fromSMT(value)(Map()))
+        val id = variables.toA(sym)
+
+        (id, fromSMT(value, id.getType)(Map()))
     }.toMap
   }
 

src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala

@@ -10,6 +10,7 @@ import Common._
 import Trees._
 import Extractors._
 import TypeTrees._
+import TreeOps.simplestValue
 
 import _root_.smtlib.sexpr.SExprs._
 import _root_.smtlib.interpreters.Z3Interpreter
@@ -26,14 +27,19 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
   val extSym = SSymbol("_")
 
   var setSort: Option[SSymbol] = None
+  var mapSort: Option[SSymbol] = None
+  var optionSort: Option[SSymbol] = None
 
   override def declareSort(t: TypeTree): SExpr = {
     val tpe = normalizeType(t)
     sorts.cachedB(tpe) {
       tpe match {
+        case MapType(from, to) =>
+          declareMapSort(from, to)
         case SetType(base) =>
           declareSetSort(base)
-        case _ => super.declareSort(t)
+        case _ =>
+          super.declareSort(t)
       }
     }
   }
@@ -53,35 +59,108 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
     SList(setSort.get, declareSort(of))
   }
 
-  override def extractSpecialSymbols(s: SSymbol): Option[Expr] = {
-    s.s.split("!").toList.reverse match {
-      case n :: "val" :: rest =>
-        val sort = rest.reverse.mkString("!")
+  def declareOptionSort(of: TypeTree) = {
+    optionSort match {
+      case None =>
+        val t      = SSymbol("T")
 
-        sorts.getA(SSymbol(sort)) match {
-          case Some(tp : TypeParameter) =>
-            Some(GenericValue(tp, n.toInt))
-          case _ =>
-            None
-        }
+        val s      = SSymbol("Option")
+        val some   = SSymbol("Some")
+        val some_v = SSymbol("Some_v")
+        val none   = SSymbol("None")
+
+        val caseSome = SList(some, SList(some_v, t))
+        val caseNone = none
+
+        val cmd = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(t), SList(SList(s, caseSome, caseNone))))
+        sendCommand(cmd)
+
+        optionSort = Some(s)
+      case _ =>
+    }
+
+    SList(optionSort.get, declareSort(of))
+  }
+
+  def declareMapSort(from: TypeTree, to: TypeTree) = {
+    mapSort match {
+      case None =>
+        val m = SSymbol("Map")
+        val a = SSymbol("A")
+        val b = SSymbol("B")
+        mapSort = Some(m)
+        declareOptionSort(to)
+
+        val cmd = NonStandardCommand(SList(SSymbol("define-sort"), m, SList(a, b), SList(SSymbol("Array"), a, SList(optionSort.get, b))))
+        sendCommand(cmd)
       case _ =>
-        None
     }
+
+    SList(mapSort.get, declareSort(from), declareSort(to))
   }
 
-  override def fromSMT(s: SExpr)(implicit bindings: Map[SSymbol, Expr]): Expr = s match {
-    case SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)) =>
-      bindings(k)
+  override def fromSMT(s: SExpr, tpe: TypeTree)(implicit letDefs: Map[SSymbol, SExpr]): Expr = (s, tpe) match {
+    case (s: SSymbol, tp: TypeParameter) =>
+      val n = s.s.split("!").toList.last
+      GenericValue(tp, n.toInt)
+
+
+    case (SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)), tpe) =>
+      if (letDefs contains k) {
+        // Need to recover value form function model
+        fromRawArray(extractRawArray(letDefs(k)), tpe)
+      } else {
+        unsupported(" as-array on non-function or unknown symbol "+k)
+      }
 
     // SMT representation for empty sets: Array(* -> false)
-    case SList(List(SList(List(SSymbol("as"), SSymbol("const"), SList(List(SSymbol("Array"), s, SSymbol("Bool"))))), SSymbol("false"))) =>
-      FiniteSet(Nil).setType(sorts.fromB(s))
+    case (SList(List(SList(List(SSymbol("as"), SSymbol("const"), SList(List(SSymbol("Array"), k, v)))), defV)), tpe) =>
+      val ktpe = sorts.fromB(k)
+      val vtpe = sorts.fromB(v)
+
+      fromRawArray(RawArrayValue(ktpe, Map(), fromSMT(defV, vtpe)), tpe)
 
     case _ =>
-      super.fromSMT(s)
+      super[SMTLIBTarget].fromSMT(s, tpe)
   }
 
   override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
+      case a @ FiniteArray(elems) =>
+        val tpe @ ArrayType(base) = normalizeType(a.getType)
+        declareSort(tpe)
+
+        var ar = SList(SList(SSymbol("as"), SSymbol("const"), declareSort(RawArrayType(Int32Type, base))), toSMT(simplestValue(base)))
+
+        for ((e, i) <- elems.zipWithIndex) {
+          ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
+        }
+
+        SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
+
+      /**
+       * ===== Map operations =====
+       */
+      case MapGet(m, k) =>
+        declareSort(m.getType)
+        SList(SSymbol("Some_v"), SList(SSymbol("select"), toSMT(m), toSMT(k)))
+
+      case MapIsDefinedAt(m, k) =>
+        declareSort(m.getType)
+        SList(SSymbol("is-Some"), SList(SSymbol("select"), toSMT(m), toSMT(k)))
+
+      case m @ FiniteMap(elems) =>
+        val ms = declareSort(m.getType)
+
+        var res = SList(SList(SSymbol("as"), SSymbol("const"), ms), SSymbol("None"))
+        for ((k, v) <- elems) {
+          res = SList(SSymbol("store"), res, toSMT(k), SList(SSymbol("Some"), toSMT(v)))
+        }
+
+        res
+
+      /**
+       * ===== Set operations =====
+       */
       case fs @ FiniteSet(elems) =>
         val ss = declareSort(fs.getType)
         var res = SList(SList(SSymbol("as"), SSymbol("const"), ss), toSMT(BooleanLiteral(false)))
@@ -92,7 +171,17 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
 
         res
 
-      case sd @ SetDifference(a, b) =>
+      case SubsetOf(ss, s) =>
+        // a isSubset b   ==>   (a zip b).map(implies) == (* => true)
+        val allTrue    = SList(SList(SSymbol("as"), SSymbol("const"), declareSort(s.getType)), SSymbol("true"))
+        val mapImplies = SList(SList(extSym, SSymbol("map"), SSymbol("implies")), toSMT(ss), toSMT(s))
+
+        SList(SSymbol("="), mapImplies, allTrue)
+
+      case ElementOfSet(e, s) =>
+        SList(SSymbol("select"), toSMT(s), toSMT(e))
+
+      case SetDifference(a, b) =>
         // a -- b
         // becomes:
         // a && not(b)
@@ -107,7 +196,40 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
         super.toSMT(e)
   }
 
-  // We use get-model instead
+  def extractRawArray(s: SExpr)(implicit letDefs: Map[SSymbol, SExpr]): RawArrayValue = s match {
+    case SList(List(SSymbol("define-fun"), a: SSymbol, SList(SList(List(arg, akind)) :: Nil), rkind, body)) =>
+      val argTpe = sorts.toA(akind)
+      val retTpe = sorts.toA(rkind)
+
+      def extractCases(e: SExpr): (Map[Expr, Expr], Expr) = e match {
+        case SList(SSymbol("ite") :: SList(SSymbol("=") :: `arg` :: k :: Nil) :: v :: e :: Nil) =>
+          val (cs, d) = extractCases(e)
+          (Map(fromSMT(k, argTpe) -> fromSMT(v, retTpe)) ++ cs, d)
+        case e =>
+          (Map(),fromSMT(e, retTpe))
+      }
+
+      val (cases, default) = extractCases(body)
+
+      RawArrayValue(argTpe, cases, default)
+    case _ =>
+      unsupported("Unable to extract "+s)
+  }
+
+  def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
+    case SetType(base) =>
+      assert(r.default == BooleanLiteral(false) && r.keyTpe == base)
+
+      FiniteSet(r.elems.keySet.toSeq).setType(tpe)
+
+    case RawArrayType(from, to) =>
+      r
+
+    case _ =>
+      unsupported("Unable to extract from raw array for "+tpe)
+  }
+
+  // EK: We use get-model instead in order to extract models for arrays
   override def getModel: Map[Identifier, Expr] = {
 
     val cmd = NonStandardCommand(SList(SSymbol("get-model")))
@@ -119,40 +241,12 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
       case _ => Nil
     }
 
-    var maps = Map[SSymbol, TypeTree]()
+    var modelFunDefs = Map[SSymbol, SExpr]()
 
     // First pass to gather functions (arrays defs)
     for (me <- smodel) me match {
-      case SList(List(SSymbol("define-fun"), a: SSymbol, SList(Nil), _, SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)))) =>
-        maps += k -> variables.toA(a).getType
-      case _ =>
-    }
-
-    var bindings = Map[SSymbol, Expr]()
-
-    // Second pass to gather functions (arrays defs)
-    for (me <- smodel) me match {
-      case SList(List(SSymbol("define-fun"), s: SSymbol, SList(SList(List(arg, _)) :: Nil), _, e)) if maps contains s =>
-        def extractCases(e: SExpr): (Map[Expr, Expr], Expr) = e match {
-          case SList(SSymbol("ite") :: SList(SSymbol("=") :: `arg` :: k :: Nil) :: v :: e :: Nil) =>
-            val (cs, d) = extractCases(e)
-            (Map(fromSMT(k)(Map()) -> fromSMT(v)(Map())) ++ cs, d)
-          case e =>
-            (Map(),fromSMT(e)(Map()))
-        }
-
-        def buildValue(cases: Map[Expr, Expr], default: Expr, tpe: TypeTree): Expr = tpe match {
-          case SetType(base) =>
-            assert(default == BooleanLiteral(false))
-            FiniteSet(cases.keySet.toSeq).setType(tpe)
-          case _ =>
-            unsupported("Cannot build array/map model to "+tpe)
-        }
-
-        val tpe = maps(s)
-        val (cases, default) = extractCases(e)
-
-        bindings += s -> buildValue(cases, default, tpe)
+      case SList(List(SSymbol("define-fun"), a: SSymbol, SList(args), _, _)) if args.nonEmpty =>
+        modelFunDefs += a -> me
       case _ =>
     }
 
@@ -161,7 +255,9 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
     for (me <- smodel) me match {
       case SList(List(SSymbol("define-fun"), s: SSymbol, SList(args), kind, e)) =>
         if (args.isEmpty) {
-          model += variables.toA(s) -> fromSMT(e)(bindings)
+          val id = variables.toA(s)
+          // EK: this is a little hack, we pass models for array functions as let-defs
+          model += id -> fromSMT(e, id.getType)(modelFunDefs)
         }
 
       case SList(SSymbol("forall") :: _) => // no body

src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala

@@ -10,6 +10,8 @@ import leon.verification.{AnalysisPhase,VerificationReport}
 import leon.frontends.scalac.ExtractionPhase
 import leon.utils.PreprocessingPhase
 
+import _root_.smtlib.interpreters._
+
 import java.io.File
 
 class PureScalaVerificationRegression extends LeonTestSuite {
@@ -48,7 +50,6 @@ class PureScalaVerificationRegression extends LeonTestSuite {
           pipeline.run(ctx)(file.getPath :: Nil)
         }
       } else {
-
         val report = pipeline.run(ctx)(file.getPath :: Nil)
 
         block(Output(report, ctx.reporter))
@@ -61,11 +62,33 @@ class PureScalaVerificationRegression extends LeonTestSuite {
       "regression/verification/purescala/" + cat,
       _.endsWith(".scala"))
 
+    val isZ3Available = try {
+      new Z3Interpreter()
+      true
+    } catch {
+      case e: java.io.IOException =>
+        false
+    }
+
+    val isCVC4Available = try {
+      //new CVC4Interpreter()
+      // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
+      false
+    } catch {
+      case e: java.io.IOException =>
+        false
+    }
+
     for(f <- fs) {
       mkTest(f, List("--feelinglucky", "--library=no"), forError)(block)
       mkTest(f, List("--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
       mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
-      mkTest(f, List("--solvers=smt-z3", "--library=no"), forError)(block)
+      if (isZ3Available) {
+        mkTest(f, List("--solvers=smt-z3", "--feelinglucky", "--library=no"), forError)(block)
+      }
+      if (isCVC4Available) {
+        mkTest(f, List("--solvers=smt-cvc4", "--feelinglucky", "--library=no"), forError)(block)
+      }
     }
   }