Merge branch 'master' into meilers_qp_set_type

src/main/resources/z3config.smt2

@@ -2,7 +2,7 @@
 ; License, v. 2.0. If a copy of the MPL was not distributed with this
 ; file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-; Requires Z3 >= 4.3.2
+; Tested with Z3 4.8.7 and 4.12.1
 
 ; ATTENTION: Continuing multi-line statements must be indented with at least
 ;            one tab or two spaces. All other lines must not start with tabs
@@ -12,53 +12,19 @@
 ; setting options, is answered by a success (or error) reply from Z3. Silicon currently relies on
 ; these replies when it interacts with Z3 via stdio.
 (set-option :print-success true) ; Boogie: false
+(set-option :global-decls true) ; Necessary for push pop mode
 
-(set-option :global-decls true) ; Boogie: default
-(set-option :auto_config false) ; Usually a good idea
-
-(set-option :smt.restart_strategy 0)
-(set-option :smt.restart_factor |1.5|)
+; These options are taken from Dafny 4.0.0 and proven to work decently well with up-to-date Z3 (currently 4.12.1),
+; unlike the options used previously.
+(set-option :auto_config false)
 (set-option :smt.case_split 3)
 (set-option :smt.delay_units true)
-(set-option :smt.delay_units_threshold 16)
-(set-option :nnf.sk_hack true)
 (set-option :type_check true)
-(set-option :smt.bv.reflect true)
-
 (set-option :smt.mbqi false)
+(set-option :pp.bv_literals false)
 (set-option :smt.qi.eager_threshold 100)
