Merge pull request #692 from viperproject/meilers_conditional_flyweight

Conditional flyweight pattern for terms

Author: marcoeilers

silver

@@ -568,6 +568,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
             proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))}
         .getOrElse(0)
 
+  lazy val useFlyweight: Boolean = prover() == "Z3-API"
+
   val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth",
     descr = "Maximal number of nested heuristics applications (default: 3)",
     default = Some(3),

src/main/scala/Config.scala

@@ -120,7 +120,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     private def getProver(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 Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter, triggerGenerator)
       case prover =>
         val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}."
         logger warn msg1
@@ -273,10 +273,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     }
 
     private def isKnownToBeTrue(t: Term) = t match {
-      case True() => true
+      case True => true
   //    case eq: BuiltinEquals => eq.p0 == eq.p1 /* WARNING: Blocking trivial equalities might hinder axiom triggering. */
       case _ if pcs.assumptions contains t => true
-      case q: Quantification if q.body == True() => true
+      case q: Quantification if q.body == True => true
       case _ => false
     }
 
@@ -382,7 +382,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def statistics(): Map[String, String] = prover.statistics()
 
-    override def generateModel(): Unit = proverAssert(False(), None)
+    override def generateModel(): Unit = proverAssert(False, None)
 
     override def getModel(): Model = prover.getModel()
 

src/main/scala/decider/Decider.scala

