Interaction with Z3 through Z3's Java API instead of StdIO

build.sbt

@@ -30,6 +30,7 @@ lazy val silicon = (project in file("."))
     libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.9.2",
     libraryDependencies += "org.apache.commons" % "commons-pool2" % "2.9.0",
     libraryDependencies += "io.spray" %%  "spray-json" % "1.3.6",
+    libraryDependencies += "com.microsoft.z3" % "z3" % "4.8.9" from "https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/com.microsoft.z3-4.8.7.jar",
 
     // Only get a few compilation errors at once
     maxErrors := 5,

src/main/scala/Config.scala

@@ -12,7 +12,7 @@ import scala.util.matching.Regex
 import scala.util.Properties._
 import org.rogach.scallop._
 import viper.silicon.Config.StateConsolidationMode.StateConsolidationMode
-import viper.silicon.decider.{Z3ProverStdIO, Cvc5ProverStdIO}
+import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverAPI, Z3ProverStdIO}
 import viper.silver.frontend.SilFrontendConfig
 
 class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
@@ -717,7 +717,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   )
 
   val prover: ScallopOption[String] = opt[String]("prover",
-    descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}. " +
+    descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}, ${Z3ProverAPI.name}. " +
             s"(default: ${Z3ProverStdIO.name}).",
     default = Some(Z3ProverStdIO.name),
     noshort = true
@@ -726,8 +726,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {
-    case Some(Z3ProverStdIO.name) | Some(Cvc5ProverStdIO.name) => Right(())
-    case prover => Left(s"Unknown prover '$prover' provided. Expected one of ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}.")
+    case Some(Z3ProverStdIO.name) | Some(Cvc5ProverStdIO.name) | Some(Z3ProverAPI.name) => Right(())
+    case prover => Left(s"Unknown prover '$prover' provided. Expected one of ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}, ${Z3ProverAPI.name}.")
   }
 
   validateOpt(timeout) {

src/main/scala/decider/CVC5ProverStdIO.scala

@@ -45,4 +45,6 @@ class Cvc5ProverStdIO(uniqueId: String,
   protected def getProverPath: Path = {
     Paths.get(Verifier.config.cvc5Exe)
   }
+
+  override def emitSettings(contents: Iterable[String]): Unit = emit(contents)
 }

src/main/scala/decider/Decider.scala

@@ -10,11 +10,11 @@ import scala.reflect.{ClassTag, classTag}
 import com.typesafe.scalalogging.Logger
 import viper.silver.ast
 import viper.silver.components.StatefulComponent
-import viper.silver.verifier.DependencyNotFoundError
+import viper.silver.verifier.{DependencyNotFoundError, Model}
 import viper.silicon._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
-import viper.silicon.interfaces.decider.{Prover, Unsat}
+import viper.silicon.interfaces.decider._
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord}
 import viper.silicon.state._
