Merge pull request #127 from polgreen/smtlib-printing

Added printing for SMTLIBInterface.
uclid-org · Nov 9, 2019 · e5f3354 · e5f3354
2 parents f5ce7ba + ec5e306
commit e5f3354
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 21 deletions.
diff --git a/src/main/scala/uclid/InteractiveProcess.scala b/src/main/scala/uclid/InteractiveProcess.scala
@@ -43,7 +43,7 @@ import scala.concurrent.SyncChannel
 import scala.collection.JavaConverters._
 import com.typesafe.scalalogging.Logger
 
-class InteractiveProcess(args: List[String]) {
+class InteractiveProcess(args: List[String], saveInput: Boolean=false) {
   val logger = Logger(classOf[InteractiveProcess])
 
   // create the process.
@@ -55,6 +55,10 @@ class InteractiveProcess(args: List[String]) {
   val in = process.getOutputStream()
   var exitValue : Option[Int] = None
 
+  // stores what we've written to the interactive process so far
+  var inputString = ""
+  override def toString() = inputString
+
   // channels for input and output.
   val inputChannel = new SyncChannel[Option[String]]()
   val outputChannel = new SyncChannel[Option[String]]()
@@ -75,14 +79,17 @@ class InteractiveProcess(args: List[String]) {
   def writeInput(str: String) {
     logger.debug("-> {}", str)
     in.write(stringToBytes(str))
+    if (saveInput) inputString += str + "\n"
   }
   // Close stdin, this may cause the process to exit.
   def finishInput() {
     in.flush()
+    inputString = ""
     in.close()
   }
   // Read from the process's output stream.
   def readOutput() : Option[String] = {
+    inputString = ""
     in.flush()
     var done = false
     while (!done) {

diff --git a/src/main/scala/uclid/Utils.scala b/src/main/scala/uclid/Utils.scala
@@ -40,8 +40,15 @@ package uclid
 
 import scala.util.parsing.input.Position
 import com.typesafe.scalalogging.Logger
+import java.io.File
+import java.io.PrintWriter
 
 object Utils {
+  def writeToFile(p: String, s: String): Unit = {
+    val pw = new PrintWriter(new File(p.replace(" ", "_")))
+    try pw.write(s) finally pw.close()
+  }
+
   def assert(b: Boolean, err: => String /* error may be lazily computed. */) : Unit = {
     if (!b) {
       throw new AssertionError(err)

diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala
@@ -310,7 +310,7 @@ class SMTLIB2Interface(args: List[String]) extends Context with SMTLIB2Base {
 
   type NameProviderFn = (String, Option[String]) => String
   var expressions : List[Expr] = List.empty
-  val solverProcess = new InteractiveProcess(args)
+  val solverProcess = new InteractiveProcess(args, true)
 
   def generateDeclaration(name: String, t: Type) = {
     val (typeName, newTypes) = generateDatatype(t)
@@ -362,17 +362,24 @@ class SMTLIB2Interface(args: List[String]) extends Context with SMTLIB2Base {
     smtlibInterfaceLogger.debug("check")
     Utils.assert(solverProcess.isAlive(), "Solver process is not alive!")
     writeCommand("(check-sat)")
-    readResponse() match {
-      case Some(strP) =>
-        val str = strP.stripLineEnd
-        str match {
-          case "sat" => SolverResult(Some(true), getModel())
-          case "unsat" => SolverResult(Some(false), None)
-          case _ =>
-            throw new Utils.AssertionError("Unexpected result from SMT solver: " + str.toString())
-        }
-      case None =>
-        throw new Utils.AssertionError("Unexpected EOF result from SMT solver.")
+    if (filePrefix == "") {
+      readResponse() match {
+        case Some(strP) =>
+          val str = strP.stripLineEnd
+          str match {
+            case "sat" => SolverResult(Some(true), getModel())
+            case "unsat" => SolverResult(Some(false), None)
+            case _ =>
+              throw new Utils.AssertionError("Unexpected result from SMT solver: " + str.toString())
+          }
+        case None =>
+          throw new Utils.AssertionError("Unexpected EOF result from SMT solver.")
+      }
+    } else {
+      val smtOutput = solverProcess.toString()
+      Utils.writeToFile(f"$filePrefix%s-$curAssertName%s-$curAssertLabel%s-$counten%04d.smt", smtOutput + "\n\n(check-sat)\n(get-info :all-statistics)\n")
+      counten += 1
+      return SolverResult(None, None)
     }
   }
 

diff --git a/src/main/scala/uclid/smt/Z3Interface.scala b/src/main/scala/uclid/smt/Z3Interface.scala
@@ -49,8 +49,6 @@ import scala.collection.JavaConverters._
 import com.microsoft.z3.enumerations.Z3_lbool
 import com.microsoft.z3.enumerations.Z3_decl_kind
 import com.typesafe.scalalogging.Logger
-import java.io.File
-import java.io.PrintWriter
 
 
 /**
@@ -492,11 +490,6 @@ class Z3Interface() extends Context {
   }
   override def preassert(e: Expr) {}
 
-  def writeToFile(p: String, s: String): Unit = {
-    val pw = new PrintWriter(new File(p.replace(" ", "_")))
-    try pw.write(s) finally pw.close()
-  }
-
   lazy val checkLogger = Logger("uclid.smt.Z3Interface.check")
   /** Check whether a particular expression is satisfiable.  */
   override def check() : SolverResult = {
@@ -521,7 +514,7 @@ class Z3Interface() extends Context {
       }
       return checkResult
     } else {
-      writeToFile(f"$filePrefix%s-$curAssertName%s-$curAssertLabel%s-$counten%04d.smt", smtOutput + "\n\n(check-sat)\n(get-info :all-statistics)\n")
+      Utils.writeToFile(f"$filePrefix%s-$curAssertName%s-$curAssertLabel%s-$counten%04d.smt", smtOutput + "\n\n(check-sat)\n(get-info :all-statistics)\n")
       counten += 1
       return SolverResult(None, None)
     }