@@ -143,7 +143,7 @@ private trait LayeredPathConditionStackLike {
   protected def conditionalized(layers: Stack[PathConditionStackLayer]): Seq[Term] = {
     var unconditionalTerms = Vector.empty[Term]
     var conditionalTerms = Vector.empty[Term]
-    var implicationLHS: Term = True()
+    var implicationLHS: Term = True
 
     for (layer <- layers.reverseIterator) {
       unconditionalTerms ++= layer.globalAssumptions
@@ -182,7 +182,7 @@ private trait LayeredPathConditionStackLike {
         Quantification(
           quantifier,
           qvars,
-          Implies(layer.branchCondition.getOrElse(True()), And(layer.nonGlobalAssumptions -- ignores)),
+          Implies(layer.branchCondition.getOrElse(True), And(layer.nonGlobalAssumptions -- ignores)),
           triggers,
           name,
           isGlobal)

src/main/scala/decider/PathConditions.scala

@@ -197,8 +197,8 @@ class TermToSMTLib2Converter
 
     /* Permissions */
 
-    case FullPerm() => "$Perm.Write"
-    case NoPerm() => "$Perm.No"
+    case FullPerm => "$Perm.Write"
+    case NoPerm => "$Perm.No"
     case FractionPermLiteral(r) => renderBinaryOp("/", renderAsReal(IntLiteral(r.numerator)), renderAsReal(IntLiteral(r.denominator)))
     case FractionPerm(n, d) => renderBinaryOp("/", renderAsReal(n), renderAsReal(d))
     case PermLess(t0, t1) => renderBinaryOp("<", render(t0), render(t1))
@@ -370,9 +370,9 @@ class TermToSMTLib2Converter
       else parens(text("- 0") <+> value(-n))
 
     case Unit => "$Snap.unit"
-    case True() => "true"
-    case False() => "false"
-    case Null() => "$Ref.null"
+    case True => "true"
+    case False => "false"
+    case Null => "$Ref.null"
     case _: SeqNil => renderApp("Seq_empty", Seq(), literal.sort)
     case _: EmptySet => renderApp("Set_empty", Seq(), literal.sort)
     case _: EmptyMultiset => renderApp("Multiset_empty", Seq(), literal.sort)

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -30,6 +30,7 @@ class TermToZ3APIConverter
 
   val sortCache = mutable.HashMap[Sort, Z3Sort]()
   val funcDeclCache = mutable.HashMap[(String, Seq[Sort], Sort), Z3FuncDecl]()
+  val termCache = mutable.HashMap[Term, Z3Expr]()
 
   def convert(s: Sort): Z3Sort = convertSort(s)
 
@@ -203,6 +204,9 @@ class TermToZ3APIConverter
 
 
   def convertTerm(term: Term): Z3Expr = {
+    val cached = termCache.get(term)
+    if (cached.isDefined)
+      return cached.get
     val res = term match {
       case l: Literal => {
         l match {
@@ -212,9 +216,9 @@ class TermToZ3APIConverter
             else
               ctx.mkUnaryMinus(ctx.mkInt((-n).toString()))
           }
-          case True() => ctx.mkTrue()
-          case False() => ctx.mkFalse()
-          case Null() => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref"))
+          case True => ctx.mkTrue()
+          case False => ctx.mkFalse()
+          case Null => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref"))
           case Unit => ctx.mkConst(getUnitConstructor)
           case _: SeqNil => createApp("Seq_empty", Seq(), l.sort)
           case _: EmptySet => createApp("Set_empty", Seq(), l.sort)
@@ -254,11 +258,13 @@ class TermToZ3APIConverter
         } else{
           val qvarExprs = vars.map(v => convert(v)).toArray
           val nonEmptyTriggers = triggers.filter(_.p.nonEmpty)
-          val patterns = if (nonEmptyTriggers.nonEmpty)
-              // Simplify trigger terms; Z3 does this automatically when used via stdio, and it sometimes makes
-              // triggers valid that would otherwise be rejected.
-              nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm).simplify()): _*)).toArray
-            else null
+          val patterns = if (nonEmptyTriggers.nonEmpty) {
+              // ME: Maybe we should simplify trigger terms here? There is some evidence that Z3 does this
+              // automatically when used via stdio, and it sometimes makes triggers valid that would otherwise be
+              // rejected. On the other hand, it's not at all obvious that simplification does not change the shape
+              // of a trigger term, which would not be what we want.
+              nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm)): _*)).toArray
+          } else null
           val weightValue = weight.getOrElse(1)
           if (quant == Forall) {
             ctx.mkForall(qvarExprs, convertTerm(body), weightValue, patterns, null, ctx.mkSymbol(name), null)
@@ -310,8 +316,8 @@ class TermToZ3APIConverter
       /* Permissions */
 
 
-      case FullPerm() => ctx.mkReal(1)
-      case NoPerm() => ctx.mkReal(0)
+      case FullPerm => ctx.mkReal(1)
+      case NoPerm => ctx.mkReal(0)
       case FractionPermLiteral(r) => ctx.mkDiv(convertToReal(IntLiteral(r.numerator)), convertToReal(IntLiteral(r.denominator)))
       case FractionPerm(n, d) => ctx.mkDiv(convertToReal(n), convertToReal(d))
       case PermLess(t0, t1) => ctx.mkLt(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
@@ -441,6 +447,7 @@ class TermToZ3APIConverter
          | _: Quantification =>
         sys.error(s"Unexpected term $term cannot be translated to SMTLib code")
     }
+    termCache.put(term, res)
     res
   }
 
@@ -516,6 +523,7 @@ class TermToZ3APIConverter
     macros.clear()
     funcDeclCache.clear()
     sortCache.clear()
+    termCache.clear()
     unitConstructor = null
     combineConstructor = null
     firstFunc = null

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -9,17 +9,19 @@ package viper.silicon.decider
 import com.typesafe.scalalogging.LazyLogging
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat}
-import viper.silicon.state.IdentifierFactory
-import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Sort, SortDecl, SortWrapperDecl, Term, sorts}
+import viper.silicon.state.{IdentifierFactory, State}
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts}
 import viper.silicon.{Config, Map}
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
 import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel}
+
 import java.io.PrintWriter
 import java.nio.file.Path
-
 import scala.collection.mutable
 import com.microsoft.z3._
+import com.microsoft.z3.enumerations.Z3_param_kind
+import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams
 import viper.silicon.reporting.ExternalToolError
 
 import scala.jdk.CollectionConverters.MapHasAsJava
