mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Cleanup spacer options

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-05 18:43:10 -07:00
parent 1994f1d7e4
commit e1a45671b3
2 changed files with 12 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -262,7 +262,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
vars.append(m_evars); vars.append(m_evars);
m_evars.reset(); m_evars.reset();
pt().mbp(vars, m_trans, mev.get_model(), pt().mbp(vars, m_trans, mev.get_model(),
true, pt().get_context().use_ground_cti()); true, pt().get_context().use_ground_pob());
m_evars.append (vars); m_evars.append (vars);
vars.reset(); vars.reset();
} }
@ -291,7 +291,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
// include m_evars in case they can eliminated now as well // include m_evars in case they can eliminated now as well
vars.append(m_evars); vars.append(m_evars);
pt().mbp(vars, post, mev.get_model(), pt().mbp(vars, post, mev.get_model(),
true, pt().get_context().use_ground_cti()); true, pt().get_context().use_ground_pob());
//qe::reduce_array_selects (*mev.get_model (), post); //qe::reduce_array_selects (*mev.get_model (), post);
} }
else { else {
@ -395,7 +395,7 @@ pob *derivation::create_next_child ()
vars.append(m_evars); vars.append(m_evars);
m_evars.reset(); m_evars.reset();
this->pt().mbp(vars, m_trans, mev.get_model(), this->pt().mbp(vars, m_trans, mev.get_model(),
true, this->pt().get_context().use_ground_cti()); true, this->pt().get_context().use_ground_pob());
// keep track of implicitly quantified variables // keep track of implicitly quantified variables
m_evars.append (vars); m_evars.append (vars);
vars.reset(); vars.reset();
@ -2224,13 +2224,6 @@ context::context(fixedpoint_params const& params,
m_last_result(l_undef), m_last_result(l_undef),
m_inductive_lvl(0), m_inductive_lvl(0),
m_expanded_lvl(0), m_expanded_lvl(0),
m_use_native_mbp(params.spacer_native_mbp ()),
m_ground_cti (params.spacer_ground_cti ()),
m_instantiate (params.spacer_q3_instantiate ()),
m_use_qlemmas (params.spacer_q3()),
m_weak_abs(params.spacer_weak_abs()),
m_use_restarts(params.spacer_restarts()),
m_restart_initial_threshold(params.spacer_restart_initial_threshold()),
m_json_marshaller(this) { m_json_marshaller(this) {
ref<solver> pool0_base = ref<solver> pool0_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null); mk_smt_solver(m, params_ref::get_empty(), symbol::null);
@ -2281,6 +2274,12 @@ void context::updt_params() {
m_use_gpdr = m_params.spacer_gpdr(); m_use_gpdr = m_params.spacer_gpdr();
m_simplify_formulas_pre = m_params.pdr_simplify_formulas_pre(); m_simplify_formulas_pre = m_params.pdr_simplify_formulas_pre();
m_simplify_formulas_post = m_params.pdr_simplify_formulas_post(); m_simplify_formulas_post = m_params.pdr_simplify_formulas_post();
m_use_native_mbp = m_params.spacer_native_mbp ();
m_instantiate = m_params.spacer_q3_instantiate ();
m_use_qlemmas = m_params.spacer_q3();
m_weak_abs = m_params.spacer_weak_abs();
m_use_restarts = m_params.spacer_restarts();
m_restart_initial_threshold = m_params.spacer_restart_initial_threshold();
if (m_use_gpdr) { if (m_use_gpdr) {
@ -3716,9 +3715,9 @@ bool context::create_children(pob& n, datalog::rule const& r,
// skolems of the pob // skolems of the pob
n.get_skolems(vars); n.get_skolems(vars);
n.pt().mbp(vars, phi, mev.get_model (), true, use_ground_cti()); n.pt().mbp(vars, phi, mev.get_model (), true, use_ground_pob());
//qe::reduce_array_selects (*mev.get_model (), phi1); //qe::reduce_array_selects (*mev.get_model (), phi1);
SASSERT (!m_ground_cti || vars.empty ()); SASSERT (!m_ground_pob || vars.empty ());
TRACE ("spacer", TRACE ("spacer",
tout << "Implicant:\n"; tout << "Implicant:\n";

3
src/muz/spacer/spacer_context.h
View file

@ -841,7 +841,6 @@ class context {
model_converter_ref m_mc; model_converter_ref m_mc;
proof_converter_ref m_pc; proof_converter_ref m_pc;
bool m_use_native_mbp; bool m_use_native_mbp;
bool m_ground_cti;
bool m_instantiate; bool m_instantiate;
bool m_use_qlemmas; bool m_use_qlemmas;
bool m_weak_abs; bool m_weak_abs;
@ -935,7 +934,7 @@ public:
const fixedpoint_params &get_params() const { return m_params; } const fixedpoint_params &get_params() const { return m_params; }
bool use_native_mbp () {return m_use_native_mbp;} bool use_native_mbp () {return m_use_native_mbp;}
bool use_ground_cti () {return m_ground_cti;} bool use_ground_pob () {return m_ground_pob;}
bool use_instantiate () {return m_instantiate;} bool use_instantiate () {return m_instantiate;}
bool weak_abs() {return m_weak_abs;} bool weak_abs() {return m_weak_abs;}
bool use_qlemmas () {return m_use_qlemmas;} bool use_qlemmas () {return m_use_qlemmas;}