mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Rename expand_node --> expand_pob

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-17 13:31:28 -07:00
parent 3f9b5bce99
commit ec8f99fee7
2 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2854,7 +2854,7 @@ bool context::check_reachability ()
node = m_pob_queue.top ();
SASSERT (node->level () <= m_pob_queue.max_level ());
switch (expand_node(*node)) {
switch (expand_pob(*node)) {
case l_true:
SASSERT (m_pob_queue.top () == node.get ());
m_pob_queue.pop ();
@ -2982,23 +2982,23 @@ bool context::is_reachable(pob &n)
}
//this processes a goal and creates sub-goal
lbool context::expand_node(pob& n)
lbool context::expand_pob(pob& n)
{
pob::on_expand_event _evt(n);
TRACE ("spacer",
tout << "expand-node: " << n.pt().head()->get_name()
tout << "expand-pob: " << n.pt().head()->get_name()
<< " level: " << n.level()
<< " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n"
<< mk_pp(n.post(), m) << "\n";);
STRACE ("spacer.expand-add",
tout << "expand-node: " << n.pt().head()->get_name()
tout << "expand-pob: " << n.pt().head()->get_name()
<< " level: " << n.level()
<< " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n"
<< mk_epp(n.post(), m) << "\n\n";);
TRACE ("core_array_eq",
tout << "expand-node: " << n.pt().head()->get_name()
tout << "expand-pob: " << n.pt().head()->get_name()
<< " level: " << n.level()
<< " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n"
<< mk_pp(n.post(), m) << "\n";);
@ -3109,7 +3109,7 @@ lbool context::expand_node(pob& n)
// n is unreachable, create new summary facts
case l_false: {
timeit _timer (is_trace_enabled("spacer_timeit"),
"spacer::expand_node::false",
"spacer::expand_pob::false",
verbose_stream ());
// -- only update expanded level when new lemmas are generated at it.
@ -3164,7 +3164,7 @@ lbool context::expand_node(pob& n)
if (n.weakness() < 100 /* MAX_WEAKENSS */) {
bool has_new_child = false;
SASSERT(m_weak_abs);
m_stats.m_expand_node_undef++;
m_stats.m_expand_pob_undef++;
if (r && r->get_uninterpreted_tail_size() > 0) {
model_evaluator_util mev(m);
mev.set_model(*model);
@ -3181,7 +3181,7 @@ lbool context::expand_node(pob& n)
// -- failed to create a child, bump weakness and repeat
// -- the recursion is bounded by the levels of weakness supported
n.bump_weakness();
return expand_node(n);
return expand_pob(n);
}
TRACE("spacer", tout << "unknown state: " << mk_and(cube) << "\n";);
throw unknown_exception();
@ -3500,8 +3500,8 @@ void context::collect_statistics(statistics& st) const
st.update("SPACER inductive level", m_inductive_lvl);
// -- length of the counterexample
st.update("SPACER cex depth", m_stats.m_cex_depth);
// -- number of times expand_node resulted in undef
st.update("SPACER expand node undef", m_stats.m_expand_node_undef);
// -- number of times expand_pobresulted in undef
st.update("SPACER expand pob undef", m_stats.m_expand_pob_undef);
// -- number of distinct lemmas constructed
st.update("SPACER num lemmas", m_stats.m_num_lemmas);
// -- number of restarts taken
@ -3730,7 +3730,7 @@ inline bool pob_lt::operator() (const pob *pn1, const pob *pn2) const
/** XXX Identical nodes. This should not happen. However,
* currently, when propagating reachability, we might call
* expand_node() twice on the same node, causing it to generate
* expand_pob() twice on the same node, causing it to generate
* the same proof obligation multiple times */
return &n1 < &n2;
}

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

@ -744,7 +744,7 @@ class context {
unsigned m_max_query_lvl;
unsigned m_max_depth;
unsigned m_cex_depth;
unsigned m_expand_node_undef;
unsigned m_expand_pob_undef;
unsigned m_num_lemmas;
unsigned m_num_restarts;
unsigned m_num_lemmas_imported;
@ -792,7 +792,7 @@ class context {
bool propagate(unsigned min_prop_lvl, unsigned max_prop_lvl,
unsigned full_prop_lvl);
bool is_reachable(pob &n);
lbool expand_node(pob& n);
lbool expand_pob(pob &n);
reach_fact *mk_reach_fact (pob& n, model_evaluator_util &mev,
datalog::rule const& r);
bool create_children(pob& n, datalog::rule const& r,