Merge pull request #141 from jad-hamza/smt-parsing

Add model extraction for #unspecified and seq.unit

Author: samarion

build.sbt

@@ -45,7 +45,7 @@ libraryDependencies ++= Seq(
 
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 // lazy val smtlib = RootProject(file("../scala-smtlib"))
-lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "5b9503e13d69c7116039a243025b2ce657c32c77")
+lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "95b5d1ed2ee9c0c1ec5cabb3c0303d27a48131cd")
 
 lazy val scriptName = settingKey[String]("Name of the generated 'inox' script")
 

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

@@ -25,12 +25,8 @@ class TipTestSuite extends TestSuite with ResourceUtils {
   private def ignoreSAT(ctx: Context, file: java.io.File): FilterStatus = 
     ctx.options.findOptionOrDefault(optSelectedSolvers).headOption match {
       case Some(solver) => (solver, file.getName) match {
-        // test containing list of booleans, so CVC4 will crash on this
-        // See http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=500
-        case ("smt-cvc4", "List-fold.tip") => Skip
         // Z3 and CVC4 binaries are exceedingly slow on these benchmarks
-        case ("smt-z3" | "smt-cvc4", "BinarySearchTreeQuant.scala-2.tip") => Ignore
-        case ("smt-z3" | "smt-cvc4", "ForallAssoc.scala-0.tip") => Ignore
+        case ("no-inc:smt-z3" | "smt-z3" | "smt-cvc4", "ForallAssoc.scala-0.tip") => Ignore
         // this test only holds when assumeChecked=false
         case (_, "LambdaEquality2.scala-1.tip") if ctx.options.findOptionOrDefault(optAssumeChecked) => Skip
         case _ => Test

src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala

@@ -224,7 +224,7 @@ trait SMTLIBParser {
       val MapType(from, to) = fromSMT(sort)
       FiniteMap(Seq.empty, d, from, to)
 
-    case _ => throw new MissformedSMTException(term, "Unknown SMT term")
+    case _ => throw new MissformedSMTException(term, "Unknown SMT term of class: " + term.getClass)
   }
 
   protected def fromSMT(sort: Sort)(implicit context: Context): Type = sort match {

src/main/scala/inox/solvers/smtlib/Z3Target.scala

@@ -144,6 +144,15 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
             unsupported(t, "woot? tester for non-adt type")
         }
 
+      case (QualifiedIdentifier(SimpleIdentifier(SSymbol("#unspecified")), None), None) =>
+        throw new MissformedSMTException(t, "Cannot extract #unspecified symbol when type is unknown")
+
+      case (QualifiedIdentifier(SimpleIdentifier(SSymbol("#unspecified")), None), Some(tpe)) =>
+        Choose(ValDef.fresh("unspecified", tpe), BooleanLiteral(true))
+
+      case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), Seq(SHexadecimal(hex))), _) =>
+        StringLiteral(utils.StringUtils.decode(hex.repr))
+
       case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe @ MapType(keyType, valueType))) =>
         val Some(Lambda(Seq(arg), body)) = context.getFunction(k, FunctionType(Seq(keyType), valueType))