From 3bc3b00fdd0f34b22722b07c2a72b285b4d82302 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 15 May 2018 15:29:29 -0700 Subject: [PATCH] Post merge compile fixes --- src/muz/spacer/CMakeLists.txt | 1 + src/muz/spacer/spacer_context.cpp | 6 +- src/muz/spacer/spacer_context.h | 2 +- src/muz/spacer/spacer_dl_interface.cpp | 2 +- src/muz/spacer/spacer_dl_interface.h | 4 +- src/muz/spacer/spacer_generalizers.cpp | 2 +- src/muz/spacer/spacer_iuc_proof.cpp | 51 ++++++------ src/muz/spacer/spacer_iuc_solver.cpp | 2 +- src/muz/spacer/spacer_json.h | 4 +- src/muz/spacer/spacer_proof_utils.cpp | 81 ++++---------------- src/muz/spacer/spacer_proof_utils.h | 35 +++------ src/muz/spacer/spacer_unsat_core_learner.cpp | 5 +- 12 files changed, 66 insertions(+), 129 deletions(-) diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index dad8dfa98..a7bc74b88 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(spacer spacer_iuc_solver.cpp spacer_virtual_solver.cpp spacer_legacy_mbp.cpp + spacer_proof_utils.cpp spacer_unsat_core_learner.cpp spacer_unsat_core_plugin.cpp spacer_matrix.cpp diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 60f6b9a85..5de817435 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -40,7 +40,7 @@ Notes: #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" #include "ast/ast_util.h" -#include "ast/proof_checker/proof_checker.h" +#include "ast/proofs/proof_checker.h" #include "smt/smt_value_sort.h" #include "ast/scoped_proof.h" #include "muz/spacer/spacer_qe_project.h" @@ -3618,9 +3618,9 @@ expr_ref context::get_constraints (unsigned level) return m_pm.mk_and (constraints); } -void context::add_constraint (unsigned level, const expr_ref& c) +void context::add_constraint (expr *c, unsigned level) { - if (!c.get()) { return; } + if (!c) { return; } if (m.is_true(c)) { return; } expr *e1, *e2; diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index ff0e90cfa..596e5e047 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -914,7 +914,7 @@ public: pob& get_root() const { return m_pob_queue.get_root(); } expr_ref get_constraints (unsigned lvl); - void add_constraint (unsigned lvl, const expr_ref& c); + void add_constraint (expr *c, unsigned lvl); void new_lemma_eh(pred_transformer &pt, lemma *lem); diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp index 69e5d76ff..b121cf50a 100644 --- a/src/muz/spacer/spacer_dl_interface.cpp +++ b/src/muz/spacer/spacer_dl_interface.cpp @@ -362,5 +362,5 @@ void dl_interface::add_callback(void *state, } void dl_interface::add_constraint (expr *c, unsigned lvl){ - m_context->add_constraint(c,lvl); + m_context->add_constraint(c, lvl); } diff --git a/src/muz/spacer/spacer_dl_interface.h b/src/muz/spacer/spacer_dl_interface.h index 2980e2a0f..9fc60dcf0 100644 --- a/src/muz/spacer/spacer_dl_interface.h +++ b/src/muz/spacer/spacer_dl_interface.h @@ -82,9 +82,9 @@ public: void add_callback(void *state, const datalog::t_new_lemma_eh new_lemma_eh, const datalog::t_predecessor_eh predecessor_eh, - const datalog::t_unfold_eh unfold_eh); + const datalog::t_unfold_eh unfold_eh) override; - void add_constraint (expr *c, unsigned lvl); + void add_constraint (expr *c, unsigned lvl) override; }; } diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index 4b0c3d15c..3f6e28be6 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -162,7 +162,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma) unsigned uses_level; expr_ref_vector core(m); - VERIFY(pt.is_invariant(old_level, lemma->get_expr(), uses_level, &core)); + VERIFY(pt.is_invariant(lemma->level(), lemma.get(), uses_level, &core)); CTRACE("spacer", old_sz > core.size(), tout << "unsat core reduced lemma from: " diff --git a/src/muz/spacer/spacer_iuc_proof.cpp b/src/muz/spacer/spacer_iuc_proof.cpp index 889f06af2..966b59df4 100644 --- a/src/muz/spacer/spacer_iuc_proof.cpp +++ b/src/muz/spacer/spacer_iuc_proof.cpp @@ -1,8 +1,7 @@ - - #include "muz/spacer/spacer_iuc_proof.h" #include "ast/for_each_expr.h" #include "ast/array_decl_plugin.h" +#include "ast/proofs/proof_utils.h" #include "muz/spacer/spacer_proof_utils.h" namespace spacer { @@ -18,7 +17,7 @@ namespace spacer { collect_symbols_b(b_conjuncts); compute_marks(b_conjuncts); } - + proof* iuc_proof::get() { return m_pr.get(); @@ -33,7 +32,7 @@ namespace spacer { 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()); @@ -42,7 +41,7 @@ namespace spacer { void operator()(var*) {} void operator()(quantifier*) {} }; - + void iuc_proof::collect_symbols_b(expr_set& b_conjuncts) { expr_mark visited; @@ -52,18 +51,18 @@ namespace spacer { for_each_expr(proc, visited, *it); } } - + 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())) { @@ -78,7 +77,7 @@ namespace spacer { 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 { @@ -92,26 +91,26 @@ namespace spacer { } return true; } - + /* * ==================================== * methods for computing which premises * have been used to derive the conclusions * ==================================== */ - + void iuc_proof::compute_marks(expr_set& b_conjuncts) { - ProofIteratorPostOrder it(m_pr, m); + proof_post_order it(m_pr, m); while (it.hasNext()) { proof* currentNode = it.next(); - + if (m.get_num_parents(currentNode) == 0) { switch(currentNode->get_decl_kind()) { - + case PR_ASSERTED: // currentNode is an axiom { if (b_conjuncts.contains(m.get_fact(currentNode))) @@ -142,23 +141,23 @@ namespace spacer { 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); @@ -166,7 +165,7 @@ namespace spacer { } } } - + bool iuc_proof::is_a_marked(proof* p) { return m_a_mark.is_marked(p); @@ -179,7 +178,7 @@ namespace spacer { { return m_h_mark.is_marked(p); } - + /* * ==================================== * methods for dot printing @@ -195,22 +194,22 @@ namespace spacer { * statistics * ==================================== */ - + void iuc_proof::print_farkas_stats() { unsigned farkas_counter = 0; unsigned farkas_counter2 = 0; - - ProofIteratorPostOrder it3(m_pr, m); + + proof_post_order it3(m_pr, m); while (it3.hasNext()) { proof* currentNode = it3.next(); - + // if node is theory lemma if (is_farkas_lemma(m, currentNode)) { farkas_counter++; - + // 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) @@ -229,7 +228,7 @@ namespace spacer { } } } - + verbose_stream() << "\nThis proof contains " << farkas_counter << " Farkas lemmas. " << farkas_counter2 << " Farkas lemmas participate in the lowest cut\n"; } } diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 90a28c341..e2334f1ba 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -19,7 +19,7 @@ Notes: #include"muz/spacer/spacer_iuc_solver.h" #include"ast/ast.h" #include"muz/spacer/spacer_util.h" -#include"muz/base/proof_utils.h" +#include"ast/proofs/proof_utils.h" #include"muz/spacer/spacer_farkas_learner.h" #include"ast/rewriter/expr_replacer.h" #include"muz/spacer/spacer_unsat_core_learner.h" diff --git a/src/muz/spacer/spacer_json.h b/src/muz/spacer/spacer_json.h index c75110371..b100a87dc 100644 --- a/src/muz/spacer/spacer_json.h +++ b/src/muz/spacer/spacer_json.h @@ -22,8 +22,8 @@ Notes: #include #include -#include "ref.h" -#include "ref_vector.h" +#include "util/ref.h" +#include "util/ref_vector.h" class ast; diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 735f94518..32391db91 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -16,20 +16,22 @@ Revision History: --*/ -#include "muz/spacer/spacer_proof_utils.h" -#include "ast/ast_util.h" - -#include "ast/ast_pp.h" - -#include "ast/proof_checker/proof_checker.h" #include -#include "params.h" -#include "muz/spacer/spacer_iuc_proof.h" +#include "util/params.h" +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/proofs/proof_checker.h" #include "muz/base/dl_util.h" +#include "muz/spacer/spacer_iuc_proof.h" + +#include "ast/proofs/proof_utils.h" +#include "muz/spacer/spacer_proof_utils.h" namespace spacer { - // arith lemmas: second parameter specifies exact type of lemma, could be "farkas", "triangle-eq", "eq-propagate", "assign-bounds", maybe also something else + // arith lemmas: second parameter specifies exact type of lemma, + // could be "farkas", "triangle-eq", "eq-propagate", + // "assign-bounds", maybe also something else bool is_arith_lemma(ast_manager& m, proof* pr) { if (pr->get_decl_kind() == PR_TH_LEMMA) @@ -61,57 +63,6 @@ namespace spacer { return false; } - /* - * ==================================== - * methods for proof traversal - * ==================================== - */ -ProofIteratorPostOrder::ProofIteratorPostOrder(proof* root, ast_manager& manager) : m(manager) -{m_todo.push_back(root);} - -bool ProofIteratorPostOrder::hasNext() -{return !m_todo.empty();} - -/* - * iterative post-order depth-first search (DFS) through the proof DAG - */ -proof* ProofIteratorPostOrder::next() -{ - while (!m_todo.empty()) { - proof* currentNode = m_todo.back(); - - // if we haven't already visited the current unit - if (!m_visited.is_marked(currentNode)) { - bool existsUnvisitedParent = false; - - // add unprocessed premises to stack for DFS. If there is at least one unprocessed premise, don't compute the result - // for currentProof now, but wait until those unprocessed premises are processed. - 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)); - - // if we haven't visited the current premise yet - if (!m_visited.is_marked(premise)) { - // add it to the stack - m_todo.push_back(premise); - existsUnvisitedParent = true; - } - } - - // if we already visited all parent-inferences, we can visit the inference too - if (!existsUnvisitedParent) { - m_visited.mark(currentNode, true); - m_todo.pop_back(); - return currentNode; - } - } else { - m_todo.pop_back(); - } - } - // we have already iterated through all inferences - return NULL; -} - /* * ==================================== * methods for dot printing @@ -140,7 +91,7 @@ proof* ProofIteratorPostOrder::next() std::unordered_map id_to_small_id; unsigned counter = 0; - ProofIteratorPostOrder it2(pr, m); + proof_post_order it2(pr, m); while (it2.hasNext()) { proof* currentNode = it2.next(); @@ -306,7 +257,7 @@ proof* ProofIteratorPostOrder::next() proof_ref theory_axiom_reducer::reduce(proof* pr) { - ProofIteratorPostOrder pit(pr, m); + proof_post_order pit(pr, m); while (pit.hasNext()) { proof* p = pit.next(); @@ -468,11 +419,11 @@ proof* ProofIteratorPostOrder::next() for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) { proof* pp = m.get_parent(p, i); - datalog::set_union(*parent_hyps, *m_parent_hyps.find(pp)); + set_union(*parent_hyps, *m_parent_hyps.find(pp)); if (!m.is_lemma(p)) // lemmas clear all hypotheses { - datalog::set_union(*active_hyps, *m_active_hyps.find(pp)); + set_union(*active_hyps, *m_active_hyps.find(pp)); } } } @@ -488,7 +439,7 @@ proof* ProofIteratorPostOrder::next() expr_set* all_hyps = m_parent_hyps.find(pr); SASSERT(all_hyps != nullptr); - ProofIteratorPostOrder pit(pr, m); + proof_post_order pit(pr, m); while (pit.hasNext()) { proof* p = pit.next(); if (!m.is_hypothesis(p)) diff --git a/src/muz/spacer/spacer_proof_utils.h b/src/muz/spacer/spacer_proof_utils.h index abd612b57..e47c9882a 100644 --- a/src/muz/spacer/spacer_proof_utils.h +++ b/src/muz/spacer/spacer_proof_utils.h @@ -21,24 +21,9 @@ Revision History: #include "ast/ast.h" namespace spacer { - + bool is_arith_lemma(ast_manager& m, proof* pr); bool is_farkas_lemma(ast_manager& m, proof* pr); -/* - * iterator, which traverses the proof in depth-first post-order. - */ -class ProofIteratorPostOrder { -public: - ProofIteratorPostOrder(proof* refutation, ast_manager& manager); - bool hasNext(); - proof* next(); - -private: - ptr_vector m_todo; - ast_mark m_visited; // the proof nodes we have already visited - - ast_manager& m; -}; /* * prints the proof pr in dot representation to the file proof.dot @@ -46,7 +31,7 @@ private: */ class iuc_proof; void pp_proof_dot(ast_manager& m, proof* pr, iuc_proof* iuc_pr = nullptr); - + class theory_axiom_reducer { public: @@ -54,16 +39,16 @@ private: // reduce theory axioms and return transformed proof proof_ref reduce(proof* pr); - + private: ast_manager &m; - + // tracking all created expressions expr_ref_vector m_pinned; - + // maps each proof of a clause to the transformed subproof of that clause obj_map m_cache; - + void reset(); }; @@ -71,7 +56,7 @@ private: { public: hypothesis_reducer(ast_manager &m) : m(m), m_pinned(m) {} - + // reduce hypothesis and return transformed proof proof_ref reduce(proof* pf); @@ -80,7 +65,7 @@ private: typedef obj_hashtable proof_set; ast_manager &m; - + expr_ref_vector m_pinned; // tracking all created expressions ptr_vector m_pinned_active_hyps; // tracking all created sets of active hypothesis ptr_vector m_pinned_parent_hyps; // tracking all created sets of parent hypothesis @@ -89,12 +74,12 @@ private: obj_map m_units; // maps each unit literal to the subproof of that unit obj_map m_active_hyps; // maps each proof of a clause to the set of proofs of active hypothesis' of the clause obj_map m_parent_hyps; // maps each proof of a clause to the hypothesis-fact, which are transitive parents of that clause, needed to avoid creating cycles in the proof. - + void reset(); void compute_hypsets(proof* pr); // compute active_hyps and parent_hyps for pr void collect_units(proof* pr); // compute m_units proof* compute_transformed_proof(proof* pf); - + proof* mk_lemma_core(proof *pf, expr *fact); proof* mk_unit_resolution_core(ptr_buffer& args); proof* mk_step_core(proof* old_step, ptr_buffer& args); diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index cb7ebff76..bb50cc5c7 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -22,6 +22,7 @@ Revision History: #include "muz/spacer/spacer_iuc_proof.h" #include "ast/for_each_expr.h" +#include "ast/proofs/proof_utils.h" #include "muz/spacer/spacer_util.h" @@ -54,7 +55,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) { SASSERT(m.is_proof(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)); } @@ -109,7 +110,7 @@ void unsat_core_learner::set_closed(proof* p, bool value) { m_closed.mark(p, value); } - + bool unsat_core_learner::is_b_open(proof *p) { return m_pr.is_b_marked(p) && !is_closed (p);