@@ -28,8 +30,8 @@ import scala.util.Random
 
 object Z3ProverAPI {
   val name = "Z3-API"
-  val minVersion = Version("4.8.6.0")
-  val maxVersion = Some(Version("4.8.7.0")) /* X.Y.Z if that is the *last supported* version */
+  val minVersion = Version("4.8.7.0")
+  val maxVersion = Some(Version("4.12.1.0")) /* X.Y.Z if that is the *last supported* version */
 
   // these are not actually used, but since there is a lot of code that expects command line parameters and a
   // config file, we just supply this information here (whose contents will then be ignored)
@@ -46,34 +48,31 @@ object Z3ProverAPI {
   val initialOptions = Map("auto_config" -> "false", "type_check" -> "true")
   val boolParams = Map(
     "smt.delay_units" -> true,
-    "delay_units" -> true,
     "smt.mbqi" -> false,
-    "mbqi" -> false,
     //"pp.bv_literals" -> false,  // This is part of z3config.smt2 but Z3 won't accept it via API.
     "model.v2" -> true
   )
   val intParams = Map(
     "smt.case_split" -> 3,
-    "case_split" -> 3,
     "smt.qi.max_multi_patterns" -> 1000,
-    "qi.max_multi_patterns" -> 1000,
     "smt.arith.solver" -> 2,
-    "arith.solver" -> 2
   )
   val stringParams: Map[String, String] = Map(
     // currently none
   )
   val doubleParams = Map(
     "smt.qi.eager_threshold" -> 100.0,
-    "qi.eager_threshold" -> 100.0,
   )
+  val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams
+  val oldVersionOnlyParams = Set("smt.arith.solver")
 }
 
 
 class Z3ProverAPI(uniqueId: String,
                   termConverter: TermToZ3APIConverter,
                   identifierFactory: IdentifierFactory,
-                  reporter: Reporter)
+                  reporter: Reporter,
+                  triggerGenerator: TriggerGenerator)
     extends Prover
       with LazyLogging
 {
@@ -114,19 +113,59 @@ class Z3ProverAPI(uniqueId: String,
     lastTimeout = -1
     ctx = new Context(Z3ProverAPI.initialOptions.asJava)
     val params = ctx.mkParams()
+
+    // When setting parameters via API, we have to remove the smt. prefix
+    def removeSmtPrefix(s: String) = {
+      if (s.startsWith("smt."))
+        s.substring(4)
+      else
+        s
+    }
+
+    val useOldVersionParams = version() <= Version("4.8.7.0")
     Z3ProverAPI.boolParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.intParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.doubleParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.stringParams.foreach{
-      case (k, v) => params.add(k, v)
+      case (k, v) =>
+        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
+          params.add(removeSmtPrefix(k), v)
     }
+    val userProvidedArgs = Verifier.config.proverConfigArgs
     prover = ctx.mkSolver()
+    val descrs = prover.getParameterDescriptions
+    for ((origKey, vl) <- userProvidedArgs) {
+      val key = if (origKey.startsWith("smt."))
+        origKey.substring(4)
+      else
+        origKey
+      val keySymbol = ctx.mkSymbol(key)
+      val param_kind = descrs.getKind(keySymbol)
+      param_kind match {
+        case Z3_param_kind.Z3_PK_BOOL =>
+          params.add(key, vl.toBoolean)
+        case Z3_param_kind.Z3_PK_UINT =>
+          params.add(key, vl.toInt)
+        case Z3_param_kind.Z3_PK_DOUBLE =>
+          params.add(key, vl.toDouble)
+        case Z3_param_kind.Z3_PK_STRING =>
+          params.add(key, vl)
+        case _ =>
+          reporter.report(InternalWarningMessage("Z3 error: unknown parameter" + key))
+      }
+    }
     prover.setParameters(params)
     termConverter.start()
     termConverter.ctx = ctx
@@ -212,7 +251,21 @@ class Z3ProverAPI(uniqueId: String,
       else
         preambleAssumes.add(termConverter.convert(term).asInstanceOf[BoolExpr])
     } catch {
-      case e: Z3Exception => reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
+      case e: Z3Exception =>
+        // The only reason we get an exception here is that we've tried to assume a quantifier with an invalid trigger.
+        // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores
+        // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually
+        // walk through all quantifiers and remove invalid terms inside the trigger.
+        triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
+        val cleanTerm = term.transform{
+          case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
+            val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{
+              case t => triggerGenerator.isForbiddenInTrigger(t)
+            }.nonEmpty))
+            q.copy(triggers = goodTriggers)
+        }()
+        prover.add(termConverter.convert(cleanTerm).asInstanceOf[BoolExpr])
+        reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
     }
   }
 