-; (set-option :smt.qi.lazy_threshold 1000000000)
-(set-option :smt.qi.cost "(+ weight generation)")
-(set-option :smt.qi.max_multi_patterns 1000)
-; (set-option :smt.qi.profile true)
-; (set-option :smt.qi.profile_freq 100000)
-
-;; [2019-07-31 Malte] The next block of options are all randomness-related options that I could
-;; find in the description Z3 -pd emits. If not stated otherwise, the options are merely explicitly
-;; set to their default values.
-(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0
-(set-option :sat.phase caching)
-(set-option :sat.random_seed 0)
-(set-option :nlsat.randomize true)
-(set-option :nlsat.seed 0)
-(set-option :nlsat.shuffle_vars false)
-(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5
-(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5
-(set-option :smt.arith.random_initial_value true) ; Boogie: true
-(set-option :smt.random_seed 0)
-(set-option :sls.random_offset true)
-(set-option :sls.random_seed 0)
-(set-option :sls.restart_init false)
-(set-option :sls.walksat_ucb true)
-
-; (set-option :smt.macro_finder true)
-; (set-option :combined_solver.solver2_timeout 500)
-; (set-option :combined_solver.solver2_unknown 2)
-; (set-option :smt.arith.nl false)
-; (set-option :smt.arith.nl.gb false)
-    ; See http://stackoverflow.com/questions/28210673
-
-; (set-option :produce-models true)
-; (set-option :model false)
+(set-option :smt.arith.solver 2)
 (set-option :model.v2 true)
-; (set-option :model.compact true)
+
+; We want unlimited multipatterns
+(set-option :smt.qi.max_multi_patterns 1000)

src/main/scala/Config.scala

@@ -172,6 +172,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val reportReasonUnknown: ScallopOption[Boolean] = opt[Boolean]("reportReasonUnknown",
+    descr = "For every verification error, include the reason the SMT solver reported unknown.",
+    default = Some(false),
+    noshort = true
+  )
+
   val recursivePredicateUnfoldings: ScallopOption[Int] = opt[Int]("recursivePredicateUnfoldings",
     descr = (  "Evaluate n unfolding expressions in the body of predicates that (transitively) unfold "
              + "other instances of themselves (default: 1)"),
@@ -419,8 +425,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
-  val disableTempDirectory: ScallopOption[Boolean] = opt[Boolean]("disableTempDirectory",
-    descr = "Disable the creation of temporary data (default: ./tmp)",
+  val enableTempDirectory: ScallopOption[Boolean] = opt[Boolean]("enableTempDirectory",
+    descr = "Enable the creation of temporary directory to log prover interactions (default: ./tmp)",
     default = Some(false),
     noshort = true
   )
@@ -562,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/decider/Decider.scala

@@ -34,7 +34,7 @@ trait Decider {
   def pushScope(): Unit
   def popScope(): Unit
 
-  def checkSmoke(): Boolean
+  def checkSmoke(isAssert: Boolean = false): Boolean
 
   def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit
   def setPathConditionMark(): Mark
@@ -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
@@ -236,7 +236,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     /* Asserting facts */
 
-    def checkSmoke(): Boolean = prover.check(Verifier.config.checkTimeout.toOption) == Unsat
+    def checkSmoke(isAssert: Boolean = false): Boolean = {
+      val timeout = if (isAssert) Verifier.config.assertTimeout.toOption else Verifier.config.checkTimeout.toOption
+      prover.check(timeout) == Unsat
+    }
 
     def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout))
 
@@ -270,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
     }
 
@@ -379,14 +382,14 @@ 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()
 
     override def hasModel(): Boolean = prover.hasModel()
 
     override def isModelValid(): Boolean = prover.isModelValid()
 
-    override def clearModel(): Unit = prover.clearLastModel()
+    override def clearModel(): Unit = prover.clearLastAssert()
   }
 }

src/main/scala/decider/PathConditions.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/ProverStdIO.scala

@@ -40,6 +40,7 @@ abstract class ProverStdIO(uniqueId: String,
   protected var output: PrintWriter = _
 
   var proverPath: Path = _
+  var lastReasonUnknown : String = _
   var lastModel : String = _
 
   def exeEnvironmentalVariable: String
@@ -82,7 +83,7 @@ abstract class ProverStdIO(uniqueId: String,
     }
     pushPopScopeDepth = 0
     lastTimeout = -1
-    logfileWriter = if (Verifier.config.disableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
+    logfileWriter = if (!Verifier.config.enableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
     proverPath = getProverPath
     prover = createProverInstance()
     input = new BufferedReader(new InputStreamReader(prover.getInputStream))
@@ -252,6 +253,7 @@ abstract class ProverStdIO(uniqueId: String,
 
     if (!result) {
       retrieveAndSaveModel()
+      retrieveReasonUnknown()
     }
 
     pop()
@@ -285,6 +287,16 @@ abstract class ProverStdIO(uniqueId: String,
     }
   }
 
+  protected def retrieveReasonUnknown(): Unit = {
+    if (Verifier.config.reportReasonUnknown()) {
+      writeLine("(get-info :reason-unknown)")
+      var result = readLine()
+      if (result.startsWith("(:reason-unknown \""))
+        result = result.substring(18, result.length - 2)
+      lastReasonUnknown = result
+    }
+  }
+
   override def hasModel(): Boolean = {
     lastModel != null
   }
@@ -474,5 +486,10 @@ abstract class ProverStdIO(uniqueId: String,
 
   override def getModel(): Model = Model(lastModel)
 
-  override def clearLastModel(): Unit = lastModel = null
+  override def getReasonUnknown(): String = lastReasonUnknown
+
+  override def clearLastAssert(): Unit = {
+    lastReasonUnknown = null
+    lastModel = null
+  }
 }

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -198,8 +198,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))
@@ -357,7 +357,7 @@ class TermToSMTLib2Converter
     if (args.nonEmpty)
       parens(docAppNoParens)
     else
-      parens(text("as") <+> docAppNoParens <+> render(outSort))
+      docAppNoParens
   }
 
   protected def render(q: Quantifier): Cont = q match {
@@ -371,9 +371,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/TermToZ3APIConverter.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