z3/src/params/smt_params_helper.pyg

def_module_params(module_name='smt',
                  class_name='smt_params_helper',
                  description='smt solver based on lazy smt',
                  export=True,
                  params=(('auto_config', BOOL, True, 'automatically configure solver'),
                          ('logic', SYMBOL, '', 'logic used to setup the SMT solver'),
                          ('random_seed', UINT, 0, 'random seed for the smt solver'),
                          ('relevancy', UINT, 2, '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'),
                          ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
                          ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'),
                          ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
                          ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
                          ('phase_selection', UINT, 3, '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'),
	                  ('phase_caching_on', UINT, 400, 'number of conflicts while phase caching is on'),
	                  ('phase_caching_off', UINT, 100, 'number of conflicts while phase caching is off'),
                          ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                          ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold'),
                          ('case_split', UINT, 1, '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'),
                          ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                          ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                          ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'),
                          ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'),
                          ('solve_eqs.non_ground', BOOL, True, 'pre-processing: solve equalities. Allow eliminating variables by non-ground solutions which can break behavior for model evaluation.'),
                          ('propagate_values', BOOL, True, 'pre-processing: propagate values'),
                          ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'),
                          ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),
                          ('refine_inj_axioms', BOOL, True, 'pre-processing: refine injectivity axioms'),
	                  ('candidate_models', BOOL, False, 'create candidate models even when quantifier or theory reasoning is incomplete'),
                          ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                          ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
	                  ('cube_depth', UINT, 1, 'cube depth.'),
                          ('threads', UINT, 1, 'maximal number of parallel threads.'),
                          ('threads.max_conflicts', UINT, 400, 'maximal number of conflicts between rounds of cubing for parallel SMT'),
                          ('threads.cube_frequency', UINT, 2, 'frequency for using cubing'), 
                          ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                          ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                          ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
                          ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'),
                          ('mbqi.trace', BOOL, False, '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'),
                          ('mbqi.force_template', UINT, 10, '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'),
                          ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'),
                          ('q.lift_ite', UINT, 0, '0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers'),
                          ('q.lite', BOOL, False, 'Use cheap quantifier elimination during pre-processing'),
                          ('qi.profile', BOOL, False, 'profile quantifier instantiation'),
                          ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
                          ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),
                          ('qi.eager_threshold', DOUBLE, 10.0, 'threshold for eager quantifier instantiation'),
                          ('qi.lazy_threshold', DOUBLE, 20.0, 'threshold for lazy quantifier instantiation'),
                          ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
                          ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
                          ('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'),
                          ('induction', BOOL, False, 'enable generation of induction lemmas'),
                          ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                          ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                          ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
                          ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
                          ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
                          ('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'),
                          ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                          ('arith.solver', UINT, 6, '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'),
                          ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
                          ('arith.nl.nra', BOOL, True, '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'),
                          ('arith.nl.nra_check_assignment', BOOL, True, 'call check_assignment in nra_solver to verify current assignment against nlsat constraints'),
                          ('arith.nl.nra_check_assignment_max_fail', UINT, 7, 'maximum consecutive check_assignment failures before disabling it'),
                          ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
                          ('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'),
                          ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),
                          ('arith.nl.order', BOOL, True, 'run order lemmas'),
                          ('arith.nl.expp', BOOL, False, 'expensive patching'),
                          ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
                          ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
                          ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
                          ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),
                          ('arith.nl.horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
                          ('arith.nl.grobner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
                          ('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'),
                          ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'),
                          ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
                          ('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'),
                          ('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
                          ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
                          ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                          ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'),
                          ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'),
                          ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'),
                          ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
                          ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),   
                          ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
                          ('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'),
                          ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
                          ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
                          ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
                          ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                          ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
                          ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                          ('arith.epsilon', DOUBLE, 1.0, 'initial value of epsilon used for model generation of infinitesimals'),
                          ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                          ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
                          ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
                          ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
                          ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
                          ('arith.dump_bound_lemmas', BOOL, False, 'dump linear solver bounds to files in smt2 format'),                          
                          ('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
                          ('arith.eager_eq_axioms', BOOL, True, 'eager equality axioms'),
                          ('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
                          ('arith.rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info'),
                          ('arith.min', BOOL, False, 'minimize cost'),
                          ('arith.print_stats', BOOL, False, 'print statistic'),
                          ('arith.validate', BOOL, False, 'validate lemmas generated by arithmetic solver'),
                          ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
                          ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
                          ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
                          ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
                          ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                          ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
                          ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'),
                          ('array.weak', BOOL, False, 'weak array theory'),
                          ('array.extensional', BOOL, True, 'extensional array theory'),
                          ('clause_proof', BOOL, False, 'record a clausal proof'),
                          ('dack', UINT, 1, '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'),
                          ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'),
                          ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
                          ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
                          ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                          ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
                          ('theory_case_split', BOOL, False, '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.'),
                          ('string_solver', SYMBOL, 'seq', '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)'),
                          ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'),
                          ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                          ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
                          ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'),
                          ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'),
                          ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
                          ('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'),
                          ('sls.parallel', BOOL, True, 'use sls co-processor in parallel or sequential with SMT engine'),
                          ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
                          ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
                          ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
                          ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
                          ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
                          ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
                          ('qsat_use_qel', BOOL, True, 'Use QEL for lite quantifier elimination and model-based projection in QSAT')
                          ))