Merge pull request #2990 from apalache-mc/igor/z3-params

Propagate z3 parameters in the tuning options

.unreleased/features/z3-parameters.md

@@ -0,0 +1 @@
+Parse and pass z3 tuning parameters in the Apalache fine-tuning parameters (#2990)

docs/src/SUMMARY.md

@@ -39,14 +39,14 @@
     - [TLA+ Execution Statistics](./apalache/statistics.md)
     - [Profiling Your Specification](./apalache/profiling.md)
     - [Five minutes of theory](./apalache/theory.md)
+- [Fine Tuning](./apalache/tuning.md)
 - [TLC Configuration Files](./apalache/tlc-config.md)
 - [The Snowcat Type Checker](./apalache/typechecker-snowcat.md)
 - [Supported Features](./apalache/features.md)
 - [Obsolete: Recursive operators and functions](./apalache/principles/recursive.md)
 - [Known Issues](./apalache/known-issues.md)
 - [Antipatterns](./apalache/antipatterns.md)
 - [TLA+ Preprocessing](./apalache/preprocessing.md)
-- [Fine Tuning](./apalache/tuning.md)
 - [Assignments and Symbolic Transitions in Depth](./apalache/assignments-in-depth.md)
 - [KerA: kernel logic of actions](./apalache/kera.md)
 

docs/src/apalache/tuning.md

@@ -15,12 +15,7 @@ passing the option `--tuning-options` that has the following format:
     ...
     ```
 
-The following options are supported:
-
-## Randomization
-
-`smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
-`sat.random_seed` and `smt.random_seed`).
+The rest of this page summarizes the supported parameters.
 
 ## Invariant mode
 
@@ -91,6 +86,46 @@ steps.
 You can also use this option to check different parts of an invariant on
 different machines to speed up turnaround time.
 
+## Z3 Tuning Parameters
+
+Z3 has a very large number of [Z3 Parameters][]. If you have a CLI version of Z3
+installed, you can see a complete list of supported parameters by running `z3`:
+
+```sh
+z3 -pd
+```
+
+In Apalache, you can pass a Z3 parameter `x.y.z=v` as a fine-tuning parameter:
+
+```
+z3.x.y.z=v
+```
+
+For example, to change the SAT and SMT restarts strategies to static:
+
+```
+z3.sat.restart = static
+z3.smt.restart_strategy = 3
+```
+
+Sometimes, the above settings help Apalache to show unsatisfiability faster.
+
+You can also employ Z3 parallelization by setting the number of threads:
+
+```
+z3.sat.threads=10
+```
+
+Technically, Apalache propagates all the parameters that start with `z3.` to Z3.
+However, some of these parameters fail in the solver, even when they work in the
+command line. Hence, you have to experiment with the choice of parameters.
+
+## Randomization
+
+`smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
+`sat.random_seed` and `smt.random_seed`). Note that this parameter sets the seed
+across the solvers for various logic theories in z3.
+
 ## Translation to SMT
 
 ### Short-circuiting
@@ -104,3 +139,4 @@ true B)`. Otherwise, disjunctions and conjunctions are directly translated to
 
 [invariants]: ../apalache/principles/invariants.md
 [trace invariants]: ../apalache/principles/invariants.md#trace-invariants
+[Z3 Parameters]: https://microsoft.github.io/z3guide/programming/Parameters

docs/src/index.md

@@ -2,7 +2,10 @@
 
 This book collects five related, but independent, sets of documentation:
 
-1. [The Apalache User Manual](./apalache/index.md)
+1. [The Apalache User Manual](./apalache/index.md). The most often needed chapters:
+   - [Installation](./apalache/installation/index.md)
+   - [Running the Tool](./apalache/running.md)
+   - [Fine Tuning](./apalache/tuning.md)
 2. [Apalache Tutorials](./tutorials/index.md)
 3. [Apalache HOWTOs](./HOWTOs/index.md)
 4. [A TLA+ Language Reference Manual](./lang/index.md)

mod-infra/src/main/scala/at/forsyte/apalache/infra/log/LogbackConfigurator.scala

@@ -24,21 +24,23 @@ class LogbackConfigurator(runDir: Option[Path], customRunDir: Option[Path]) exte
     setContext(loggerContext)
     runDir match {
       case Some(_) => configure(loggerContext)
-      case None    => configureSilent(loggerContext)
+      case None    => configureConsoleOnlyWarn(loggerContext)
     }
   }
 
-  def configureSilent(loggerContext: LoggerContext): Unit = {
+  def configureConsoleOnlyWarn(loggerContext: LoggerContext): Unit = {
     loggerContext.reset() // forget everything that was configured automagically
     val rootLogger = loggerContext.getLogger(org.slf4j.Logger.ROOT_LOGGER_NAME)
-    rootLogger.setLevel(Level.OFF)
+    val consoleAppender = mkConsoleAppender(loggerContext, isDecorated = false)
+    rootLogger.addAppender(consoleAppender)
+    rootLogger.setLevel(Level.WARN)
   }
 
   override def configure(loggerContext: LoggerContext): Configurator.ExecutionStatus = {
     addInfo("Setting up a logback configuration")
     loggerContext.reset() // forget everything that was configured automagically
     val rootLogger = loggerContext.getLogger(org.slf4j.Logger.ROOT_LOGGER_NAME)
-    val consoleAppender = mkConsoleAppender(loggerContext)
+    val consoleAppender = mkConsoleAppender(loggerContext, isDecorated = true)
     // only warnings at the root level
     rootLogger.setLevel(Level.WARN)
     (runDir ++ customRunDir).foreach(d =>
@@ -50,7 +52,7 @@ class LogbackConfigurator(runDir: Option[Path], customRunDir: Option[Path]) exte
     Configurator.ExecutionStatus.NEUTRAL
   }
 
-  private def mkConsoleAppender(loggerContext: LoggerContext): ConsoleAppender[ILoggingEvent] = {
+  private def mkConsoleAppender(loggerContext: LoggerContext, isDecorated: Boolean): ConsoleAppender[ILoggingEvent] = {
     // set up ConsoleAppender
     val app = new ConsoleAppender[ILoggingEvent]()
     app.setContext(loggerContext)
@@ -61,7 +63,7 @@ class LogbackConfigurator(runDir: Option[Path], customRunDir: Option[Path]) exte
     filter.start()
     app.addFilter(filter)
     val layout = new PatternLayout()
-    layout.setPattern("%-65msg %.-1level@%d{HH:mm:ss.SSS}%n")
+    layout.setPattern(if (isDecorated) "%-65msg %.-1level@%d{HH:mm:ss.SSS}%n" else "%-80msg%n")
     layout.setContext(loggerContext)
     layout.start()
     val encoder = new LayoutWrappingEncoder[ILoggingEvent]()