Merge pull request #159 from jad-hamza/strings

Add string parsing alternative for Z3 4.8.12 + Respect timeouts/interrupts in non-incremental solver

Author: samarion

src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala

@@ -25,41 +25,55 @@ trait NonIncrementalSolver extends AbstractSolver { self =>
   def assertCnstr(expression: Trees): Unit = assertions += expression
   def reset(): Unit = assertions.clear()
   def free(): Unit = for (solver <- currentSolver) solver.free()
-  def interrupt(): Unit = for (solver <- currentSolver) solver.interrupt()
+
+  var interrupted = false
+
+  def interrupt(): Unit = {
+    interrupted = true
+    for (solver <- currentSolver) solver.interrupt()
+  }
 
   override def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
-    assert(currentSolver.isEmpty,
-      "`currentSolver` should be empty when invoking `check` in NonIncrementalSolver")
-    val newSolver = underlying()
-    try {
-      currentSolver = Some(newSolver)
-      for (expression <- assertions)
-        newSolver.assertCnstr(expression)
-      val res = newSolver.check(config)
-      currentSolver = None
-      res
-    } finally {
-      newSolver.free()
+    if (!interrupted) {
+      assert(currentSolver.isEmpty,
+        "`currentSolver` should be empty when invoking `check` in NonIncrementalSolver")
+      val newSolver = underlying()
+      try {
+        currentSolver = Some(newSolver)
+        for (expression <- assertions)
+          newSolver.assertCnstr(expression)
+        val res = newSolver.check(config)
+        currentSolver = None
+        res
+      } finally {
+        newSolver.free()
+      }
+    } else {
+      config.cast(SolverResponses.Unknown)
     }
   }
 
   override def checkAssumptions(config: Configuration)
                                (assumptions: Set[Trees]): config.Response[Model, Assumptions] = {
-    assert(currentSolver.isEmpty,
-      "`currentSolver` should be empty when invoking `checkAssumptions` in NonIncrementalSolver")
-    val newSolver = underlying()
-    try {
-      currentSolver = Some(newSolver)
-      for (expression <- assertions)
-        newSolver.assertCnstr(expression)
-      // we assert the assumptions to address: https://github.com/Z3Prover/z3/issues/5257
-      for (assumption <- assumptions)
-        newSolver.assertCnstr(assumption)
-      val res = newSolver.checkAssumptions(config)(Set())
-      currentSolver = None
-      res
-    } finally {
-      newSolver.free()
+    if (!interrupted) {
+      assert(currentSolver.isEmpty,
+        "`currentSolver` should be empty when invoking `checkAssumptions` in NonIncrementalSolver")
+      val newSolver = underlying()
+      try {
+        currentSolver = Some(newSolver)
+        for (expression <- assertions)
+          newSolver.assertCnstr(expression)
+        // we assert the assumptions to address: https://github.com/Z3Prover/z3/issues/5257
+        for (assumption <- assumptions)
+          newSolver.assertCnstr(assumption)
+        val res = newSolver.checkAssumptions(config)(Set())
+        currentSolver = None
+        res
+      } finally {
+        newSolver.free()
+      }
+    } else {
+      config.cast(SolverResponses.Unknown)
     }
   }
 

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

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

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

@@ -153,11 +153,17 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
       case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), Seq(SHexadecimal(hex))), _) =>
         StringLiteral(utils.StringUtils.decode(hex.repr))
 
+      case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), args), Some(StringType())) =>
+        StringLiteral(args.map(fromSMT(_, Some(CharType())).asInstanceOf[CharLiteral].value).mkString)
+
       case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("str.++")), None), strs), _) =>
         val strings = strs.map(fromSMT(_, Some(StringType())))
         if (strings.isEmpty) StringLiteral("")
         else strings.tail.foldRight(strings.head)(StringConcat(_, _))
 
+      case (QualifiedIdentifier(SMTIdentifier(SSymbol("Char"), Seq(SNumeral(n))), None), Some(CharType())) =>
+        CharLiteral(n.toChar)
+
       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))