wip on #318: setting random_seed in z3

CHANGES.md

@@ -1,5 +1,6 @@
 ## Unreleased #unstable
 
+ * random seed for z3, see docs/tuning.md and #318
  * correct translation of chained substitutions in INSTANCEs, see #143
  * friendly messages for unexpected expressions, see #303
  * better operator inlining, see #283

docs/tuning.md

@@ -5,7 +5,9 @@ The parameters for fine tuning can be passed to the checker in a properties file
 Its name is given with the command-line option ``--tuning=my.properties.`` This file
 supports variable substitution, e.g., ``${x}`` is replaced with the value of ``x``, if it was
 previously declared.
-
+
+1. __Randomization__: `smt.randomSeed=<int>` passes the random seed to `z3` (via
+  `z3`'s parameters `sat.random_seed` and `smt.random_seed`). 
 
 1. __Timeouts__: ``search.transition.timeout=<seconds>`` and ``search.invariant.timeout=<seconds>`` set timeouts
   in seconds for checking whether a transition is enabled and whether the invariant holds, respectively.

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -39,7 +39,7 @@ class CheckCmd extends Command(name = "check",
       description = "the bound on the computation length, default: 10")
   var tuning: String =
     opt[String](name="tuning", default = "",
-      description = "filename of the tuning options, see docs/tuning.md")
+      description = "filename of the tuning options, see apalache/docs/tuning.md")
 
   var randomizeDfs: Boolean = opt[Boolean](
     name = "randomizeDfs", default = true,

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/ModelChecker.scala

@@ -1,24 +1,21 @@
 package at.forsyte.apalache.tla.bmcmt
 
 import java.io.{FileWriter, PrintWriter, StringWriter}
-import java.util.Calendar
 
-import at.forsyte.apalache.tla.assignments.FalseEx
 import at.forsyte.apalache.tla.bmcmt.analyses.{ExprGradeStore, FormulaHintsStore}
 import at.forsyte.apalache.tla.bmcmt.rewriter.{ConstSimplifierForSmt, RewriterConfig}
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, MockOracle, Oracle}
 import at.forsyte.apalache.tla.bmcmt.search.SearchStrategy
 import at.forsyte.apalache.tla.bmcmt.search.SearchStrategy._
-import at.forsyte.apalache.tla.bmcmt.smt.{SolverContext, Z3SolverContext}
+import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, SolverContext, Z3SolverContext}
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.bmcmt.util.TlaExUtil
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.convenience.tla
 import at.forsyte.apalache.tla.lir.io._
