diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 35d1b3457..6d00b5761 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -8,7 +8,7 @@ ############################################ from mk_util import * -set_build_dir('build-test') +set_build_dir('build') set_src_dir('src') set_modes(['Debug', 'Release']) set_platforms(['Win32', 'x64']) diff --git a/src/framework/cmd_context.cpp b/src/framework/cmd_context.cpp index 1eb0f63e7..5e80863de 100644 --- a/src/framework/cmd_context.cpp +++ b/src/framework/cmd_context.cpp @@ -1601,3 +1601,4 @@ std::ostream & operator<<(std::ostream & out, cmd_context::status st) { } return out; } + diff --git a/src/framework/cmd_context.h b/src/framework/cmd_context.h index 017f26428..08122f7d2 100644 --- a/src/framework/cmd_context.h +++ b/src/framework/cmd_context.h @@ -23,6 +23,7 @@ Notes: #include #include"ast.h" +#include"ast_printer.h" #include"pdecl.h" #include"dictionary.h" #include"solver.h" @@ -111,7 +112,7 @@ struct builtin_decl { builtin_decl(family_id fid, decl_kind k, builtin_decl * n = 0):m_fid(fid), m_decl(k), m_next(n) {} }; -class cmd_context : public progress_callback, public tactic_manager { +class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context { public: enum status { UNSAT, SAT, UNKNOWN @@ -329,8 +330,8 @@ public: void reset_user_tactics(); void set_regular_stream(char const * name) { m_regular.set(name); } void set_diagnostic_stream(char const * name); - std::ostream & regular_stream() { return *m_regular; } - std::ostream & diagnostic_stream() { return *m_diagnostic; } + virtual std::ostream & regular_stream() { return *m_regular; } + virtual std::ostream & diagnostic_stream() { return *m_diagnostic; } char const * get_regular_stream_name() const { return m_regular.name(); } char const * get_diagnostic_stream_name() const { return m_diagnostic.name(); } typedef dictionary::iterator cmd_iterator; @@ -385,10 +386,10 @@ public: void pp(func_decl * f, format_ns::format_ref & r) const; void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) const; void pp(expr * n, format_ns::format_ref & r) const; - void display(std::ostream & out, sort * s, unsigned indent = 0) const; - void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const; - void display(std::ostream & out, expr * n, unsigned indent = 0) const; - void display(std::ostream & out, func_decl * f, unsigned indent = 0) const; + virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const; + virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const; + virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const; + virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const; // dump assertions in out using the pretty printer. void dump_assertions(std::ostream & out) const; diff --git a/src/framework/goal.cpp b/src/framework/goal.cpp index a84b34dd5..6897097be 100644 --- a/src/framework/goal.cpp +++ b/src/framework/goal.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include"goal.h" -#include"cmd_context.h" #include"ast_ll_pp.h" #include"ast_smt2_pp.h" #include"for_each_expr.h" @@ -235,17 +234,17 @@ void goal::reset() { m_inconsistent = false; } -void goal::display(cmd_context & ctx, std::ostream & out) const { +void goal::display(ast_printer & prn, std::ostream & out) const { out << "(goal"; unsigned sz = size(); for (unsigned i = 0; i < sz; i++) { out << "\n "; - ctx.display(out, form(i), 2); + prn.display(out, form(i), 2); } out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl; } -void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) const { +void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) const { ptr_vector deps; obj_hashtable to_pp; out << "(goal"; @@ -267,7 +266,7 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons } } out << "\n "; - ctx.display(out, form(i), 2); + prn.display(out, form(i), 2); } if (!to_pp.empty()) { out << "\n :dependencies-definitions ("; @@ -276,7 +275,7 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons for (; it != end; ++it) { expr * d = *it; out << "\n (#" << d->get_id() << "\n "; - ctx.display(out, d, 2); + prn.display(out, d, 2); out << ")"; } out << ")"; @@ -308,11 +307,11 @@ void goal::display_with_dependencies(std::ostream & out) const { out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl; } -void goal::display(cmd_context & ctx) const { +void goal::display(ast_printer_context & ctx) const { display(ctx, ctx.regular_stream()); } -void goal::display_with_dependencies(cmd_context & ctx) const { +void goal::display_with_dependencies(ast_printer_context & ctx) const { display_with_dependencies(ctx, ctx.regular_stream()); } @@ -546,32 +545,6 @@ bool goal::is_well_sorted() const { return true; } -/** - \brief Assert expressions from ctx into t. -*/ -void assert_exprs_from(cmd_context const & ctx, goal & t) { - if (ctx.produce_proofs() && ctx.produce_unsat_cores()) - throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores"); - ast_manager & m = t.m(); - bool proofs_enabled = t.proofs_enabled(); - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0); - } - if (ctx.produce_unsat_cores()) { - SASSERT(!ctx.produce_proofs()); - it = ctx.begin_assumptions(); - end = ctx.end_assumptions(); - for (; it != end; ++it) { - t.assert_expr(*it, 0, m.mk_leaf(*it)); - } - } - else { - SASSERT(ctx.begin_assumptions() == ctx.end_assumptions()); - } -} - /** \brief Translate the assertion set to a new one that uses a different ast_manager. */ diff --git a/src/framework/goal.h b/src/framework/goal.h index 61c7e2081..c1dcaa6f6 100644 --- a/src/framework/goal.h +++ b/src/framework/goal.h @@ -30,13 +30,12 @@ Revision History: #include"ast.h" #include"ast_translation.h" +#include"ast_printer.h" #include"for_each_expr.h" #include"ref.h" #include"ref_vector.h" #include"ref_buffer.h" -class cmd_context; - class goal { public: enum precision { @@ -172,14 +171,14 @@ public: void elim_true(); void elim_redundancies(); - void display(cmd_context & ctx, std::ostream & out) const; - void display(cmd_context & ctx) const; + void display(ast_printer & prn, std::ostream & out) const; + void display(ast_printer_context & ctx) const; void display(std::ostream & out) const; void display_ll(std::ostream & out) const; void display_as_and(std::ostream & out) const; void display_dimacs(std::ostream & out) const; - void display_with_dependencies(cmd_context & ctx, std::ostream & out) const; - void display_with_dependencies(cmd_context & ctx) const; + void display_with_dependencies(ast_printer & prn, std::ostream & out) const; + void display_with_dependencies(ast_printer_context & ctx) const; void display_with_dependencies(std::ostream & out) const; bool sat_preserved() const { @@ -220,8 +219,6 @@ inline bool is_decided_sat(GoalCollection const & c) { return c.size() == 1 && c template inline bool is_decided_unsat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_unsat(); } -void assert_exprs_from(cmd_context const & ctx, goal & t); - template void for_each_expr_at(ForEachProc& proc, goal const & s) { expr_mark visited; diff --git a/src/framework/tactic.cpp b/src/framework/tactic.cpp index cc2f3bc3f..d5ef15499 100644 --- a/src/framework/tactic.cpp +++ b/src/framework/tactic.cpp @@ -81,25 +81,17 @@ void report_tactic_progress(char const * id, unsigned val) { } } - -class skip_tactic : public tactic { -public: - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - result.reset(); - result.push_back(in.get()); - mc = 0; - pc = 0; - core = 0; - } - - virtual void cleanup() {} - - virtual tactic * translate(ast_manager & m) { return this; } -}; +void skip_tactic::operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + result.reset(); + result.push_back(in.get()); + mc = 0; + pc = 0; + core = 0; +} tactic * mk_skip_tactic() { return alloc(skip_tactic); @@ -163,69 +155,6 @@ tactic * mk_trace_tactic(char const * tag) { return alloc(trace_tactic, tag); } -class echo_tactic : public skip_tactic { - cmd_context & m_ctx; - char const * m_msg; - bool m_newline; -public: - echo_tactic(cmd_context & ctx, char const * msg, bool newline):m_ctx(ctx), m_msg(msg), m_newline(newline) {} - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - #pragma omp critical (echo_tactic) - { - m_ctx.diagnostic_stream() << m_msg; - if (m_newline) - m_ctx.diagnostic_stream() << std::endl; - } - skip_tactic::operator()(in, result, mc, pc, core); - } -}; - -tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline) { - return alloc(echo_tactic, ctx, msg, newline); -} - -class probe_value_tactic : public skip_tactic { - cmd_context & m_ctx; - char const * m_msg; - probe * m_p; - bool m_newline; -public: - probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline):m_ctx(ctx), m_msg(msg), m_p(p), m_newline(newline) { - SASSERT(m_p); - m_p->inc_ref(); - } - - ~probe_value_tactic() { - m_p->dec_ref(); - } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - double val = (*m_p)(*(in.get())).get_value(); - #pragma omp critical (probe_value_tactic) - { - if (m_msg) - m_ctx.diagnostic_stream() << m_msg << " "; - m_ctx.diagnostic_stream() << val; - if (m_newline) - m_ctx.diagnostic_stream() << std::endl; - } - skip_tactic::operator()(in, result, mc, pc, core); - } -}; - -tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline) { - return alloc(probe_value_tactic, ctx, msg, p, newline); -} - class fail_if_undecided_tactic : public skip_tactic { public: fail_if_undecided_tactic() {} diff --git a/src/framework/tactic.h b/src/framework/tactic.h index 2b3a34ca6..fb443cd41 100644 --- a/src/framework/tactic.h +++ b/src/framework/tactic.h @@ -117,17 +117,19 @@ public: void report_tactic_progress(char const * id, unsigned val); +class skip_tactic : public tactic { +public: + virtual void operator()(goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); + virtual void cleanup() {} + virtual tactic * translate(ast_manager & m) { return this; } +}; + tactic * mk_skip_tactic(); tactic * mk_fail_tactic(); tactic * mk_fail_if_undecided_tactic(); tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl); tactic * mk_trace_tactic(char const * tag); -tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline = true); -// Display the value returned by p in the diagnostic_stream -class probe; -tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline = true); - class tactic_factory { public: diff --git a/src/framework/tactic_cmds.cpp b/src/framework/tactic_cmds.cpp index c7351d455..f6d9a5e5f 100644 --- a/src/framework/tactic_cmds.cpp +++ b/src/framework/tactic_cmds.cpp @@ -30,6 +30,8 @@ Notes: #include"tactical.h" #include"probe.h" #include"check_sat_result.h" +#include"cmd_context_to_goal.h" +#include"echo_tactic.h" tactic_cmd::~tactic_cmd() { dealloc(m_factory);