Support get-model for arrays in z3-smt

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 = "d4622f38a04a191798eb29f39d3c8b2ec312e811"
+    private val scalaSmtLibVersion = "90f66cf07aef34b05dc5585bb35aca773b3d0d43"
     lazy val scalaSmtLib = RootProject(uri("git://github.com/regb/scala-smtlib.git#%s".format(scalaSmtLibVersion)))
   }
 }

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

@@ -100,7 +100,7 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
               reporter.debug(" - more unrollings")
               val newClauses = unrollOneStep()
               reporter.debug(s"   - ${newClauses.size} new clauses")
-              readLine()
+              //readLine()
               solver.assertCnstr(And(newClauses))
           }
 

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

@@ -13,11 +13,6 @@ import TreeOps._
 import TypeTrees._
 import Definitions._
 
-import _root_.smtlib.{PrettyPrinter => SMTPrinter, Interpreter => SMTInterpreter}
-import _root_.smtlib.Commands.{Identifier => _, Assert => SMTAssert, _}
-import _root_.smtlib.CommandResponses.{Error => ErrorResponse, _}
-import _root_.smtlib.sexpr.SExprs._
-import _root_.smtlib.interpreters._
 
 abstract class SMTLIBSolver(val context: LeonContext,
                             val program: Program)
@@ -28,41 +23,15 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
   override def name: String = "smt-"+targetName
 
-  override def assertCnstr(expr: Expr): Unit = {
-    variablesOf(expr).foreach(declareVariable)
-    val sexpr = toSMT(expr)(Map())
-    sendCommand(SMTAssert(sexpr))
-  }
-
-  override def check: Option[Boolean] = sendCommand(CheckSat) match {
-    case CheckSatResponse(SatStatus)     => Some(true)
-    case CheckSatResponse(UnsatStatus)   => Some(false)
-    case CheckSatResponse(UnknownStatus) => None
-  }
-
-  override def getModel: Map[Identifier, Expr] = {
-    val syms = variables.bSet.toList
-    val cmd: Command = GetValue(syms.head, syms.tail)
-
-    val GetValueResponse(valuationPairs) = sendCommand(cmd)
-
-    valuationPairs.collect {
-      case (sym: SSymbol, value) if variables.containsB(sym) =>
-        //println("Getting model for "+sym)
-        //println("Value "+value)
-        (variables.toA(sym), fromSMT(value)(Map()))
-    }.toMap
-  }
+  /**
+   * Most of the solver functionality is defined, and thus extensible, in
+   * SMTLIBTarget, which gets specialized based on how individual solvers
+   * diverge from the SMTLib standard.
+   */
 
   override def free() = {
     interpreter.free()
     out.close
   }
 
-  override def push(): Unit = {
-    sendCommand(Push(1))
-  }
-  override def pop(lvl: Int = 1): Unit = {
-    sendCommand(Pop(1))
-  }
 }

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

@@ -28,12 +28,12 @@ trait SMTLIBTarget {
 
   val interpreter = getNewInterpreter()
 
-  val out = new java.io.FileWriter(s"vcs-$targetName.log", true)
+  val out = new java.io.FileWriter(s"vcs-$targetName.smt2", true)
   reporter.ifDebug { debug =>
     out.write("; -----------------------------------------------------\n")
   }
 
-  def id2sym(id: Identifier): SSymbol = SSymbol(id.name.toUpperCase+"!"+id.globalId)
+  def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.globalId)
 
   // metadata for CC, and variables
   val constructors = new Bijection[TypeTree, SSymbol]()
@@ -57,6 +57,11 @@ 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 TypeParameter(id) =>
           val s = id2sym(id)
           val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
@@ -276,10 +281,14 @@ trait SMTLIBTarget {
     }
   }
 
+  def extractSpecialSymbols(s: SSymbol): Option[Expr] = {
+    None
+  }
+
   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 SSymbol("true")  => BooleanLiteral(true)
