mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

added parameters that seem to work well with quantifiers and arith

Browse source
This commit is contained in:
Arie Gurfinkel 2017-08-17 17:50:47 -04:00
parent 27d8fa4a34
commit 371ba4fbc0
1 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2212,6 +2212,19 @@ void context::init_lemma_generalizers(datalog::rule_set& rules)
fparams.m_mbqi = m_params.spacer_mbqi(); fparams.m_mbqi = m_params.spacer_mbqi();
if (!m_params.spacer_ground_cti()) {
fparams.m_pi_use_database = true;
fparams.m_phase_selection = PS_CACHING_CONSERVATIVE2;
fparams.m_restart_strategy = RS_GEOMETRIC;
fparams.m_restart_factor = 1.5;
fparams.m_eliminate_bounds = true;
fparams.m_qi_quick_checker = MC_UNSAT;
fparams.m_propagate_booleans = true;
fparams.m_qi_eager_threshold = 10;
fparams.m_qi_lazy_threshold = 20;
fparams.m_ng_lift_ite = LI_FULL;
}
if (get_params().spacer_use_eqclass()) { if (get_params().spacer_use_eqclass()) {
m_lemma_generalizers.push_back (alloc(lemma_eq_generalizer, *this)); m_lemma_generalizers.push_back (alloc(lemma_eq_generalizer, *this));
} }