From 371ba4fbc0a06710d9946cec7c411077892be5c7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 17 Aug 2017 17:50:47 -0400 Subject: [PATCH] added parameters that seem to work well with quantifiers and arith --- src/muz/spacer/spacer_context.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index ba4958d06..c42bfbbc3 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2212,6 +2212,19 @@ void context::init_lemma_generalizers(datalog::rule_set& rules) 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()) { m_lemma_generalizers.push_back (alloc(lemma_eq_generalizer, *this)); }