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

params for theory aware branching

Browse source
This commit is contained in:
Murphy Berzish 2017-05-02 10:39:32 -04:00
parent 48e37b0e16
commit 6cd1f877b8
3 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/params/smt_params.cpp
View file

@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_restart_factor = p.restart_factor();
m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
m_theory_case_split = p.theory_case_split();
m_theory_aware_branching = p.theory_aware_branching();
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter

3
src/smt/params/smt_params.h
View file

@ -110,6 +110,7 @@ struct smt_params : public preprocessor_params,
unsigned m_rel_case_split_order;
bool m_lookahead_diseq;
bool m_theory_case_split;
bool m_theory_aware_branching;
// -----------------------------------
//
@ -240,6 +241,8 @@ struct smt_params : public preprocessor_params,
m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
m_rel_case_split_order(0),
m_lookahead_diseq(false),
m_theory_case_split(false),
m_theory_aware_branching(false),
m_delay_units(false),
m_delay_units_threshold(32),
m_theory_resolve(false),

1
src/smt/params/smt_params_helper.pyg
View file

@ -62,6 +62,7 @@ def_module_params(module_name='smt',
('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.'),
('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('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'),