mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

parameters neatified

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-08-16 09:14:34 -07:00
parent 498b6de3a7
commit 9d6de2f873
2 changed files with 606 additions and 607 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
Parameters.md
View file

@ -1,9 +1,8 @@
Z3 Options Enabled
## Module pi ## Module pi
Description: pattern inference (heuristics) for universal formulas (without annotation) Description: pattern inference (heuristics) for universal formulas (without annotation)
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
arith | unsigned int | 0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms | 1 arith | unsigned int | 0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms | 1
arith_weight | unsigned int | default weight for quantifiers where the only available pattern has nested arithmetic terms | 5 arith_weight | unsigned int | default weight for quantifiers where the only available pattern has nested arithmetic terms | 5
block_loop_patterns | bool | block looping patterns during pattern inference | true block_loop_patterns | bool | block looping patterns during pattern inference | true
@ -17,7 +16,7 @@ warnings | bool | enable/disable warning messages in the pattern inference mod
Description: tactic parameters Description: tactic parameters
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
blast_term_ite.max_inflation | unsigned int | multiplicative factor of initial term size. | 4294967295 blast_term_ite.max_inflation | unsigned int | multiplicative factor of initial term size. | 4294967295
blast_term_ite.max_steps | unsigned int | maximal number of steps allowed for tactic. | 4294967295 blast_term_ite.max_steps | unsigned int | maximal number of steps allowed for tactic. | 4294967295
default_tactic | symbol | overwrite default tactic in strategic solver | default_tactic | symbol | overwrite default tactic in strategic solver |
@ -31,7 +30,7 @@ solve_eqs.theory_solver | bool | use theory solvers. | true
Description: pretty printer Description: pretty printer
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
bounded | bool | ignore characters exceeding max width | false bounded | bool | ignore characters exceeding max width | false
bv_literals | bool | use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing | true bv_literals | bool | use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing | true
bv_neg | bool | use bvneg when displaying Bit-Vector literals where the most significant bit is 1 | false bv_neg | bool | use bvneg when displaying Bit-Vector literals where the most significant bit is 1 | false
@ -54,7 +53,7 @@ single_line | bool | ignore line breaks when true | false
Description: propositional SAT solver Description: propositional SAT solver
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
abce | bool | eliminate blocked clauses using asymmetric literals | false abce | bool | eliminate blocked clauses using asymmetric literals | false
acce | bool | eliminate covered clauses using asymmetric added literals | false acce | bool | eliminate covered clauses using asymmetric added literals | false
anf | bool | enable ANF based simplification in-processing | false anf | bool | enable ANF based simplification in-processing | false
@ -197,7 +196,7 @@ variable_decay | unsigned int | multiplier (divided by 100) for the VSIDS acti
Description: solver parameters Description: solver parameters
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
axioms2files | bool | print negated theory axioms to separate files during search | false axioms2files | bool | print negated theory axioms to separate files during search | false
cancel_backup_file | symbol | file to save partial search state if search is canceled | cancel_backup_file | symbol | file to save partial search state if search is canceled |
lemmas2console | bool | print lemmas during search | false lemmas2console | bool | print lemmas during search | false
@ -208,7 +207,7 @@ timeout | unsigned int | timeout on the solver object; overwrites a global tim
Description: optimization parameters Description: optimization parameters
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
dump_benchmarks | bool | dump benchmarks for profiling | false dump_benchmarks | bool | dump benchmarks for profiling | false
dump_models | bool | display intermediary models to stdout | false dump_models | bool | display intermediary models to stdout | false
elim_01 | bool | eliminate 01 variables | true elim_01 | bool | eliminate 01 variables | true
@ -242,7 +241,7 @@ timeout | unsigned int | timeout (in milliseconds) (UINT_MAX and 0 mean no tim
Description: parameters for parallel solver Description: parameters for parallel solver
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
conquer.backtrack_frequency | unsigned int | frequency to apply core minimization during conquer | 10 conquer.backtrack_frequency | unsigned int | frequency to apply core minimization during conquer | 10
conquer.batch_size | unsigned int | number of cubes to batch together for fast conquer | 100 conquer.batch_size | unsigned int | number of cubes to batch together for fast conquer | 100
conquer.delay | unsigned int | delay of cubes until applying conquer | 10 conquer.delay | unsigned int | delay of cubes until applying conquer | 10
@ -258,7 +257,7 @@ threads.max | unsigned int | caps maximal number of threads below the number o
Description: negation normal form Description: negation normal form
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
ignore_labels | bool | remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false ignore_labels | bool | remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false
max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295
mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem
@ -268,7 +267,7 @@ sk_hack | bool | hack for VCC | false
Description: real algebraic number package. Non-default parameter settings are not supported Description: real algebraic number package. Non-default parameter settings are not supported
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
factor | bool | use polynomial factorization to simplify polynomials representing algebraic numbers | true factor | bool | use polynomial factorization to simplify polynomials representing algebraic numbers | true
factor_max_prime | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31 factor_max_prime | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31
factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1 factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1
@ -280,7 +279,7 @@ zero_accuracy | unsigned int | one of the most time-consuming operations in th
Description: combines two solvers: non-incremental (solver1) and incremental (solver2) Description: combines two solvers: non-incremental (solver1) and incremental (solver2)
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
ignore_solver1 | bool | if true, solver 2 is always used | false ignore_solver1 | bool | if true, solver 2 is always used | false
solver2_timeout | unsigned int | fallback to solver 1 after timeout even when in incremental model | 4294967295 solver2_timeout | unsigned int | fallback to solver 1 after timeout even when in incremental model | 4294967295
solver2_unknown | unsigned int | what should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 1 | 1 solver2_unknown | unsigned int | what should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 1 | 1
@ -289,19 +288,20 @@ solver2_unknown | unsigned int | what should be done when solver 2 returns unk
Description: real closed fields Description: real closed fields
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
clean_denominators | bool | clean denominators before root isolation | true clean_denominators | bool | clean denominators before root isolation | true
inf_precision | unsigned int | a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values | 24 inf_precision | unsigned int | a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values | 24
initial_precision | unsigned int | a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division | 24 initial_precision | unsigned int | a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division | 24
lazy_algebraic_normalization | bool | during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the defining polynomial is monic | true lazy_algebraic_normalization | bool | during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the defining polynomial is monic | true
max_precision | unsigned int | during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision | 128 max_precision | unsigned int | during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision | 128
use_prem | bool | use pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequences | true use_prem | bool | use pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequences | true
ERROR: unknown module 'rewriter, description: new formula simplification module used in the tactic framework'
## Module ackermannization ## Module ackermannization
Description: solving UF via ackermannization Description: solving UF via ackermannization
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
eager | bool | eagerly instantiate all congruence rules | true eager | bool | eagerly instantiate all congruence rules | true
inc_sat_backend | bool | use incremental SAT | false inc_sat_backend | bool | use incremental SAT | false
sat_backend | bool | use SAT rather than SMT in qfufbv_ackr_tactic | false sat_backend | bool | use SAT rather than SMT in qfufbv_ackr_tactic | false
@ -310,7 +310,7 @@ sat_backend | bool | use SAT rather than SMT in qfufbv_ackr_tactic | false
Description: nonlinear solver Description: nonlinear solver
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false
factor | bool | factor polynomials produced during conflict resolution. | true factor | bool | factor polynomials produced during conflict resolution. | true
inline_vars | bool | inline variables that can be isolated from equations (not supported in incremental mode) | false inline_vars | bool | inline variables that can be isolated from equations (not supported in incremental mode) | false
@ -330,7 +330,7 @@ simplify_conflicts | bool | simplify conflicts using equalities before resolvi
Description: fixedpoint parameters Description: fixedpoint parameters
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
bmc.linear_unrolling_depth | unsigned int | Maximal level to explore | 4294967295 bmc.linear_unrolling_depth | unsigned int | Maximal level to explore | 4294967295
datalog.all_or_nothing_deltas | bool | compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not | false datalog.all_or_nothing_deltas | bool | compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not | false
datalog.check_relation | symbol | name of default relation to check. operations on the default relation will be verified using SMT solving | null datalog.check_relation | symbol | name of default relation to check. operations on the default relation will be verified using SMT solving | null
@ -448,7 +448,7 @@ xform.unfold_rules | unsigned int | unfold rules statically using iterative sq
Description: smt solver based on lazy smt Description: smt solver based on lazy smt
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
arith.auto_config_simplex | bool | force simplex solver in auto_config | false arith.auto_config_simplex | bool | force simplex solver in auto_config | false
arith.bprop_on_pivoted_rows | bool | propagate bounds on rows changed by the pivot operation | true arith.bprop_on_pivoted_rows | bool | propagate bounds on rows changed by the pivot operation | true
arith.branch_cut_ratio | unsigned int | branch/cut ratio for linear integer arithmetic | 2 arith.branch_cut_ratio | unsigned int | branch/cut ratio for linear integer arithmetic | 2
@ -580,7 +580,7 @@ threads.max_conflicts | unsigned int | maximal number of conflicts between rou
Description: Experimental Stochastic Local Search Solver (for QFBV only). Description: Experimental Stochastic Local Search Solver (for QFBV only).
Parameter | Type | Description | Default Parameter | Type | Description | Default
---------------------------------------- ----------|------|-------------|--------
early_prune | bool | use early pruning for score prediction | true early_prune | bool | use early pruning for score prediction | true
max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295
max_restarts | unsigned int | maximum number of restarts | 4294967295 max_restarts | unsigned int | maximum number of restarts | 4294967295
@ -603,4 +603,3 @@ walksat_ucb_forget | double | scale touched by this factor every base restart
walksat_ucb_init | bool | initialize total ucb touched to formula size | false walksat_ucb_init | bool | initialize total ucb touched to formula size | false
walksat_ucb_noise | double | add noise 0 <= 256 * ucb_noise to ucb score for assertion selection | 0.0002 walksat_ucb_noise | double | add noise 0 <= 256 * ucb_noise to ucb score for assertion selection | 0.0002
wp | unsigned int | random walk with probability wp / 1024 | 100 wp | unsigned int | random walk with probability wp / 1024 | 100

2
src/util/params.cpp
View file

@ -169,7 +169,7 @@ struct param_descrs::imp {
std::sort(names.begin(), names.end(), symlt()); std::sort(names.begin(), names.end(), symlt());
if (markdown) { if (markdown) {
out << " Parameter | Type | Description | Default\n"; out << " Parameter | Type | Description | Default\n";
out << " ----------------------------------------\n"; out << " ----------|------|-------------|--------\n";
} }
for (symbol const& name : names) { for (symbol const& name : names) {
for (unsigned i = 0; i < indent; i++) out << " "; for (unsigned i = 0; i < indent; i++) out << " ";