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

Refactoring

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-17 13:43:35 -07:00
parent ec8f99fee7
commit a696a40a3a
2 changed files with 27 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2981,6 +2981,24 @@ bool context::is_reachable(pob &n)
return next ? is_reachable(*next) : true;
}
void context::dump_json()
{
if(m_params.spacer_print_json().size()) {
std::ofstream of;
of.open(m_params.spacer_print_json().bare_str());
m_json_marshaller.marshal(of);
of.close();
}
}
void context::predecessor_eh()
{
for (unsigned i = 0; i < m_callbacks.size(); i++) {
if(m_callbacks[i]->predecessor())
m_callbacks[i]->predecessor_eh();
}
}
//this processes a goal and creates sub-goal
lbool context::expand_pob(pob& n)
{
@ -3040,10 +3058,7 @@ lbool context::expand_pob(pob& n)
tout << "This pob can be blocked by instantiation\n";);
}
for (unsigned i = 0; i < m_callbacks.size(); i++){
if(m_callbacks[i]->predecessor())
m_callbacks[i]->predecessor_eh();
}
predecessor_eh();
lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r,
reach_pred_used, num_reuse_reach);
@ -3106,8 +3121,9 @@ lbool context::expand_pob(pob& n)
return l_undef;
}
case l_false:
// n is unreachable, create new summary facts
case l_false: {
{
timeit _timer (is_trace_enabled("spacer_timeit"),
"spacer::expand_pob::false",
verbose_stream ());
@ -3133,9 +3149,9 @@ lbool context::expand_pob(pob& n)
(*m_lemma_generalizers[i])(lemma);
}
DEBUG_CODE(
lemma_sanity_checker sanity_checker(*this);
sanity_checker(lemma);
);
lemma_sanity_checker sanity_checker(*this);
sanity_checker(lemma);
);
TRACE("spacer", tout << "invariant state: "

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

@ -824,14 +824,9 @@ class context {
unsigned get_cex_depth ();
void dump_json() {
if(m_params.spacer_print_json().size()) {
std::ofstream of;
of.open(m_params.spacer_print_json().bare_str());
m_json_marshaller.marshal(of);
of.close();
}
}
void dump_json();
void predecessor_eh();
public:
/**