mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add flag to control whether ite-lifting under quantifiers is conservative or full for #4746, use smt.q.lift_ite=2 to obtain legacy behavior

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-27 16:27:24 -07:00
parent e2fbd05fe7
commit 07680408a6
3 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -26,6 +26,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
m_restricted_quasi_macros = p.restricted_quasi_macros();
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
m_refine_inj_axiom = p.refine_inj_axioms();
m_ng_lift_ite = static_cast<lift_ite_kind>(p.q_lift_ite());
}
void preprocessor_params::updt_params(params_ref const & p) {

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

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

6
src/smt/smt_setup.cpp
View file

@ -640,7 +640,8 @@ namespace smt {
// It destroys the existing patterns.
// m_params.m_macro_finder = true;
m_params.m_ng_lift_ite = LI_CONSERVATIVE;
if (m_params.m_ng_lift_ite == LI_NONE)
m_params.m_ng_lift_ite = LI_CONSERVATIVE;
TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
setup_arrays();
@ -664,7 +665,8 @@ namespace smt {
m_params.m_qi_lazy_threshold = 20;
//
m_params.m_macro_finder = true;
m_params.m_ng_lift_ite = LI_CONSERVATIVE;
if (m_params.m_ng_lift_ite == LI_NONE)
m_params.m_ng_lift_ite = LI_CONSERVATIVE;
m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP
m_params.m_array_lazy_ieq = true;
m_params.m_array_lazy_ieq_delay = 4;