From abe67705d3cbead80481f06bf21f3ea4a7208118 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 16 May 2018 10:09:26 -0700 Subject: [PATCH] Cleanup iuc_proof --- src/muz/spacer/spacer_iuc_proof.cpp | 345 +++++++++----------- src/muz/spacer/spacer_iuc_proof.h | 94 +++--- src/muz/spacer/spacer_iuc_solver.cpp | 8 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 24 +- 4 files changed, 211 insertions(+), 260 deletions(-) diff --git a/src/muz/spacer/spacer_iuc_proof.cpp b/src/muz/spacer/spacer_iuc_proof.cpp index 966b59df4..4ee887df5 100644 --- a/src/muz/spacer/spacer_iuc_proof.cpp +++ b/src/muz/spacer/spacer_iuc_proof.cpp @@ -6,229 +6,182 @@ namespace spacer { - /* - * ==================================== - * init - * ==================================== - */ - iuc_proof::iuc_proof(ast_manager& m, proof* pr, expr_set& b_conjuncts) : m(m), m_pr(pr,m) - { - // init A-marks and B-marks - collect_symbols_b(b_conjuncts); - compute_marks(b_conjuncts); - } +/* + * ==================================== + * init + * ==================================== + */ +iuc_proof::iuc_proof(ast_manager& m, proof* pr, expr_set& core_lits) : + m(m), m_pr(pr,m) { + // init A-marks and B-marks + collect_core_symbols(core_lits); + compute_marks(core_lits); +} - proof* iuc_proof::get() - { - return m_pr.get(); - } +/* + * ==================================== + * methods for computing symbol colors + * ==================================== + */ +class collect_pure_proc { + func_decl_set& m_symbs; +public: + collect_pure_proc(func_decl_set& s):m_symbs(s) {} - /* - * ==================================== - * methods for computing symbol colors - * ==================================== - */ - class collect_pure_proc { - func_decl_set& m_symbs; - public: - collect_pure_proc(func_decl_set& s):m_symbs(s) {} - - void operator()(app* a) { - if (a->get_family_id() == null_family_id) { - m_symbs.insert(a->get_decl()); - } - } - void operator()(var*) {} - void operator()(quantifier*) {} - }; - - void iuc_proof::collect_symbols_b(expr_set& b_conjuncts) - { - expr_mark visited; - collect_pure_proc proc(m_symbols_b); - for (expr_set::iterator it = b_conjuncts.begin(); it != b_conjuncts.end(); ++it) - { - for_each_expr(proc, visited, *it); + void operator()(app* a) { + if (a->get_family_id() == null_family_id) { + m_symbs.insert(a->get_decl()); } } + void operator()(var*) {} + void operator()(quantifier*) {} +}; - class is_pure_expr_proc { - func_decl_set const& m_symbs; - array_util m_au; - public: - struct non_pure {}; +void iuc_proof::collect_core_symbols(expr_set& core_lits) +{ + expr_mark visited; + collect_pure_proc proc(m_core_symbols); + for (expr_set::iterator it = core_lits.begin(); it != core_lits.end(); ++it) { + for_each_expr(proc, visited, *it); + } +} - is_pure_expr_proc(func_decl_set const& s, ast_manager& m): +class is_pure_expr_proc { + func_decl_set const& m_symbs; + array_util m_au; +public: + struct non_pure {}; + + is_pure_expr_proc(func_decl_set const& s, ast_manager& m): m_symbs(s), m_au (m) {} - void operator()(app* a) { - if (a->get_family_id() == null_family_id) { - if (!m_symbs.contains(a->get_decl())) { - throw non_pure(); - } - } - else if (a->get_family_id () == m_au.get_family_id () && - a->is_app_of (a->get_family_id (), OP_ARRAY_EXT)) { + void operator()(app* a) { + if (a->get_family_id() == null_family_id) { + if (!m_symbs.contains(a->get_decl())) { throw non_pure(); } } - void operator()(var*) {} - void operator()(quantifier*) {} - }; - - // requires that m_symbols_b has already been computed, which is done during initialization. - bool iuc_proof::only_contains_symbols_b(expr* expr) const - { - is_pure_expr_proc proc(m_symbols_b, m); - try { - for_each_expr(proc, expr); + else if (a->get_family_id () == m_au.get_family_id () && + a->is_app_of (a->get_family_id (), OP_ARRAY_EXT)) { + throw non_pure(); } - catch (is_pure_expr_proc::non_pure) - { - return false; - } - return true; } + void operator()(var*) {} + void operator()(quantifier*) {} +}; - /* - * ==================================== - * methods for computing which premises - * have been used to derive the conclusions - * ==================================== - */ +bool iuc_proof::is_core_pure(expr* e) const +{ + is_pure_expr_proc proc(m_core_symbols, m); + try { + for_each_expr(proc, e); + } + catch (is_pure_expr_proc::non_pure) + {return false;} - void iuc_proof::compute_marks(expr_set& b_conjuncts) + return true; +} + +void iuc_proof::compute_marks(expr_set& core_lits) +{ + proof_post_order it(m_pr, m); + while (it.hasNext()) { - proof_post_order it(m_pr, m); - while (it.hasNext()) + proof* cur = it.next(); + if (m.get_num_parents(cur) == 0) { - proof* currentNode = it.next(); - - if (m.get_num_parents(currentNode) == 0) + switch(cur->get_decl_kind()) { - switch(currentNode->get_decl_kind()) - { - - case PR_ASSERTED: // currentNode is an axiom - { - if (b_conjuncts.contains(m.get_fact(currentNode))) - { - m_b_mark.mark(currentNode, true); - } - else - { - m_a_mark.mark(currentNode, true); - } - break; - } - // currentNode is a hypothesis: - case PR_HYPOTHESIS: - { - m_h_mark.mark(currentNode, true); - break; - } - default: - { - break; - } - } - } - else - { - // collect from parents whether derivation of current node contains A-axioms, B-axioms and hypothesis - bool need_to_mark_a = false; - bool need_to_mark_b = false; - bool need_to_mark_h = false; - - for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) - { - SASSERT(m.is_proof(currentNode->get_arg(i))); - proof* premise = to_app(currentNode->get_arg(i)); - - need_to_mark_a = need_to_mark_a || m_a_mark.is_marked(premise); - need_to_mark_b = need_to_mark_b || m_b_mark.is_marked(premise); - need_to_mark_h = need_to_mark_h || m_h_mark.is_marked(premise); - } - - // if current node is application of lemma, we know that all hypothesis are removed - if(currentNode->get_decl_kind() == PR_LEMMA) - { - need_to_mark_h = false; - } - - // save results - m_a_mark.mark(currentNode, need_to_mark_a); - m_b_mark.mark(currentNode, need_to_mark_b); - m_h_mark.mark(currentNode, need_to_mark_h); + case PR_ASSERTED: + if (core_lits.contains(m.get_fact(cur))) + m_b_mark.mark(cur, true); + else + m_a_mark.mark(cur, true); + break; + case PR_HYPOTHESIS: + m_h_mark.mark(cur, true); + break; + default: + break; } } - } - - bool iuc_proof::is_a_marked(proof* p) - { - return m_a_mark.is_marked(p); - } - bool iuc_proof::is_b_marked(proof* p) - { - return m_b_mark.is_marked(p); - } - bool iuc_proof::is_h_marked(proof* p) - { - return m_h_mark.is_marked(p); - } - - /* - * ==================================== - * methods for dot printing - * ==================================== - */ - void iuc_proof::pp_dot() - { - pp_proof_dot(m, m_pr, this); - } - - /* - * ==================================== - * statistics - * ==================================== - */ - - void iuc_proof::print_farkas_stats() - { - unsigned farkas_counter = 0; - unsigned farkas_counter2 = 0; - - proof_post_order it3(m_pr, m); - while (it3.hasNext()) + else { - proof* currentNode = it3.next(); + // collect from parents whether derivation of current node + // contains A-axioms, B-axioms and hypothesis + bool need_to_mark_a = false; + bool need_to_mark_b = false; + bool need_to_mark_h = false; - // if node is theory lemma - if (is_farkas_lemma(m, currentNode)) + for (unsigned i = 0; i < m.get_num_parents(cur); ++i) { - farkas_counter++; + SASSERT(m.is_proof(cur->get_arg(i))); + proof* premise = to_app(cur->get_arg(i)); - // check whether farkas lemma is to be interpolated (could potentially miss farkas lemmas, which are interpolated, because we potentially don't want to use the lowest cut) - bool has_blue_nonred_parent = false; - for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) - { - proof* premise = to_app(currentNode->get_arg(i)); - if (!is_a_marked(premise) && is_b_marked(premise)) - { - has_blue_nonred_parent = true; - break; - } - } - if (has_blue_nonred_parent && is_a_marked(currentNode)) - { - SASSERT(is_b_marked(currentNode)); - farkas_counter2++; - } + need_to_mark_a |= m_a_mark.is_marked(premise); + need_to_mark_b |= m_b_mark.is_marked(premise); + need_to_mark_h |= m_h_mark.is_marked(premise); } - } - verbose_stream() << "\nThis proof contains " << farkas_counter << " Farkas lemmas. " << farkas_counter2 << " Farkas lemmas participate in the lowest cut\n"; + // if current node is application of a lemma, then all + // active hypotheses are removed + if(cur->get_decl_kind() == PR_LEMMA) need_to_mark_h = false; + + // save results + m_a_mark.mark(cur, need_to_mark_a); + m_b_mark.mark(cur, need_to_mark_b); + m_h_mark.mark(cur, need_to_mark_h); + } } } + +/* + * ==================================== + * statistics + * ==================================== + */ + +// debug method +void iuc_proof::dump_farkas_stats() +{ + unsigned fl_total = 0; + unsigned fl_lowcut = 0; + + proof_post_order it(m_pr, m); + while (it.hasNext()) + { + proof* cur = it.next(); + + // if node is theory lemma + if (is_farkas_lemma(m, cur)) + { + fl_total++; + + // check whether farkas lemma is to be interpolated (could + // potentially miss farkas lemmas, which are interpolated, + // because we potentially don't want to use the lowest + // cut) + bool has_blue_nonred_parent = false; + for (unsigned i = 0; i < m.get_num_parents(cur); ++i) { + proof* premise = to_app(cur->get_arg(i)); + if (!is_a_marked(premise) && is_b_marked(premise)) { + has_blue_nonred_parent = true; + break; + } + } + + if (has_blue_nonred_parent && is_a_marked(cur)) + { + SASSERT(is_b_marked(cur)); + fl_lowcut++; + } + } + } + + IF_VERBOSE(1, verbose_stream() + << "\n total farkas lemmas " << fl_total + << " farkas lemmas in lowest cut " << fl_lowcut << "\n";); +} +} diff --git a/src/muz/spacer/spacer_iuc_proof.h b/src/muz/spacer/spacer_iuc_proof.h index 205648109..97c00ea9b 100644 --- a/src/muz/spacer/spacer_iuc_proof.h +++ b/src/muz/spacer/spacer_iuc_proof.h @@ -4,62 +4,58 @@ #include "ast/ast.h" namespace spacer { - typedef obj_hashtable expr_set; - typedef obj_hashtable func_decl_set; +typedef obj_hashtable expr_set; +typedef obj_hashtable func_decl_set; - /* - * an iuc_proof is a proof together with information of the coloring of the axioms. - */ - class iuc_proof - { - public: - - iuc_proof(ast_manager& m, proof* pr, expr_set& b_conjuncts); - - proof* get(); +/* + * An iuc_proof is a proof together with information of the + * coloring of the axioms. + */ +class iuc_proof +{ +public: - /* - * returns whether symbol contains only symbols which occur in B. - */ - bool only_contains_symbols_b(expr* expr) const; + // Constructs an iuc_proof given an ast_manager, a proof, and a set of + // literals core_lits that might be included in the unsat core + iuc_proof(ast_manager& m, proof* pr, expr_set& core_lits); - bool is_a_marked(proof* p); - bool is_b_marked(proof* p); - bool is_h_marked(proof* p); + // returns the proof object + proof* get() {return m_pr.get();} - bool is_b_pure (proof *p) - {return !is_h_marked (p) && only_contains_symbols_b (m.get_fact (p));} + // returns true if all uninterpreted symbols of e are from the core literals + // requires that m_core_symbols has already been computed + bool is_core_pure(expr* e) const; - /* - * print dot-representation to file proof.dot - * use Graphviz's dot with option -Tpdf to convert dot-representation into pdf - */ - void pp_dot(); - - void print_farkas_stats(); - private: - ast_manager& m; - proof_ref m_pr; - - ast_mark m_a_mark; - ast_mark m_b_mark; - ast_mark m_h_mark; - - func_decl_set m_symbols_b; // symbols, which occur in any b-asserted formula + bool is_a_marked(proof* p) {return m_a_mark.is_marked(p);} + bool is_b_marked(proof* p) {return m_b_mark.is_marked(p);} + bool is_h_marked(proof* p) {return m_h_mark.is_marked(p);} + + bool is_b_pure (proof *p) { + return !is_h_marked (p) && is_core_pure(m.get_fact (p)); + } + + // debug method + void dump_farkas_stats(); +private: + ast_manager& m; + proof_ref m_pr; + + ast_mark m_a_mark; + ast_mark m_b_mark; + ast_mark m_h_mark; + + // symbols that occur in any literals in the core + func_decl_set m_core_symbols; + + // collect symbols occuring in B (the core) + void collect_core_symbols(expr_set& core_lits); + + // compute for each formula of the proof whether it derives + // from A or from B + void compute_marks(expr_set& core_lits); +}; - // collect symbols occuring in B - void collect_symbols_b(expr_set& b_conjuncts); - // compute for each formula of the proof whether it derives from A and whether it derives from B - void compute_marks(expr_set& b_conjuncts); - - void pp_dot_to_stream(std::ofstream& dotstream); - std::string escape_dot(const std::string &s); - - void post_process_dot(std::string dot_filepath, std::ofstream& dotstream); - }; - - } #endif /* IUC_PROOF_H_ */ diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index e2334f1ba..7c159746f 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -289,7 +289,7 @@ void iuc_solver::get_iuc(expr_ref_vector &core) { iuc_proof iuc_before(m, res.get(), B); verbose_stream() << "\nStats before transformation:"; - iuc_before.print_farkas_stats(); + iuc_before.dump_farkas_stats(); } proof_utils::reduce_hypotheses(res); @@ -299,7 +299,7 @@ void iuc_solver::get_iuc(expr_ref_vector &core) { iuc_proof iuc_after(m, res.get(), B); verbose_stream() << "Stats after transformation:"; - iuc_after.print_farkas_stats(); + iuc_after.dump_farkas_stats(); } } else // -- new hypothesis reducer @@ -309,7 +309,7 @@ void iuc_solver::get_iuc(expr_ref_vector &core) { iuc_proof iuc_before(m, res.get(), B); verbose_stream() << "\nStats before transformation:"; - iuc_before.print_farkas_stats(); + iuc_before.dump_farkas_stats(); } theory_axiom_reducer ta_reducer(m); @@ -324,7 +324,7 @@ void iuc_solver::get_iuc(expr_ref_vector &core) { iuc_proof iuc_after(m, res.get(), B); verbose_stream() << "Stats after transformation:"; - iuc_after.print_farkas_stats(); + iuc_after.dump_farkas_stats(); } } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 863023d5b..557983628 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -331,11 +331,13 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vectorassert_expr(lb); s->assert_expr(ub); } } - + // assert: forall i,j: a_ij = sum_k w_ik * s_jk for (unsigned i=0; i < matrix.num_rows(); ++i) { @@ -563,13 +565,13 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vectorget_model(model); - + for (unsigned k=0; k < n; ++k) { ptr_vector literals; vector coefficients; for (unsigned j=0; j < matrix.num_cols(); ++j) { expr_ref evaluation(m); - + model.get()->eval(bounded_vectors[j][k].get(), evaluation, false); if (!util.is_zero(evaluation)) { literals.push_back(ordered_basis[j]); @@ -579,7 +581,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector& todo) { bool is_sink = true; @@ -709,7 +711,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector