diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp new file mode 100644 index 000000000..015075d9b --- /dev/null +++ b/src/ast/ast_printer.cpp @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + ast_printer.cpp + +Abstract: + + Abstract AST printer + +Author: + + Leonardo de Moura (leonardo) 2012-10-21 + +Revision History: + +--*/ +#include"ast_printer.h" +#include"pp.h" + +class simple_ast_printer_context : public ast_printer_context { + ast_manager & m_manager; + smt2_pp_environment_dbg m_env; +public: + simple_ast_printer_context(ast_manager & m):m_manager(m), m_env(m) {} + virtual ~simple_ast_printer_context() {} + ast_manager & m() const { return m_manager; } + virtual ast_manager & get_ast_manager() { return m_manager; } + virtual void display(std::ostream & out, sort * s, unsigned indent = 0) { out << mk_ismt2_pp(s, m(), indent); } + virtual void display(std::ostream & out, expr * n, unsigned indent = 0) { out << mk_ismt2_pp(n, m(), indent); } + virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const { + out << f->get_name(); + } + virtual void pp(sort * s, format_ns::format_ref & r) { mk_smt2_format(s, m_env, get_pp_default_params(), r); } + virtual void pp(func_decl * f, format_ns::format_ref & r) { mk_smt2_format(f, m_env, get_pp_default_params(), r); } + virtual void pp(expr * n, format_ns::format_ref & r) { + sbuffer buf; + mk_smt2_format(n, m_env, get_pp_default_params(), 0, 0, r, buf); + } + virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) { + mk_smt2_format(n, m_env, get_pp_default_params(), num_vars, var_prefix, r, var_names); + } + virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const { + NOT_IMPLEMENTED_YET(); + } + +}; + +ast_printer_context * mk_simple_ast_printer_context(ast_manager & m) { + return alloc(simple_ast_printer_context, m); +} diff --git a/src/ast/ast_printer.h b/src/ast/ast_printer.h new file mode 100644 index 000000000..3566c62bb --- /dev/null +++ b/src/ast/ast_printer.h @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + ast_printer.h + +Abstract: + + Abstract AST printer + +Author: + + Leonardo de Moura (leonardo) 2012-10-21 + +Revision History: + +--*/ +#ifndef _AST_PRINTER_H_ +#define _AST_PRINTER_H_ + +#include"ast.h" +#include"ast_smt2_pp.h" + +class ast_printer { +public: + virtual ~ast_printer() {} + virtual void pp(sort * s, format_ns::format_ref & r) const { UNREACHABLE(); } + virtual void pp(func_decl * f, format_ns::format_ref & r) const { UNREACHABLE(); } + virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer & var_names) const { UNREACHABLE(); } + virtual void pp(expr * n, format_ns::format_ref & r) const { UNREACHABLE(); } + virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const { + out << "#" << s->get_id() << "\n"; + } + virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const { + out << "#" << n->get_id() << "\n"; + } + virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const { + out << "#" << n->get_id() << "\n"; + } + virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const { + out << "#" << f->get_id() << "\n"; + } +}; + +class ast_printer_context : public ast_printer { +public: + virtual ~ast_printer_context() {} + virtual ast_manager & get_ast_manager() = 0; + virtual std::ostream & regular_stream() { return std::cout; } + virtual std::ostream & diagnostic_stream() { return std::cerr; } +}; + + +ast_printer_context * mk_simple_ast_printer_context(ast_manager & m); + +#endif diff --git a/src/framework/README b/src/framework/README index 695db970b..c44a00690 100644 --- a/src/framework/README +++ b/src/framework/README @@ -1 +1,2 @@ -tactic and command context frameworks. \ No newline at end of file +Command context provides the infrastructure for executing commands in front-ends such as SMT-LIB 2.0. +It is also provides the solver abstraction to plugin solvers in this kind of front-end. \ No newline at end of file diff --git a/src/framework/cmd_context_to_goal.cpp b/src/framework/cmd_context_to_goal.cpp new file mode 100644 index 000000000..21f8445d5 --- /dev/null +++ b/src/framework/cmd_context_to_goal.cpp @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + cmd_context_to_goal.cpp + +Abstract: + Procedure for copying the assertions in the + command context to a goal object. + +Author: + + Leonardo (leonardo) 2012-10-21 + +Notes: + +--*/ +#include"cmd_context.h" +#include"goal.h" + +/** + \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()); + } +} diff --git a/src/framework/cmd_context_to_goal.h b/src/framework/cmd_context_to_goal.h new file mode 100644 index 000000000..2bc27baa7 --- /dev/null +++ b/src/framework/cmd_context_to_goal.h @@ -0,0 +1,24 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + cmd_context_to_goal.h + +Abstract: + Procedure for copying the assertions in the + command context to a goal object. + +Author: + + Leonardo (leonardo) 2012-10-21 + +Notes: + +--*/ +#ifndef _CMD_CONTEXT_TO_GOAL_H_ +#define _CMD_CONTEXT_TO_GOAL_H_ + +void assert_exprs_from(cmd_context const & ctx, goal & t); + +#endif diff --git a/src/framework/echo_tactic.cpp b/src/framework/echo_tactic.cpp new file mode 100644 index 000000000..10d671542 --- /dev/null +++ b/src/framework/echo_tactic.cpp @@ -0,0 +1,84 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + echo_tactic.h + +Abstract: + + Tactic and probe for dumping data. + +Author: + + Leonardo (leonardo) 2012-10-20 + +Notes: + +--*/ +#include"tactic.h" +#include"probe.h" +#include"cmd_context.h" + +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); +} diff --git a/src/framework/echo_tactic.h b/src/framework/echo_tactic.h new file mode 100644 index 000000000..8760820bd --- /dev/null +++ b/src/framework/echo_tactic.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + echo_tactic.h + +Abstract: + + Tactic and probe for dumping data. + +Author: + + Leonardo (leonardo) 2012-10-20 + +Notes: + +--*/ +#ifndef _ECHO_TACTICS_H_ +#define _ECHO_TACTICS_H_ + +class cmd_context; +class tactic; +class probe; + +tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline = true); +// Display the value returned by p in the diagnostic_stream +tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline = true); + +#endif