checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<symbol> 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<symbol> & 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<symbol> & var_names) const {
+        NOT_IMPLEMENTED_YET();
+    }
+
+};
+
+ast_printer_context * mk_simple_ast_printer_context(ast_manager & m) {
+    return alloc(simple_ast_printer_context, m);
+}

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<symbol> & 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<symbol> & 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

src/framework/README

@@ -1 +1,2 @@
-tactic and command context frameworks.
+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.

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<expr>::const_iterator it  = ctx.begin_assertions();
+    ptr_vector<expr>::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());
+    }
+}

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

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);
+}

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