From 683687b153f88a07fed8fa0f66c4c93ec67a18b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Oct 2012 10:54:59 -0700 Subject: [PATCH] more cleanup Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 3 +- src/ast/ast_dag_pp.cpp | 353 --------------------- src/ast/ast_dag_pp.h | 31 -- src/ast/expr2dot.cpp | 84 ----- src/ast/expr2dot.h | 27 -- src/{util => math/interval}/interval.h | 0 src/{util => math/interval}/interval_def.h | 0 src/{util => muz_qe}/imdd.cpp | 0 src/{util => muz_qe}/imdd.h | 0 src/{util => muz_qe}/interval_skip_list.h | 0 src/{util => muz_qe}/skip_list_base.h | 0 src/{util => smt}/diff_logic.h | 0 src/{util => smt}/old_interval.cpp | 0 src/{util => smt}/old_interval.h | 0 src/tactic/sls/sls_tactic.cpp | 12 - 15 files changed, 2 insertions(+), 508 deletions(-) delete mode 100644 src/ast/ast_dag_pp.cpp delete mode 100644 src/ast/ast_dag_pp.h delete mode 100644 src/ast/expr2dot.cpp delete mode 100644 src/ast/expr2dot.h rename src/{util => math/interval}/interval.h (100%) rename src/{util => math/interval}/interval_def.h (100%) rename src/{util => muz_qe}/imdd.cpp (100%) rename src/{util => muz_qe}/imdd.h (100%) rename src/{util => muz_qe}/interval_skip_list.h (100%) rename src/{util => muz_qe}/skip_list_base.h (100%) rename src/{util => smt}/diff_logic.h (100%) rename src/{util => smt}/old_interval.cpp (100%) rename src/{util => smt}/old_interval.h (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 3c7d6e70a..d6c97c8ac 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -14,7 +14,8 @@ def init_project_def(): add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) add_lib('nlsat', ['polynomial', 'sat']) - add_lib('subpaving', ['util'], 'math/subpaving') + add_lib('interval', ['util'], 'math/interval') + add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter') add_lib('model', ['rewriter']) diff --git a/src/ast/ast_dag_pp.cpp b/src/ast/ast_dag_pp.cpp deleted file mode 100644 index 893ef09b6..000000000 --- a/src/ast/ast_dag_pp.cpp +++ /dev/null @@ -1,353 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - ast_dag_pp.cpp - -Abstract: - - AST low level pretty printer. - -Author: - - Leonardo de Moura (leonardo) 2006-10-19. - Nikolaj Bjorner (nbjorner) 2007-07-17 - -Revision History: - ---*/ - -#include -#include"for_each_ast.h" -#include"arith_decl_plugin.h" -#include"bv_decl_plugin.h" -#include"ast_pp.h" - -class dag_printer { - ast_manager& m_manager; - std::ostream & m_out; - ast_mark& m_mark; - bool m_initialized; - svector m_names; - family_id m_basic_fid; - family_id m_bv_fid; - family_id m_arith_fid; - family_id m_array_fid; - arith_util m_arith; - bv_util m_bv; - bool m_enable_shortcut; - - void process_ast(ast* a) { - for_each_ast(*this, m_mark, a); - } - - void process_info(decl_info* info) { - if (!info) { - return; - } - unsigned num_params = info->get_num_parameters(); - for (unsigned i = 0; i < num_params; ++i) { - parameter const& p = info->get_parameter(i); - - if (p.is_ast() && !m_mark.is_marked(p.get_ast())) { - process_ast(p.get_ast()); - } - } - } - - template - void display_children(unsigned num_children, T * const * children) { - for (unsigned i = 0; i < num_children; i++) { - display_node_id(children[i]); - } - } - - void display_node_id(ast* n) { - unsigned id = n->get_id(); - switch(n->get_kind()) { - case AST_FUNC_DECL: - case AST_SORT: - m_out << "$d" << (id - (1 << 31)) << " "; - break; - default: - m_out << "$" << id << " "; - break; - } - } - - void display_parameter(parameter const& p) - { - if (p.is_int()) { - m_out << p.get_int() << " "; - } - else if (p.is_ast()) { - SASSERT(p.is_ast()); - display_node_id(p.get_ast()); - } - else if (p.is_rational()) { - m_out << p.get_rational() << " "; - } - else if (p.is_symbol()) { - display_symbol(p.get_symbol()); - } - else { - UNREACHABLE(); - } - } - - // Display: - // App name [ parameters] arguments - // - void display_builtin(app* n) { - func_decl* d = n->get_decl(); - unsigned num_params = d->get_num_parameters(); - - m_out << "App "; - display_node_id(n); - display_symbol(d->get_name()); - if (num_params > 0) { - m_out << "[ "; - for (unsigned i = 0; i < num_params; ++i) { - display_parameter(d->get_parameter(i)); - } - m_out << "] "; - } - display_children(n->get_num_args(), n->get_args()); - m_out << "\n"; - } - - void display_info(func_decl_info* info) { - if (!info) { - return; - } - m_out << "BUILTIN " << get_family_name(info->get_family_id()) << " " << info->get_decl_kind() << " "; - - if (info->is_associative()) { - m_out << ":assoc "; - } - if (info->is_commutative()) { - m_out << ":comm "; - } - if (info->is_injective()) { - m_out << ":inj "; - } - for (unsigned i = 0; i < info->get_num_parameters(); ++i) { - display_parameter(info->get_parameter(i)); - } - } - - void display_info(sort_info* info) { - if (!info) { - return; - } - m_out << "BUILTIN " << get_family_name(info->get_family_id()) << " " << info->get_decl_kind() << " "; - // TODO: remove this if... it doesn't make sense... - if (!info->is_infinite() && !info->is_very_big()) { - m_out << "Size " << info->get_num_elements().size() << " "; - } - for (unsigned i = 0; i < info->get_num_parameters(); ++i) { - display_parameter(info->get_parameter(i)); - } - } - - symbol get_family_name(family_id id) { - if (id == null_family_id) { - return symbol("null"); - } - if (!m_initialized) { - svector names; - svector range; - m_manager.get_dom(names); - m_manager.get_range(range); - m_names.resize(range.size()); - for (unsigned i = 0; i < range.size(); ++i) { - SASSERT(range[i] < static_cast(range.size())); - m_names[range[i]] = names[i]; - } - m_initialized = true; - } - SASSERT(id < static_cast(m_names.size())); - return m_names[id]; - } - - bool has_special_char(char const* s) { - while (s && *s) { - if (*s == ' ') { - return true; - } - ++s; - } - return false; - } - - void display_symbol(symbol const& s) { - if (s.is_numerical()) { - m_out << s << " "; - } - else if (!(s.bare_str()[0])) { - m_out << "\"null\" "; - } - else if (!has_special_char(s.bare_str())) { - m_out << s << " "; - } - else { - char const* r = s.bare_str(); - m_out << "\""; - while (*r) { - if (*r == ' ' || *r == '\n' || - *r == '\t' || *r == '\r') { - m_out << "\\" << ((unsigned)(*r)); - } - else { - m_out << *r; - } - ++r; - } - m_out << "\" "; - } - } - -public: - - dag_printer(ast_manager& mgr, std::ostream & out, ast_mark& mark): - m_manager(mgr), - m_out(out), - m_mark(mark), - m_initialized(false), - m_basic_fid(mgr.get_basic_family_id()), - m_bv_fid(mgr.get_family_id("bv")), - m_arith_fid(mgr.get_family_id("arith")), - m_array_fid(mgr.get_family_id("array")), - m_arith(mgr), - m_bv(mgr), - m_enable_shortcut(true) - { - } - - void operator()(sort * n) { - process_info(n->get_info()); - m_out << "Ty "; - display_node_id(n); - display_symbol(n->get_name()); - display_info(n->get_info()); - m_out << "\n"; - } - - void pp_num(app* n, rational const& r) { - m_out << "Num "; - display_node_id(n); - m_out << r << " "; - display_node_id(m_manager.get_sort(n)); - m_out << "\n"; - } - - void operator()(var * n) { - process_ast(n->get_sort()); - m_out << "Var "; - display_node_id(n); - m_out << n->get_idx() << " "; - display_node_id(n->get_sort()); - m_out << "\n"; - } - - void operator()(func_decl * n) { - - process_info(n->get_info()); - - family_id fid = n->get_family_id(); - if (m_arith_fid == fid && - n->get_info()->get_decl_kind() == OP_NUM) { - return; - } - - if (m_bv_fid == fid && - n->get_info()->get_decl_kind() == OP_BV_NUM) { - return; - } - - m_out << "Dec "; - display_node_id(n); - display_symbol(n->get_name()); - unsigned dom_size = n->get_arity(); - for (unsigned i = 0; i < dom_size; ++i) { - display_node_id(n->get_domain(i)); - } - display_node_id(n->get_range()); - display_info(n->get_info()); - m_out << "\n"; - } - - void operator()(app * n) { - process_ast(n->get_decl()); - family_id fid = n->get_family_id(); - unsigned bv_size; - rational val; - if (m_arith.is_numeral(n, val)) { - pp_num(n, val); - } - else if (m_bv.is_numeral(n, val, bv_size)) { - pp_num(n, val); - } - else if (m_enable_shortcut && - fid != null_family_id && - (fid == m_basic_fid || fid == m_bv_fid || fid == m_array_fid || fid == m_arith_fid)) { - display_builtin(n); - } - else if (n->get_num_args() == 0 && fid == null_family_id) { - func_decl* d = n->get_decl(); - m_out << "Const "; - display_node_id(n); - display_symbol(d->get_name()); - display_node_id(d->get_range()); - m_out << "\n"; - } - else { - m_out << "Fun "; - display_node_id(n); - display_node_id(n->get_decl()); - display_children(n->get_num_args(), n->get_args()); - m_out << "\n"; - } - } - - void operator()(quantifier * n) { - m_out << "Qua "; - display_node_id(n); - m_out << (n->is_forall() ? "FORALL" : "EXISTS") << " "; - m_out << n->get_weight() << " "; - if (symbol::null != n->get_skid()) { - m_out << "\"" << n->get_skid() << "\" "; - } - else { - m_out << "\"null\" "; - } - if (symbol::null != n->get_qid()) { - m_out << "\"" << n->get_qid() << "\" "; - } - else { - m_out << "\"null\" "; - } - unsigned num_decls = n->get_num_decls(); - m_out << num_decls << " "; - for (unsigned i = 0; i < num_decls; i++) { - m_out << n->get_decl_name(i) << " "; - display_node_id(n->get_decl_sort(i)); - } - m_out << n->get_num_patterns() << " "; - display_children(n->get_num_patterns(), n->get_patterns()); - display_node_id(n->get_expr()); - m_out << "\n"; - } -}; - -void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast_mark& mark, ast * n) { - dag_printer p(mgr, out, mark); - for_each_ast(p, mark, n, true); -} - -void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast * n) { - ast_mark mark; - ast_dag_pp(out, mgr, mark, n); -} - diff --git a/src/ast/ast_dag_pp.h b/src/ast/ast_dag_pp.h deleted file mode 100644 index fa933e22f..000000000 --- a/src/ast/ast_dag_pp.h +++ /dev/null @@ -1,31 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - ast_dag_pp.h - -Abstract: - - AST low level pretty printer. - -Author: - - Leonardo de Moura (leonardo) 2006-10-19. - -Revision History: - ---*/ -#ifndef _AST_DAG_PP_H_ -#define _AST_DAG_PP_H_ - -#include - -class ast; - -void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast * n); - -void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast_mark& mark, ast * n); - -#endif /* _AST_DAG_PP_H_ */ - diff --git a/src/ast/expr2dot.cpp b/src/ast/expr2dot.cpp deleted file mode 100644 index b0fef27d0..000000000 --- a/src/ast/expr2dot.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - expr2dot.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-03-07. - -Revision History: - ---*/ -#include"expr2dot.h" -#include"for_each_expr.h" - -class dot_printer { - std::ostream & m_out; - ast_manager & m_manager; - bool m_proofs_only; -public: - dot_printer(std::ostream & out, ast_manager & m, bool proofs): - m_out(out), - m_manager(m), - m_proofs_only(proofs) { - } - - char const * get_color(app * n) { - if (m_manager.is_unit_resolution(n)) - return "blue"; - else if (m_manager.is_lemma(n)) - return "gold"; - else if (m_manager.is_transitivity(n)) - return "red"; - else if (m_manager.is_monotonicity(n)) - return "green"; - else - return "black"; - } - - void operator()(var * n) { - if (!m_proofs_only) { - m_out << n->get_id() << "[label=\"\",shape=circle];\n"; - } - } - - void operator()(quantifier * n) { - if (!m_proofs_only) { - m_out << n->get_id() << "[label=\"\",shape=circle,color=gray];\n"; - m_out << n->get_expr()->get_id() << " -> " << n->get_id() << ";\n"; - } - } - - void operator()(app * n) { - if (!m_proofs_only || m_manager.is_proof(n)) { - char const * c = get_color(n); - m_out << n->get_id() << "[label=\"\",shape=circle,color=" << c << "];\n"; - if (m_proofs_only) { - unsigned num = m_manager.get_num_parents(n); - for (unsigned i = 0; i < num; i++) - m_out << m_manager.get_parent(n, i)->get_id() << " -> " << n->get_id() << " [color=" << c << "];\n"; - } - else { - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) - m_out << n->get_arg(i)->get_id() << " -> " << n->get_id() << " [color=" << c << "];\n"; - } - } - } -}; - -void expr2dot(std::ostream & out, expr * n, ast_manager & m, bool proofs) { - out << "digraph \"ast\" {\n"; - dot_printer p(out, m, proofs); - for_each_expr(p, n); - out << "}\n"; -} - - diff --git a/src/ast/expr2dot.h b/src/ast/expr2dot.h deleted file mode 100644 index 54c65b034..000000000 --- a/src/ast/expr2dot.h +++ /dev/null @@ -1,27 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - expr2dot.h - -Abstract: - - Convert expressions into a .DOT file - -Author: - - Leonardo de Moura (leonardo) 2008-03-07. - -Revision History: - ---*/ -#ifndef _EXPR2DOT_H_ -#define _EXPR2DOT_H_ - -#include"ast.h" - -void expr2dot(std::ostream & out, expr * a, ast_manager & m, bool proofs = false); - -#endif /* _AST2DOT_H_ */ - diff --git a/src/util/interval.h b/src/math/interval/interval.h similarity index 100% rename from src/util/interval.h rename to src/math/interval/interval.h diff --git a/src/util/interval_def.h b/src/math/interval/interval_def.h similarity index 100% rename from src/util/interval_def.h rename to src/math/interval/interval_def.h diff --git a/src/util/imdd.cpp b/src/muz_qe/imdd.cpp similarity index 100% rename from src/util/imdd.cpp rename to src/muz_qe/imdd.cpp diff --git a/src/util/imdd.h b/src/muz_qe/imdd.h similarity index 100% rename from src/util/imdd.h rename to src/muz_qe/imdd.h diff --git a/src/util/interval_skip_list.h b/src/muz_qe/interval_skip_list.h similarity index 100% rename from src/util/interval_skip_list.h rename to src/muz_qe/interval_skip_list.h diff --git a/src/util/skip_list_base.h b/src/muz_qe/skip_list_base.h similarity index 100% rename from src/util/skip_list_base.h rename to src/muz_qe/skip_list_base.h diff --git a/src/util/diff_logic.h b/src/smt/diff_logic.h similarity index 100% rename from src/util/diff_logic.h rename to src/smt/diff_logic.h diff --git a/src/util/old_interval.cpp b/src/smt/old_interval.cpp similarity index 100% rename from src/util/old_interval.cpp rename to src/smt/old_interval.cpp diff --git a/src/util/old_interval.h b/src/smt/old_interval.h similarity index 100% rename from src/util/old_interval.h rename to src/smt/old_interval.h diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 1b95cb1ed..0ad845095 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -31,7 +31,6 @@ Notes: #include"max_bv_sharing_tactic.h" #include"simplify_tactic.h" #include"stopwatch.h" -#include"expr2dot.h" #include"propagate_values_tactic.h" #include"sls_tactic.h" #include"nnf_tactic.h" @@ -1727,17 +1726,6 @@ class sls_tactic : public tactic { } void operator()(goal_ref const & g, model_converter_ref & mc) { - //#ifdef _DEBUG - //ptr_vector es; - //for (unsigned i = 0; i < g->size(); i++) - // es.push_back(g->form(i)); - //expr_ref a(m_manager); - //a = m_manager.mk_and(g->size(), es.c_ptr()); - //std::ofstream dot_out("top.dot", std::ios::out); - //expr2dot(dot_out, a, m_manager); - //dot_out.close(); - //#endif - if (g->inconsistent()) { mc = 0; return;