+    case SSymbol("false") => BooleanLiteral(false)
     case s: SSymbol if constructors.containsB(s) =>
       constructors.toA(s) match {
         case cct: CaseClassType =>
@@ -289,8 +298,10 @@ trait SMTLIBTarget {
       }
 
     case s: SSymbol =>
-      println(s)
-      bindings.getOrElse(s, variables.fromB(s).toVariable)
+      (bindings.get(s) orElse variables.getA(s).map(_.toVariable)
+                       orElse extractSpecialSymbols(s)).getOrElse {
+        unsupported("Unknown symbol: "+s)
+      }
 
     case SList((s: SSymbol) :: args) if(constructors.containsB(s)) => 
       val rargs = args.map(fromSMT)
@@ -303,7 +314,7 @@ trait SMTLIBTarget {
           unsupported("Woot? structural type that is non-structural: "+t)
       }
 
-    case SList(List(SSymbol("LET"), SList(defs), body)) =>
+    case SList(List(SSymbol("let"), SList(defs), body)) =>
       val leonDefs: Seq[(SSymbol, Identifier, Expr)] = defs.map {
         case SList(List(s : SSymbol, value)) =>
           (s, FreshIdentifier(s.s), fromSMT(value))
@@ -343,4 +354,35 @@ trait SMTLIBTarget {
     assert(!response.isInstanceOf[Error])
     response
   }
+
+  override def assertCnstr(expr: Expr): Unit = {
+    variablesOf(expr).foreach(declareVariable)
+    val sexpr = toSMT(expr)(Map())
+    sendCommand(Assert(sexpr))
+  }
+
+  override def check: Option[Boolean] = sendCommand(CheckSat) match {
+    case CheckSatResponse(SatStatus)     => Some(true)
+    case CheckSatResponse(UnsatStatus)   => Some(false)
+    case CheckSatResponse(UnknownStatus) => None
+  }
+
+  override def getModel: Map[Identifier, Expr] = {
+    val syms = variables.bSet.toList
+    val cmd: Command = GetValue(syms.head, syms.tail)
+
+    val GetValueResponse(valuationPairs) = sendCommand(cmd)
+
+    valuationPairs.collect {
+      case (sym: SSymbol, value) if variables.containsB(sym) =>
+        (variables.toA(sym), fromSMT(value)(Map()))
+    }.toMap
+  }
+
+  override def push(): Unit = {
+    sendCommand(Push(1))
+  }
+  override def pop(lvl: Int = 1): Unit = {
+    sendCommand(Pop(1))
+  }
 }

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

@@ -13,8 +13,8 @@ import TypeTrees._
 
 import _root_.smtlib.sexpr.SExprs._
 import _root_.smtlib.interpreters.Z3Interpreter
-
-import _root_.smtlib.Commands.NonStandardCommand
+import _root_.smtlib.Commands.{GetValue, NonStandardCommand}
+import _root_.smtlib.CommandResponses.SExprResponse
 
 trait SMTLIBZ3Target extends SMTLIBTarget {
   this: SMTLIBSolver =>
@@ -53,6 +53,33 @@ 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("!")
+
+        sorts.getA(SSymbol(sort)) match {
+          case Some(tp : TypeParameter) =>
+            Some(GenericValue(tp, n.toInt))
+          case _ =>
+            None
+        }
+      case _ =>
+        None
+    }
+  }
+
+  override def fromSMT(s: SExpr)(implicit bindings: Map[SSymbol, Expr]): Expr = s match {
+    case SList(List(`extSym`, SSymbol("as-array"), k: SSymbol)) =>
+      bindings(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 _ =>
+      super.fromSMT(s)
+  }
 
   override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
       case fs @ FiniteSet(elems) =>
@@ -79,4 +106,75 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
       case _ =>
         super.toSMT(e)
   }
+
+  // We use get-model instead
+  override def getModel: Map[Identifier, Expr] = {
+
+    val cmd = NonStandardCommand(SList(SSymbol("get-model")))
+
+    val res = sendCommand(cmd)
+
+    val smodel = res match {
+      case SExprResponse(SList(SSymbol("model") :: entries)) => entries
+      case _ => Nil
+    }
+
+    var maps = Map[SSymbol, TypeTree]()
+
+    // 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 _ =>
+    }
+
+    var model = Map[Identifier, Expr]()
+
+    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)
+        }
+
+      case SList(SSymbol("forall") :: _) => // no body
+        // Ignore
+
+      case SList(SSymbol("declare-fun") :: _) => // no body
+        // Ignore
+
+      case _ =>
+        unsupported("Unknown model entry: "+me)
+    }
+
+
+    model
+  }
 }

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -558,7 +558,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
               solver.assertCnstr(ncl)
             }
 
-            readLine()
+            //readLine()
 
             reporter.debug(" - finished unrolling")
           }