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

Debug print

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-06 09:34:03 -07:00
parent c3fb863ad1
commit 54add824e9
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -246,8 +246,8 @@ lbool context::gpdr_solve_core() {
} }
// communicate failure to datalog::context // communicate failure to datalog::context
if (m_context) { if (m_context) {
m_context->set_status(datalog::BOUNDED); m_context->set_status(datalog::BOUNDED);
} }
return l_undef; return l_undef;
} }
@ -279,7 +279,7 @@ bool context::gpdr_check_reachability(unsigned lvl, model_search &ms) {
TRACE("spacer_pdr", TRACE("spacer_pdr",
tout << "looking at pob at level " << pob->level() << " " tout << "looking at pob at level " << pob->level() << " "
<< mk_pp(pob->post(), m) << "\n";); << mk_pp(pob->post(), m) << "\n";);
if (pob != node->pob()) if (pob != node->pob())
ms.add_leaf(alloc(model_node, node, pob)); ms.add_leaf(alloc(model_node, node, pob));
} }
node->check_pre_closed(); node->check_pre_closed();
@ -332,6 +332,13 @@ bool context::gpdr_create_split_children(pob &n, const datalog::rule &r,
<< (k->use_farkas_generalizer() ? "FAR " : "SUB ") << (k->use_farkas_generalizer() ? "FAR " : "SUB ")
<< k->post()->get_id(); << k->post()->get_id();
verbose_stream().flush();); verbose_stream().flush(););
TRACE ("spacer",
tout << "create-pob: " << k->pt().head()->get_name()
<< " level: " << k->level()
<< " depth: " << k->depth ()
<< " fvsz: " << k->get_free_vars_size() << "\n"
<< mk_pp(k->post(), m) << "\n";);
} }