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

add params for theory case split

Browse source
This commit is contained in:
Murphy Berzish 2017-05-01 10:18:38 -04:00
parent aceee3fac8
commit f655e1976e
3 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -31,6 +31,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
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_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
@ -155,4 +156,4 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_check_at_labels);
DISPLAY_PARAM(m_dump_goal_as_smt);
DISPLAY_PARAM(m_auto_config);
}
}

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

@ -109,6 +109,7 @@ struct smt_params : public preprocessor_params,
case_split_strategy m_case_split_strategy;
unsigned m_rel_case_split_order;
bool m_lookahead_diseq;
bool m_theory_case_split;
// -----------------------------------
//

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

@ -61,6 +61,7 @@ def_module_params(module_name='smt',
('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.'),
('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'),