From 58dc5451e159866f4655184837de7fbf233d5dc2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 21 Jun 2018 17:16:23 -0400 Subject: [PATCH] iuc code cleanup --- src/muz/spacer/spacer_unsat_core_learner.cpp | 33 ++-- src/muz/spacer/spacer_unsat_core_learner.h | 25 +-- src/muz/spacer/spacer_unsat_core_plugin.cpp | 152 +++++++++---------- src/muz/spacer/spacer_unsat_core_plugin.h | 16 +- 4 files changed, 114 insertions(+), 112 deletions(-) diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index da0d6ec34..08f7f7ce8 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -36,28 +36,27 @@ void unsat_core_learner::register_plugin(unsat_core_plugin* plugin) { } void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) { - // traverse proof proof_post_order it(m_pr.get(), m); while (it.hasNext()) { - proof* currentNode = it.next(); + proof* curr = it.next(); - if (m.get_num_parents(currentNode) > 0) { - bool need_to_mark_closed = true; + bool done = is_closed(curr); + if (done) continue; - for (proof* premise : m.get_parents(currentNode)) { - need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise)); - } - - // save result - m_closed.mark(currentNode, need_to_mark_closed); + if (m.get_num_parents(curr) > 0) { + done = true; + for (proof* p : m.get_parents(curr)) done &= !is_b_open(p); + set_closed(curr, done); } - // we have now collected all necessary information, so we can visit the node - // if the node mixes A-reasoning and B-reasoning and contains non-closed premises - if (m_pr.is_a_marked(currentNode) && - m_pr.is_b_marked(currentNode) && - !m_closed.is_marked(currentNode)) { - compute_partial_core(currentNode); // then we need to compute a partial core + // we have now collected all necessary information, + // so we can visit the node + // if the node mixes A-reasoning and B-reasoning + // and contains non-closed premises + if (!done) { + if (m_pr.is_a_marked(curr) && m_pr.is_b_marked(curr)) { + compute_partial_core(curr); + } } } @@ -74,7 +73,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) { void unsat_core_learner::compute_partial_core(proof* step) { for (unsat_core_plugin* plugin : m_plugins) { - if (m_closed.is_marked(step)) break; + if (is_closed(step)) break; plugin->compute_partial_core(step); } } diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h index 327b12eb6..42ad71501 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.h +++ b/src/muz/spacer/spacer_unsat_core_learner.h @@ -22,6 +22,7 @@ Revision History: #include "ast/ast.h" #include "muz/spacer/spacer_util.h" #include "muz/spacer/spacer_proof_utils.h" +#include "muz/spacer/spacer_iuc_proof.h" namespace spacer { @@ -31,13 +32,25 @@ namespace spacer { class unsat_core_learner { typedef obj_hashtable expr_set; + ast_manager& m; + iuc_proof& m_pr; + + ptr_vector m_plugins; + ast_mark m_closed; + + expr_ref_vector m_unsat_core; + public: unsat_core_learner(ast_manager& m, iuc_proof& pr) : m(m), m_pr(pr), m_unsat_core(m) {}; virtual ~unsat_core_learner(); - ast_manager& m; - iuc_proof& m_pr; + ast_manager& get_manager() {return m;} + + bool is_a(proof *pr) {return m_pr.is_a_marked(pr);} + bool is_b(proof *pr) {return m_pr.is_b_marked(pr);} + bool is_h(proof *pr) {return m_pr.is_h_marked(pr);} + bool is_b_pure(proof *pr) { return m_pr.is_b_pure(pr);} /* * register a plugin for computation of partial unsat cores @@ -67,14 +80,6 @@ namespace spacer { void add_lemma_to_core(expr* lemma); private: - ptr_vector m_plugins; - ast_mark m_closed; - - /* - * collects the lemmas of the unsat-core - * will at the end be inserted into unsat_core. - */ - expr_ref_vector m_unsat_core; /* * computes partial core for step by delegating computation to plugins diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 79bafdfeb..ef97d81df 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -34,27 +34,25 @@ Revision History: namespace spacer { - unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner): - m(learner.m), m_learner(learner) {}; + unsat_core_plugin::unsat_core_plugin(unsat_core_learner& ctx): + m(ctx.get_manager()), m_ctx(ctx) {}; void unsat_core_plugin_lemma::compute_partial_core(proof* step) { - SASSERT(m_learner.m_pr.is_a_marked(step)); - SASSERT(m_learner.m_pr.is_b_marked(step)); + SASSERT(m_ctx.is_a(step)); + SASSERT(m_ctx.is_b(step)); - for (proof* premise : m.get_parents(step)) { - - if (m_learner.is_b_open (premise)) { + for (auto* p : m.get_parents(step)) { + if (m_ctx.is_b_open (p)) { // by IH, premises that are AB marked are already closed - SASSERT(!m_learner.m_pr.is_a_marked(premise)); - add_lowest_split_to_core(premise); + SASSERT(!m_ctx.is_a(p)); + add_lowest_split_to_core(p); } } - m_learner.set_closed(step, true); + m_ctx.set_closed(step, true); } - void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const - { - SASSERT(m_learner.is_b_open(step)); + void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const { + SASSERT(m_ctx.is_b_open(step)); ptr_buffer todo; todo.push_back(step); @@ -64,44 +62,45 @@ namespace spacer { todo.pop_back(); // if current step hasn't been processed, - if (!m_learner.is_closed(pf)) { - m_learner.set_closed(pf, true); + if (!m_ctx.is_closed(pf)) { + m_ctx.set_closed(pf, true); // the step is b-marked and not closed. // by I.H. the step must be already visited // so if it is also a-marked, it must be closed - SASSERT(m_learner.m_pr.is_b_marked(pf)); - SASSERT(!m_learner.m_pr.is_a_marked(pf)); + SASSERT(m_ctx.is_b(pf)); + SASSERT(!m_ctx.is_a(pf)); // the current step needs to be interpolated: expr* fact = m.get_fact(pf); // if we trust the current step and we are able to use it - if (m_learner.m_pr.is_b_pure (pf) && - (m.is_asserted(pf) || is_literal(m, fact))) { + if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || is_literal(m, fact))) { // just add it to the core - m_learner.add_lemma_to_core(fact); + m_ctx.add_lemma_to_core(fact); } // otherwise recurse on premises else { for (proof* premise : m.get_parents(pf)) - if (m_learner.is_b_open(premise)) + if (m_ctx.is_b_open(premise)) todo.push_back(premise); } - } } } - void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step) - { - SASSERT(m_learner.m_pr.is_a_marked(step)); - SASSERT(m_learner.m_pr.is_b_marked(step)); + /*** + * FARKAS + */ + void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step) { + SASSERT(m_ctx.is_a(step)); + SASSERT(m_ctx.is_b(step)); // XXX this assertion should be true so there is no need to check for it - SASSERT (!m_learner.is_closed (step)); + SASSERT (!m_ctx.is_closed (step)); func_decl* d = step->get_decl(); symbol sym; - if (!m_learner.is_closed(step) && // if step is not already interpolated - is_farkas_lemma(m, step)) { + TRACE("spacer.farkas", + tout << "looking at: " << mk_pp(step, m) << "\n";); + if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) { // weaker check : d->get_num_parameters() >= m.get_num_parents(step) + 2 SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); @@ -136,24 +135,24 @@ namespace spacer { parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient TRACE("spacer.farkas", - tout << "Farkas input: "<< "\n"; - for (unsigned i = 0; i < m.get_num_parents(step); ++i) { - proof * prem = m.get_parent(step, i); - rational coef = params[i].get_rational(); - bool b_pure = m_learner.m_pr.is_b_pure (prem); - tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; - } - ); + tout << "Farkas input: "<< "\n"; + for (unsigned i = 0; i < m.get_num_parents(step); ++i) { + proof * prem = m.get_parent(step, i); + rational coef = params[i].get_rational(); + bool b_pure = m_ctx.is_b_pure (prem); + tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; + } + ); - bool can_be_closed = true; + bool done = true; for (unsigned i = 0; i < m.get_num_parents(step); ++i) { proof * premise = m.get_parent(step, i); - if (m_learner.is_b_open (premise)) { - SASSERT(!m_learner.m_pr.is_a_marked(premise)); + if (m_ctx.is_b_open (premise)) { + SASSERT(!m_ctx.is_a(premise)); - if (m_learner.m_pr.is_b_pure (premise)) { + if (m_ctx.is_b_pure (premise)) { if (!m_use_constant_from_a) { rational coefficient = params[i].get_rational(); coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); @@ -161,7 +160,7 @@ namespace spacer { } else { // -- mixed premise, won't be able to close this proof step - can_be_closed = false; + done = false; if (m_use_constant_from_a) { rational coefficient = params[i].get_rational(); @@ -177,6 +176,7 @@ namespace spacer { } } + // TBD: factor into another method if (m_use_constant_from_a) { params += m.get_num_parents(step); // point to the first Farkas coefficient, which corresponds to a formula in the conclusion @@ -208,11 +208,9 @@ namespace spacer { // only if all b-premises can be used directly, add the farkas core and close the step // AG: this decision needs to be re-evaluated. If the proof cannot be closed, literals above // AG: it will go into the core. However, it does not mean that this literal should/could not be added. - if (can_be_closed) { - m_learner.set_closed(step, true); - expr_ref res = compute_linear_combination(coeff_lits); - m_learner.add_lemma_to_core(res); - } + m_ctx.set_closed(step, done); + expr_ref res = compute_linear_combination(coeff_lits); + m_ctx.add_lemma_to_core(res); } } @@ -236,12 +234,12 @@ namespace spacer { void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step) { - SASSERT(m_learner.m_pr.is_a_marked(step)); - SASSERT(m_learner.m_pr.is_b_marked(step)); + SASSERT(m_ctx.is_a(step)); + SASSERT(m_ctx.is_b(step)); func_decl* d = step->get_decl(); symbol sym; - if (!m_learner.is_closed(step) && // if step is not already interpolated + if (!m_ctx.is_closed(step) && // if step is not already interpolated is_farkas_lemma(m, step)) { SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); SASSERT(m.has_fact(step)); @@ -250,25 +248,25 @@ namespace spacer { parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient - STRACE("spacer.farkas", - verbose_stream() << "Farkas input: "<< "\n"; - for (unsigned i = 0; i < m.get_num_parents(step); ++i) { - proof * prem = m.get_parent(step, i); - rational coef = params[i].get_rational(); - bool b_pure = m_learner.m_pr.is_b_pure (prem); - verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m_learner.m) << "\n"; - } - ); + TRACE("spacer.farkas", + tout << "Farkas input: "<< "\n"; + for (unsigned i = 0; i < m.get_num_parents(step); ++i) { + proof * prem = m.get_parent(step, i); + rational coef = params[i].get_rational(); + bool b_pure = m_ctx.is_b_pure (prem); + tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; + } + ); bool can_be_closed = true; for (unsigned i = 0; i < m.get_num_parents(step); ++i) { proof * premise = m.get_parent(step, i); - if (m_learner.m_pr.is_b_marked(premise) && !m_learner.is_closed(premise)) + if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise)) { - SASSERT(!m_learner.m_pr.is_a_marked(premise)); + SASSERT(!m_ctx.is_a(premise)); - if (m_learner.m_pr.is_b_pure(premise)) + if (m_ctx.is_b_pure(premise)) { rational coefficient = params[i].get_rational(); linear_combination.push_back @@ -284,7 +282,7 @@ namespace spacer { // only if all b-premises can be used directly, close the step and add linear combinations for later processing if (can_be_closed) { - m_learner.set_closed(step, true); + m_ctx.set_closed(step, true); if (!linear_combination.empty()) { m_linear_combinations.push_back(linear_combination); @@ -350,7 +348,7 @@ namespace spacer { SASSERT(!coeff_lits.empty()); expr_ref linear_combination = compute_linear_combination(coeff_lits); - m_learner.add_lemma_to_core(linear_combination); + m_ctx.add_lemma_to_core(linear_combination); } } @@ -481,7 +479,7 @@ namespace spacer { SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already expr_ref linear_combination = compute_linear_combination(coeff_lits); - m_learner.add_lemma_to_core(linear_combination); + m_ctx.add_lemma_to_core(linear_combination); } return; } @@ -505,10 +503,10 @@ namespace spacer { { ptr_vector todo; - SASSERT(m_learner.m_pr.is_a_marked(step)); - SASSERT(m_learner.m_pr.is_b_marked(step)); + SASSERT(m_ctx.is_a(step)); + SASSERT(m_ctx.is_b(step)); SASSERT(m.get_num_parents(step) > 0); - SASSERT(!m_learner.is_closed(step)); + SASSERT(!m_ctx.is_closed(step)); todo.push_back(step); while (!todo.empty()) @@ -517,7 +515,7 @@ namespace spacer { todo.pop_back(); // if we need to deal with the node and if we haven't added the corresponding edges so far - if (!m_learner.is_closed(current) && !m_visited.is_marked(current)) + if (!m_ctx.is_closed(current) && !m_visited.is_marked(current)) { // compute smallest subproof rooted in current, which has only good edges // add an edge from current to each leaf of that subproof @@ -528,7 +526,7 @@ namespace spacer { } } - m_learner.set_closed(step, true); + m_ctx.set_closed(step, true); } @@ -539,7 +537,7 @@ namespace spacer { ptr_buffer todo_subproof; for (proof* premise : m.get_parents(step)) { - if (m_learner.m_pr.is_b_marked(premise)) { + if (m_ctx.is_b(premise)) { todo_subproof.push_back(premise); } } @@ -549,21 +547,21 @@ namespace spacer { todo_subproof.pop_back(); // if we need to deal with the node - if (!m_learner.is_closed(current)) + if (!m_ctx.is_closed(current)) { - SASSERT(!m_learner.m_pr.is_a_marked(current)); // by I.H. the step must be already visited + SASSERT(!m_ctx.is_a(current)); // by I.H. the step must be already visited // and the current step needs to be interpolated: - if (m_learner.m_pr.is_b_marked(current)) + if (m_ctx.is_b(current)) { // if we trust the current step and we are able to use it - if (m_learner.m_pr.is_b_pure (current) && + if (m_ctx.is_b_pure (current) && (m.is_asserted(current) || is_literal(m, m.get_fact(current)))) { // we found a leaf of the subproof, so // 1) we add corresponding edges - if (m_learner.m_pr.is_a_marked(step)) + if (m_ctx.is_a(step)) { add_edge(nullptr, current); // current is sink } @@ -685,7 +683,7 @@ namespace spacer { m_min_cut.compute_min_cut(cut_nodes); for (unsigned cut_node : cut_nodes) { - m_learner.add_lemma_to_core(m_node_to_formula[cut_node]); + m_ctx.add_lemma_to_core(m_node_to_formula[cut_node]); } } } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h index c05bcc5b9..746f21b19 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.h +++ b/src/muz/spacer/spacer_unsat_core_plugin.h @@ -35,14 +35,14 @@ namespace spacer { virtual ~unsat_core_plugin() {}; virtual void compute_partial_core(proof* step) = 0; virtual void finalize(){}; - - unsat_core_learner& m_learner; + + unsat_core_learner& m_ctx; }; - class unsat_core_plugin_lemma : public unsat_core_plugin { + class unsat_core_plugin_lemma : public unsat_core_plugin { public: - unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){}; - void compute_partial_core(proof* step) override; + unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){}; + void compute_partial_core(proof* step) override; private: void add_lowest_split_to_core(proof* step) const; }; @@ -54,7 +54,7 @@ namespace spacer { bool use_constant_from_a=true) : unsat_core_plugin(learner), m_split_literals(split_literals), - m_use_constant_from_a(use_constant_from_a) {}; + m_use_constant_from_a(use_constant_from_a) {}; void compute_partial_core(proof* step) override; private: bool m_split_literals; @@ -64,8 +64,8 @@ namespace spacer { */ expr_ref compute_linear_combination(const coeff_lits_t& coeff_lits); }; - - class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin { + + class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin { public: unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {}; void compute_partial_core(proof* step) override;