From d67f3c14668b8f6f679f361575ad6cd3461dfa6f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Oct 2017 03:08:56 -0700 Subject: [PATCH] create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 4 +- src/CMakeLists.txt | 2 +- .../{proof_checker => proofs}/CMakeLists.txt | 5 ++- .../proof_checker.cpp | 3 +- .../{proof_checker => proofs}/proof_checker.h | 0 .../proofs/proof_utils.cpp} | 37 ++++++++++--------- .../proofs/proof_utils.h} | 21 +++++------ src/muz/pdr/pdr_context.cpp | 2 +- src/muz/spacer/CMakeLists.txt | 1 - src/muz/spacer/spacer_context.cpp | 2 +- src/muz/spacer/spacer_legacy_frames.cpp | 2 +- src/muz/spacer/spacer_unsat_core_learner.cpp | 6 +-- src/muz/spacer/spacer_unsat_core_learner.h | 2 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 2 +- src/muz/spacer/spacer_virtual_solver.cpp | 2 +- src/smt/CMakeLists.txt | 2 +- src/smt/asserted_formulas.cpp | 10 ++--- src/smt/smt_context.cpp | 2 +- src/test/proof_checker.cpp | 2 +- 19 files changed, 53 insertions(+), 54 deletions(-) rename src/ast/{proof_checker => proofs}/CMakeLists.txt (60%) rename src/ast/{proof_checker => proofs}/proof_checker.cpp (99%) rename src/ast/{proof_checker => proofs}/proof_checker.h (100%) rename src/{muz/spacer/spacer_proof_utils.cpp => ast/proofs/proof_utils.cpp} (93%) rename src/{muz/spacer/spacer_proof_utils.h => ast/proofs/proof_utils.h} (58%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 923b948a6..ddf439e10 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -43,14 +43,14 @@ def init_project_def(): add_lib('cmd_context', ['solver', 'rewriter', 'interp']) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') - add_lib('proof_checker', ['rewriter'], 'ast/proof_checker') + add_lib('proofs', ['rewriter'], 'ast/proofs') add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa') add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern') add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster') add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params') add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', - 'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa', 'lp']) + 'substitution', 'grobner', 'euclid', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp']) add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 277335ce9..cfe6e5265 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -67,7 +67,7 @@ add_subdirectory(interp) add_subdirectory(cmd_context) add_subdirectory(cmd_context/extra_cmds) add_subdirectory(parsers/smt2) -add_subdirectory(ast/proof_checker) +add_subdirectory(ast/proofs) add_subdirectory(ast/fpa) add_subdirectory(ast/macros) add_subdirectory(ast/pattern) diff --git a/src/ast/proof_checker/CMakeLists.txt b/src/ast/proofs/CMakeLists.txt similarity index 60% rename from src/ast/proof_checker/CMakeLists.txt rename to src/ast/proofs/CMakeLists.txt index 5c947adec..6eedb0fac 100644 --- a/src/ast/proof_checker/CMakeLists.txt +++ b/src/ast/proofs/CMakeLists.txt @@ -1,6 +1,7 @@ -z3_add_component(proof_checker +z3_add_component(proofs SOURCES proof_checker.cpp + proof_utils.cpp COMPONENT_DEPENDENCIES rewriter -) +) \ No newline at end of file diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp similarity index 99% rename from src/ast/proof_checker/proof_checker.cpp rename to src/ast/proofs/proof_checker.cpp index afe2baeed..3f9438229 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -4,10 +4,9 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#include "ast/proof_checker/proof_checker.h" +#include "ast/proofs/proof_checker.h" #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" -// include "spc_decl_plugin.h" #include "ast/ast_smt_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" diff --git a/src/ast/proof_checker/proof_checker.h b/src/ast/proofs/proof_checker.h similarity index 100% rename from src/ast/proof_checker/proof_checker.h rename to src/ast/proofs/proof_checker.h diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/ast/proofs/proof_utils.cpp similarity index 93% rename from src/muz/spacer/spacer_proof_utils.cpp rename to src/ast/proofs/proof_utils.cpp index 6edb29881..bd82696ea 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/ast/proofs/proof_utils.cpp @@ -3,7 +3,7 @@ Copyright (c) 2017 Arie Gurfinkel Module Name: - spacer_proof_utils.cpp + proof_utils.cpp Abstract: Utilities to traverse and manipulate proofs @@ -16,24 +16,23 @@ Revision History: --*/ -#include "muz/spacer/spacer_proof_utils.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" +#include "ast/proofs/proof_utils.h" +#include "ast/proofs/proof_checker.h" -#include "ast/proof_checker/proof_checker.h" -namespace spacer { -ProofIteratorPostOrder::ProofIteratorPostOrder(proof* root, ast_manager& manager) : m(manager) +proof_post_order::proof_post_order(proof* root, ast_manager& manager) : m(manager) {m_todo.push_back(root);} -bool ProofIteratorPostOrder::hasNext() +bool proof_post_order::hasNext() {return !m_todo.empty();} /* * iterative post-order depth-first search (DFS) through the proof DAG */ -proof* ProofIteratorPostOrder::next() +proof* proof_post_order::next() { while (!m_todo.empty()) { proof* currentNode = m_todo.back(); @@ -42,7 +41,8 @@ proof* ProofIteratorPostOrder::next() 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 + // 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))); @@ -67,7 +67,7 @@ proof* ProofIteratorPostOrder::next() } } // we have already iterated through all inferences - return NULL; + return nullptr; } @@ -117,20 +117,21 @@ class reduce_hypotheses { return hyp_mark; } - void compute_marks(proof* pr) - { + void compute_marks(proof* pr) { proof *p; - ProofIteratorPostOrder pit(pr, m); + proof_post_order pit(pr, m); while (pit.hasNext()) { p = pit.next(); if (m.is_hypothesis(p)) { m_hypmark.mark(p, true); m_hyps.insert(m.get_fact(p)); - } else { + } + else { bool hyp_mark = compute_mark1(p); // collect units that are hyp-free and are used as hypotheses somewhere - if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p))) - { m_units.insert(m.get_fact(p), p); } + if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p))) { + m_units.insert(m.get_fact(p), p); + } } } } @@ -220,6 +221,7 @@ class reduce_hypotheses { return m_units.contains(e); } + proof *mk_lemma_core(proof *pf, expr *fact) { ptr_buffer args; @@ -319,8 +321,8 @@ public: reset(); } }; -void reduce_hypotheses(proof_ref &pr) -{ + +void reduce_hypotheses(proof_ref &pr) { ast_manager &m = pr.get_manager(); class reduce_hypotheses hypred(m); hypred(pr); @@ -329,4 +331,3 @@ void reduce_hypotheses(proof_ref &pr) SASSERT(pc.check(pr, side)); ); } -} diff --git a/src/muz/spacer/spacer_proof_utils.h b/src/ast/proofs/proof_utils.h similarity index 58% rename from src/muz/spacer/spacer_proof_utils.h rename to src/ast/proofs/proof_utils.h index f2897f7ec..7963d52de 100644 --- a/src/muz/spacer/spacer_proof_utils.h +++ b/src/ast/proofs/proof_utils.h @@ -3,7 +3,7 @@ Copyright (c) 2017 Arie Gurfinkel Module Name: - spacer_proof_utils.cpp + proof_utils.h Abstract: Utilities to traverse and manipulate proofs @@ -16,28 +16,27 @@ Revision History: --*/ -#ifndef _SPACER_PROOF_UTILS_H_ -#define _SPACER_PROOF_UTILS_H_ +#ifndef _PROOF_UTILS_H_ +#define _PROOF_UTILS_H_ #include "ast/ast.h" -namespace spacer { /* * iterator, which traverses the proof in depth-first post-order. */ -class ProofIteratorPostOrder { + +class proof_post_order { public: - ProofIteratorPostOrder(proof* refutation, ast_manager& manager); + proof_post_order(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; + ast_mark m_visited; // the proof nodes we have already visited + ast_manager& m; }; - void reduce_hypotheses(proof_ref &pr); -} + + #endif diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index e6d91c87e..a1878dc7a 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -41,7 +41,7 @@ Notes: #include "ast/ast_smt2_pp.h" #include "qe/qe_lite.h" #include "ast/ast_ll_pp.h" -#include "ast/proof_checker/proof_checker.h" +#include "ast/proofs/proof_checker.h" #include "smt/smt_value_sort.h" #include "muz/base/proof_utils.h" #include "muz/base/dl_boogie_proof.h" diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index bc2f45b43..94e429171 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -15,7 +15,6 @@ z3_add_component(spacer spacer_itp_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 7ab78d453..b057730d8 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" diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index 9c302e5fd..dd2a16abd 100644 --- a/src/muz/spacer/spacer_legacy_frames.cpp +++ b/src/muz/spacer/spacer_legacy_frames.cpp @@ -23,7 +23,7 @@ #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 "muz/base/proof_utils.h" #include "ast/scoped_proof.h" diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index 222ca146c..d478b1e8f 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -41,7 +41,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e // transform proof in order to get a proof which is better suited for unsat-core-extraction proof_ref pr(root, m); - spacer::reduce_hypotheses(pr); + reduce_hypotheses(pr); STRACE("spacer.unsat_core_learner", verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n"; ); @@ -50,7 +50,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e collect_symbols_b(asserted_b); // traverse proof - ProofIteratorPostOrder it(root, m); + proof_post_order it(root, m); while (it.hasNext()) { proof* currentNode = it.next(); @@ -138,7 +138,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e std::unordered_map id_to_small_id; unsigned counter = 0; - ProofIteratorPostOrder it2(root, m); + proof_post_order it2(root, m); while (it2.hasNext()) { proof* currentNode = it2.next(); diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h index 6ee7c3b37..a7c9f6aa7 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.h +++ b/src/muz/spacer/spacer_unsat_core_learner.h @@ -20,7 +20,7 @@ Revision History: #include "ast/ast.h" #include "muz/spacer/spacer_util.h" -#include "muz/spacer/spacer_proof_utils.h" +#include "ast/proofs/proof_utils.h" namespace spacer { diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 0d90d2653..3f1e53778 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -20,13 +20,13 @@ Revision History: #include "ast/rewriter/bool_rewriter.h" #include "ast/arith_decl_plugin.h" +#include "ast/proofs/proof_utils.h" #include "solver/solver.h" #include "smt/smt_farkas_util.h" #include "smt/smt_solver.h" -#include "muz/spacer/spacer_proof_utils.h" #include "muz/spacer/spacer_matrix.h" #include "muz/spacer/spacer_unsat_core_plugin.h" #include "muz/spacer/spacer_unsat_core_learner.h" diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp index ebaef14f0..244a97d22 100644 --- a/src/muz/spacer/spacer_virtual_solver.cpp +++ b/src/muz/spacer/spacer_virtual_solver.cpp @@ -23,7 +23,7 @@ Notes: #include "muz/spacer/spacer_util.h" #include "ast/rewriter/bool_rewriter.h" -#include "ast/proof_checker/proof_checker.h" +#include "ast/proofs/proof_checker.h" #include "ast/scoped_proof.h" diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 41890dd05..e102bd28b 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -75,7 +75,7 @@ z3_add_component(smt normal_forms parser_util pattern - proof_checker + proofs proto_model simplex substitution diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 9f68f2412..dd92f250a 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -163,7 +163,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } void asserted_formulas::assert_expr(expr * e) { - assert_expr(e, m.mk_asserted(e)); + assert_expr(e, m.proofs_enabled() ? m.mk_asserted(e) : nullptr); } void asserted_formulas::get_assertions(ptr_vector & result) const { @@ -365,7 +365,7 @@ void asserted_formulas::nnf_cnf() { CASSERT("well_sorted", is_well_sorted(m, n)); apply_nnf(n, push_todo, push_todo_prs, r1, pr1); CASSERT("well_sorted",is_well_sorted(m, r1)); - pr = m.mk_modus_ponens(pr, pr1); + pr = m.proofs_enabled() ? m.mk_modus_ponens(pr, pr1) : nullptr; push_todo.push_back(r1); push_todo_prs.push_back(pr); @@ -506,16 +506,16 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { } if (is_gt(rhs, lhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";); - m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr)); + m_scoped_substitution.insert(rhs, lhs, m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr); return; } TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } if (m.is_not(n, n1)) { - m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr)); + m_scoped_substitution.insert(n1, m.mk_false(), m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr); } else { - m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr)); + m_scoped_substitution.insert(n, m.mk_true(), m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr); } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 48d02da26..c508a65cb 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -23,7 +23,7 @@ Revision History: #include "ast/ast_ll_pp.h" #include "util/warning.h" #include "smt/smt_quick_checker.h" -#include "ast/proof_checker/proof_checker.h" +#include "ast/proofs/proof_checker.h" #include "ast/ast_util.h" #include "smt/uses_theory.h" #include "model/model.h" diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index 33a908f24..7a9b619cd 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -4,7 +4,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#include "ast/proof_checker/proof_checker.h" +#include "ast/proofs/proof_checker.h" #include "ast/ast_ll_pp.h" void tst_checker1() {