@@ -60,8 +60,10 @@ trait Decider {
   def appliedFresh(id: String, sort: Sort, appliedArgs: Seq[Term]): App
 
   def generateModel(): Unit
-  def getModel(): String
+  def getModel(): Model
   def clearModel(): Unit
+  def hasModel(): Boolean
+  def isModelValid(): Boolean
 
 /* [BRANCH-PARALLELISATION] */
 //  def freshFunctions: InsertionOrderedSet[FunctionDecl]
@@ -87,23 +89,24 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
   def identifierFactory: IdentifierFactory
 
   object decider extends Decider with StatefulComponent {
-    private var proverStdIO: ProverStdIO = _
+    private var proverStdIO: Prover = _
     private var pathConditions: PathConditionStack = _
 
 //    private var _freshFunctions: InsertionOrderedSet[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
 //    private var _freshMacros: Vector[MacroDecl] = _
 
-    def prover: ProverStdIO = proverStdIO
+    def prover: Prover = proverStdIO
 
     def pcs: PathConditionStack = pathConditions
 
 //    def setPcs(other: PathConditionStack) = { /* [BRANCH-PARALLELISATION] */
 //      pathConditions = other
 //      pathConditions.assumptions foreach prover.assume
 //    }
-    private def getProverStdIO(prover: String): ProverStdIO = prover match {
+    private def getProverStdIO(prover: String): Prover = prover match {
       case Z3ProverStdIO.name => new Z3ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
       case Cvc5ProverStdIO.name => new Cvc5ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
+      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter)
       case prover =>
         val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}."
         logger warn msg1
@@ -118,7 +121,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       val proverStdIOVersion = proverStdIO.version()
       // One can pass some options. This allows to check whether they have been received.
 
-      val msg = s"Using ${proverStdIO.name} $proverStdIOVersion located at ${proverStdIO.proverPath}"
+      val path = prover match {
+        case pio: ProverStdIO => pio.proverPath
+        case _ => "No Path"
+      }
+      val msg = s"Using ${proverStdIO.name} $proverStdIOVersion located at ${path}"
       reporter report ConfigurationConfirmation(msg)
       logger debug msg
 
@@ -362,7 +369,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     override def generateModel(): Unit = proverAssert(False(), None)
 
-    override def getModel(): String = prover.getLastModel()
+    override def getModel(): Model = prover.getModel()
+
+    override def hasModel(): Boolean = prover.hasModel()
+
+    override def isModelValid(): Boolean = prover.isModelValid()
 
     override def clearModel(): Unit = prover.clearLastModel()
   }

src/main/scala/decider/ProverStdIO.scala

@@ -20,6 +20,7 @@ import viper.silicon.verifier.Verifier
 import viper.silver.verifier.{DefaultDependency => SilDefaultDependency}
 import viper.silicon.{Config, Map, toMap}
 import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage, Reporter}
+import viper.silver.verifier.Model
 
 import scala.collection.mutable
 
@@ -41,14 +42,9 @@ abstract class ProverStdIO(uniqueId: String,
   var proverPath: Path = _
   var lastModel : String = _
 
-  def name: String
-  def minVersion: Version
-  def maxVersion: Option[Version]
   def exeEnvironmentalVariable: String
   def dependencies: Seq[SilDefaultDependency]
-  def staticPreamble: String
   def startUpArgs: Seq[String]
-  def randomizeSeedsOptions: Seq[String]
 
   protected def setTimeout(timeout: Option[Int]): Unit
   protected def getProverPath: Path
@@ -289,6 +285,14 @@ abstract class ProverStdIO(uniqueId: String,
     }
   }
 
+  override def hasModel(): Boolean = {
+    lastModel != null
+  }
+
+  override def isModelValid(): Boolean = {
+    lastModel != null && !lastModel.contains("model is not available")
+  }
+
   protected def assertUsingSoftConstraints(goal: String): (Boolean, Long) = {
     val guard = fresh("grd", Nil, sorts.Bool)
 
@@ -457,7 +461,7 @@ abstract class ProverStdIO(uniqueId: String,
     output.println(out)
   }
 
-  override def getLastModel(): String = lastModel
+  override def getModel(): Model = Model(lastModel)
 
   override def clearLastModel(): Unit = lastModel = null
 }

src/main/scala/decider/SMTLib2PreambleReader.scala

@@ -54,15 +54,18 @@ class SMTLib2PreambleReader extends PreambleReader[String, String] {
         lineAcc.replace(orig, repl)})
   }
 
-  def emitPreamble(preamble: Iterable[String], sink: ProverLike): Unit = {
-    sink.emit(preamble)
+  def emitPreamble(preamble: Iterable[String], sink: ProverLike, isOptions: Boolean): Unit = {
+    if (isOptions)
+      sink.emitSettings(preamble)
+    else
+      sink.emit(preamble)
   }
 
   def emitParametricPreamble(resource: String,
                              substitutions: Map[String, String],
                              sink: ProverLike)
                             : Unit = {
 
-    emitPreamble(readParametricPreamble(resource, substitutions), sink)
+    emitPreamble(readParametricPreamble(resource, substitutions), sink, false)
   }
 }

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -380,7 +380,7 @@ class TermToSMTLib2Converter
     else
       render(t)
 
-  protected def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
+  def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
     val repr: String = id match {
       case SimpleIdentifier(name) => name
       case SuffixedIdentifier(prefix, separator, suffix) => s"${render(prefix, false)}$separator$suffix"