Periodically print Z3 statistics

.unreleased/features/z3-stats.md

@@ -0,0 +1 @@
+Periodically print Z3 statistics when `--debug` is on (#2992)

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

@@ -75,7 +75,9 @@ class BoundedCheckerPassImpl @Inject() (
 
     val smtProfile = options.common.smtprof
     val smtRandomSeed = tuning.getOrElse("smt.randomSeed", "0").toInt
-    val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding)
+    val smtStatsSec =
+      tuning.getOrElse("smt.statsSec", SolverConfig.default.z3StatsSec.toString).toInt
+    val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtStatsSec, smtEncoding)
 
     val result = options.checker.algo match {
       case Algorithm.Incremental => runIncrementalChecker(params, input, tuning, solverConfig)

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

@@ -22,6 +22,7 @@ sealed case class SolverConfig(
     debug: Boolean,
     profile: Boolean,
     randomSeed: Int,
+    z3StatsSec: Int,
     smtEncoding: SMTEncoding) {}
 
 object SolverConfig {
@@ -30,5 +31,6 @@ object SolverConfig {
    * Get the default configuration.
    */
   val default: SolverConfig =
-    new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19)
+    new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19,
+        z3StatsSec = 60)
 }

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

@@ -18,6 +18,7 @@ import com.typesafe.scalalogging.LazyLogging
 
 import java.io.PrintWriter
 import java.util.concurrent.atomic.AtomicLong
+import java.util.concurrent.locks.ReentrantLock
 import scala.collection.mutable
 import scala.collection.mutable.ListBuffer
 
@@ -120,17 +121,61 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
    */
   private var maxCellIdPerContext = List(-1)
 
+  private trait ContextState
+  private case class Running() extends ContextState
+  private case class Disposed() extends ContextState
+
+  // the state of the context: Running or Disposed
+  private var state: ContextState = Running()
+
+  // the lock shared between the context and the statistics thread
+  private val statisticsLock: ReentrantLock = new ReentrantLock()
+  // start a new thread to collect statistics
+  private val statisticsThread = new Thread(() => {
+    while (state == Running()) {
+      // Sleep for a while.
+      // If we call printStatistics right away, we can easily run into a race condition with Z3 initializing.
+      // This produces a core dump.
+      Thread.sleep(config.z3StatsSec * 1000)
+      // make sure that the context is not being disposed right now. Otherwise, we can get a nice core dump.
+      statisticsLock.lock()
+      try {
+        if (state == Running()) {
+          printStatistics()
+        }
+      } finally {
+        statisticsLock.unlock()
+      }
+    }
+  })
+
+  if (config.debug && config.z3StatsSec > 0) {
+    statisticsThread.start()
+  }
+
   /**
    * Dispose whatever has to be disposed in the end.
    */
   override def dispose(): Unit = {
     logger.debug(s"Disposing Z3 solver context ${id}")
-    z3context.close()
-    closeLogs()
-    cellCache.clear()
-    inCache.clear()
-    funDecls.clear()
-    cellSorts.clear()
+    state = Disposed()
+    // Try to obtain the lock, to let the statistics thread finish its work.
+    // If it is stuck for some reason, continue after the timeout in any case.
+    statisticsLock.tryLock(2 * config.z3StatsSec, java.util.concurrent.TimeUnit.SECONDS)
+    try {
+      if (config.debug) {
+        printStatistics()
+      }
+      z3context.close()
+      closeLogs()
+      cellCache.clear()
+      inCache.clear()
+      funDecls.clear()
+      cellSorts.clear()
+    } finally {
+      // it's not that important at this point, but let's unlock it for the piece of mind
+      statisticsLock.unlock()
+    }
   }
 
   /**
@@ -1014,6 +1059,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
     flushLogs()
     throw e
   }
+
+  private def printStatistics(): Unit = {
+    logger.info(s"Z3 statistics for context $id...")
+    val entries = z3solver.getStatistics.getEntries.map(stat => {
+      s"${stat.Key}=${stat.getValueString}"
+    })
+    logger.info(entries.mkString(",") + "\n")
+  }
 }
 
 object Z3SolverContext {

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

@@ -183,7 +183,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers {
     val checkerParams = new ModelCheckerParams(checkerInput, 0)
 
     val solverContext =
-      new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding))
+      new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding,
+              z3StatsSec = 0))
     val rewriter: SymbStateRewriterImpl = smtEncoding match {
       case SMTEncoding.OOPSLA19  => new SymbStateRewriterImpl(solverContext, renaming)
       case SMTEncoding.Arrays    => new SymbStateRewriterImplWithArrays(solverContext, renaming)

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

@@ -13,7 +13,7 @@ import org.scalatestplus.junit.JUnitRunner
 class TestSeqModelCheckerWithArrays extends TestSeqModelCheckerTrait {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.Arrays))
+      .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays))
     val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl)
     test(rewriter)
   }

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

@@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner
 class TestSeqModelCheckerWithFunArrays extends TestSeqModelCheckerTrait {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.FunArrays))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays))
     val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl)
     test(rewriter)
   }

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

@@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner
 class TestSeqModelCheckerWithOOPSLA19 extends TestSeqModelCheckerTrait {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.OOPSLA19))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19))
     val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl)
     test(rewriter)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala

@@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays)
+    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+        smtEncoding = SMTEncoding.Arrays)
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala

@@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithFunArrays extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays)
+    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+        smtEncoding = SMTEncoding.FunArrays)
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala

@@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19)
+    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+        smtEncoding = SMTEncoding.OOPSLA19)
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala

@@ -12,7 +12,7 @@ class TestTransitionExecutorWithIncrementalAndArrays
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver =
-      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0,
+      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
               smtEncoding = SMTEncoding.Arrays))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala

@@ -11,7 +11,7 @@ class TestTransitionExecutorWithIncrementalAndFunArrays
     extends TestTransitionExecutorImpl[IncrementalExecutionContextSnapshot]
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
-    val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0,
+    val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
             smtEncoding = SMTEncoding.FunArrays))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala

@@ -18,7 +18,7 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver =
-      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0,
+      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
               smtEncoding = SMTEncoding.OOPSLA19))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala

@@ -12,7 +12,9 @@ import org.scalatestplus.junit.JUnitRunner
 class TestTransitionExecutorWithOfflineAndArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+              smtEncoding = SMTEncoding.Arrays))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala

@@ -13,7 +13,9 @@ class TestTransitionExecutorWithOfflineAndFunArrays
     extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+              smtEncoding = SMTEncoding.FunArrays))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala

@@ -18,7 +18,9 @@ import org.scalatestplus.junit.JUnitRunner
 class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] {
   override def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
-      .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19))
+      .createZ3(None,
+          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
+              smtEncoding = SMTEncoding.OOPSLA19))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }