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

Bug fix for quantified pob generation

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-04 15:54:05 -07:00
parent 2a243d38d1
commit e860e4d045
1 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -288,24 +288,26 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
timeit _timer2(is_trace_enabled("spacer_timeit"), timeit _timer2(is_trace_enabled("spacer_timeit"),
"create_next_child::qproject2", "create_next_child::qproject2",
verbose_stream ()); verbose_stream ());
// include m_evars in case they can eliminated now as well
vars.append(m_evars); vars.append(m_evars);
m_evars.reset();
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_cti());
//qe::reduce_array_selects (*mev.get_model (), post); //qe::reduce_array_selects (*mev.get_model (), post);
}
// remember variables that need to be existentially quantified else {
m_evars.append(vars); // if no variables to eliminate, don't forget about m_evars
vars.reset(); // that occur in m_trans
vars.append(m_evars);
} }
if (!m_evars.empty()) { if (!vars.empty()) {
// existentially quantify out m_evars from post and skolemize the result // existentially quantify out vars from post and skolemize the result
exist_skolemize(post.get(), m_evars, post); exist_skolemize(post.get(), vars, post);
} }
get_manager ().formula_o2n (post.get (), post, get_manager ().formula_o2n (post.get (), post,
m_premises [m_active].get_oidx (), m_evars.empty()); m_premises [m_active].get_oidx (),
vars.empty());
/* The level and depth are taken from the parent, not the sibling. /* The level and depth are taken from the parent, not the sibling.
@ -313,7 +315,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
and lower level is a better starting point. */ and lower level is a better starting point. */
pob *n = m_premises[m_active].pt().mk_pob(&m_parent, pob *n = m_premises[m_active].pt().mk_pob(&m_parent,
prev_level (m_parent.level ()), prev_level (m_parent.level ()),
m_parent.depth (), post, m_evars); m_parent.depth (), post, vars);
IF_VERBOSE (1, verbose_stream () IF_VERBOSE (1, verbose_stream ()
<< "\n\tcreate_child: " << n->pt ().head ()->get_name () << "\n\tcreate_child: " << n->pt ().head ()->get_name ()
<< " (" << n->level () << ", " << n->depth () << ") " << " (" << n->level () << ", " << n->depth () << ") "