diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h new file mode 100644 index 000000000..a8f54b2c3 --- /dev/null +++ b/src/ast/ast_pp_util.h @@ -0,0 +1,81 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + ast_pp_util.h + +Abstract: + + + +Author: + + Nikolaj Bjorner (nbjorner) 2015-8-6. + +Revision History: + +--*/ +#ifndef AST_PP_UTIL_H_ +#define AST_PP_UTIL_H_ + +#include "decl_collector.h" +#include "ast_smt2_pp.h" +#include "ast_smt_pp.h" + +class ast_pp_util { + ast_manager& m; + public: + + decl_collector coll; + + ast_pp_util(ast_manager& m): m(m), coll(m, false) {} + + void collect(expr* e) { + coll.visit(e); + } + + void collect(unsigned n, expr* const* es) { + for (unsigned i = 0; i < n; ++i) { + coll.visit(es[i]); + } + } + + void collect(expr_ref_vector const& es) { + collect(es.size(), es.c_ptr()); + } + + void display_decls(std::ostream& out) { + smt2_pp_environment_dbg env(m); + unsigned n = coll.get_num_sorts(); + for (unsigned i = 0; i < n; ++i) { + ast_smt2_pp(out, coll.get_sorts()[i], env); + } + n = coll.get_num_decls(); + for (unsigned i = 0; i < n; ++i) { + ast_smt2_pp(out, coll.get_func_decls()[i], env); + out << "\n"; + } + } + + void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true) { + if (neat) { + smt2_pp_environment_dbg env(m); + for (unsigned i = 0; i < fmls.size(); ++i) { + out << "(assert "; + ast_smt2_pp(out, fmls[i], env); + out << ")\n"; + } + } + else { + ast_smt_pp ll_smt2_pp(m); + for (unsigned i = 0; i < fmls.size(); ++i) { + out << "(assert "; + ll_smt2_pp.display_expr_smt2(out, fmls[i]); + out << ")\n"; + } + } + } +}; + +#endif /* AST_PP_UTIL_H_ */ diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 52d28ab5f..678f3805d 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -43,6 +43,8 @@ public: ast_manager & m() { return m_manager; } void visit(ast * n); + void visit(unsigned n, expr* const* es); + void visit(expr_ref_vector const& es); unsigned get_num_sorts() const { return m_sorts.size(); } unsigned get_num_decls() const { return m_decls.size(); } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index a84b1899c..60de96e1d 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -28,6 +28,7 @@ Revision History: #include"datatype_decl_plugin.h" #include"scoped_proof.h" #include"fixedpoint_params.hpp" +#include"ast_pp_util.h" namespace datalog { @@ -957,31 +958,13 @@ namespace datalog { } // NB: algebraic data-types declarations will not be printed. - class free_func_visitor { - ast_manager& m; - func_decl_set m_funcs; - obj_hashtable m_sorts; - public: - free_func_visitor(ast_manager& m): m(m) {} - void operator()(var * n) { } - void operator()(app * n) { - m_funcs.insert(n->get_decl()); - sort* s = m.get_sort(n); - if (s->get_family_id() == null_family_id) { - m_sorts.insert(s); - } - } - void operator()(quantifier * n) { } - func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } - }; static void collect_free_funcs(unsigned sz, expr* const* exprs, - expr_mark& visited, free_func_visitor& v, + ast_pp_util& v, mk_fresh_name& fresh_names) { + v.collect(sz, exprs); for (unsigned i = 0; i < sz; ++i) { expr* e = exprs[i]; - for_each_expr(v, visited, e); while (is_quantifier(e)) { e = to_quantifier(e)->get_expr(); } @@ -1051,8 +1034,7 @@ namespace datalog { void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) { ast_manager& m = get_manager(); - free_func_visitor visitor(m); - expr_mark visited; + ast_pp_util visitor(m); func_decl_set rels; unsigned num_axioms = m_background.size(); expr* const* axioms = m_background.c_ptr(); @@ -1070,14 +1052,13 @@ namespace datalog { smt2_pp_environment_dbg env(m); mk_fresh_name fresh_names; - collect_free_funcs(num_axioms, axioms, visited, visitor, fresh_names); - collect_free_funcs(rules.size(), rules.c_ptr(), visited, visitor, fresh_names); - collect_free_funcs(queries.size(), queries.c_ptr(), visited, visitor, fresh_names); + collect_free_funcs(num_axioms, axioms, visitor, fresh_names); + collect_free_funcs(rules.size(), rules.c_ptr(), visitor, fresh_names); + collect_free_funcs(queries.size(), queries.c_ptr(), visitor, fresh_names); func_decl_set funcs; - func_decl_set::iterator it = visitor.funcs().begin(); - func_decl_set::iterator end = visitor.funcs().end(); - for (; it != end; ++it) { - func_decl* f = *it; + unsigned sz = visitor.coll.get_num_decls(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* f = visitor.coll.get_func_decls()[i]; if (f->get_family_id() != null_family_id) { // } @@ -1092,20 +1073,9 @@ namespace datalog { if (!use_fixedpoint_extensions) { out << "(set-logic HORN)\n"; } - - it = funcs.begin(), end = funcs.end(); - - obj_hashtable& sorts = visitor.sorts(); - obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); - for (; sit != send; ++sit) { - PP(*sit); - } - for (; it != end; ++it) { - func_decl* f = *it; - PP(f); - out << "\n"; - } - it = rels.begin(); end = rels.end(); + + visitor.display_decls(out); + func_decl_set::iterator it = rels.begin(), end = rels.end(); for (; it != end; ++it) { func_decl* f = *it; out << "(declare-rel " << f->get_name() << " ("; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d7d96b2d1..35a69b15c 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -40,6 +40,7 @@ Notes: #include "pb_decl_plugin.h" #include "ast_smt_pp.h" #include "filter_model_converter.h" +#include "ast_pp_util.h" namespace opt { @@ -1255,44 +1256,13 @@ namespace opt { m_pp_neat = _p.pp_neat(); } - typedef obj_hashtable func_decl_set; - - struct context::free_func_visitor { - ast_manager& m; - func_decl_set m_funcs; - obj_hashtable m_sorts; - expr_mark m_visited; - public: - free_func_visitor(ast_manager& m): m(m) {} - void operator()(var * n) { } - void operator()(app * n) { - if (n->get_family_id() == null_family_id) { - m_funcs.insert(n->get_decl()); - } - sort* s = m.get_sort(n); - if (s->get_family_id() == null_family_id) { - m_sorts.insert(s); - } - } - void operator()(quantifier * n) { } - func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } - - void collect(expr* e) { - for_each_expr(*this, m_visited, e); - } - }; - std::string context::to_string() const { smt2_pp_environment_dbg env(m); - ast_smt_pp ll_smt2_pp(m); - free_func_visitor visitor(m); + ast_pp_util visitor(m); std::ostringstream out; #define PP(_e_) ast_smt2_pp(out, _e_, env); -#define PPE(_e_) if (m_pp_neat) ast_smt2_pp(out, _e_, env); else ll_smt2_pp.display_expr_smt2(out, _e_); - for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) { - visitor.collect(m_scoped_state.m_hard[i]); - } + visitor.collect(m_scoped_state.m_hard); + for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { objective const& obj = m_scoped_state.m_objectives[i]; switch(obj.m_type) { @@ -1301,9 +1271,7 @@ namespace opt { visitor.collect(obj.m_term); break; case O_MAXSMT: - for (unsigned j = 0; j < obj.m_terms.size(); ++j) { - visitor.collect(obj.m_terms[j]); - } + visitor.collect(obj.m_terms); break; default: UNREACHABLE(); @@ -1311,22 +1279,8 @@ namespace opt { } } - obj_hashtable::iterator sit = visitor.sorts().begin(); - obj_hashtable::iterator send = visitor.sorts().end(); - for (; sit != send; ++sit) { - PP(*sit); - } - func_decl_set::iterator it = visitor.funcs().begin(); - func_decl_set::iterator end = visitor.funcs().end(); - for (; it != end; ++it) { - PP(*it); - out << "\n"; - } - for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) { - out << "(assert "; - PPE(m_scoped_state.m_hard[i]); - out << ")\n"; - } + visitor.display_decls(out); + visitor.display_asserts(out, m_scoped_state.m_hard, m_pp_neat); for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { objective const& obj = m_scoped_state.m_objectives[i]; switch(obj.m_type) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index d17cc3748..50847134d 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -68,7 +68,6 @@ namespace opt { public opt_wrapper, public pareto_callback, public maxsat_context { - struct free_func_visitor; typedef map map_t; typedef map map_id; typedef vector > bounds_t; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 375f35ed1..c19bb7547 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -22,6 +22,7 @@ Notes: #include"solver_na2as.h" #include"tactic.h" #include"ast_smt2_pp.h" +#include"ast_pp_util.h" /** \brief Simulates the incremental solver interface using a tactic. @@ -221,6 +222,11 @@ expr * tactic2solver::get_assertion(unsigned idx) const { } void tactic2solver::display(std::ostream & out) const { + ast_pp_util visitor(m_assertions.m()); + visitor.collect(m_assertions); + visitor.display_decls(out); + visitor.display_asserts(out, m_assertions, true); +#if 0 ast_manager & m = m_assertions.m(); unsigned num = m_assertions.size(); out << "(solver"; @@ -228,6 +234,7 @@ void tactic2solver::display(std::ostream & out) const { out << "\n " << mk_ismt2_pp(m_assertions.get(i), m, 2); } out << ")"; +#endif } solver * mk_tactic2solver(ast_manager & m,