diff --git a/.unreleased/features/z3-parameters.md b/.unreleased/features/z3-parameters.md new file mode 100644 index 0000000000..82195d8708 --- /dev/null +++ b/.unreleased/features/z3-parameters.md @@ -0,0 +1 @@ +Parse and pass z3 tuning parameters in the Apalache fine-tuning parameters (#2990) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 420f96efe2..b591cab5bf 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -39,6 +39,7 @@ - [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) @@ -46,7 +47,6 @@ - [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) diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index 22aa77b99a..56518e6e4c 100644 --- a/docs/src/apalache/tuning.md +++ b/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=` 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=` 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 diff --git a/docs/src/index.md b/docs/src/index.md index 4ff19a632d..66d84cab52 100644 --- a/docs/src/index.md +++ b/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) diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/log/LogbackConfigurator.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/log/LogbackConfigurator.scala index 07c697676c..ba91b0ef78 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/log/LogbackConfigurator.scala +++ b/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]() diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/FineTuningParser.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/FineTuningParser.scala new file mode 100644 index 0000000000..e8341e33ea --- /dev/null +++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/FineTuningParser.scala @@ -0,0 +1,578 @@ +package at.forsyte.apalache.infra.passes + +import java.util.regex.{Pattern, PatternSyntaxException} +import scala.collection.immutable + +trait ConfigFieldType + +case class StringFieldType() extends ConfigFieldType +case class UnsignedIntFieldType() extends ConfigFieldType +case class IntFieldType() extends ConfigFieldType +case class BoolFieldType() extends ConfigFieldType +case class DoubleFieldType() extends ConfigFieldType +case class EnumFieldType(values: String*) extends ConfigFieldType + +case class RegexFieldType() extends ConfigFieldType + +/** + * A configuration class that mirrors the parameters that can be passed via `--tuning-options-file` and + * `--tuning-options` to the commands `check` and `simulate`. [[FineTuningParser]] ensures that the parameters have + * proper syntax. It would be great to use [[https://pureconfig.github.io/docs/index.html PureConfig]] here, but it is + * too opinionated. + * + * @see + * [[https://apalache-mc.org/docs/apalache/tuning.html Tuning parameters]]. + * @author + * Igor Konnov, 2024 + */ +object FineTuningParser { + val fieldTypes: Map[String, ConfigFieldType] = immutable.Map( + "search.invariant.mode" -> EnumFieldType("before", "after"), + "search.transitionFilter" -> RegexFieldType(), + "search.invariantFilter" -> RegexFieldType(), + "rewriter.shortCircuit" -> BoolFieldType(), + // keeping for backwards compatibility + "smt.randomSeed" -> UnsignedIntFieldType(), + // For the parameters starting with "z3.", see: + // https://microsoft.github.io/z3guide/programming/Parameters/ + // Some of the fine-tuning parameters of Z3 are irrelevant for Apalache. + // We only omitted the parameters for the theories that are clearly not used by Apalache. + // To refresh the list of the z3 parameters, print the parameters with "z3 -p" and ask ChatGPT to update them. + // Double-check the enums though, as "z3 -p" only shows the default values. + "z3.auto_config" -> BoolFieldType(), + "z3.debug_ref_count" -> BoolFieldType(), + "z3.dot_proof_file" -> StringFieldType(), + "z3.dump_models" -> BoolFieldType(), + "z3.encoding" -> StringFieldType(), + "z3.memory_high_watermark" -> UnsignedIntFieldType(), + "z3.memory_high_watermark_mb" -> UnsignedIntFieldType(), + "z3.memory_max_alloc_count" -> UnsignedIntFieldType(), + "z3.memory_max_size" -> UnsignedIntFieldType(), + "z3.model" -> BoolFieldType(), + "z3.model_validate" -> BoolFieldType(), + "z3.proof" -> BoolFieldType(), + "z3.rlimit" -> UnsignedIntFieldType(), + "z3.smtlib2_compliant" -> BoolFieldType(), + "z3.stats" -> BoolFieldType(), + "z3.timeout" -> UnsignedIntFieldType(), + "z3.trace" -> BoolFieldType(), + "z3.trace_file_name" -> StringFieldType(), + "z3.type_check" -> BoolFieldType(), + "z3.unsat_core" -> BoolFieldType(), + "z3.verbose" -> UnsignedIntFieldType(), + "z3.warning" -> BoolFieldType(), + "z3.well_sorted_check" -> BoolFieldType(), + "z3.pi.arith" -> UnsignedIntFieldType(), + "z3.pi.arith_weight" -> UnsignedIntFieldType(), + "z3.pi.block_loop_patterns" -> BoolFieldType(), + "z3.pi.max_multi_patterns" -> UnsignedIntFieldType(), + "z3.pi.non_nested_arith_weight" -> UnsignedIntFieldType(), + "z3.pi.pull_quantifiers" -> BoolFieldType(), + "z3.pi.use_database" -> BoolFieldType(), + "z3.pi.warnings" -> BoolFieldType(), + "z3.tactic.blast_term_ite.max_inflation" -> UnsignedIntFieldType(), + "z3.tactic.blast_term_ite.max_steps" -> UnsignedIntFieldType(), + "z3.tactic.default_tactic" -> StringFieldType(), + "z3.tactic.propagate_values.max_rounds" -> UnsignedIntFieldType(), + "z3.tactic.solve_eqs.context_solve" -> BoolFieldType(), + "z3.tactic.solve_eqs.ite_solver" -> BoolFieldType(), + "z3.tactic.solve_eqs.max_occs" -> UnsignedIntFieldType(), + "z3.tactic.solve_eqs.theory_solver" -> BoolFieldType(), + "z3.pp.bounded" -> BoolFieldType(), + "z3.pp.bv_literals" -> BoolFieldType(), + "z3.pp.bv_neg" -> BoolFieldType(), + "z3.pp.decimal" -> BoolFieldType(), + "z3.pp.decimal_precision" -> UnsignedIntFieldType(), + "z3.pp.fixed_indent" -> BoolFieldType(), + "z3.pp.flat_assoc" -> BoolFieldType(), + "z3.pp.fp_real_literals" -> BoolFieldType(), + "z3.pp.max_depth" -> UnsignedIntFieldType(), + "z3.pp.max_indent" -> UnsignedIntFieldType(), + "z3.pp.max_num_lines" -> UnsignedIntFieldType(), + "z3.pp.max_ribbon" -> UnsignedIntFieldType(), + "z3.pp.max_width" -> UnsignedIntFieldType(), + "z3.pp.min_alias_size" -> UnsignedIntFieldType(), + "z3.pp.pretty_proof" -> BoolFieldType(), + "z3.pp.simplify_implies" -> BoolFieldType(), + "z3.pp.single_line" -> BoolFieldType(), + "z3.sat.abce" -> BoolFieldType(), + "z3.sat.acce" -> BoolFieldType(), + "z3.sat.anf" -> BoolFieldType(), + "z3.sat.anf.delay" -> UnsignedIntFieldType(), + "z3.sat.anf.exlin" -> BoolFieldType(), + "z3.sat.asymm_branch" -> BoolFieldType(), + "z3.sat.asymm_branch.all" -> BoolFieldType(), + "z3.sat.asymm_branch.delay" -> UnsignedIntFieldType(), + "z3.sat.asymm_branch.limit" -> UnsignedIntFieldType(), + "z3.sat.asymm_branch.rounds" -> UnsignedIntFieldType(), + "z3.sat.asymm_branch.sampled" -> BoolFieldType(), + "z3.sat.ate" -> BoolFieldType(), + "z3.sat.backtrack.conflicts" -> UnsignedIntFieldType(), + "z3.sat.backtrack.scopes" -> UnsignedIntFieldType(), + "z3.sat.bca" -> BoolFieldType(), + "z3.sat.bce" -> BoolFieldType(), + "z3.sat.bce_at" -> UnsignedIntFieldType(), + "z3.sat.bce_delay" -> UnsignedIntFieldType(), + "z3.sat.binspr" -> BoolFieldType(), + "z3.sat.blocked_clause_limit" -> UnsignedIntFieldType(), + "z3.sat.branching.anti_exploration" -> BoolFieldType(), + "z3.sat.branching.heuristic" -> EnumFieldType("vsids", "chb"), + "z3.sat.burst_search" -> UnsignedIntFieldType(), + "z3.sat.cardinality.encoding" -> EnumFieldType("grouped", "bimander", "ordered", "unate", "circuit"), + "z3.sat.cardinality.solver" -> BoolFieldType(), + "z3.sat.cce" -> BoolFieldType(), + "z3.sat.core.minimize" -> BoolFieldType(), + "z3.sat.core.minimize_partial" -> BoolFieldType(), + "z3.sat.cut" -> BoolFieldType(), + "z3.sat.cut.aig" -> BoolFieldType(), + "z3.sat.cut.delay" -> UnsignedIntFieldType(), + "z3.sat.cut.dont_cares" -> BoolFieldType(), + "z3.sat.cut.force" -> BoolFieldType(), + "z3.sat.cut.lut" -> BoolFieldType(), + "z3.sat.cut.npn3" -> BoolFieldType(), + "z3.sat.cut.redundancies" -> BoolFieldType(), + "z3.sat.cut.xor" -> BoolFieldType(), + "z3.sat.ddfw.init_clause_weight" -> UnsignedIntFieldType(), + "z3.sat.ddfw.reinit_base" -> UnsignedIntFieldType(), + "z3.sat.ddfw.restart_base" -> UnsignedIntFieldType(), + "z3.sat.ddfw.threads" -> UnsignedIntFieldType(), + "z3.sat.ddfw.use_reward_pct" -> UnsignedIntFieldType(), + "z3.sat.ddfw_search" -> BoolFieldType(), + "z3.sat.dimacs.core" -> BoolFieldType(), + "z3.sat.drat.activity" -> BoolFieldType(), + "z3.sat.drat.binary" -> BoolFieldType(), + "z3.sat.drat.check_sat" -> BoolFieldType(), + "z3.sat.drat.check_unsat" -> BoolFieldType(), + "z3.sat.drat.disable" -> BoolFieldType(), + "z3.sat.drat.file" -> StringFieldType(), + "z3.sat.dyn_sub_res" -> BoolFieldType(), + "z3.sat.elim_vars" -> BoolFieldType(), + "z3.sat.elim_vars_bdd" -> BoolFieldType(), + "z3.sat.elim_vars_bdd_delay" -> UnsignedIntFieldType(), + "z3.sat.enable_pre_simplify" -> BoolFieldType(), + "z3.sat.euf" -> BoolFieldType(), + "z3.sat.force_cleanup" -> BoolFieldType(), + "z3.sat.gc" -> EnumFieldType("psm", "glue", "glue_psm", "dyn_psm"), + "z3.sat.gc.burst" -> BoolFieldType(), + "z3.sat.gc.defrag" -> BoolFieldType(), + "z3.sat.gc.increment" -> UnsignedIntFieldType(), + "z3.sat.gc.initial" -> UnsignedIntFieldType(), + "z3.sat.gc.k" -> UnsignedIntFieldType(), + "z3.sat.gc.small_lbd" -> UnsignedIntFieldType(), + "z3.sat.inprocess.max" -> UnsignedIntFieldType(), + "z3.sat.inprocess.out" -> StringFieldType(), + "z3.sat.local_search" -> BoolFieldType(), + "z3.sat.local_search_dbg_flips" -> BoolFieldType(), + "z3.sat.local_search_mode" -> EnumFieldType("wsat", "qsat"), + "z3.sat.local_search_threads" -> UnsignedIntFieldType(), + "z3.sat.lookahead.cube.cutoff" -> EnumFieldType("depth", "freevars", "psat", "adaptive_freevars", + "adaptive_psat"), + "z3.sat.lookahead.cube.depth" -> UnsignedIntFieldType(), + "z3.sat.lookahead.cube.fraction" -> DoubleFieldType(), + "z3.sat.lookahead.cube.freevars" -> DoubleFieldType(), + "z3.sat.lookahead.cube.psat.clause_base" -> DoubleFieldType(), + "z3.sat.lookahead.cube.psat.trigger" -> DoubleFieldType(), + "z3.sat.lookahead.cube.psat.var_exp" -> DoubleFieldType(), + "z3.sat.lookahead.delta_fraction" -> DoubleFieldType(), + "z3.sat.lookahead.double" -> BoolFieldType(), + "z3.sat.lookahead.global_autarky" -> BoolFieldType(), + "z3.sat.lookahead.preselect" -> BoolFieldType(), + "z3.sat.lookahead.reward" -> EnumFieldType("march_cu", "ternary", "heule_schur", "heuleu", "unit"), + "z3.sat.lookahead.use_learned" -> BoolFieldType(), + "z3.sat.lookahead_scores" -> BoolFieldType(), + "z3.sat.lookahead_simplify" -> BoolFieldType(), + "z3.sat.lookahead_simplify.bca" -> BoolFieldType(), + "z3.sat.max_conflicts" -> UnsignedIntFieldType(), + "z3.sat.max_memory" -> UnsignedIntFieldType(), + "z3.sat.minimize_lemmas" -> BoolFieldType(), + "z3.sat.override_incremental" -> BoolFieldType(), + "z3.sat.pb.lemma_format" -> EnumFieldType("cardinality", "lemmas"), + "z3.sat.pb.min_arity" -> UnsignedIntFieldType(), + "z3.sat.pb.resolve" -> EnumFieldType("cardinality", "rounding"), + "z3.sat.pb.solver" -> EnumFieldType("solver", "circuit", "sorting", "totalizer", "binary_merge", "segmented"), + "z3.sat.phase" -> EnumFieldType("caching", "always_false", "always_true", "basic_caching", "random"), + "z3.sat.phase.sticky" -> BoolFieldType(), + "z3.sat.prob_search" -> BoolFieldType(), + "z3.sat.probing" -> BoolFieldType(), + "z3.sat.probing_binary" -> BoolFieldType(), + "z3.sat.probing_cache" -> BoolFieldType(), + "z3.sat.probing_cache_limit" -> UnsignedIntFieldType(), + "z3.sat.probing_limit" -> UnsignedIntFieldType(), + "z3.sat.propagate.prefetch" -> BoolFieldType(), + "z3.sat.random_freq" -> DoubleFieldType(), + "z3.sat.random_seed" -> UnsignedIntFieldType(), + "z3.sat.reorder.activity_scale" -> UnsignedIntFieldType(), + "z3.sat.reorder.base" -> UnsignedIntFieldType(), + "z3.sat.reorder.itau" -> DoubleFieldType(), + "z3.sat.rephase.base" -> UnsignedIntFieldType(), + "z3.sat.resolution.cls_cutoff1" -> UnsignedIntFieldType(), + "z3.sat.resolution.cls_cutoff2" -> UnsignedIntFieldType(), + "z3.sat.resolution.limit" -> UnsignedIntFieldType(), + "z3.sat.resolution.lit_cutoff_range1" -> UnsignedIntFieldType(), + "z3.sat.resolution.lit_cutoff_range2" -> UnsignedIntFieldType(), + "z3.sat.resolution.lit_cutoff_range3" -> UnsignedIntFieldType(), + "z3.sat.resolution.occ_cutoff" -> UnsignedIntFieldType(), + "z3.sat.resolution.occ_cutoff_range1" -> UnsignedIntFieldType(), + "z3.sat.resolution.occ_cutoff_range2" -> UnsignedIntFieldType(), + "z3.sat.resolution.occ_cutoff_range3" -> UnsignedIntFieldType(), + "z3.sat.restart" -> EnumFieldType("static", "luby", "ema", "geometric"), + "z3.sat.restart.emafastglue" -> DoubleFieldType(), + "z3.sat.restart.emaslowglue" -> DoubleFieldType(), + "z3.sat.restart.factor" -> DoubleFieldType(), + "z3.sat.restart.fast" -> BoolFieldType(), + "z3.sat.restart.initial" -> UnsignedIntFieldType(), + "z3.sat.restart.margin" -> DoubleFieldType(), + "z3.sat.restart.max" -> UnsignedIntFieldType(), + "z3.sat.retain_blocked_clauses" -> BoolFieldType(), + "z3.sat.scc" -> BoolFieldType(), + "z3.sat.scc.tr" -> BoolFieldType(), + "z3.sat.search.sat.conflicts" -> UnsignedIntFieldType(), + "z3.sat.search.unsat.conflicts" -> UnsignedIntFieldType(), + "z3.sat.simplify.delay" -> UnsignedIntFieldType(), + "z3.sat.smt" -> BoolFieldType(), + "z3.sat.smt.proof.check" -> BoolFieldType(), + "z3.sat.subsumption" -> BoolFieldType(), + "z3.sat.subsumption.limit" -> UnsignedIntFieldType(), + "z3.sat.threads" -> UnsignedIntFieldType(), + "z3.sat.variable_decay" -> UnsignedIntFieldType(), + "z3.model.compact" -> BoolFieldType(), + "z3.model.completion" -> BoolFieldType(), + "z3.model.inline_def" -> BoolFieldType(), + "z3.model.partial" -> BoolFieldType(), + "z3.model.user_functions" -> BoolFieldType(), + "z3.model.v1" -> BoolFieldType(), + "z3.model.v2" -> BoolFieldType(), + "z3.solver.axioms2files" -> BoolFieldType(), + "z3.solver.cancel_backup_file" -> StringFieldType(), + "z3.solver.instantiations2console" -> BoolFieldType(), + "z3.solver.lemmas2console" -> BoolFieldType(), + "z3.solver.proof.check" -> BoolFieldType(), + "z3.solver.proof.check_rup" -> BoolFieldType(), + "z3.solver.proof.log" -> StringFieldType(), + "z3.solver.proof.save" -> BoolFieldType(), + "z3.solver.proof.trim" -> BoolFieldType(), + "z3.solver.smtlib2_log" -> StringFieldType(), + "z3.solver.timeout" -> UnsignedIntFieldType(), + "z3.opt.dump_benchmarks" -> BoolFieldType(), + "z3.opt.dump_models" -> BoolFieldType(), + "z3.opt.elim_01" -> BoolFieldType(), + "z3.opt.enable_core_rotate" -> BoolFieldType(), + "z3.opt.enable_lns" -> BoolFieldType(), + "z3.opt.enable_sat" -> BoolFieldType(), + "z3.opt.enable_sls" -> BoolFieldType(), + "z3.opt.incremental" -> BoolFieldType(), + "z3.opt.lns_conflicts" -> UnsignedIntFieldType(), + "z3.opt.maxlex.enable" -> BoolFieldType(), + "z3.opt.maxres.add_upper_bound_block" -> BoolFieldType(), + "z3.opt.maxres.hill_climb" -> BoolFieldType(), + "z3.opt.maxres.max_core_size" -> UnsignedIntFieldType(), + "z3.opt.maxres.max_correction_set_size" -> UnsignedIntFieldType(), + "z3.opt.maxres.max_num_cores" -> UnsignedIntFieldType(), + "z3.opt.maxres.maximize_assignment" -> BoolFieldType(), + "z3.opt.maxres.pivot_on_correction_set" -> BoolFieldType(), + "z3.opt.maxres.wmax" -> BoolFieldType(), + "z3.opt.maxsat_engine" -> EnumFieldType("core_maxsat", "wmax", "maxres", "pd-maxres", "maxres-bin", "rc2"), + "z3.opt.optsmt_engine" -> EnumFieldType("basic", "symba"), + "z3.opt.pb.compile_equality" -> BoolFieldType(), + "z3.opt.pp.neat" -> BoolFieldType(), + "z3.opt.pp.wcnf" -> BoolFieldType(), + "z3.opt.priority" -> EnumFieldType("lex", "pareto", "box"), + "z3.opt.rc2.totalizer" -> BoolFieldType(), + "z3.opt.rlimit" -> UnsignedIntFieldType(), + "z3.opt.solution_prefix" -> StringFieldType(), + "z3.opt.timeout" -> UnsignedIntFieldType(), + "z3.parallel.conquer.backtrack_frequency" -> UnsignedIntFieldType(), + "z3.parallel.conquer.batch_size" -> UnsignedIntFieldType(), + "z3.parallel.conquer.delay" -> UnsignedIntFieldType(), + "z3.parallel.conquer.restart.max" -> UnsignedIntFieldType(), + "z3.parallel.enable" -> BoolFieldType(), + "z3.parallel.simplify.exp" -> DoubleFieldType(), + "z3.parallel.simplify.inprocess.max" -> UnsignedIntFieldType(), + "z3.parallel.simplify.max_conflicts" -> UnsignedIntFieldType(), + "z3.parallel.simplify.restart.max" -> UnsignedIntFieldType(), + "z3.parallel.threads.max" -> UnsignedIntFieldType(), + "z3.nnf.ignore_labels" -> BoolFieldType(), + "z3.nnf.max_memory" -> UnsignedIntFieldType(), + "z3.nnf.mode" -> EnumFieldType("skolem", "quantifiers", "full"), + "z3.nnf.sk_hack" -> BoolFieldType(), + "z3.algebraic.factor" -> BoolFieldType(), + "z3.algebraic.factor_max_prime" -> UnsignedIntFieldType(), + "z3.algebraic.factor_num_primes" -> UnsignedIntFieldType(), + "z3.algebraic.factor_search_size" -> UnsignedIntFieldType(), + "z3.algebraic.min_mag" -> UnsignedIntFieldType(), + "z3.algebraic.zero_accuracy" -> UnsignedIntFieldType(), + "z3.combined_solver.ignore_solver1" -> BoolFieldType(), + "z3.combined_solver.solver2_timeout" -> UnsignedIntFieldType(), + "z3.combined_solver.solver2_unknown" -> UnsignedIntFieldType(), + "z3.ackermannization.eager" -> BoolFieldType(), + "z3.ackermannization.inc_sat_backend" -> BoolFieldType(), + "z3.ackermannization.sat_backend" -> BoolFieldType(), + "z3.nlsat.check_lemmas" -> BoolFieldType(), + "z3.nlsat.factor" -> BoolFieldType(), + "z3.nlsat.inline_vars" -> BoolFieldType(), + "z3.nlsat.lazy" -> UnsignedIntFieldType(), + "z3.nlsat.log_lemmas" -> BoolFieldType(), + "z3.nlsat.max_conflicts" -> UnsignedIntFieldType(), + "z3.nlsat.max_memory" -> UnsignedIntFieldType(), + "z3.nlsat.minimize_conflicts" -> BoolFieldType(), + "z3.nlsat.randomize" -> BoolFieldType(), + "z3.nlsat.reorder" -> BoolFieldType(), + "z3.nlsat.seed" -> UnsignedIntFieldType(), + "z3.nlsat.shuffle_vars" -> BoolFieldType(), + "z3.nlsat.simplify_conflicts" -> BoolFieldType(), + "z3.rewriter.algebraic_number_evaluator" -> BoolFieldType(), + "z3.rewriter.arith_ineq_lhs" -> BoolFieldType(), + "z3.rewriter.arith_lhs" -> BoolFieldType(), + "z3.rewriter.bit2bool" -> BoolFieldType(), + "z3.rewriter.blast_distinct" -> BoolFieldType(), + "z3.rewriter.blast_distinct_threshold" -> UnsignedIntFieldType(), + "z3.rewriter.blast_eq_value" -> BoolFieldType(), + "z3.rewriter.blast_select_store" -> BoolFieldType(), + "z3.rewriter.bv_extract_prop" -> BoolFieldType(), + "z3.rewriter.bv_ineq_consistency_test_max" -> UnsignedIntFieldType(), + "z3.rewriter.bv_ite2id" -> BoolFieldType(), + "z3.rewriter.bv_le2extract" -> BoolFieldType(), + "z3.rewriter.bv_le_extra" -> BoolFieldType(), + "z3.rewriter.bv_not_simpl" -> BoolFieldType(), + "z3.rewriter.bv_sort_ac" -> BoolFieldType(), + "z3.rewriter.cache_all" -> BoolFieldType(), + "z3.rewriter.coalesce_chars" -> BoolFieldType(), + "z3.rewriter.div0_ackermann_limit" -> UnsignedIntFieldType(), + "z3.rewriter.elim_and" -> BoolFieldType(), + "z3.rewriter.elim_ite" -> BoolFieldType(), + "z3.rewriter.elim_rem" -> BoolFieldType(), + "z3.rewriter.elim_sign_ext" -> BoolFieldType(), + "z3.rewriter.elim_to_real" -> BoolFieldType(), + "z3.rewriter.enable_der" -> BoolFieldType(), + "z3.rewriter.eq2ineq" -> BoolFieldType(), + "z3.rewriter.expand_nested_stores" -> BoolFieldType(), + "z3.rewriter.expand_power" -> BoolFieldType(), + "z3.rewriter.expand_select_ite" -> BoolFieldType(), + "z3.rewriter.expand_select_store" -> BoolFieldType(), + "z3.rewriter.expand_store_eq" -> BoolFieldType(), + "z3.rewriter.expand_tan" -> BoolFieldType(), + "z3.rewriter.flat" -> BoolFieldType(), + "z3.rewriter.flat_and_or" -> BoolFieldType(), + "z3.rewriter.gcd_rounding" -> BoolFieldType(), + "z3.rewriter.hi_div0" -> BoolFieldType(), + "z3.rewriter.hi_fp_unspecified" -> BoolFieldType(), + "z3.rewriter.hoist_ite" -> BoolFieldType(), + "z3.rewriter.hoist_mul" -> BoolFieldType(), + "z3.rewriter.ignore_patterns_on_ground_qbody" -> BoolFieldType(), + "z3.rewriter.ite_extra_rules" -> BoolFieldType(), + "z3.rewriter.local_ctx" -> BoolFieldType(), + "z3.rewriter.local_ctx_limit" -> UnsignedIntFieldType(), + "z3.rewriter.max_degree" -> UnsignedIntFieldType(), + "z3.rewriter.max_memory" -> UnsignedIntFieldType(), + "z3.rewriter.max_steps" -> UnsignedIntFieldType(), + "z3.rewriter.mul2concat" -> BoolFieldType(), + "z3.rewriter.mul_to_power" -> BoolFieldType(), + "z3.rewriter.pull_cheap_ite" -> BoolFieldType(), + "z3.rewriter.push_ite_arith" -> BoolFieldType(), + "z3.rewriter.push_ite_bv" -> BoolFieldType(), + "z3.rewriter.push_to_real" -> BoolFieldType(), + "z3.rewriter.rewrite_patterns" -> BoolFieldType(), + "z3.rewriter.som" -> BoolFieldType(), + "z3.rewriter.som_blowup" -> UnsignedIntFieldType(), + "z3.rewriter.sort_disjunctions" -> BoolFieldType(), + "z3.rewriter.sort_store" -> BoolFieldType(), + "z3.rewriter.sort_sums" -> BoolFieldType(), + "z3.rewriter.split_concat_eq" -> BoolFieldType(), + "z3.smt.arith.auto_config_simplex" -> BoolFieldType(), + "z3.smt.arith.bprop_on_pivoted_rows" -> BoolFieldType(), + "z3.smt.arith.branch_cut_ratio" -> UnsignedIntFieldType(), + "z3.smt.arith.dump_lemmas" -> BoolFieldType(), + "z3.smt.arith.eager_eq_axioms" -> BoolFieldType(), + "z3.smt.arith.enable_hnf" -> BoolFieldType(), + "z3.smt.arith.greatest_error_pivot" -> BoolFieldType(), + "z3.smt.arith.ignore_int" -> BoolFieldType(), + "z3.smt.arith.int_eq_branch" -> BoolFieldType(), + "z3.smt.arith.min" -> BoolFieldType(), + "z3.smt.arith.nl" -> BoolFieldType(), + "z3.smt.arith.nl.branching" -> BoolFieldType(), + "z3.smt.arith.nl.cross_nested" -> BoolFieldType(), + "z3.smt.arith.nl.delay" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.expensive_patching" -> BoolFieldType(), + "z3.smt.arith.nl.expp" -> BoolFieldType(), + "z3.smt.arith.nl.gr_q" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner" -> BoolFieldType(), + "z3.smt.arith.nl.grobner_cnfl_to_report" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_eqs_growth" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_expr_degree_growth" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_expr_size_growth" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_frequency" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_max_simplified" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_row_length_limit" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.grobner_subs_fixed" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.horner" -> BoolFieldType(), + "z3.smt.arith.nl.horner_frequency" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.horner_row_length_limit" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.horner_subs_fixed" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.nra" -> BoolFieldType(), + "z3.smt.arith.nl.optimize_bounds" -> BoolFieldType(), + "z3.smt.arith.nl.order" -> BoolFieldType(), + "z3.smt.arith.nl.propagate_linear_monomials" -> BoolFieldType(), + "z3.smt.arith.nl.rounds" -> UnsignedIntFieldType(), + "z3.smt.arith.nl.tangents" -> BoolFieldType(), + "z3.smt.arith.print_ext_var_names" -> BoolFieldType(), + "z3.smt.arith.print_stats" -> BoolFieldType(), + "z3.smt.arith.propagate_eqs" -> BoolFieldType(), + "z3.smt.arith.propagation_mode" -> UnsignedIntFieldType(), + "z3.smt.arith.random_initial_value" -> BoolFieldType(), + "z3.smt.arith.rep_freq" -> UnsignedIntFieldType(), + "z3.smt.arith.simplex_strategy" -> UnsignedIntFieldType(), + "z3.smt.arith.solver" -> UnsignedIntFieldType(), + "z3.smt.arith.validate" -> BoolFieldType(), + "z3.smt.array.extensional" -> BoolFieldType(), + "z3.smt.array.weak" -> BoolFieldType(), + "z3.smt.auto_config" -> BoolFieldType(), + "z3.smt.bound_simplifier" -> BoolFieldType(), + "z3.smt.bv.delay" -> BoolFieldType(), + "z3.smt.bv.enable_int2bv" -> BoolFieldType(), + "z3.smt.bv.reflect" -> BoolFieldType(), + "z3.smt.bv.size_reduce" -> BoolFieldType(), + "z3.smt.bv.solver" -> UnsignedIntFieldType(), + "z3.smt.bv.watch_diseq" -> BoolFieldType(), + "z3.smt.candidate_models" -> BoolFieldType(), + "z3.smt.case_split" -> UnsignedIntFieldType(), + "z3.smt.clause_proof" -> BoolFieldType(), + "z3.smt.core.extend_nonlocal_patterns" -> BoolFieldType(), + "z3.smt.core.extend_patterns" -> BoolFieldType(), + "z3.smt.core.extend_patterns.max_distance" -> UnsignedIntFieldType(), + "z3.smt.core.minimize" -> BoolFieldType(), + "z3.smt.core.validate" -> BoolFieldType(), + "z3.smt.cube_depth" -> UnsignedIntFieldType(), + "z3.smt.dack" -> UnsignedIntFieldType(), + "z3.smt.dack.eq" -> BoolFieldType(), + "z3.smt.dack.factor" -> DoubleFieldType(), + "z3.smt.dack.gc" -> UnsignedIntFieldType(), + "z3.smt.dack.gc_inv_decay" -> DoubleFieldType(), + "z3.smt.dack.threshold" -> UnsignedIntFieldType(), + "z3.smt.delay_units" -> BoolFieldType(), + "z3.smt.delay_units_threshold" -> UnsignedIntFieldType(), + "z3.smt.dt_lazy_splits" -> UnsignedIntFieldType(), + "z3.smt.elim_unconstrained" -> BoolFieldType(), + "z3.smt.ematching" -> BoolFieldType(), + "z3.smt.induction" -> BoolFieldType(), + "z3.smt.lemma_gc_strategy" -> UnsignedIntFieldType(), + "z3.smt.logic" -> StringFieldType(), + "z3.smt.macro_finder" -> BoolFieldType(), + "z3.smt.max_conflicts" -> UnsignedIntFieldType(), + "z3.smt.mbqi" -> BoolFieldType(), + "z3.smt.mbqi.force_template" -> UnsignedIntFieldType(), + "z3.smt.mbqi.id" -> StringFieldType(), + "z3.smt.mbqi.max_cexs" -> UnsignedIntFieldType(), + "z3.smt.mbqi.max_cexs_incr" -> UnsignedIntFieldType(), + "z3.smt.mbqi.max_iterations" -> UnsignedIntFieldType(), + "z3.smt.mbqi.trace" -> BoolFieldType(), + "z3.smt.pb.conflict_frequency" -> UnsignedIntFieldType(), + "z3.smt.pb.learn_complements" -> BoolFieldType(), + "z3.smt.phase_caching_off" -> UnsignedIntFieldType(), + "z3.smt.phase_caching_on" -> UnsignedIntFieldType(), + "z3.smt.phase_selection" -> UnsignedIntFieldType(), + "z3.smt.propagate_values" -> BoolFieldType(), + "z3.smt.pull_nested_quantifiers" -> BoolFieldType(), + "z3.smt.q.lift_ite" -> UnsignedIntFieldType(), + "z3.smt.q.lite" -> BoolFieldType(), + "z3.smt.qi.cost" -> StringFieldType(), + "z3.smt.qi.eager_threshold" -> DoubleFieldType(), + "z3.smt.qi.lazy_threshold" -> DoubleFieldType(), + "z3.smt.qi.max_instances" -> UnsignedIntFieldType(), + "z3.smt.qi.max_multi_patterns" -> UnsignedIntFieldType(), + "z3.smt.qi.profile" -> BoolFieldType(), + "z3.smt.qi.profile_freq" -> UnsignedIntFieldType(), + "z3.smt.qi.quick_checker" -> UnsignedIntFieldType(), + "z3.smt.qsat_use_qel" -> BoolFieldType(), + "z3.smt.quasi_macros" -> BoolFieldType(), + "z3.smt.random_seed" -> UnsignedIntFieldType(), + "z3.smt.refine_inj_axioms" -> BoolFieldType(), + "z3.smt.relevancy" -> UnsignedIntFieldType(), + "z3.smt.restart.max" -> UnsignedIntFieldType(), + "z3.smt.restart_factor" -> DoubleFieldType(), + "z3.smt.restart_strategy" -> UnsignedIntFieldType(), + "z3.smt.restricted_quasi_macros" -> BoolFieldType(), + "z3.smt.seq.max_unfolding" -> UnsignedIntFieldType(), + "z3.smt.seq.min_unfolding" -> UnsignedIntFieldType(), + "z3.smt.seq.split_w_len" -> BoolFieldType(), + "z3.smt.seq.validate" -> BoolFieldType(), + "z3.smt.solve_eqs" -> BoolFieldType(), + "z3.smt.str.aggressive_length_testing" -> BoolFieldType(), + "z3.smt.str.aggressive_unroll_testing" -> BoolFieldType(), + "z3.smt.str.aggressive_value_testing" -> BoolFieldType(), + "z3.smt.str.fast_length_tester_cache" -> BoolFieldType(), + "z3.smt.str.fast_value_tester_cache" -> BoolFieldType(), + "z3.smt.str.fixed_length_naive_cex" -> BoolFieldType(), + "z3.smt.str.fixed_length_refinement" -> BoolFieldType(), + "z3.smt.str.overlap_priority" -> DoubleFieldType(), + "z3.smt.str.regex_automata_difficulty_threshold" -> UnsignedIntFieldType(), + "z3.smt.str.regex_automata_failed_automaton_threshold" -> UnsignedIntFieldType(), + "z3.smt.str.regex_automata_failed_intersection_threshold" -> UnsignedIntFieldType(), + "z3.smt.str.regex_automata_intersection_difficulty_threshold" -> UnsignedIntFieldType(), + "z3.smt.str.regex_automata_length_attempt_threshold" -> UnsignedIntFieldType(), + "z3.smt.str.string_constant_cache" -> BoolFieldType(), + "z3.smt.str.strong_arrangements" -> BoolFieldType(), + "z3.smt.string_solver" -> EnumFieldType("seq"), + "z3.smt.theory_aware_branching" -> BoolFieldType(), + "z3.smt.theory_case_split" -> BoolFieldType(), + "z3.smt.threads" -> UnsignedIntFieldType(), + "z3.smt.threads.cube_frequency" -> UnsignedIntFieldType(), + "z3.smt.threads.max_conflicts" -> UnsignedIntFieldType(), + "z3.smt.up.persist_clauses" -> BoolFieldType(), + ) + + def fromStrings(input: Map[String, String]): Either[String, Map[String, Object]] = { + val parsed = input.toList.map({ case (k, v) => mapKV(k, v) }) + val (errors, noErrors) = parsed.partition(_.isLeft) + if (errors.isEmpty) { + Right(noErrors.collect({ case Right(kv) => kv }).toMap) + } else { + Left(errors.mkString("; ")) + } + } + + private def mapKV(key: String, value: String): Either[String, (String, Object)] = { + fieldTypes.get(key) match { + case Some(StringFieldType()) => + Right((key, value.asInstanceOf[Object])) + + case Some(IntFieldType()) => + value.toIntOption.toRight(s"Non-integer value $value for $key").map(v => (key, v.asInstanceOf[Object])) + + case Some(UnsignedIntFieldType()) => + // even though Z3 has some parameters that are unsigned 32-bit integers, the Java API only supports signed integers + value.toIntOption match { + case Some(v) if v >= 0 => Right((key, v.asInstanceOf[Object])) + case _ => Left(s"Expected an unsigned integer for $key, but got $value") + } + + case Some(BoolFieldType()) => + value.toBooleanOption.toRight(s"Non-Boolean value $value for $key").map(v => (key, v.asInstanceOf[Object])) + + case Some(DoubleFieldType()) => + Right((key, value.toDouble.asInstanceOf[Object])) + + case Some(EnumFieldType(values @ _*)) => + if (values.contains(value)) { + Right((key, value)) + } else { + Left(s"Invalid value $value for $key, expected one of ${values.mkString(", ")}") + } + + case Some(RegexFieldType()) => + parseRegex(value).map((key, _)) + + case _ => + Left(s"Unexpected field $key") + } + } + + private def parseRegex(r: String): Either[String, String] = { + try { + Pattern.compile(r) + Right(r) + } catch { + case e: PatternSyntaxException => + Left(s"Invalid regex $r: ${e.getMessage}") + } + } +} diff --git a/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestFineTuningParser.scala b/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestFineTuningParser.scala new file mode 100644 index 0000000000..ed8f0fda80 --- /dev/null +++ b/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestFineTuningParser.scala @@ -0,0 +1,72 @@ +package at.forsyte.apalache.infra.passes + +import org.junit.runner.RunWith +import org.scalatest.funsuite.AnyFunSuite +import org.scalatestplus.junit.JUnitRunner + +@RunWith(classOf[JUnitRunner]) +class TestFineTuningParser extends AnyFunSuite { + test("can parse empty tuning options") { + val config: Either[String, Map[String, Object]] = FineTuningParser.fromStrings(Map[String, String]()) + assert(config.isRight && config.map(_.isEmpty).contains(true)) + } + + test("parses rewriter.shortCircuit") { + val config = FineTuningParser.fromStrings(Map("rewriter.shortCircuit" -> "true")) + assert(config.isRight && config.exists(_.get("rewriter.shortCircuit").contains(true))) + } + + test("fails on wrong rewriter.shortCircuit") { + val r = "12333" + val config = FineTuningParser.fromStrings(Map("rewriter.shortCircuit" -> r)) + assert(config.isLeft) + } + + test("parses search.transitionFilter") { + val r = "(0->0|1->5|2->(2|3)|[3-9]->.*|[1-9][0-9]+->.*)" + val config = + FineTuningParser.fromStrings(Map("search.transitionFilter" -> r)) + assert(config.isRight && config.exists(_.get("search.transitionFilter").contains(r))) + } + + test("fails on wrong search.transitionFilter") { + val r = "(aaaa" + val config = + FineTuningParser.fromStrings(Map("search.transitionFilter" -> r)) + assert(config.isLeft) + } + + test("parses search.invariantFilter") { + val r = "(0->0|1->5|2->(2|3)|[3-9]->.*|[1-9][0-9]+->.*)" + val config = + FineTuningParser.fromStrings(Map("search.invariantFilter" -> r)) + assert(config.isRight && config.exists(_.get("search.invariantFilter").contains(r))) + } + + test("fails on wrong search.invariantFilter") { + val r = "(aaaa" + val config = + FineTuningParser.fromStrings(Map("search.invariantFilter" -> r)) + assert(config.isLeft) + } + + test("parses z3.memory_high_watermark_mb") { + val config = FineTuningParser.fromStrings(Map("z3.memory_high_watermark_mb" -> "123")) + assert(config.isRight && config.exists(_.get("z3.memory_high_watermark_mb").contains(123))) + } + + test("fails on wrong z3.memory_high_watermark_mb") { + val config = FineTuningParser.fromStrings(Map("z3.memory_high_watermark_mb" -> "aaaa")) + assert(config.isLeft) + } + + test("parses z3.sat.cardinality.encoding") { + val config = FineTuningParser.fromStrings(Map("z3.sat.cardinality.encoding" -> "circuit")) + assert(config.isRight && config.exists(_.get("z3.sat.cardinality.encoding").contains("circuit"))) + } + + test("fails on wrong z3.sat.cardinality.encoding") { + val config = FineTuningParser.fromStrings(Map("z3.sat.cardinality.encoding" -> "aaaa")) + assert(config.isLeft) + } +} diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala index dbe3854f05..95174141f1 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala +++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala @@ -82,6 +82,8 @@ object Tool extends LazyLogging { * the exit code; as usual, 0 means success. */ def run(args: Array[String]): Int = { + // Configure the silent logger first. Otherwise, Apache Commons spills a lot of text to the console. + new LogbackConfigurator(None, None).configureDefaultContext() // first, call the arguments parser, which can also handle the standard commands such as version val cli = Cli .parse(args) @@ -104,7 +106,6 @@ object Tool extends LazyLogging { case None => ExitCodes.OK // One of our commands. case Some(cmd) => { - printStatsConfig() val exitcode = outputAndLogConfig(cmd) match { diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala index 20a5773436..5578c1065b 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala +++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala @@ -14,8 +14,9 @@ import at.forsyte.apalache.infra.passes.options.Config import at.forsyte.apalache.infra.passes.options.OptionGroup import org.apache.commons.io.FilenameUtils import at.forsyte.apalache.infra.passes.options.SourceOption -import at.forsyte.apalache.infra.passes.PassChainExecutor +import at.forsyte.apalache.infra.passes.{FineTuningParser, PassChainExecutor} import at.forsyte.apalache.infra.passes.options.Algorithm + import scala.util.Try /** @@ -147,7 +148,11 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci for (name: String <- config.getKeys.asScala) { map += (name -> config.getString(name)) } - map + // parse the properties and convert them back to strings for config serialization + FineTuningParser.fromStrings(map) match { + case Right(parsed) => parsed.view.mapValues(_.toString).toMap + case Left(error) => throw new PassOptionException(s"Error in the properties file $filename: $error") + } } catch { case _: FileNotFoundException => throw new PassOptionException(s"The properties file $filename not found") @@ -170,7 +175,11 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci val hereProps = { if (propsAsString.trim.nonEmpty) { - propsAsString.split(':').map(parseKeyValue).toMap + // parse the properties and convert them back to strings for config serialization + FineTuningParser.fromStrings(propsAsString.split(':').map(parseKeyValue).toMap) match { + case Right(parsed) => parsed.view.mapValues(_.toString).toMap + case Left(error) => throw new PassOptionException(s"Error in the properties string $propsAsString: $error") + } } else { Map.empty } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala index e505371812..71c00aa3c2 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala @@ -1,7 +1,8 @@ package at.forsyte.apalache.tla.bmcmt.passes import at.forsyte.apalache.infra.passes.options.SMTEncoding -import at.forsyte.apalache.infra.ExitCodes +import at.forsyte.apalache.infra.{ExitCodes, PassOptionException} +import at.forsyte.apalache.infra.passes.FineTuningParser import at.forsyte.apalache.infra.passes.Pass.PassResult import at.forsyte.apalache.tla.assignments.ModuleAdapter import at.forsyte.apalache.tla.bmcmt._ @@ -77,7 +78,14 @@ class BoundedCheckerPassImpl @Inject() ( val smtRandomSeed = tuning.getOrElse("smt.randomSeed", "0").toInt val smtStatsSec = tuning.getOrElse("smt.statsSec", SolverConfig.default.z3StatsSec.toString).toInt - val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtStatsSec, smtEncoding) + // Parse the tuning parameters that are relevant to Z3. + // Currently, `tuning` may contain more configuration options (added by some passes) than we parse in + // `FineTuningParser`. + val z3Parameters = FineTuningParser.fromStrings(tuning.filter(_._1.startsWith("z3."))) match { + case Right(params) => params.map { case (k, v) => (k.substring("z3.".length), v) } + case Left(error) => throw new PassOptionException(s"Error in tuning parameters: $error") + } + val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding, smtStatsSec, z3Parameters) val result = options.checker.algo match { case Algorithm.Incremental => runIncrementalChecker(params, input, tuning, solverConfig) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala index 0a4d6face7..fcd282e5c9 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala @@ -14,6 +14,8 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding * The random seed to be passed to z3 as :random-seed. * @param smtEncoding * The SMT encoding to be used. + * @param z3Params + * The parameters to be passed to z3, which must contain proper keys and values. * * @author * Igor Konnov, Rodrigo Otoni @@ -22,8 +24,9 @@ sealed case class SolverConfig( debug: Boolean, profile: Boolean, randomSeed: Int, + smtEncoding: SMTEncoding, z3StatsSec: Int, - smtEncoding: SMTEncoding) {} + z3Params: Map[String, Object] = Map()) {} object SolverConfig { @@ -32,5 +35,5 @@ object SolverConfig { */ val default: SolverConfig = new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19, - z3StatsSec = 60) + z3StatsSec = 60, z3Params = Map()) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 0c9ea9476e..a978d637bb 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -62,8 +62,20 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL // Set random seed. We are also setting it via global parameters above, but `Global.setParameter()` says: // "When a Z3 module is initialized it will use the value of these parameters when Z3_params objects are not provided." params.add("seed", config.randomSeed) + // When the user sets z3.smt.logic = QF_LIA, z3 complains about random_seed. + // https://github.com/apalache-mc/apalache/issues/2989 params.add("random_seed", config.randomSeed) - // params.add("array.extensional", false) // disables extensionality for the theory of arrays + config.z3Params.foreach { case (k, v) => + if (v.isInstanceOf[Int]) { + params.add(k, v.asInstanceOf[Int]) + } else if (v.isInstanceOf[Boolean]) { + params.add(k, v.asInstanceOf[Boolean]) + } else if (v.isInstanceOf[Double]) { + params.add(k, v.asInstanceOf[Double]) + } else { + params.add(k, v.toString) + } + } z3solver.setParameters(params) log(s";; ${params}")