From 9e61820125fc16e6d596f379ad5cc8195adcd496 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Aug 2013 21:49:53 -0700 Subject: [PATCH] re-organizing muz Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 1 + src/muz/dl_context.cpp | 3 +- src/muz/dl_rule.cpp | 1 + src/muz/dl_util.cpp | 3 +- src/muz/dl_util.h | 30 ---------- src/muz/equiv_proof_converter.cpp | 4 +- src/muz/{ => fp}/datalog_parser.cpp | 0 src/muz/{ => fp}/datalog_parser.h | 0 src/muz/pdr/pdr_context.cpp | 5 +- src/muz/pdr/pdr_dl_interface.cpp | 5 +- src/muz/pdr/pdr_util.cpp | 5 +- src/muz/scoped_proof.h | 55 +++++++++++++++++++ src/muz/tab/tab_context.cpp | 1 + src/{muz => qe}/vsubst_tactic.cpp | 0 src/{muz => qe}/vsubst_tactic.h | 0 .../tactic}/unit_subsumption_tactic.cpp | 0 .../tactic}/unit_subsumption_tactic.h | 0 .../arith}/arith_bounds_tactic.cpp | 0 .../arith}/arith_bounds_tactic.h | 0 20 files changed, 73 insertions(+), 42 deletions(-) rename src/muz/{ => fp}/datalog_parser.cpp (100%) rename src/muz/{ => fp}/datalog_parser.h (100%) create mode 100644 src/muz/scoped_proof.h rename src/{muz => qe}/vsubst_tactic.cpp (100%) rename src/{muz => qe}/vsubst_tactic.h (100%) rename src/{muz => smt/tactic}/unit_subsumption_tactic.cpp (100%) rename src/{muz => smt/tactic}/unit_subsumption_tactic.h (100%) rename src/{muz => tactic/arith}/arith_bounds_tactic.cpp (100%) rename src/{muz => tactic/arith}/arith_bounds_tactic.h (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index a2b4ef9b2..248d45382 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -57,7 +57,7 @@ def init_project_def(): add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe']) add_lib('transforms', ['muz'], 'muz/transforms') add_lib('rel', ['muz', 'transforms'], 'muz/rel') - add_lib('pdr', ['muz', 'transforms'], 'muz/pdr') + add_lib('pdr', ['muz', 'transforms', 'arith_tactics', 'smt_tactic'], 'muz/pdr') add_lib('clp', ['muz', 'transforms'], 'muz/clp') add_lib('tab', ['muz', 'transforms'], 'muz/tab') add_lib('bmc', ['muz', 'transforms'], 'muz/bmc') diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 72e40590e..60d285a55 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -31,6 +31,7 @@ Revision History: #include "rewriter_def.h" #include "dl_transforms.h" #include "dl_mk_rule_inliner.h" +#include "scoped_proof.h" namespace datalog { diff --git a/src/muz/dl_context.cpp b/src/muz/dl_context.cpp index 5e707e315..11cb48490 100644 --- a/src/muz/dl_context.cpp +++ b/src/muz/dl_context.cpp @@ -19,8 +19,6 @@ Revision History: #include #include -#include"arith_simplifier_plugin.h" -#include"basic_simplifier_plugin.h" #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"dl_context.h" @@ -28,6 +26,7 @@ Revision History: #include"ast_smt_pp.h" #include"ast_smt2_pp.h" #include"datatype_decl_plugin.h" +#include"scoped_proof.h" namespace datalog { diff --git a/src/muz/dl_rule.cpp b/src/muz/dl_rule.cpp index 5ac580cb8..96e2b163a 100644 --- a/src/muz/dl_rule.cpp +++ b/src/muz/dl_rule.cpp @@ -42,6 +42,7 @@ Revision History: #include"bool_rewriter.h" #include"expr_safe_replace.h" #include"filter_model_converter.h" +#include"scoped_proof.h" namespace datalog { diff --git a/src/muz/dl_util.cpp b/src/muz/dl_util.cpp index e32999ddc..2f9eb519c 100644 --- a/src/muz/dl_util.cpp +++ b/src/muz/dl_util.cpp @@ -25,9 +25,10 @@ Revision History: #endif #include"ast_pp.h" #include"bool_rewriter.h" +#include"for_each_expr.h" +#include"scoped_proof.h" #include"dl_context.h" #include"dl_rule.h" -#include"for_each_expr.h" #include"dl_util.h" namespace datalog { diff --git a/src/muz/dl_util.h b/src/muz/dl_util.h index d805e683b..a6bd7f7f8 100644 --- a/src/muz/dl_util.h +++ b/src/muz/dl_util.h @@ -124,36 +124,6 @@ namespace datalog { */ void display_fact(context & ctx, app * f, std::ostream & out); - class scoped_proof_mode { - ast_manager& m; - proof_gen_mode m_mode; - public: - scoped_proof_mode(ast_manager& m, proof_gen_mode mode): m(m) { - m_mode = m.proof_mode(); - m.toggle_proof_mode(mode); - } - ~scoped_proof_mode() { - m.toggle_proof_mode(m_mode); - } - - }; - - class scoped_proof : public scoped_proof_mode { - public: - scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {} - }; - - class scoped_no_proof : public scoped_proof_mode { - public: - scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} - }; - - class scoped_restore_proof : public scoped_proof_mode { - public: - scoped_restore_proof(ast_manager& m): scoped_proof_mode(m, m.proof_mode()) {} - }; - - class variable_intersection diff --git a/src/muz/equiv_proof_converter.cpp b/src/muz/equiv_proof_converter.cpp index 98ea88044..13b759f7e 100644 --- a/src/muz/equiv_proof_converter.cpp +++ b/src/muz/equiv_proof_converter.cpp @@ -19,11 +19,11 @@ Revision History: #include "equiv_proof_converter.h" #include "ast_pp.h" -#include "dl_util.h" +#include "scoped_proof.h" void equiv_proof_converter::insert(expr* fml1, expr* fml2) { if (fml1 != fml2) { - datalog::scoped_proof _sp(m); + scoped_proof _sp(m); proof_ref p1(m), p2(m), p3(m); p1 = m.mk_asserted(fml1); p2 = m.mk_rewrite(fml1, fml2); diff --git a/src/muz/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp similarity index 100% rename from src/muz/datalog_parser.cpp rename to src/muz/fp/datalog_parser.cpp diff --git a/src/muz/datalog_parser.h b/src/muz/fp/datalog_parser.h similarity index 100% rename from src/muz/datalog_parser.h rename to src/muz/fp/datalog_parser.h diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index db85bc5a9..f3e253071 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -46,6 +46,7 @@ Notes: #include "proof_utils.h" #include "dl_boogie_proof.h" #include "qe_util.h" +#include "scoped_proof.h" namespace pdr { @@ -1719,7 +1720,7 @@ namespace pdr { } proof_ref context::get_proof() const { - datalog::scoped_proof _sc(m); + scoped_proof _sc(m); proof_ref proof(m); SASSERT(m_last_result == l_true); proof = m_search.get_proof_trace(*this); @@ -1959,7 +1960,7 @@ namespace pdr { void context::create_children(model_node& n) { SASSERT(n.level() > 0); bool use_model_generalizer = m_params.use_model_generalizer(); - datalog::scoped_no_proof _sc(m); + scoped_no_proof _sc(m); pred_transformer& pt = n.pt(); model_ref M = n.get_model_ptr(); diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp index ccd22d57f..45872fe99 100644 --- a/src/muz/pdr/pdr_dl_interface.cpp +++ b/src/muz/pdr/pdr_dl_interface.cpp @@ -31,8 +31,9 @@ Revision History: #include "dl_mk_slice.h" #include "dl_mk_unfold.h" #include "dl_mk_coalesce.h" -#include "model_smt2_pp.h" #include "dl_transforms.h" +#include "scoped_proof.h" +#include "model_smt2_pp.h" using namespace pdr; @@ -149,7 +150,7 @@ lbool dl_interface::query(expr * query) { m_ctx.reopen(); m_ctx.replace_rules(old_rules); - datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. + scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. m_context->set_proof_converter(m_ctx.get_proof_converter()); m_context->set_model_converter(m_ctx.get_model_converter()); diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index d23dc186e..4db835bed 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -45,6 +45,7 @@ Notes: #include "poly_rewriter.h" #include "poly_rewriter_def.h" #include "arith_rewriter.h" +#include "scoped_proof.h" @@ -1072,7 +1073,7 @@ namespace pdr { void hoist_non_bool_if(expr_ref& fml) { ast_manager& m = fml.get_manager(); - datalog::scoped_no_proof _sp(m); + scoped_no_proof _sp(m); params_ref p; ite_hoister_star ite_rw(m, p); expr_ref tmp(m); @@ -1419,7 +1420,7 @@ namespace pdr { void normalize_arithmetic(expr_ref& t) { ast_manager& m = t.get_manager(); - datalog::scoped_no_proof _sp(m); + scoped_no_proof _sp(m); params_ref p; arith_normalizer_star rw(m, p); expr_ref tmp(m); diff --git a/src/muz/scoped_proof.h b/src/muz/scoped_proof.h new file mode 100644 index 000000000..e37290c03 --- /dev/null +++ b/src/muz/scoped_proof.h @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + scoped_proof.h + +Abstract: + + Scoped proof environments. Toggles enabling proofs. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-08-28 + +Revision History: + +--*/ +#ifndef _SCOPED_PROOF__H_ +#define _SCOPED_PROOF_H_ + +#include "ast.h" + +class scoped_proof_mode { + ast_manager& m; + proof_gen_mode m_mode; +public: + scoped_proof_mode(ast_manager& m, proof_gen_mode mode): m(m) { + m_mode = m.proof_mode(); + m.toggle_proof_mode(mode); + } + ~scoped_proof_mode() { + m.toggle_proof_mode(m_mode); + } + +}; + +class scoped_proof : public scoped_proof_mode { +public: + scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {} +}; + +class scoped_no_proof : public scoped_proof_mode { +public: + scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} +}; + +class scoped_restore_proof : public scoped_proof_mode { +public: + scoped_restore_proof(ast_manager& m): scoped_proof_mode(m, m.proof_mode()) {} +}; + + + +#endif diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index a56d16a0e..2201be73e 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -29,6 +29,7 @@ Revision History: #include "datatype_decl_plugin.h" #include "for_each_expr.h" #include "matcher.h" +#include "scoped_proof.h" namespace tb { diff --git a/src/muz/vsubst_tactic.cpp b/src/qe/vsubst_tactic.cpp similarity index 100% rename from src/muz/vsubst_tactic.cpp rename to src/qe/vsubst_tactic.cpp diff --git a/src/muz/vsubst_tactic.h b/src/qe/vsubst_tactic.h similarity index 100% rename from src/muz/vsubst_tactic.h rename to src/qe/vsubst_tactic.h diff --git a/src/muz/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp similarity index 100% rename from src/muz/unit_subsumption_tactic.cpp rename to src/smt/tactic/unit_subsumption_tactic.cpp diff --git a/src/muz/unit_subsumption_tactic.h b/src/smt/tactic/unit_subsumption_tactic.h similarity index 100% rename from src/muz/unit_subsumption_tactic.h rename to src/smt/tactic/unit_subsumption_tactic.h diff --git a/src/muz/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp similarity index 100% rename from src/muz/arith_bounds_tactic.cpp rename to src/tactic/arith/arith_bounds_tactic.cpp diff --git a/src/muz/arith_bounds_tactic.h b/src/tactic/arith/arith_bounds_tactic.h similarity index 100% rename from src/muz/arith_bounds_tactic.h rename to src/tactic/arith/arith_bounds_tactic.h