From 7dd28781ab5f26703e8bb79ceee79e4c44bdc339 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Aug 2017 16:33:36 -0700 Subject: [PATCH] remove simplifier dependencies from cmakelist.txt files Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/CMakeLists.txt | 2 +- src/ast/macros/CMakeLists.txt | 2 +- src/ast/pattern/CMakeLists.txt | 2 +- src/ast/pattern/pattern_inference.cpp | 19 ++++++++++++------- src/ast/pattern/pattern_inference.h | 2 ++ src/ast/rewriter/bit_blaster/CMakeLists.txt | 1 - src/model/model_core.cpp | 16 ++++++---------- .../dl_mk_quantifier_instantiation.cpp | 2 +- src/smt/proto_model/CMakeLists.txt | 2 +- 9 files changed, 25 insertions(+), 23 deletions(-) diff --git a/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt index 4a9506d16..2a6d0763c 100644 --- a/src/ast/fpa/CMakeLists.txt +++ b/src/ast/fpa/CMakeLists.txt @@ -5,7 +5,7 @@ z3_add_component(fpa fpa2bv_rewriter.cpp COMPONENT_DEPENDENCIES ast - simplifier + rewriter model util PYG_FILES diff --git a/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt index ca38b4759..ec6d7e26c 100644 --- a/src/ast/macros/CMakeLists.txt +++ b/src/ast/macros/CMakeLists.txt @@ -5,5 +5,5 @@ z3_add_component(macros macro_util.cpp quasi_macros.cpp COMPONENT_DEPENDENCIES - simplifier + rewriter ) diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt index 6e8301afc..5531bb29b 100644 --- a/src/ast/pattern/CMakeLists.txt +++ b/src/ast/pattern/CMakeLists.txt @@ -29,7 +29,7 @@ z3_add_component(pattern ${CMAKE_CURRENT_BINARY_DIR}/database.h COMPONENT_DEPENDENCIES normal_forms - simplifier + rewriter smt2parser PYG_FILES pattern_inference_params_helper.pyg diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 94a90d829..dfeb29ffe 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -89,6 +89,15 @@ bool smaller_pattern::operator()(unsigned num_bindings, expr * p1, expr * p2) { return process(p1, p2); } + +#ifdef _TRACE +static void dump_app_vector(std::ostream & out, ptr_vector const & v, ast_manager & m) { + for (app * e : v) + out << mk_pp(e, m) << "\n"; +} +#endif + +#if 0 pattern_inference_old::pattern_inference_old(ast_manager & m, pattern_inference_params & params): simplifier(m), m_params(params), @@ -470,12 +479,6 @@ void pattern_inference_old::reset_pre_patterns() { m_pre_patterns.reset(); } -#ifdef _TRACE -static void dump_app_vector(std::ostream & out, ptr_vector const & v, ast_manager & m) { - for (app * e : v) - out << mk_pp(e, m) << "\n"; -} -#endif bool pattern_inference_old::is_forbidden(app * n) const { func_decl const * decl = n->get_decl(); @@ -567,7 +570,6 @@ void pattern_inference_old::mk_patterns(unsigned num_bindings, m_candidates.reset(); } -#include "ast/pattern/database.h" void pattern_inference_old::reduce1_quantifier(quantifier * q) { TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";); @@ -729,6 +731,9 @@ void pattern_inference_old::reduce1_quantifier(quantifier * q) { cache_result(q, new_q, pr); } +#endif + +#include "ast/pattern/database.h" pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_params & params): diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index 7b0ec9cfe..281c3ff8b 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -61,6 +61,7 @@ public: bool operator()(unsigned num_bindings, expr * p1, expr * p2); }; +#if 0 class pattern_inference_old : public simplifier { pattern_inference_params & m_params; family_id m_bfid; @@ -244,6 +245,7 @@ public: bool is_forbidden(app * n) const; }; +#endif class pattern_inference_cfg : public default_rewriter_cfg { ast_manager& m; diff --git a/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt index 9eea1558e..c8985a051 100644 --- a/src/ast/rewriter/bit_blaster/CMakeLists.txt +++ b/src/ast/rewriter/bit_blaster/CMakeLists.txt @@ -4,5 +4,4 @@ z3_add_component(bit_blaster bit_blaster_rewriter.cpp COMPONENT_DEPENDENCIES rewriter - simplifier ) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 5eb1eb00d..2fd2d8746 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -19,18 +19,14 @@ Revision History: #include "model/model_core.h" model_core::~model_core() { - decl2expr::iterator it1 = m_interp.begin(); - decl2expr::iterator end1 = m_interp.end(); - for (; it1 != end1; ++it1) { - m_manager.dec_ref(it1->m_key); - m_manager.dec_ref(it1->m_value); + for (auto & kv : m_interp) { + m_manager.dec_ref(kv.m_key); + m_manager.dec_ref(kv.m_value); } - decl2finterp::iterator it2 = m_finterp.begin(); - decl2finterp::iterator end2 = m_finterp.end(); - for (; it2 != end2; ++it2) { - m_manager.dec_ref(it2->m_key); - dealloc(it2->m_value); + for (auto & kv : m_finterp) { + m_manager.dec_ref(kv.m_key); + dealloc(kv.m_value); } } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index cfb998a32..f32840c49 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -70,7 +70,7 @@ namespace datalog { if (q->get_num_patterns() == 0) { proof_ref new_pr(m); pattern_inference_params params; - pattern_inference_old infer(m, params); + pattern_inference_rw infer(m, params); infer(q, qe, new_pr); q = to_quantifier(qe); } diff --git a/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt index 0539c0fb0..c5f6c4b18 100644 --- a/src/smt/proto_model/CMakeLists.txt +++ b/src/smt/proto_model/CMakeLists.txt @@ -8,6 +8,6 @@ z3_add_component(proto_model value_factory.cpp COMPONENT_DEPENDENCIES model - simplifier + rewriter smt_params )