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

Moved farkas stats printing to before and after the hyp-reduction

Browse source
This commit is contained in:
Bernhard Gleiss 2017-12-01 15:23:07 +01:00 • committed by Arie Gurfinkel
parent de31b07008
commit 0f25e9e831
2 changed files with 22 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz/spacer/spacer_itp_solver.cpp
View file

@ -281,7 +281,23 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
// preprocess proof in order to get a proof which is better suited for unsat-core-extraction // preprocess proof in order to get a proof which is better suited for unsat-core-extraction
proof_ref pr(get_proof(), m); proof_ref pr(get_proof(), m);
if (m_print_farkas_stats)
{
iuc_proof iuc_before(m, pr.get(), B);
verbose_stream() << "Stats before transformation:";
iuc_before.print_farkas_stats();
}
spacer::reduce_hypotheses(pr); spacer::reduce_hypotheses(pr);
spacer::reduce_hypotheses(pr);
if (m_print_farkas_stats)
{
iuc_proof iuc_after(m, pr.get(), B);
verbose_stream() << "Stats after transformation:";
iuc_after.print_farkas_stats();
}
STRACE("spacer.unsat_core_learner", STRACE("spacer.unsat_core_learner",
verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n"; verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";
); );

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

@ -41,7 +41,7 @@ void unsat_core_learner::register_plugin(unsat_core_plugin* plugin)
void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
{ {
// traverse proof // traverse proof
proof_post_order it(m_pr.get(), m); proof_post_order it(m_pr.get(), m);
while (it.hasNext()) while (it.hasNext())
{ {
proof* currentNode = it.next(); proof* currentNode = it.next();
@ -54,7 +54,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
{ {
SASSERT(m.is_proof(currentNode->get_arg(i))); SASSERT(m.is_proof(currentNode->get_arg(i)));
proof* premise = to_app(currentNode->get_arg(i)); proof* premise = to_app(currentNode->get_arg(i));
need_to_mark_closed = need_to_mark_closed && (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise)); need_to_mark_closed = need_to_mark_closed && (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
} }
@ -75,16 +75,6 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
// TODO: remove duplicates from unsat core? // TODO: remove duplicates from unsat core?
// count both number of all Farkas lemmas and number of Farkas lemmas in the cut
if (m_print_farkas_stats)
{
m_pr.print_farkas_stats();
}
//TODO remove this
if(m_iuc_debug_proof)
{
}
verbose_stream() << std::endl; verbose_stream() << std::endl;
// move all lemmas into vector // move all lemmas into vector
for (expr* const* it = m_unsat_core.begin(); it != m_unsat_core.end(); ++it) for (expr* const* it = m_unsat_core.begin(); it != m_unsat_core.end(); ++it)
@ -119,14 +109,14 @@ void unsat_core_learner::set_closed(proof* p, bool value)
{ {
m_closed.mark(p, value); m_closed.mark(p, value);
} }
bool unsat_core_learner::is_b_open(proof *p) bool unsat_core_learner::is_b_open(proof *p)
{ {
return m_pr.is_b_marked(p) && !is_closed (p); return m_pr.is_b_marked(p) && !is_closed (p);
} }
void unsat_core_learner::add_lemma_to_core(expr* lemma) void unsat_core_learner::add_lemma_to_core(expr* lemma)
{ {
m_unsat_core.push_back(lemma); m_unsat_core.push_back(lemma);
} }
} }