Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Propagate z3 parameters in the tuning options #2990

Merged
merged 18 commits into from
Sep 23, 2024
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .unreleased/features/z3-parameters.md
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Parse and pass z3 tuning parameters in the Apalache fine-tuning parameters (#2990)
2 changes: 1 addition & 1 deletion docs/src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
49 changes: 43 additions & 6 deletions docs/src/apalache/tuning.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -91,6 +86,47 @@ 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

**DEPRECATED:** You can now pass the seeds directly to Z3 via [Z3 Tuning Parameters](#z3-tuning-parameters).

`smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
`sat.random_seed` and `smt.random_seed`).
konnov marked this conversation as resolved.
Show resolved Hide resolved

## Translation to SMT

### Short-circuiting
Expand All @@ -104,3 +140,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
5 changes: 4 additions & 1 deletion docs/src/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 => configureConsoleOnly(loggerContext)
konnov marked this conversation as resolved.
Show resolved Hide resolved
}
}

def configureSilent(loggerContext: LoggerContext): Unit = {
def configureConsoleOnly(loggerContext: LoggerContext): Unit = {
konnov marked this conversation as resolved.
Show resolved Hide resolved
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 =>
Expand All @@ -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)
Expand All @@ -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]()
Expand Down
Loading
Loading