mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

Option to enable cube normalization in quic generalizer

Browse source
This commit is contained in:
Arie Gurfinkel 2018-01-04 15:59:44 -05:00
parent 852e181fed
commit 04a778f2fd
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz/base/fixedpoint_params.pyg
View file

@ -189,6 +189,7 @@ def_module_params('fixedpoint',
('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes'), ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes'),
('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints'), ('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints'),
('spacer.use_quant_generalizer', BOOL, False, 'use quantified lemma generalizer'), ('spacer.use_quant_generalizer', BOOL, False, 'use quantified lemma generalizer'),
('spacer.quic_gen_normalize', BOOL, True, 'normalize cube before quantified generalization'),
)) ))

6
src/muz/spacer/spacer_context.cpp
View file

@ -2284,8 +2284,10 @@ void context::init_lemma_generalizers(datalog::rule_set& rules)
} }
if (m_params.spacer_use_quant_generalizer()) { if (m_params.spacer_use_quant_generalizer()) {
m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, *this, 0, true)); m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer,
m_lemma_generalizers.push_back(alloc(lemma_quantifier_generalizer, *this)); *this, 0, true));
m_lemma_generalizers.push_back(alloc(lemma_quantifier_generalizer, *this,
m_params.spacer_quic_gen_normalize()));
} }
if (get_params().spacer_use_eqclass()) { if (get_params().spacer_use_eqclass()) {