@@ -316,7 +369,13 @@ class Z3ProverAPI(uniqueId: String,
     if (!preamblePhaseOver) {
       preamblePhaseOver = true
 
-      val merged = emittedPreambleString.mkString("\n")
+      // Setting all options again , since otherwise some of them seem to get lost.
+      val standardOptionPrefix = Seq("(set-option :auto_config false)", "(set-option :type_check true)") ++
+        Z3ProverAPI.allParams.map(bp => s"(set-option :${bp._1} ${bp._2})")
+
+      val customOptionPrefix = Verifier.config.proverConfigArgs.map(a => s"(set-option :${a._1} ${a._2})")
+
+      val merged = (standardOptionPrefix ++ customOptionPrefix ++ emittedPreambleString).mkString("\n")
       val parsed = ctx.parseSMTLIB2String(merged, emittedSortSymbols.toArray, emittedSorts.toArray, emittedFuncSymbols.toArray, emittedFuncs.toArray)
       prover.add(parsed: _*)
       prover.add(preambleAssumes.toSeq : _*)

src/main/scala/decider/Z3ProverAPI.scala

@@ -151,7 +151,7 @@ object Converter {
   lazy val symbolConverter: SymbolConverter = new DefaultSymbolConverter
   //some tokens used for naming model entries in a more maintainable way
   lazy val snapUnitId: String = termconverter.convert(Unit)
-  lazy val nullRefId: String = termconverter.convert(Null())
+  lazy val nullRefId: String = termconverter.convert(Null)
 
   def getFunctionValue(model: Model,
                        fname: String,
@@ -254,7 +254,7 @@ object Converter {
       case Unit              => UnprocessedModelEntry(ConstantEntry(snapUnitId))
       case IntLiteral(x)     => LitIntEntry(x)
       case t: BooleanLiteral => LitBoolEntry(t.value)
-      case Null()            => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
+      case Null              => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
       case Var(_, sort) =>
         val key: String = term.toString
         val entry: Option[ModelEntry] = model.entries.get(key)
@@ -416,8 +416,8 @@ object Converter {
         case _ => None
       }
       case App(_, _) => None
-      case NoPerm() => Some(Rational.zero)
-      case FullPerm() => Some(Rational.one)
+      case NoPerm => Some(Rational.zero)
+      case FullPerm => Some(Rational.one)
       case FractionPermLiteral(r) => Some(r)
       case _: FractionPerm => None
       case IsValidPermVar(_) => None

src/main/scala/reporting/Converter.scala

@@ -58,7 +58,7 @@ class DefaultStateFormatter extends StateFormatter {
       case    c: BuiltinEquals if c.p0.isInstanceOf[Combine]
            || c.p1.isInstanceOf[Combine]
            => true
-      case Not(BuiltinEquals(_, Null())) => true
+      case Not(BuiltinEquals(_, Null)) => true
       case _ => false
     }.mkString("(", ", ", ")")
   }
@@ -92,7 +92,7 @@ class DefaultStateFormatter extends StateFormatter {
     val filteredPcs = pcs.filterNot {
       case c: BuiltinEquals if c.p0.isInstanceOf[Combine]
         || c.p1.isInstanceOf[Combine] => true
-      case Not(BuiltinEquals(_, Null())) => true
+      case Not(BuiltinEquals(_, Null)) => true
       case _ => false
     }
     if (filteredPcs.isEmpty) "[]" else filteredPcs.mkString("[\"", "\",\"", "\"]")