-import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
-import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaStr}
+import at.forsyte.apalache.tla.lir.values.TlaBool
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.collection.immutable.SortedMap
@@ -50,7 +47,9 @@ class ModelChecker(typeFinder: TypeFinder[CellT],
     */
   private var stack: List[(SymbState, Oracle)] = List()
   private var typesStack: Seq[SortedMap[String, CellT]] = Seq()
-  private val solverContext: SolverContext = new Z3SolverContext(debug, profile)
+  private val solverContext: SolverContext =
+    new Z3SolverContext(SolverConfig(debug, profile,
+      randomSeed = tuningOptions.getOrElse("smt.randomSeed", "0").toInt))
   // TODO: figure out why the preprocessor slows down invariant checking. Most likely, there is a bug.
   //      new PreproSolverContext(new Z3SolverContext(debug, profile))
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala

@@ -0,0 +1,23 @@
+package at.forsyte.apalache.tla.bmcmt.smt
+
+/**
+  * Configuration option to be passed to SolverContext. This class is declared as a case class
+  * to enable the concise copy syntax of Scala.
+  *
+  * @param debug Enable the debug mode (activated with --debug). Write the log file to log%d.smt.
+  * @param profile Enable the profile mode (activated with --profile). Report the metrics.
+  * @param randomSeed The random seed to be passed to z3 as :random-seed.
+  *
+  * @author Igor Konnov
+  */
+sealed case class SolverConfig(debug: Boolean,
+                               profile: Boolean,
+                               randomSeed: Int) {
+}
+
+object SolverConfig {
+  /**
+    * Get the default configuration.
+    */
+  val default: SolverConfig = new SolverConfig(debug = false, profile = false, randomSeed = 0)
+}

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

@@ -17,18 +17,33 @@ import com.microsoft.z3.enumerations.Z3_lbool
 import scala.collection.mutable
 
 /**
-  * An implementation of a SolverContext using Z3.
+  * <p>
+  * An implementation of a SolverContext using Z3. Note that this class overrides the global z3 settings
+  * `sat.random_seed`, `smt.random_seed`, `fp.spacer.random_seed`, and `sls.random_seed` with `config.randomSeed`.
+  * Although it is usually not a good idea to override the global settings, we do it to isolate the code
+  * specific to z3 in this class.
+  * </p>
   *
   * @author Igor Konnov
   */
-class Z3SolverContext(debug: Boolean = false, profile: Boolean = false) extends SolverContext {
+class Z3SolverContext(config: SolverConfig) extends SolverContext {
   private val id: Long = Z3SolverContext.createId()
 
   /**
     * A log writer, for debugging purposes.
     */
   private val logWriter: PrintWriter = initLog()
 
+  // dump the configuration parameters in the log
+  // set the global configuration parameters for z3 modules
+  Z3SolverContext.RANDOM_SEED_PARAMS.foreach {
+    p =>
+      Global.setParameter(p, config.randomSeed.toString)
+      logWriter.println(";; %s = %s".format(p, config.randomSeed))
+//    the following fails with an exception: java.lang.NoSuchFieldError: value
+//      logWriter.println(";; %s = %s".format(p, Global.getParameter(p)))
+  }
+
   var level: Int = 0
   var nBoolConsts: Int = 0 // the solver introduces Boolean constants internally
   private val z3context: Context = new Context()
@@ -175,14 +190,18 @@ class Z3SolverContext(debug: Boolean = false, profile: Boolean = false) extends
     log(s"(assert ${z3expr.toString})")
     z3solver.add(z3expr.asInstanceOf[BoolExpr])
 
-    if (profile) {
+    /**
+    // The old and inefficient way to profile.
+    // Instead, use: https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#profiler
+    if (config.profile) {
       val timeBefore = System.nanoTime()
       sat()
       val timeAfter = System.nanoTime()
       val diffSec = (timeAfter - timeBefore) / 1000000000
       val diffNano = (timeAfter - timeBefore) % 1000000000
       log(";;;;;  @@ TIME TO SAT: %05d.%09d sec @@".format(diffSec, diffNano))
     }
+    */
   }
 
   /**
@@ -214,7 +233,7 @@ class Z3SolverContext(debug: Boolean = false, profile: Boolean = false) extends
 
   private def initLog(): PrintWriter = {
     val writer = new PrintWriter(new File(s"log$id.smt"))
-    if (!debug) {
+    if (!config.debug) {
       writer.println("Logging is disabled (Z3SolverContext.debug = false). Activate with --debug.")
       writer.flush()
     }
@@ -227,7 +246,7 @@ class Z3SolverContext(debug: Boolean = false, profile: Boolean = false) extends
     * @param message message text, called by name, so evaluated only when needed
     */
   def log(message: => String): Unit = {
-    if (debug) {
+    if (config.debug) {
       logWriter.println(message)
     }
   }
@@ -583,4 +602,10 @@ object Z3SolverContext {
   private def createId(): Long = {
     nextId.getAndIncrement()
   }
+
+  /**
+    * The names of all parameters that are used to set the random seeds in z3.
+    */
+  val RANDOM_SEED_PARAMS: List[String] =
+    List("sat.random_seed", "smt.random_seed", "fp.spacer.random_seed", "sls.random_seed")
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala

@@ -2,17 +2,17 @@ package at.forsyte.apalache.tla.bmcmt
 
 import java.io.{PrintWriter, StringWriter}
 
-import at.forsyte.apalache.tla.bmcmt.smt.{PreproSolverContext, SolverContext, Z3SolverContext}
+import at.forsyte.apalache.tla.bmcmt.smt.{PreproSolverContext, SolverConfig, SolverContext, Z3SolverContext}
 import at.forsyte.apalache.tla.bmcmt.types.eager.TrivialTypeFinder
 import at.forsyte.apalache.tla.lir.convenience.tla
 import org.scalatest.{BeforeAndAfterEach, FunSuite}
 
 class RewriterBase extends FunSuite with BeforeAndAfterEach {
-  protected var solverContext: SolverContext = new PreproSolverContext(new Z3SolverContext())
-  protected var arena: Arena = Arena.create(solverContext)
+  protected var solverContext: SolverContext = _
+  protected var arena: Arena = _
 
   override def beforeEach() {
-    solverContext = new PreproSolverContext(new Z3SolverContext(debug = true))
+    solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true)))
     arena = Arena.create(solverContext)
   }
 

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala

@@ -1,16 +1,25 @@
 package at.forsyte.apalache.tla.bmcmt
 
-import at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext
+import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext}
 import at.forsyte.apalache.tla.bmcmt.types.{BoolT, FinSetT, UnknownT}
 import org.junit.runner.RunWith
-import org.scalatest.FunSuite
 import org.scalatest.junit.JUnitRunner
+import org.scalatest.{BeforeAndAfterEach, FunSuite}
 
 @RunWith(classOf[JUnitRunner])
-class TestArena extends FunSuite {
+class TestArena extends FunSuite with BeforeAndAfterEach {
+  private var solver: Z3SolverContext = _
+
+  override protected def beforeEach(): Unit = {
+    solver = new Z3SolverContext(SolverConfig.default.copy(debug = true))
+  }
+
+  override protected def afterEach(): Unit = {
+    solver.dispose()
+  }
+
   test("create cells") {
-    val solverContext = new Z3SolverContext()
-    val emptyArena = Arena.create(solverContext)
+    val emptyArena = Arena.create(solver)
     val arena = emptyArena.appendCell(UnknownT())
     assert(emptyArena.cellCount + 1 == arena.cellCount)
     assert(UnknownT() == arena.topCell.cellType)
@@ -20,8 +29,7 @@ class TestArena extends FunSuite {
   }
 
   test("add 'has' edges") {
-    val solverContext = new Z3SolverContext()
-    val arena = Arena.create(solverContext).appendCell(FinSetT(UnknownT()))
+    val arena = Arena.create(solver).appendCell(FinSetT(UnknownT()))
     val set = arena.topCell
     val arena2 = arena.appendCell(BoolT())
     val elem = arena2.topCell
@@ -30,8 +38,7 @@ class TestArena extends FunSuite {
   }
 
   test("BOOLEAN has FALSE and TRUE") {
-    val solverContext = new Z3SolverContext()
-    val arena = Arena.create(solverContext)
+    val arena = Arena.create(solver)
     val boolean = arena.cellBooleanSet()
     assert(List(arena.cellFalse(), arena.cellTrue()) == arena.getHas(arena.cellBooleanSet()))
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterControl.scala

@@ -227,7 +227,7 @@ class TestSymbStateRewriterControl extends RewriterBase with TestingPredefs {
 
     for (i <- List(1, 2, 3)) {
       // reinitialize the arena and the solver
-      solverContext = new PreproSolverContext(new Z3SolverContext(debug = true))
+      solverContext = new PreproSolverContext(solverContext)
       arena = Arena.create(solverContext)
       arena = arena.appendCell(IntT())
       val icell = arena.topCell
@@ -271,7 +271,7 @@ class TestSymbStateRewriterControl extends RewriterBase with TestingPredefs {
 
     for (i <- List(1, 2, 3, 99)) {
       // reinitialize the arena and the solver
-      solverContext = new PreproSolverContext(new Z3SolverContext(debug = true))
+      solverContext = new PreproSolverContext(solverContext)
       arena = Arena.create(solverContext)
       arena = arena.appendCell(IntT())
       val icell = arena.topCell