mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 20:46:01 +00:00
Code Activity

add notes on parameter tuning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-12 14:56:14 -07:00
parent 648e051156
commit 9e00b4b813
1 changed files with 66 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

66
PARALLEL_PROJECT_NOTES.md
View file

@ -150,3 +150,69 @@ Weighted sampling works as follows: You are given a set of items with weights $(
Add $w = \sum_j w_j$. Pick a random number $w_0$ in the range $0\ldots w$.
Then you pick item $i_n$ such that $n$ is the smallest index with $\sum_{j = 1}^n w_j \geq w_0$.
SMT parameters that could be tuned:
<pre>
arith.bprop_on_pivoted_rows (bool) (default: true)
arith.branch_cut_ratio (unsigned int) (default: 2)
arith.eager_eq_axioms (bool) (default: true)
arith.enable_hnf (bool) (default: true)
arith.greatest_error_pivot (bool) (default: false)
arith.int_eq_branch (bool) (default: false)
arith.min (bool) (default: false)
arith.nl.branching (bool) (default: true)
arith.nl.cross_nested (bool) (default: true)
arith.nl.delay (unsigned int) (default: 10)
arith.nl.expensive_patching (bool) (default: false)
arith.nl.expp (bool) (default: false)
arith.nl.gr_q (unsigned int) (default: 10)
arith.nl.grobner (bool) (default: true)
arith.nl.grobner_cnfl_to_report (unsigned int) (default: 1)
arith.nl.grobner_eqs_growth (unsigned int) (default: 10)
arith.nl.grobner_expr_degree_growth (unsigned int) (default: 2)
arith.nl.grobner_expr_size_growth (unsigned int) (default: 2)
arith.nl.grobner_frequency (unsigned int) (default: 4)
arith.nl.grobner_max_simplified (unsigned int) (default: 10000)
arith.nl.grobner_row_length_limit (unsigned int) (default: 10)
arith.nl.grobner_subs_fixed (unsigned int) (default: 1)
arith.nl.horner (bool) (default: true)
arith.nl.horner_frequency (unsigned int) (default: 4)
arith.nl.horner_row_length_limit (unsigned int) (default: 10)
arith.nl.horner_subs_fixed (unsigned int) (default: 2)
arith.nl.nra (bool) (default: true)
arith.nl.optimize_bounds (bool) (default: true)
arith.nl.order (bool) (default: true)
arith.nl.propagate_linear_monomials (bool) (default: true)
arith.nl.rounds (unsigned int) (default: 1024)
arith.nl.tangents (bool) (default: true)
arith.propagate_eqs (bool) (default: true)
arith.propagation_mode (unsigned int) (default: 1)
arith.random_initial_value (bool) (default: false)
arith.rep_freq (unsigned int) (default: 0)
arith.simplex_strategy (unsigned int) (default: 0)
dack (unsigned int) (default: 1)
dack.eq (bool) (default: false)
dack.factor (double) (default: 0.1)
dack.gc (unsigned int) (default: 2000)
dack.gc_inv_decay (double) (default: 0.8)
dack.threshold (unsigned int) (default: 10)
delay_units (bool) (default: false)
delay_units_threshold (unsigned int) (default: 32)
dt_lazy_splits (unsigned int) (default: 1)
lemma_gc_strategy (unsigned int) (default: 0)
phase_caching_off (unsigned int) (default: 100)
phase_caching_on (unsigned int) (default: 400)
phase_selection (unsigned int) (default: 3)
qi.eager_threshold (double) (default: 10.0)
qi.lazy_threshold (double) (default: 20.0)
qi.quick_checker (unsigned int) (default: 0)
relevancy (unsigned int) (default: 2)
restart_factor (double) (default: 1.1)
restart_strategy (unsigned int) (default: 1)
seq.max_unfolding (unsigned int) (default: 1000000000)
seq.min_unfolding (unsigned int) (default: 1)
seq.split_w_len (bool) (default: true)
</pre>