diff --git a/Parameters.md b/Parameters.md index 47a61826af3..ea69becade2 100644 --- a/Parameters.md +++ b/Parameters.md @@ -1,606 +1,605 @@ -Z3 Options Enabled -## Module pi - -Description: pattern inference (heuristics) for universal formulas (without annotation) - 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_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 -max_multi_patterns | unsigned int | when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern | 0 -non_nested_arith_weight | unsigned int | default weight for quantifiers where the only available pattern has non nested arithmetic terms | 10 -pull_quantifiers | bool | pull nested quantifiers, if no pattern was found | true -use_database | bool | use pattern database | false -warnings | bool | enable/disable warning messages in the pattern inference module | false - -## Module tactic - -Description: tactic parameters - Parameter | Type | Description | Default - ---------------------------------------- -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 -default_tactic | symbol | overwrite default tactic in strategic solver | -propagate_values.max_rounds | unsigned int | maximal number of rounds to propagate values. | 4 -solve_eqs.context_solve | bool | solve equalities within disjunctions. | true -solve_eqs.ite_solver | bool | use if-then-else solvers. | true -solve_eqs.max_occs | unsigned int | maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295 -solve_eqs.theory_solver | bool | use theory solvers. | true - -## Module pp - -Description: pretty printer - Parameter | Type | Description | Default - ---------------------------------------- -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_neg | bool | use bvneg when displaying Bit-Vector literals where the most significant bit is 1 | false -decimal | bool | pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise | false -decimal_precision | unsigned int | maximum number of decimal places to be used when pp.decimal=true | 10 -fixed_indent | bool | use a fixed indentation for applications | false -flat_assoc | bool | flat associative operators (when pretty printing SMT2 terms/formulas) | true -fp_real_literals | bool | use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing | false -max_depth | unsigned int | max. term depth (when pretty printing SMT2 terms/formulas) | 5 -max_indent | unsigned int | max. indentation in pretty printer | 4294967295 -max_num_lines | unsigned int | max. number of lines to be displayed in pretty printer | 4294967295 -max_ribbon | unsigned int | max. ribbon (width - indentation) in pretty printer | 80 -max_width | unsigned int | max. width in pretty printer | 80 -min_alias_size | unsigned int | min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas) | 10 -pretty_proof | bool | use slower, but prettier, printer for proofs | false -simplify_implies | bool | simplify nested implications for pretty printing | true -single_line | bool | ignore line breaks when true | false - -## Module sat - -Description: propositional SAT solver - Parameter | Type | Description | Default - ---------------------------------------- -abce | bool | eliminate blocked clauses using asymmetric literals | false -acce | bool | eliminate covered clauses using asymmetric added literals | false -anf | bool | enable ANF based simplification in-processing | false -anf.delay | unsigned int | delay ANF simplification by in-processing round | 2 -anf.exlin | bool | enable extended linear simplification | false -asymm_branch | bool | asymmetric branching | true -asymm_branch.all | bool | asymmetric branching on all literals per clause | false -asymm_branch.delay | unsigned int | number of simplification rounds to wait until invoking asymmetric branch simplification | 1 -asymm_branch.limit | unsigned int | approx. maximum number of literals visited during asymmetric branching | 100000000 -asymm_branch.rounds | unsigned int | maximal number of rounds to run asymmetric branch simplifications if progress is made | 2 -asymm_branch.sampled | bool | use sampling based asymmetric branching based on binary implication graph | true -ate | bool | asymmetric tautology elimination | true -backtrack.conflicts | unsigned int | number of conflicts before enabling chronological backtracking | 4000 -backtrack.scopes | unsigned int | number of scopes to enable chronological backtracking | 100 -bca | bool | blocked clause addition - add blocked binary clauses | false -bce | bool | eliminate blocked clauses | false -bce_at | unsigned int | eliminate blocked clauses only once at the given simplification round | 2 -bce_delay | unsigned int | delay eliminate blocked clauses until simplification round | 2 -binspr | bool | enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models | false -blocked_clause_limit | unsigned int | maximum number of literals visited during blocked clause elimination | 100000000 -branching.anti_exploration | bool | apply anti-exploration heuristic for branch selection | false -branching.heuristic | symbol | branching heuristic vsids, chb | vsids -burst_search | unsigned int | number of conflicts before first global simplification | 100 -cardinality.encoding | symbol | encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit | grouped -cardinality.solver | bool | use cardinality solver | true -cce | bool | eliminate covered clauses | false -core.minimize | bool | minimize computed core | false -core.minimize_partial | bool | apply partial (cheap) core minimization | false -cut | bool | enable AIG based simplification in-processing | false -cut.aig | bool | extract aigs (and ites) from cluases for cut simplification | false -cut.delay | unsigned int | delay cut simplification by in-processing round | 2 -cut.dont_cares | bool | integrate dont cares with cuts | true -cut.force | bool | force redoing cut-enumeration until a fixed-point | false -cut.lut | bool | extract luts from clauses for cut simplification | false -cut.npn3 | bool | extract 3 input functions from clauses for cut simplification | false -cut.redundancies | bool | integrate redundancy checking of cuts | true -cut.xor | bool | extract xors from clauses for cut simplification | false -ddfw.init_clause_weight | unsigned int | initial clause weight for DDFW local search | 8 -ddfw.reinit_base | unsigned int | increment basis for geometric backoff scheme of re-initialization of weights | 10000 -ddfw.restart_base | unsigned int | number of flips used a starting point for hessitant restart backoff | 100000 -ddfw.threads | unsigned int | number of ddfw threads to run in parallel with sat solver | 0 -ddfw.use_reward_pct | unsigned int | percentage to pick highest reward variable when it has reward 0 | 15 -ddfw_search | bool | use ddfw local search instead of CDCL | false -dimacs.core | bool | extract core from DIMACS benchmarks | false -drat.activity | bool | dump variable activities | false -drat.binary | bool | use Binary DRAT output format | false -drat.check_sat | bool | build up internal trace, check satisfying model | false -drat.check_unsat | bool | build up internal proof and check | false -drat.file | symbol | file to dump DRAT proofs | -drup.trim | bool | build and trim drup proof | false -dyn_sub_res | bool | dynamic subsumption resolution for minimizing learned clauses | true -elim_vars | bool | enable variable elimination using resolution during simplification | true -elim_vars_bdd | bool | enable variable elimination using BDD recompilation during simplification | true -elim_vars_bdd_delay | unsigned int | delay elimination of variables using BDDs until after simplification round | 3 -enable_pre_simplify | bool | enable pre simplifications before the bounded search | false -euf | bool | enable euf solver (this feature is preliminary and not ready for general consumption) | false -force_cleanup | bool | force cleanup to remove tautologies and simplify clauses | false -gc | symbol | garbage collection strategy: psm, glue, glue_psm, dyn_psm | glue_psm -gc.burst | bool | perform eager garbage collection during initialization | false -gc.defrag | bool | defragment clauses when garbage collecting | true -gc.increment | unsigned int | increment to the garbage collection threshold | 500 -gc.initial | unsigned int | learned clauses garbage collection frequency | 20000 -gc.k | unsigned int | learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm) | 7 -gc.small_lbd | unsigned int | learned clauses with small LBD are never deleted (only used in dyn_psm) | 3 -inprocess.max | unsigned int | maximal number of inprocessing passes | 4294967295 -inprocess.out | symbol | file to dump result of the first inprocessing step and exit | -local_search | bool | use local search instead of CDCL | false -local_search_dbg_flips | bool | write debug information for number of flips | false -local_search_mode | symbol | local search algorithm, either default wsat or qsat | wsat -local_search_threads | unsigned int | number of local search threads to find satisfiable solution | 0 -lookahead.cube.cutoff | symbol | cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat | depth -lookahead.cube.depth | unsigned int | cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth. | 1 -lookahead.cube.fraction | double | adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat | 0.4 -lookahead.cube.freevars | double | cube free variable fraction. Used when lookahead.cube.cutoff is freevars | 0.8 -lookahead.cube.psat.clause_base | double | clause base for PSAT cutoff | 2 -lookahead.cube.psat.trigger | double | trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat | 5 -lookahead.cube.psat.var_exp | double | free variable exponent for PSAT cutoff | 1 -lookahead.delta_fraction | double | number between 0 and 1, the smaller the more literals are selected for double lookahead | 1.0 -lookahead.double | bool | enable doubld lookahead | true -lookahead.global_autarky | bool | prefer to branch on variables that occur in clauses that are reduced | false -lookahead.preselect | bool | use pre-selection of subset of variables for branching | false -lookahead.reward | symbol | select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu | march_cu -lookahead.use_learned | bool | use learned clauses when selecting lookahead literal | false -lookahead_scores | bool | extract lookahead scores. A utility that can only be used from the DIMACS front-end | false -lookahead_simplify | bool | use lookahead solver during simplification | false -lookahead_simplify.bca | bool | add learned binary clauses as part of lookahead simplification | true -max_conflicts | unsigned int | maximum number of conflicts | 4294967295 -max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 -minimize_lemmas | bool | minimize learned clauses | true -override_incremental | bool | override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused | false -pb.lemma_format | symbol | generate either cardinality or pb lemmas | cardinality -pb.min_arity | unsigned int | minimal arity to compile pb/cardinality constraints to CNF | 9 -pb.resolve | symbol | resolution strategy for boolean algebra solver: cardinality, rounding | cardinality -pb.solver | symbol | method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver) | solver -phase | symbol | phase selection strategy: always_false, always_true, basic_caching, random, caching | caching -phase.sticky | bool | use sticky phase caching | true -prob_search | bool | use probsat local search instead of CDCL | false -probing | bool | apply failed literal detection during simplification | true -probing_binary | bool | probe binary clauses | true -probing_cache | bool | add binary literals as lemmas | true -probing_cache_limit | unsigned int | cache binaries unless overall memory usage exceeds cache limit | 1024 -probing_limit | unsigned int | limit to the number of probe calls | 5000000 -propagate.prefetch | bool | prefetch watch lists for assigned literals | true -random_freq | double | frequency of random case splits | 0.01 -random_seed | unsigned int | random seed | 0 -reorder.activity_scale | unsigned int | scaling factor for activity update | 100 -reorder.base | unsigned int | number of conflicts per random reorder | 4294967295 -reorder.itau | double | inverse temperature for softmax | 4.0 -rephase.base | unsigned int | number of conflicts per rephase | 1000 -resolution.cls_cutoff1 | unsigned int | limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination | 100000000 -resolution.cls_cutoff2 | unsigned int | limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination | 700000000 -resolution.limit | unsigned int | approx. maximum number of literals visited during variable elimination | 500000000 -resolution.lit_cutoff_range1 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 700 -resolution.lit_cutoff_range2 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 400 -resolution.lit_cutoff_range3 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 300 -resolution.occ_cutoff | unsigned int | first cutoff (on number of positive/negative occurrences) for Boolean variable elimination | 10 -resolution.occ_cutoff_range1 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 8 -resolution.occ_cutoff_range2 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 5 -resolution.occ_cutoff_range3 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 3 -restart | symbol | restart strategy: static, luby, ema or geometric | ema -restart.emafastglue | double | ema alpha factor for fast moving average | 0.03 -restart.emaslowglue | double | ema alpha factor for slow moving average | 1e-05 -restart.factor | double | restart increment factor for geometric strategy | 1.5 -restart.fast | bool | use fast restart approach only removing less active literals. | true -restart.initial | unsigned int | initial restart (number of conflicts) | 2 -restart.margin | double | margin between fast and slow restart factors. For ema | 1.1 -restart.max | unsigned int | maximal number of restarts. | 4294967295 -retain_blocked_clauses | bool | retain blocked clauses as lemmas | true -scc | bool | eliminate Boolean variables by computing strongly connected components | true -scc.tr | bool | apply transitive reduction, eliminate redundant binary clauses | true -search.sat.conflicts | unsigned int | period for solving for sat (in number of conflicts) | 400 -search.unsat.conflicts | unsigned int | period for solving for unsat (in number of conflicts) | 400 -simplify.delay | unsigned int | set initial delay of simplification by a conflict count | 0 -subsumption | bool | eliminate subsumed clauses | true -subsumption.limit | unsigned int | approx. maximum number of literals visited during subsumption (and subsumption resolution) | 100000000 -threads | unsigned int | number of parallel threads to use | 1 -variable_decay | unsigned int | multiplier (divided by 100) for the VSIDS activity increment | 110 - -## Module solver - -Description: solver parameters - Parameter | Type | Description | Default - ---------------------------------------- -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 | -lemmas2console | bool | print lemmas during search | false -smtlib2_log | symbol | file to save solver interaction | -timeout | unsigned int | timeout on the solver object; overwrites a global timeout | 4294967295 - -## Module opt - -Description: optimization parameters - Parameter | Type | Description | Default - ---------------------------------------- -dump_benchmarks | bool | dump benchmarks for profiling | false -dump_models | bool | display intermediary models to stdout | false -elim_01 | bool | eliminate 01 variables | true -enable_core_rotate | bool | enable core rotation to both sample cores and correction sets | false -enable_lns | bool | enable LNS during weighted maxsat | false -enable_sat | bool | enable the new SAT core for propositional constraints | true -enable_sls | bool | enable SLS tuning during weighted maxsat | false -incremental | bool | set incremental mode. It disables pre-processing and enables adding constraints in model event handler | false -lns_conflicts | unsigned int | initial conflict count for LNS search | 1000 -maxlex.enable | bool | enable maxlex heuristic for lexicographic MaxSAT problems | true -maxres.add_upper_bound_block | bool | restict upper bound with constraint | false -maxres.hill_climb | bool | give preference for large weight cores | true -maxres.max_core_size | unsigned int | break batch of generated cores if size reaches this number | 3 -maxres.max_correction_set_size | unsigned int | allow generating correction set constraints up to maximal size | 3 -maxres.max_num_cores | unsigned int | maximal number of cores per round | 200 -maxres.maximize_assignment | bool | find an MSS/MCS to improve current assignment | false -maxres.pivot_on_correction_set | bool | reduce soft constraints if the current correction set is smaller than current core | true -maxres.wmax | bool | use weighted theory solver to constrain upper bounds | false -maxsat_engine | symbol | select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2' | maxres -optsmt_engine | symbol | select optimization engine: 'basic', 'symba' | basic -pb.compile_equality | bool | compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites) | false -pp.neat | bool | use neat (as opposed to less readable, but faster) pretty printer when displaying context | true -pp.wcnf | bool | print maxsat benchmark into wcnf format | false -priority | symbol | select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box' | lex -rc2.totalizer | bool | use totalizer for rc2 encoding | true -rlimit | unsigned int | resource limit (0 means no limit) | 0 -solution_prefix | symbol | path prefix to dump intermediary, but non-optimal, solutions | -timeout | unsigned int | timeout (in milliseconds) (UINT_MAX and 0 mean no timeout) | 4294967295 - -## Module parallel - -Description: parameters for parallel solver - Parameter | Type | Description | Default - ---------------------------------------- -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.delay | unsigned int | delay of cubes until applying conquer | 10 -conquer.restart.max | unsigned int | maximal number of restarts during conquer phase | 5 -enable | bool | enable parallel solver by default on selected tactics (for QF_BV) | false -simplify.exp | double | restart and inprocess max is multiplied by simplify.exp ^ depth | 1 -simplify.inprocess.max | unsigned int | maximal number of inprocessing steps during simplification | 2 -simplify.max_conflicts | unsigned int | maximal number of conflicts during simplifcation phase | 4294967295 -simplify.restart.max | unsigned int | maximal number of restarts during simplification phase | 5000 -threads.max | unsigned int | caps maximal number of threads below the number of processors | 10000 - -## Module nnf - -Description: negation normal form - Parameter | Type | Description | Default - ---------------------------------------- -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 -mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem -sk_hack | bool | hack for VCC | false - -## Module algebraic - -Description: real algebraic number package. Non-default parameter settings are not supported - Parameter | Type | Description | Default - ---------------------------------------- -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_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_search_size | 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 can be used to limit the search space | 5000 -min_mag | unsigned int | Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16 -zero_accuracy | unsigned int | one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0 - -## Module combined_solver - -Description: combines two solvers: non-incremental (solver1) and incremental (solver2) - Parameter | Type | Description | Default - ---------------------------------------- -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_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 - -## Module rcf - -Description: real closed fields - Parameter | Type | Description | Default - ---------------------------------------- -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 -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 -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 - -## Module ackermannization - -Description: solving UF via ackermannization - Parameter | Type | Description | Default - ---------------------------------------- -eager | bool | eagerly instantiate all congruence rules | true -inc_sat_backend | bool | use incremental SAT | false -sat_backend | bool | use SAT rather than SMT in qfufbv_ackr_tactic | false - -## Module nlsat - -Description: nonlinear solver - Parameter | Type | Description | Default - ---------------------------------------- -check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false -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 -lazy | unsigned int | how lazy the solver is. | 0 -log_lemmas | bool | display lemmas as self-contained SMT formulas | false -max_conflicts | unsigned int | maximum number of conflicts. | 4294967295 -max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 -minimize_conflicts | bool | minimize conflicts | false -randomize | bool | randomize selection of a witness in nlsat. | true -reorder | bool | reorder variables. | true -seed | unsigned int | random seed. | 0 -shuffle_vars | bool | use a random variable order. | false -simplify_conflicts | bool | simplify conflicts using equalities before resolving them in nlsat solver. | true - - -## Module fp - -Description: fixedpoint parameters - Parameter | Type | Description | Default - ---------------------------------------- -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.check_relation | symbol | name of default relation to check. operations on the default relation will be verified using SMT solving | null -datalog.compile_with_widening | bool | widening will be used to compile recursive rules | false -datalog.dbg_fpr_nonempty_relation_signature | bool | if true, finite_product_relation will attempt to avoid creating inner relation with empty signature by putting in half of the table columns, if it would have been empty otherwise | false -datalog.default_relation | symbol | default relation implementation: external_relation, pentagon | pentagon -datalog.default_table | symbol | default table implementation: sparse, hashtable, bitvector, interval | sparse -datalog.default_table_checked | bool | if true, the default table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table | false -datalog.default_table_checker | symbol | see default_table_checked | null -datalog.explanations_on_relation_level | bool | if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect) | false -datalog.generate_explanations | bool | produce explanations for produced facts when using the datalog engine | false -datalog.initial_restart_timeout | unsigned int | length of saturation run before the first restart (in ms), zero means no restarts | 0 -datalog.magic_sets_for_queries | bool | magic set transformation will be used for queries | false -datalog.output_profile | bool | determines whether profile information should be output when outputting Datalog rules or instructions | false -datalog.print.tuples | bool | determines whether tuples for output predicates should be output | true -datalog.profile_timeout_milliseconds | unsigned int | instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list | 0 -datalog.similarity_compressor | bool | rules that differ only in values of constants will be merged into a single rule | true -datalog.similarity_compressor_threshold | unsigned int | if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged | 11 -datalog.subsumption | bool | if true, removes/filters predicates with total transitions | true -datalog.timeout | unsigned int | Time limit used for saturation | 0 -datalog.unbound_compressor | bool | auxiliary relations will be introduced to avoid unbound variables in rule heads | true -datalog.use_map_names | bool | use names from map files when displaying tuples | true -engine | symbol | Select: auto-config, datalog, bmc, spacer | auto-config -generate_proof_trace | bool | trace for 'sat' answer as proof object | false -print_aig | symbol | Dump clauses in AIG text format (AAG) to the given file name | -print_answer | bool | print answer instance(s) to query | false -print_boogie_certificate | bool | print certificate for reachability or non-reachability using a format understood by Boogie | false -print_certificate | bool | print certificate for reachability or non-reachability | false -print_fixedpoint_extensions | bool | use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules | true -print_low_level_smt2 | bool | use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable) | false -print_statistics | bool | print statistics | false -print_with_variable_declarations | bool | use variable declarations when displaying rules (instead of attempting to use original names) | true -spacer.arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 2 -spacer.blast_term_ite_inflation | unsigned int | Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative) | 3 -spacer.ctp | bool | Enable counterexample-to-pushing | true -spacer.dump_benchmarks | bool | Dump SMT queries as benchmarks | false -spacer.dump_threshold | double | Threshold in seconds on dumping benchmarks | 5.0 -spacer.elim_aux | bool | Eliminate auxiliary variables in reachability facts | true -spacer.eq_prop | bool | Enable equality and bound propagation in arithmetic | true -spacer.gpdr | bool | Use GPDR solving strategy for non-linear CHC | false -spacer.gpdr.bfs | bool | Use BFS exploration strategy for expanding model search | true -spacer.ground_pobs | bool | Ground pobs by using values from a model | true -spacer.iuc | unsigned int | 0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization | 1 -spacer.iuc.arith | unsigned int | 0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin | 1 -spacer.iuc.debug_proof | bool | prints proof used by unsat-core-learner for debugging purposes (debugging) | false -spacer.iuc.old_hyp_reducer | bool | use old hyp reducer instead of new implementation, for debugging only | false -spacer.iuc.print_farkas_stats | bool | prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging) | false -spacer.iuc.split_farkas_literals | bool | Split Farkas literals | false -spacer.keep_proxy | bool | keep proxy variables (internal parameter) | true -spacer.logic | symbol | SMT-LIB logic to configure internal SMT solvers | -spacer.max_level | unsigned int | Maximum level to explore | 4294967295 -spacer.max_num_contexts | unsigned int | maximal number of contexts to create | 500 -spacer.mbqi | bool | Enable mbqi | true -spacer.min_level | unsigned int | Minimal level to explore | 0 -spacer.native_mbp | bool | Use native mbp of Z3 | true -spacer.order_children | unsigned int | SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random) | 0 -spacer.p3.share_invariants | bool | Share invariants lemmas | false -spacer.p3.share_lemmas | bool | Share frame lemmas | false -spacer.print_json | symbol | Print pobs tree in JSON format to a given file | -spacer.propagate | bool | Enable propagate/pushing phase | true -spacer.push_pob | bool | push blocked pobs to higher level | false -spacer.push_pob_max_depth | unsigned int | Maximum depth at which push_pob is enabled | 4294967295 -spacer.q3 | bool | Allow quantified lemmas in frames | true -spacer.q3.instantiate | bool | Instantiate quantified lemmas | true -spacer.q3.qgen.normalize | bool | normalize cube before quantified generalization | true -spacer.q3.use_qgen | bool | use quantified lemma generalizer | false -spacer.random_seed | unsigned int | Random seed to be used by SMT solver | 0 -spacer.reach_dnf | bool | Restrict reachability facts to DNF | true -spacer.reset_pob_queue | bool | SPACER: reset pob obligation queue when entering a new level | true -spacer.restart_initial_threshold | unsigned int | Initial threshold for restarts | 10 -spacer.restarts | bool | Enable resetting obligation queue | false -spacer.simplify_lemmas_post | bool | simplify derived lemmas after inductive propagation | false -spacer.simplify_lemmas_pre | bool | simplify derived lemmas before inductive propagation | false -spacer.simplify_pob | bool | simplify pobs by removing redundant constraints | false -spacer.trace_file | symbol | Log file for progress events | -spacer.use_array_eq_generalizer | bool | SPACER: attempt to generalize lemmas with array equalities | true -spacer.use_bg_invs | bool | Enable external background invariants | false -spacer.use_derivations | bool | SPACER: using derivation mechanism to cache intermediate results for non-linear rules | true -spacer.use_euf_gen | bool | Generalize lemmas and pobs using implied equalities | false -spacer.use_inc_clause | bool | Use incremental clause to represent trans | true -spacer.use_inductive_generalizer | bool | generalize lemmas using induction strengthening | true -spacer.use_lemma_as_cti | bool | SPACER: use a lemma instead of a CTI in flexible_trace | false -spacer.use_lim_num_gen | bool | Enable limit numbers generalizer to get smaller numbers | false -spacer.validate_lemmas | bool | Validate each lemma after generalization | false -spacer.weak_abs | bool | Weak abstraction | true -tab.selection | symbol | selection method for tabular strategy: weight (default), first, var-use | weight -validate | bool | validate result (by proof checking or model checking) | false -xform.array_blast | bool | try to eliminate local array terms using Ackermannization -- some array terms may remain | false -xform.array_blast_full | bool | eliminate all local array variables by QE | false -xform.bit_blast | bool | bit-blast bit-vectors | false -xform.coalesce_rules | bool | coalesce rules | false -xform.coi | bool | use cone of influence simplification | true -xform.compress_unbound | bool | compress tails with unbound variables | true -xform.elim_term_ite | bool | Eliminate term-ite expressions | false -xform.elim_term_ite.inflation | unsigned int | Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative) | 3 -xform.fix_unbound_vars | bool | fix unbound variables in tail | false -xform.inline_eager | bool | try eager inlining of rules | true -xform.inline_linear | bool | try linear inlining method | true -xform.inline_linear_branch | bool | try linear inlining method with potential expansion | false -xform.instantiate_arrays | bool | Transforms P(a) into P(i, a[i] a) | false -xform.instantiate_arrays.enforce | bool | Transforms P(a) into P(i, a[i]), discards a from predicate | false -xform.instantiate_arrays.nb_quantifier | unsigned int | Gives the number of quantifiers per array | 1 -xform.instantiate_arrays.slice_technique | symbol | => GetId(i) = i, => GetId(i) = true | no-slicing -xform.instantiate_quantifiers | bool | instantiate quantified Horn clauses using E-matching heuristic | false -xform.magic | bool | perform symbolic magic set transformation | false -xform.quantify_arrays | bool | create quantified Horn clauses from clauses with arrays | false -xform.scale | bool | add scaling variable to linear real arithmetic clauses | false -xform.slice | bool | simplify clause set using slicing | true -xform.subsumption_checker | bool | Enable subsumption checker (no support for model conversion) | true -xform.tail_simplifier_pve | bool | propagate_variable_equivalences | true -xform.transform_arrays | bool | Rewrites arrays equalities and applies select over store | false -xform.unfold_rules | unsigned int | unfold rules statically using iterative squaring | 0 - -## Module smt - -Description: smt solver based on lazy smt - Parameter | Type | Description | Default - ---------------------------------------- -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.branch_cut_ratio | unsigned int | branch/cut ratio for linear integer arithmetic | 2 -arith.dump_lemmas | bool | dump arithmetic theory lemmas to files | false -arith.eager_eq_axioms | bool | eager equality axioms | true -arith.enable_hnf | bool | enable hnf (Hermite Normal Form) cuts | true -arith.greatest_error_pivot | bool | Pivoting strategy | false -arith.ignore_int | bool | treat integer variables as real | false -arith.int_eq_branch | bool | branching using derived integer equations | false -arith.min | bool | minimize cost | false -arith.nl | bool | (incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2 | true -arith.nl.branching | bool | branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2 | true -arith.nl.delay | unsigned int | number of calls to final check before invoking bounded nlsat check | 500 -arith.nl.expp | bool | expensive patching | false -arith.nl.gr_q | unsigned int | grobner's quota | 10 -arith.nl.grobner | bool | run grobner's basis heuristic | true -arith.nl.grobner_cnfl_to_report | unsigned int | grobner's maximum number of conflicts to report | 1 -arith.nl.grobner_eqs_growth | unsigned int | grobner's number of equalities growth | 10 -arith.nl.grobner_expr_degree_growth | unsigned int | grobner's maximum expr degree growth | 2 -arith.nl.grobner_expr_size_growth | unsigned int | grobner's maximum expr size growth | 2 -arith.nl.grobner_frequency | unsigned int | grobner's call frequency | 4 -arith.nl.grobner_max_simplified | unsigned int | grobner's maximum number of simplifications | 10000 -arith.nl.grobner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 1 -arith.nl.horner | bool | run horner's heuristic | true -arith.nl.horner_frequency | unsigned int | horner's call frequency | 4 -arith.nl.horner_row_length_limit | unsigned int | row is disregarded by the heuristic if its length is longer than the value | 10 -arith.nl.horner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 2 -arith.nl.nra | bool | call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6 | true -arith.nl.order | bool | run order lemmas | true -arith.nl.rounds | unsigned int | threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2 | 1024 -arith.nl.tangents | bool | run tangent lemmas | true -arith.print_ext_var_names | bool | print external variable names | false -arith.print_stats | bool | print statistic | false -arith.propagate_eqs | bool | propagate (cheap) equalities | true -arith.propagation_mode | unsigned int | 0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds | 1 -arith.random_initial_value | bool | use random initial values in the simplex-based procedure for linear arithmetic | false -arith.rep_freq | unsigned int | the report frequency, in how many iterations print the cost and other info | 0 -arith.simplex_strategy | unsigned int | simplex strategy for the solver | 0 -arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 6 -array.extensional | bool | extensional array theory | true -array.weak | bool | weak array theory | false -auto_config | bool | automatically configure solver | true -bv.delay | bool | delay internalize expensive bit-vector operations | true -bv.enable_int2bv | bool | enable support for int2bv and bv2int operators | true -bv.eq_axioms | bool | enable redundant equality axioms for bit-vectors | true -bv.reflect | bool | create enode for every bit-vector term | true -bv.watch_diseq | bool | use watch lists instead of eager axioms for bit-vectors | false -candidate_models | bool | create candidate models even when quantifier or theory reasoning is incomplete | false -case_split | unsigned int | 0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity | 1 -clause_proof | bool | record a clausal proof | false -core.extend_nonlocal_patterns | bool | extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body | false -core.extend_patterns | bool | extend unsat core with literals that trigger (potential) quantifier instances | false -core.extend_patterns.max_distance | unsigned int | limits the distance of a pattern-extended unsat core | 4294967295 -core.minimize | bool | minimize unsat core produced by SMT context | false -core.validate | bool | [internal] validate unsat core produced by SMT context. This option is intended for debugging | false -cube_depth | unsigned int | cube depth. | 1 -dack | unsigned int | 0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution | 1 -dack.eq | bool | enable dynamic ackermannization for transtivity of equalities | false -dack.factor | double | number of instance per conflict | 0.1 -dack.gc | unsigned int | Dynamic ackermannization garbage collection frequency (per conflict) | 2000 -dack.gc_inv_decay | double | Dynamic ackermannization garbage collection decay | 0.8 -dack.threshold | unsigned int | number of times the congruence rule must be used before Leibniz's axiom is expanded | 10 -delay_units | bool | if true then z3 will not restart when a unit clause is learned | false -delay_units_threshold | unsigned int | maximum number of learned unit clauses before restarting, ignored if delay_units is false | 32 -dt_lazy_splits | unsigned int | How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy | 1 -ematching | bool | E-Matching based quantifier instantiation | true -induction | bool | enable generation of induction lemmas | false -lemma_gc_strategy | unsigned int | lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none | 0 -logic | symbol | logic used to setup the SMT solver | -macro_finder | bool | try to find universally quantified formulas that can be viewed as macros | false -max_conflicts | unsigned int | maximum number of conflicts before giving up. | 4294967295 -mbqi | bool | model based quantifier instantiation (MBQI) | true -mbqi.force_template | unsigned int | some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template | 10 -mbqi.id | string | Only use model-based instantiation for quantifiers with id's beginning with string | -mbqi.max_cexs | unsigned int | initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation | 1 -mbqi.max_cexs_incr | unsigned int | increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI | 0 -mbqi.max_iterations | unsigned int | maximum number of rounds of MBQI | 1000 -mbqi.trace | bool | generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied | false -pb.conflict_frequency | unsigned int | conflict frequency for Pseudo-Boolean theory | 1000 -pb.learn_complements | bool | learn complement literals for Pseudo-Boolean theory | true -phase_caching_off | unsigned int | number of conflicts while phase caching is off | 100 -phase_caching_on | unsigned int | number of conflicts while phase caching is on | 400 -phase_selection | unsigned int | phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory | 3 -pull_nested_quantifiers | bool | pull nested quantifiers | false -q.lift_ite | unsigned int | 0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers | 0 -q.lite | bool | Use cheap quantifier elimination during pre-processing | false -qi.cost | string | expression specifying what is the cost of a given quantifier instantiation | (+ weight generation) -qi.eager_threshold | double | threshold for eager quantifier instantiation | 10.0 -qi.lazy_threshold | double | threshold for lazy quantifier instantiation | 20.0 -qi.max_instances | unsigned int | maximum number of quantifier instantiations | 4294967295 -qi.max_multi_patterns | unsigned int | specify the number of extra multi patterns | 0 -qi.profile | bool | profile quantifier instantiation | false -qi.profile_freq | unsigned int | how frequent results are reported by qi.profile | 4294967295 -qi.quick_checker | unsigned int | specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances | 0 -quasi_macros | bool | try to find universally quantified formulas that are quasi-macros | false -random_seed | unsigned int | random seed for the smt solver | 0 -refine_inj_axioms | bool | refine injectivity axioms | true -relevancy | unsigned int | relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant | 2 -restart.max | unsigned int | maximal number of restarts. | 4294967295 -restart_factor | double | when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold | 1.1 -restart_strategy | unsigned int | 0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic | 1 -restricted_quasi_macros | bool | try to find universally quantified formulas that are restricted quasi-macros | false -seq.max_unfolding | unsigned int | maximal unfolding depth for checking string equations and regular expressions | 1000000000 -seq.split_w_len | bool | enable splitting guided by length constraints | true -seq.validate | bool | enable self-validation of theory axioms created by seq theory | false -str.aggressive_length_testing | bool | prioritize testing concrete length values over generating more options | false -str.aggressive_unroll_testing | bool | prioritize testing concrete regex unroll counts over generating more options | true -str.aggressive_value_testing | bool | prioritize testing concrete string constant values over generating more options | false -str.fast_length_tester_cache | bool | cache length tester constants instead of regenerating them | false -str.fast_value_tester_cache | bool | cache value tester constants instead of regenerating them | true -str.fixed_length_naive_cex | bool | construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only) | true -str.fixed_length_refinement | bool | use abstraction refinement in fixed-length equation solver (Z3str3 only) | false -str.overlap_priority | double | theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true | -0.1 -str.regex_automata_difficulty_threshold | unsigned int | difficulty threshold for regex automata heuristics | 1000 -str.regex_automata_failed_automaton_threshold | unsigned int | number of failed automaton construction attempts after which a full automaton is automatically built | 10 -str.regex_automata_failed_intersection_threshold | unsigned int | number of failed automaton intersection attempts after which intersection is always computed | 10 -str.regex_automata_intersection_difficulty_threshold | unsigned int | difficulty threshold for regex intersection heuristics | 1000 -str.regex_automata_length_attempt_threshold | unsigned int | number of length/path constraint attempts before checking unsatisfiability of regex terms | 10 -str.string_constant_cache | bool | cache all generated string constants generated from anywhere in theory_str | true -str.strong_arrangements | bool | assert equivalences instead of implications when generating string arrangement axioms | true -string_solver | symbol | solver for string/sequence theories. options are: 'z3str3' (specialized string solver), 'seq' (sequence solver), 'auto' (use static features to choose best solver), 'empty' (a no-op solver that forces an answer unknown if strings were used), 'none' (no solver) | seq -theory_aware_branching | bool | Allow the context to use extra information from theory solvers regarding literal branching prioritization. | false -theory_case_split | bool | Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead. | false -threads | unsigned int | maximal number of parallel threads. | 1 -threads.cube_frequency | unsigned int | frequency for using cubing | 2 -threads.max_conflicts | unsigned int | maximal number of conflicts between rounds of cubing for parallel SMT | 400 - -## Module sls - -Description: Experimental Stochastic Local Search Solver (for QFBV only). - Parameter | Type | Description | Default - ---------------------------------------- -early_prune | bool | use early pruning for score prediction | true -max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 -max_restarts | unsigned int | maximum number of restarts | 4294967295 -paws_init | unsigned int | initial/minimum assertion weights | 40 -paws_sp | unsigned int | smooth assertion weights with probability paws_sp / 1024 | 52 -random_offset | bool | use random offset for candidate evaluation | true -random_seed | unsigned int | random seed | 0 -rescore | bool | rescore/normalize top-level score every base restart interval | true -restart_base | unsigned int | base restart interval given by moves per run | 100 -restart_init | bool | initialize to 0 or random value (= 1) after restart | false -scale_unsat | double | scale score of unsat expressions by this factor | 0.5 -track_unsat | bool | keep a list of unsat assertions as done in SAT - currently disabled internally | false -vns_mc | unsigned int | in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit | 0 -vns_repick | bool | in local minima, try picking a different assertion (only for walksat) | false -walksat | bool | use walksat assertion selection (instead of gsat) | true -walksat_repick | bool | repick assertion if randomizing in local minima | true -walksat_ucb | bool | use bandit heuristic for walksat assertion selection (instead of random) | true -walksat_ucb_constant | double | the ucb constant c in the term score + c * f(touched) | 20.0 -walksat_ucb_forget | double | scale touched by this factor every base restart interval | 1.0 -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 -wp | unsigned int | random walk with probability wp / 1024 | 100 - +## Module pi + +Description: pattern inference (heuristics) for universal formulas (without annotation) + 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_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 +max_multi_patterns | unsigned int | when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern | 0 +non_nested_arith_weight | unsigned int | default weight for quantifiers where the only available pattern has non nested arithmetic terms | 10 +pull_quantifiers | bool | pull nested quantifiers, if no pattern was found | true +use_database | bool | use pattern database | false +warnings | bool | enable/disable warning messages in the pattern inference module | false + +## Module tactic + +Description: tactic parameters + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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 +default_tactic | symbol | overwrite default tactic in strategic solver | +propagate_values.max_rounds | unsigned int | maximal number of rounds to propagate values. | 4 +solve_eqs.context_solve | bool | solve equalities within disjunctions. | true +solve_eqs.ite_solver | bool | use if-then-else solvers. | true +solve_eqs.max_occs | unsigned int | maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295 +solve_eqs.theory_solver | bool | use theory solvers. | true + +## Module pp + +Description: pretty printer + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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_neg | bool | use bvneg when displaying Bit-Vector literals where the most significant bit is 1 | false +decimal | bool | pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise | false +decimal_precision | unsigned int | maximum number of decimal places to be used when pp.decimal=true | 10 +fixed_indent | bool | use a fixed indentation for applications | false +flat_assoc | bool | flat associative operators (when pretty printing SMT2 terms/formulas) | true +fp_real_literals | bool | use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing | false +max_depth | unsigned int | max. term depth (when pretty printing SMT2 terms/formulas) | 5 +max_indent | unsigned int | max. indentation in pretty printer | 4294967295 +max_num_lines | unsigned int | max. number of lines to be displayed in pretty printer | 4294967295 +max_ribbon | unsigned int | max. ribbon (width - indentation) in pretty printer | 80 +max_width | unsigned int | max. width in pretty printer | 80 +min_alias_size | unsigned int | min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas) | 10 +pretty_proof | bool | use slower, but prettier, printer for proofs | false +simplify_implies | bool | simplify nested implications for pretty printing | true +single_line | bool | ignore line breaks when true | false + +## Module sat + +Description: propositional SAT solver + Parameter | Type | Description | Default + ----------|------|-------------|-------- +abce | bool | eliminate blocked clauses using asymmetric literals | false +acce | bool | eliminate covered clauses using asymmetric added literals | false +anf | bool | enable ANF based simplification in-processing | false +anf.delay | unsigned int | delay ANF simplification by in-processing round | 2 +anf.exlin | bool | enable extended linear simplification | false +asymm_branch | bool | asymmetric branching | true +asymm_branch.all | bool | asymmetric branching on all literals per clause | false +asymm_branch.delay | unsigned int | number of simplification rounds to wait until invoking asymmetric branch simplification | 1 +asymm_branch.limit | unsigned int | approx. maximum number of literals visited during asymmetric branching | 100000000 +asymm_branch.rounds | unsigned int | maximal number of rounds to run asymmetric branch simplifications if progress is made | 2 +asymm_branch.sampled | bool | use sampling based asymmetric branching based on binary implication graph | true +ate | bool | asymmetric tautology elimination | true +backtrack.conflicts | unsigned int | number of conflicts before enabling chronological backtracking | 4000 +backtrack.scopes | unsigned int | number of scopes to enable chronological backtracking | 100 +bca | bool | blocked clause addition - add blocked binary clauses | false +bce | bool | eliminate blocked clauses | false +bce_at | unsigned int | eliminate blocked clauses only once at the given simplification round | 2 +bce_delay | unsigned int | delay eliminate blocked clauses until simplification round | 2 +binspr | bool | enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models | false +blocked_clause_limit | unsigned int | maximum number of literals visited during blocked clause elimination | 100000000 +branching.anti_exploration | bool | apply anti-exploration heuristic for branch selection | false +branching.heuristic | symbol | branching heuristic vsids, chb | vsids +burst_search | unsigned int | number of conflicts before first global simplification | 100 +cardinality.encoding | symbol | encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit | grouped +cardinality.solver | bool | use cardinality solver | true +cce | bool | eliminate covered clauses | false +core.minimize | bool | minimize computed core | false +core.minimize_partial | bool | apply partial (cheap) core minimization | false +cut | bool | enable AIG based simplification in-processing | false +cut.aig | bool | extract aigs (and ites) from cluases for cut simplification | false +cut.delay | unsigned int | delay cut simplification by in-processing round | 2 +cut.dont_cares | bool | integrate dont cares with cuts | true +cut.force | bool | force redoing cut-enumeration until a fixed-point | false +cut.lut | bool | extract luts from clauses for cut simplification | false +cut.npn3 | bool | extract 3 input functions from clauses for cut simplification | false +cut.redundancies | bool | integrate redundancy checking of cuts | true +cut.xor | bool | extract xors from clauses for cut simplification | false +ddfw.init_clause_weight | unsigned int | initial clause weight for DDFW local search | 8 +ddfw.reinit_base | unsigned int | increment basis for geometric backoff scheme of re-initialization of weights | 10000 +ddfw.restart_base | unsigned int | number of flips used a starting point for hessitant restart backoff | 100000 +ddfw.threads | unsigned int | number of ddfw threads to run in parallel with sat solver | 0 +ddfw.use_reward_pct | unsigned int | percentage to pick highest reward variable when it has reward 0 | 15 +ddfw_search | bool | use ddfw local search instead of CDCL | false +dimacs.core | bool | extract core from DIMACS benchmarks | false +drat.activity | bool | dump variable activities | false +drat.binary | bool | use Binary DRAT output format | false +drat.check_sat | bool | build up internal trace, check satisfying model | false +drat.check_unsat | bool | build up internal proof and check | false +drat.file | symbol | file to dump DRAT proofs | +drup.trim | bool | build and trim drup proof | false +dyn_sub_res | bool | dynamic subsumption resolution for minimizing learned clauses | true +elim_vars | bool | enable variable elimination using resolution during simplification | true +elim_vars_bdd | bool | enable variable elimination using BDD recompilation during simplification | true +elim_vars_bdd_delay | unsigned int | delay elimination of variables using BDDs until after simplification round | 3 +enable_pre_simplify | bool | enable pre simplifications before the bounded search | false +euf | bool | enable euf solver (this feature is preliminary and not ready for general consumption) | false +force_cleanup | bool | force cleanup to remove tautologies and simplify clauses | false +gc | symbol | garbage collection strategy: psm, glue, glue_psm, dyn_psm | glue_psm +gc.burst | bool | perform eager garbage collection during initialization | false +gc.defrag | bool | defragment clauses when garbage collecting | true +gc.increment | unsigned int | increment to the garbage collection threshold | 500 +gc.initial | unsigned int | learned clauses garbage collection frequency | 20000 +gc.k | unsigned int | learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm) | 7 +gc.small_lbd | unsigned int | learned clauses with small LBD are never deleted (only used in dyn_psm) | 3 +inprocess.max | unsigned int | maximal number of inprocessing passes | 4294967295 +inprocess.out | symbol | file to dump result of the first inprocessing step and exit | +local_search | bool | use local search instead of CDCL | false +local_search_dbg_flips | bool | write debug information for number of flips | false +local_search_mode | symbol | local search algorithm, either default wsat or qsat | wsat +local_search_threads | unsigned int | number of local search threads to find satisfiable solution | 0 +lookahead.cube.cutoff | symbol | cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat | depth +lookahead.cube.depth | unsigned int | cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth. | 1 +lookahead.cube.fraction | double | adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat | 0.4 +lookahead.cube.freevars | double | cube free variable fraction. Used when lookahead.cube.cutoff is freevars | 0.8 +lookahead.cube.psat.clause_base | double | clause base for PSAT cutoff | 2 +lookahead.cube.psat.trigger | double | trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat | 5 +lookahead.cube.psat.var_exp | double | free variable exponent for PSAT cutoff | 1 +lookahead.delta_fraction | double | number between 0 and 1, the smaller the more literals are selected for double lookahead | 1.0 +lookahead.double | bool | enable doubld lookahead | true +lookahead.global_autarky | bool | prefer to branch on variables that occur in clauses that are reduced | false +lookahead.preselect | bool | use pre-selection of subset of variables for branching | false +lookahead.reward | symbol | select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu | march_cu +lookahead.use_learned | bool | use learned clauses when selecting lookahead literal | false +lookahead_scores | bool | extract lookahead scores. A utility that can only be used from the DIMACS front-end | false +lookahead_simplify | bool | use lookahead solver during simplification | false +lookahead_simplify.bca | bool | add learned binary clauses as part of lookahead simplification | true +max_conflicts | unsigned int | maximum number of conflicts | 4294967295 +max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 +minimize_lemmas | bool | minimize learned clauses | true +override_incremental | bool | override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused | false +pb.lemma_format | symbol | generate either cardinality or pb lemmas | cardinality +pb.min_arity | unsigned int | minimal arity to compile pb/cardinality constraints to CNF | 9 +pb.resolve | symbol | resolution strategy for boolean algebra solver: cardinality, rounding | cardinality +pb.solver | symbol | method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver) | solver +phase | symbol | phase selection strategy: always_false, always_true, basic_caching, random, caching | caching +phase.sticky | bool | use sticky phase caching | true +prob_search | bool | use probsat local search instead of CDCL | false +probing | bool | apply failed literal detection during simplification | true +probing_binary | bool | probe binary clauses | true +probing_cache | bool | add binary literals as lemmas | true +probing_cache_limit | unsigned int | cache binaries unless overall memory usage exceeds cache limit | 1024 +probing_limit | unsigned int | limit to the number of probe calls | 5000000 +propagate.prefetch | bool | prefetch watch lists for assigned literals | true +random_freq | double | frequency of random case splits | 0.01 +random_seed | unsigned int | random seed | 0 +reorder.activity_scale | unsigned int | scaling factor for activity update | 100 +reorder.base | unsigned int | number of conflicts per random reorder | 4294967295 +reorder.itau | double | inverse temperature for softmax | 4.0 +rephase.base | unsigned int | number of conflicts per rephase | 1000 +resolution.cls_cutoff1 | unsigned int | limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination | 100000000 +resolution.cls_cutoff2 | unsigned int | limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination | 700000000 +resolution.limit | unsigned int | approx. maximum number of literals visited during variable elimination | 500000000 +resolution.lit_cutoff_range1 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 700 +resolution.lit_cutoff_range2 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 400 +resolution.lit_cutoff_range3 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 300 +resolution.occ_cutoff | unsigned int | first cutoff (on number of positive/negative occurrences) for Boolean variable elimination | 10 +resolution.occ_cutoff_range1 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 8 +resolution.occ_cutoff_range2 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 5 +resolution.occ_cutoff_range3 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 3 +restart | symbol | restart strategy: static, luby, ema or geometric | ema +restart.emafastglue | double | ema alpha factor for fast moving average | 0.03 +restart.emaslowglue | double | ema alpha factor for slow moving average | 1e-05 +restart.factor | double | restart increment factor for geometric strategy | 1.5 +restart.fast | bool | use fast restart approach only removing less active literals. | true +restart.initial | unsigned int | initial restart (number of conflicts) | 2 +restart.margin | double | margin between fast and slow restart factors. For ema | 1.1 +restart.max | unsigned int | maximal number of restarts. | 4294967295 +retain_blocked_clauses | bool | retain blocked clauses as lemmas | true +scc | bool | eliminate Boolean variables by computing strongly connected components | true +scc.tr | bool | apply transitive reduction, eliminate redundant binary clauses | true +search.sat.conflicts | unsigned int | period for solving for sat (in number of conflicts) | 400 +search.unsat.conflicts | unsigned int | period for solving for unsat (in number of conflicts) | 400 +simplify.delay | unsigned int | set initial delay of simplification by a conflict count | 0 +subsumption | bool | eliminate subsumed clauses | true +subsumption.limit | unsigned int | approx. maximum number of literals visited during subsumption (and subsumption resolution) | 100000000 +threads | unsigned int | number of parallel threads to use | 1 +variable_decay | unsigned int | multiplier (divided by 100) for the VSIDS activity increment | 110 + +## Module solver + +Description: solver parameters + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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 | +lemmas2console | bool | print lemmas during search | false +smtlib2_log | symbol | file to save solver interaction | +timeout | unsigned int | timeout on the solver object; overwrites a global timeout | 4294967295 + +## Module opt + +Description: optimization parameters + Parameter | Type | Description | Default + ----------|------|-------------|-------- +dump_benchmarks | bool | dump benchmarks for profiling | false +dump_models | bool | display intermediary models to stdout | false +elim_01 | bool | eliminate 01 variables | true +enable_core_rotate | bool | enable core rotation to both sample cores and correction sets | false +enable_lns | bool | enable LNS during weighted maxsat | false +enable_sat | bool | enable the new SAT core for propositional constraints | true +enable_sls | bool | enable SLS tuning during weighted maxsat | false +incremental | bool | set incremental mode. It disables pre-processing and enables adding constraints in model event handler | false +lns_conflicts | unsigned int | initial conflict count for LNS search | 1000 +maxlex.enable | bool | enable maxlex heuristic for lexicographic MaxSAT problems | true +maxres.add_upper_bound_block | bool | restict upper bound with constraint | false +maxres.hill_climb | bool | give preference for large weight cores | true +maxres.max_core_size | unsigned int | break batch of generated cores if size reaches this number | 3 +maxres.max_correction_set_size | unsigned int | allow generating correction set constraints up to maximal size | 3 +maxres.max_num_cores | unsigned int | maximal number of cores per round | 200 +maxres.maximize_assignment | bool | find an MSS/MCS to improve current assignment | false +maxres.pivot_on_correction_set | bool | reduce soft constraints if the current correction set is smaller than current core | true +maxres.wmax | bool | use weighted theory solver to constrain upper bounds | false +maxsat_engine | symbol | select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2' | maxres +optsmt_engine | symbol | select optimization engine: 'basic', 'symba' | basic +pb.compile_equality | bool | compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites) | false +pp.neat | bool | use neat (as opposed to less readable, but faster) pretty printer when displaying context | true +pp.wcnf | bool | print maxsat benchmark into wcnf format | false +priority | symbol | select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box' | lex +rc2.totalizer | bool | use totalizer for rc2 encoding | true +rlimit | unsigned int | resource limit (0 means no limit) | 0 +solution_prefix | symbol | path prefix to dump intermediary, but non-optimal, solutions | +timeout | unsigned int | timeout (in milliseconds) (UINT_MAX and 0 mean no timeout) | 4294967295 + +## Module parallel + +Description: parameters for parallel solver + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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.delay | unsigned int | delay of cubes until applying conquer | 10 +conquer.restart.max | unsigned int | maximal number of restarts during conquer phase | 5 +enable | bool | enable parallel solver by default on selected tactics (for QF_BV) | false +simplify.exp | double | restart and inprocess max is multiplied by simplify.exp ^ depth | 1 +simplify.inprocess.max | unsigned int | maximal number of inprocessing steps during simplification | 2 +simplify.max_conflicts | unsigned int | maximal number of conflicts during simplifcation phase | 4294967295 +simplify.restart.max | unsigned int | maximal number of restarts during simplification phase | 5000 +threads.max | unsigned int | caps maximal number of threads below the number of processors | 10000 + +## Module nnf + +Description: negation normal form + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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 +mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem +sk_hack | bool | hack for VCC | false + +## Module algebraic + +Description: real algebraic number package. Non-default parameter settings are not supported + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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_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_search_size | 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 can be used to limit the search space | 5000 +min_mag | unsigned int | Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16 +zero_accuracy | unsigned int | one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0 + +## Module combined_solver + +Description: combines two solvers: non-incremental (solver1) and incremental (solver2) + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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_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 + +## Module rcf + +Description: real closed fields + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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 +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 +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 +ERROR: unknown module 'rewriter, description: new formula simplification module used in the tactic framework' + +## Module ackermannization + +Description: solving UF via ackermannization + Parameter | Type | Description | Default + ----------|------|-------------|-------- +eager | bool | eagerly instantiate all congruence rules | true +inc_sat_backend | bool | use incremental SAT | false +sat_backend | bool | use SAT rather than SMT in qfufbv_ackr_tactic | false + +## Module nlsat + +Description: nonlinear solver + Parameter | Type | Description | Default + ----------|------|-------------|-------- +check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false +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 +lazy | unsigned int | how lazy the solver is. | 0 +log_lemmas | bool | display lemmas as self-contained SMT formulas | false +max_conflicts | unsigned int | maximum number of conflicts. | 4294967295 +max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 +minimize_conflicts | bool | minimize conflicts | false +randomize | bool | randomize selection of a witness in nlsat. | true +reorder | bool | reorder variables. | true +seed | unsigned int | random seed. | 0 +shuffle_vars | bool | use a random variable order. | false +simplify_conflicts | bool | simplify conflicts using equalities before resolving them in nlsat solver. | true + + +## Module fp + +Description: fixedpoint parameters + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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.check_relation | symbol | name of default relation to check. operations on the default relation will be verified using SMT solving | null +datalog.compile_with_widening | bool | widening will be used to compile recursive rules | false +datalog.dbg_fpr_nonempty_relation_signature | bool | if true, finite_product_relation will attempt to avoid creating inner relation with empty signature by putting in half of the table columns, if it would have been empty otherwise | false +datalog.default_relation | symbol | default relation implementation: external_relation, pentagon | pentagon +datalog.default_table | symbol | default table implementation: sparse, hashtable, bitvector, interval | sparse +datalog.default_table_checked | bool | if true, the default table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table | false +datalog.default_table_checker | symbol | see default_table_checked | null +datalog.explanations_on_relation_level | bool | if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect) | false +datalog.generate_explanations | bool | produce explanations for produced facts when using the datalog engine | false +datalog.initial_restart_timeout | unsigned int | length of saturation run before the first restart (in ms), zero means no restarts | 0 +datalog.magic_sets_for_queries | bool | magic set transformation will be used for queries | false +datalog.output_profile | bool | determines whether profile information should be output when outputting Datalog rules or instructions | false +datalog.print.tuples | bool | determines whether tuples for output predicates should be output | true +datalog.profile_timeout_milliseconds | unsigned int | instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list | 0 +datalog.similarity_compressor | bool | rules that differ only in values of constants will be merged into a single rule | true +datalog.similarity_compressor_threshold | unsigned int | if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged | 11 +datalog.subsumption | bool | if true, removes/filters predicates with total transitions | true +datalog.timeout | unsigned int | Time limit used for saturation | 0 +datalog.unbound_compressor | bool | auxiliary relations will be introduced to avoid unbound variables in rule heads | true +datalog.use_map_names | bool | use names from map files when displaying tuples | true +engine | symbol | Select: auto-config, datalog, bmc, spacer | auto-config +generate_proof_trace | bool | trace for 'sat' answer as proof object | false +print_aig | symbol | Dump clauses in AIG text format (AAG) to the given file name | +print_answer | bool | print answer instance(s) to query | false +print_boogie_certificate | bool | print certificate for reachability or non-reachability using a format understood by Boogie | false +print_certificate | bool | print certificate for reachability or non-reachability | false +print_fixedpoint_extensions | bool | use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules | true +print_low_level_smt2 | bool | use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable) | false +print_statistics | bool | print statistics | false +print_with_variable_declarations | bool | use variable declarations when displaying rules (instead of attempting to use original names) | true +spacer.arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 2 +spacer.blast_term_ite_inflation | unsigned int | Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative) | 3 +spacer.ctp | bool | Enable counterexample-to-pushing | true +spacer.dump_benchmarks | bool | Dump SMT queries as benchmarks | false +spacer.dump_threshold | double | Threshold in seconds on dumping benchmarks | 5.0 +spacer.elim_aux | bool | Eliminate auxiliary variables in reachability facts | true +spacer.eq_prop | bool | Enable equality and bound propagation in arithmetic | true +spacer.gpdr | bool | Use GPDR solving strategy for non-linear CHC | false +spacer.gpdr.bfs | bool | Use BFS exploration strategy for expanding model search | true +spacer.ground_pobs | bool | Ground pobs by using values from a model | true +spacer.iuc | unsigned int | 0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization | 1 +spacer.iuc.arith | unsigned int | 0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin | 1 +spacer.iuc.debug_proof | bool | prints proof used by unsat-core-learner for debugging purposes (debugging) | false +spacer.iuc.old_hyp_reducer | bool | use old hyp reducer instead of new implementation, for debugging only | false +spacer.iuc.print_farkas_stats | bool | prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging) | false +spacer.iuc.split_farkas_literals | bool | Split Farkas literals | false +spacer.keep_proxy | bool | keep proxy variables (internal parameter) | true +spacer.logic | symbol | SMT-LIB logic to configure internal SMT solvers | +spacer.max_level | unsigned int | Maximum level to explore | 4294967295 +spacer.max_num_contexts | unsigned int | maximal number of contexts to create | 500 +spacer.mbqi | bool | Enable mbqi | true +spacer.min_level | unsigned int | Minimal level to explore | 0 +spacer.native_mbp | bool | Use native mbp of Z3 | true +spacer.order_children | unsigned int | SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random) | 0 +spacer.p3.share_invariants | bool | Share invariants lemmas | false +spacer.p3.share_lemmas | bool | Share frame lemmas | false +spacer.print_json | symbol | Print pobs tree in JSON format to a given file | +spacer.propagate | bool | Enable propagate/pushing phase | true +spacer.push_pob | bool | push blocked pobs to higher level | false +spacer.push_pob_max_depth | unsigned int | Maximum depth at which push_pob is enabled | 4294967295 +spacer.q3 | bool | Allow quantified lemmas in frames | true +spacer.q3.instantiate | bool | Instantiate quantified lemmas | true +spacer.q3.qgen.normalize | bool | normalize cube before quantified generalization | true +spacer.q3.use_qgen | bool | use quantified lemma generalizer | false +spacer.random_seed | unsigned int | Random seed to be used by SMT solver | 0 +spacer.reach_dnf | bool | Restrict reachability facts to DNF | true +spacer.reset_pob_queue | bool | SPACER: reset pob obligation queue when entering a new level | true +spacer.restart_initial_threshold | unsigned int | Initial threshold for restarts | 10 +spacer.restarts | bool | Enable resetting obligation queue | false +spacer.simplify_lemmas_post | bool | simplify derived lemmas after inductive propagation | false +spacer.simplify_lemmas_pre | bool | simplify derived lemmas before inductive propagation | false +spacer.simplify_pob | bool | simplify pobs by removing redundant constraints | false +spacer.trace_file | symbol | Log file for progress events | +spacer.use_array_eq_generalizer | bool | SPACER: attempt to generalize lemmas with array equalities | true +spacer.use_bg_invs | bool | Enable external background invariants | false +spacer.use_derivations | bool | SPACER: using derivation mechanism to cache intermediate results for non-linear rules | true +spacer.use_euf_gen | bool | Generalize lemmas and pobs using implied equalities | false +spacer.use_inc_clause | bool | Use incremental clause to represent trans | true +spacer.use_inductive_generalizer | bool | generalize lemmas using induction strengthening | true +spacer.use_lemma_as_cti | bool | SPACER: use a lemma instead of a CTI in flexible_trace | false +spacer.use_lim_num_gen | bool | Enable limit numbers generalizer to get smaller numbers | false +spacer.validate_lemmas | bool | Validate each lemma after generalization | false +spacer.weak_abs | bool | Weak abstraction | true +tab.selection | symbol | selection method for tabular strategy: weight (default), first, var-use | weight +validate | bool | validate result (by proof checking or model checking) | false +xform.array_blast | bool | try to eliminate local array terms using Ackermannization -- some array terms may remain | false +xform.array_blast_full | bool | eliminate all local array variables by QE | false +xform.bit_blast | bool | bit-blast bit-vectors | false +xform.coalesce_rules | bool | coalesce rules | false +xform.coi | bool | use cone of influence simplification | true +xform.compress_unbound | bool | compress tails with unbound variables | true +xform.elim_term_ite | bool | Eliminate term-ite expressions | false +xform.elim_term_ite.inflation | unsigned int | Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative) | 3 +xform.fix_unbound_vars | bool | fix unbound variables in tail | false +xform.inline_eager | bool | try eager inlining of rules | true +xform.inline_linear | bool | try linear inlining method | true +xform.inline_linear_branch | bool | try linear inlining method with potential expansion | false +xform.instantiate_arrays | bool | Transforms P(a) into P(i, a[i] a) | false +xform.instantiate_arrays.enforce | bool | Transforms P(a) into P(i, a[i]), discards a from predicate | false +xform.instantiate_arrays.nb_quantifier | unsigned int | Gives the number of quantifiers per array | 1 +xform.instantiate_arrays.slice_technique | symbol | => GetId(i) = i, => GetId(i) = true | no-slicing +xform.instantiate_quantifiers | bool | instantiate quantified Horn clauses using E-matching heuristic | false +xform.magic | bool | perform symbolic magic set transformation | false +xform.quantify_arrays | bool | create quantified Horn clauses from clauses with arrays | false +xform.scale | bool | add scaling variable to linear real arithmetic clauses | false +xform.slice | bool | simplify clause set using slicing | true +xform.subsumption_checker | bool | Enable subsumption checker (no support for model conversion) | true +xform.tail_simplifier_pve | bool | propagate_variable_equivalences | true +xform.transform_arrays | bool | Rewrites arrays equalities and applies select over store | false +xform.unfold_rules | unsigned int | unfold rules statically using iterative squaring | 0 + +## Module smt + +Description: smt solver based on lazy smt + Parameter | Type | Description | Default + ----------|------|-------------|-------- +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.branch_cut_ratio | unsigned int | branch/cut ratio for linear integer arithmetic | 2 +arith.dump_lemmas | bool | dump arithmetic theory lemmas to files | false +arith.eager_eq_axioms | bool | eager equality axioms | true +arith.enable_hnf | bool | enable hnf (Hermite Normal Form) cuts | true +arith.greatest_error_pivot | bool | Pivoting strategy | false +arith.ignore_int | bool | treat integer variables as real | false +arith.int_eq_branch | bool | branching using derived integer equations | false +arith.min | bool | minimize cost | false +arith.nl | bool | (incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2 | true +arith.nl.branching | bool | branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2 | true +arith.nl.delay | unsigned int | number of calls to final check before invoking bounded nlsat check | 500 +arith.nl.expp | bool | expensive patching | false +arith.nl.gr_q | unsigned int | grobner's quota | 10 +arith.nl.grobner | bool | run grobner's basis heuristic | true +arith.nl.grobner_cnfl_to_report | unsigned int | grobner's maximum number of conflicts to report | 1 +arith.nl.grobner_eqs_growth | unsigned int | grobner's number of equalities growth | 10 +arith.nl.grobner_expr_degree_growth | unsigned int | grobner's maximum expr degree growth | 2 +arith.nl.grobner_expr_size_growth | unsigned int | grobner's maximum expr size growth | 2 +arith.nl.grobner_frequency | unsigned int | grobner's call frequency | 4 +arith.nl.grobner_max_simplified | unsigned int | grobner's maximum number of simplifications | 10000 +arith.nl.grobner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 1 +arith.nl.horner | bool | run horner's heuristic | true +arith.nl.horner_frequency | unsigned int | horner's call frequency | 4 +arith.nl.horner_row_length_limit | unsigned int | row is disregarded by the heuristic if its length is longer than the value | 10 +arith.nl.horner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 2 +arith.nl.nra | bool | call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6 | true +arith.nl.order | bool | run order lemmas | true +arith.nl.rounds | unsigned int | threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2 | 1024 +arith.nl.tangents | bool | run tangent lemmas | true +arith.print_ext_var_names | bool | print external variable names | false +arith.print_stats | bool | print statistic | false +arith.propagate_eqs | bool | propagate (cheap) equalities | true +arith.propagation_mode | unsigned int | 0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds | 1 +arith.random_initial_value | bool | use random initial values in the simplex-based procedure for linear arithmetic | false +arith.rep_freq | unsigned int | the report frequency, in how many iterations print the cost and other info | 0 +arith.simplex_strategy | unsigned int | simplex strategy for the solver | 0 +arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 6 +array.extensional | bool | extensional array theory | true +array.weak | bool | weak array theory | false +auto_config | bool | automatically configure solver | true +bv.delay | bool | delay internalize expensive bit-vector operations | true +bv.enable_int2bv | bool | enable support for int2bv and bv2int operators | true +bv.eq_axioms | bool | enable redundant equality axioms for bit-vectors | true +bv.reflect | bool | create enode for every bit-vector term | true +bv.watch_diseq | bool | use watch lists instead of eager axioms for bit-vectors | false +candidate_models | bool | create candidate models even when quantifier or theory reasoning is incomplete | false +case_split | unsigned int | 0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity | 1 +clause_proof | bool | record a clausal proof | false +core.extend_nonlocal_patterns | bool | extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body | false +core.extend_patterns | bool | extend unsat core with literals that trigger (potential) quantifier instances | false +core.extend_patterns.max_distance | unsigned int | limits the distance of a pattern-extended unsat core | 4294967295 +core.minimize | bool | minimize unsat core produced by SMT context | false +core.validate | bool | [internal] validate unsat core produced by SMT context. This option is intended for debugging | false +cube_depth | unsigned int | cube depth. | 1 +dack | unsigned int | 0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution | 1 +dack.eq | bool | enable dynamic ackermannization for transtivity of equalities | false +dack.factor | double | number of instance per conflict | 0.1 +dack.gc | unsigned int | Dynamic ackermannization garbage collection frequency (per conflict) | 2000 +dack.gc_inv_decay | double | Dynamic ackermannization garbage collection decay | 0.8 +dack.threshold | unsigned int | number of times the congruence rule must be used before Leibniz's axiom is expanded | 10 +delay_units | bool | if true then z3 will not restart when a unit clause is learned | false +delay_units_threshold | unsigned int | maximum number of learned unit clauses before restarting, ignored if delay_units is false | 32 +dt_lazy_splits | unsigned int | How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy | 1 +ematching | bool | E-Matching based quantifier instantiation | true +induction | bool | enable generation of induction lemmas | false +lemma_gc_strategy | unsigned int | lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none | 0 +logic | symbol | logic used to setup the SMT solver | +macro_finder | bool | try to find universally quantified formulas that can be viewed as macros | false +max_conflicts | unsigned int | maximum number of conflicts before giving up. | 4294967295 +mbqi | bool | model based quantifier instantiation (MBQI) | true +mbqi.force_template | unsigned int | some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template | 10 +mbqi.id | string | Only use model-based instantiation for quantifiers with id's beginning with string | +mbqi.max_cexs | unsigned int | initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation | 1 +mbqi.max_cexs_incr | unsigned int | increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI | 0 +mbqi.max_iterations | unsigned int | maximum number of rounds of MBQI | 1000 +mbqi.trace | bool | generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied | false +pb.conflict_frequency | unsigned int | conflict frequency for Pseudo-Boolean theory | 1000 +pb.learn_complements | bool | learn complement literals for Pseudo-Boolean theory | true +phase_caching_off | unsigned int | number of conflicts while phase caching is off | 100 +phase_caching_on | unsigned int | number of conflicts while phase caching is on | 400 +phase_selection | unsigned int | phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory | 3 +pull_nested_quantifiers | bool | pull nested quantifiers | false +q.lift_ite | unsigned int | 0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers | 0 +q.lite | bool | Use cheap quantifier elimination during pre-processing | false +qi.cost | string | expression specifying what is the cost of a given quantifier instantiation | (+ weight generation) +qi.eager_threshold | double | threshold for eager quantifier instantiation | 10.0 +qi.lazy_threshold | double | threshold for lazy quantifier instantiation | 20.0 +qi.max_instances | unsigned int | maximum number of quantifier instantiations | 4294967295 +qi.max_multi_patterns | unsigned int | specify the number of extra multi patterns | 0 +qi.profile | bool | profile quantifier instantiation | false +qi.profile_freq | unsigned int | how frequent results are reported by qi.profile | 4294967295 +qi.quick_checker | unsigned int | specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances | 0 +quasi_macros | bool | try to find universally quantified formulas that are quasi-macros | false +random_seed | unsigned int | random seed for the smt solver | 0 +refine_inj_axioms | bool | refine injectivity axioms | true +relevancy | unsigned int | relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant | 2 +restart.max | unsigned int | maximal number of restarts. | 4294967295 +restart_factor | double | when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold | 1.1 +restart_strategy | unsigned int | 0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic | 1 +restricted_quasi_macros | bool | try to find universally quantified formulas that are restricted quasi-macros | false +seq.max_unfolding | unsigned int | maximal unfolding depth for checking string equations and regular expressions | 1000000000 +seq.split_w_len | bool | enable splitting guided by length constraints | true +seq.validate | bool | enable self-validation of theory axioms created by seq theory | false +str.aggressive_length_testing | bool | prioritize testing concrete length values over generating more options | false +str.aggressive_unroll_testing | bool | prioritize testing concrete regex unroll counts over generating more options | true +str.aggressive_value_testing | bool | prioritize testing concrete string constant values over generating more options | false +str.fast_length_tester_cache | bool | cache length tester constants instead of regenerating them | false +str.fast_value_tester_cache | bool | cache value tester constants instead of regenerating them | true +str.fixed_length_naive_cex | bool | construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only) | true +str.fixed_length_refinement | bool | use abstraction refinement in fixed-length equation solver (Z3str3 only) | false +str.overlap_priority | double | theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true | -0.1 +str.regex_automata_difficulty_threshold | unsigned int | difficulty threshold for regex automata heuristics | 1000 +str.regex_automata_failed_automaton_threshold | unsigned int | number of failed automaton construction attempts after which a full automaton is automatically built | 10 +str.regex_automata_failed_intersection_threshold | unsigned int | number of failed automaton intersection attempts after which intersection is always computed | 10 +str.regex_automata_intersection_difficulty_threshold | unsigned int | difficulty threshold for regex intersection heuristics | 1000 +str.regex_automata_length_attempt_threshold | unsigned int | number of length/path constraint attempts before checking unsatisfiability of regex terms | 10 +str.string_constant_cache | bool | cache all generated string constants generated from anywhere in theory_str | true +str.strong_arrangements | bool | assert equivalences instead of implications when generating string arrangement axioms | true +string_solver | symbol | solver for string/sequence theories. options are: 'z3str3' (specialized string solver), 'seq' (sequence solver), 'auto' (use static features to choose best solver), 'empty' (a no-op solver that forces an answer unknown if strings were used), 'none' (no solver) | seq +theory_aware_branching | bool | Allow the context to use extra information from theory solvers regarding literal branching prioritization. | false +theory_case_split | bool | Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead. | false +threads | unsigned int | maximal number of parallel threads. | 1 +threads.cube_frequency | unsigned int | frequency for using cubing | 2 +threads.max_conflicts | unsigned int | maximal number of conflicts between rounds of cubing for parallel SMT | 400 + +## Module sls + +Description: Experimental Stochastic Local Search Solver (for QFBV only). + Parameter | Type | Description | Default + ----------|------|-------------|-------- +early_prune | bool | use early pruning for score prediction | true +max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 +max_restarts | unsigned int | maximum number of restarts | 4294967295 +paws_init | unsigned int | initial/minimum assertion weights | 40 +paws_sp | unsigned int | smooth assertion weights with probability paws_sp / 1024 | 52 +random_offset | bool | use random offset for candidate evaluation | true +random_seed | unsigned int | random seed | 0 +rescore | bool | rescore/normalize top-level score every base restart interval | true +restart_base | unsigned int | base restart interval given by moves per run | 100 +restart_init | bool | initialize to 0 or random value (= 1) after restart | false +scale_unsat | double | scale score of unsat expressions by this factor | 0.5 +track_unsat | bool | keep a list of unsat assertions as done in SAT - currently disabled internally | false +vns_mc | unsigned int | in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit | 0 +vns_repick | bool | in local minima, try picking a different assertion (only for walksat) | false +walksat | bool | use walksat assertion selection (instead of gsat) | true +walksat_repick | bool | repick assertion if randomizing in local minima | true +walksat_ucb | bool | use bandit heuristic for walksat assertion selection (instead of random) | true +walksat_ucb_constant | double | the ucb constant c in the term score + c * f(touched) | 20.0 +walksat_ucb_forget | double | scale touched by this factor every base restart interval | 1.0 +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 +wp | unsigned int | random walk with probability wp / 1024 | 100 diff --git a/src/util/params.cpp b/src/util/params.cpp index 9831d92a0fb..e15d40fe2d2 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -169,7 +169,7 @@ struct param_descrs::imp { std::sort(names.begin(), names.end(), symlt()); if (markdown) { out << " Parameter | Type | Description | Default\n"; - out << " ----------------------------------------\n"; + out << " ----------|------|-------------|--------\n"; } for (symbol const& name : names) { for (unsigned i = 0; i < indent; i++) out << " ";