Reorganizing the code

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

src/framework/tactic2solver.cpp

@@ -0,0 +1,249 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic2solver.cpp
+
+Abstract:
+
+    Wrapper for implementing the solver interface
+    using a tactic.
+
+    This is a light version of the strategic solver.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#include"tactic2solver.h"
+#include"params2front_end_params.h"
+#include"ast_smt2_pp.h"
+
+tactic2solver::ctx::ctx(ast_manager & m, symbol const & logic):
+    m_logic(logic),
+    m_assertions(m) {
+}
+
+tactic2solver::~tactic2solver() {
+}
+
+void tactic2solver::init(ast_manager & m, symbol const & logic) {
+    m_ctx = alloc(ctx, m, logic);
+}
+
+void tactic2solver::updt_params(params_ref const & p) {
+    m_params = p;
+}
+
+void tactic2solver::collect_param_descrs(param_descrs & r) {
+    if (m_ctx) {
+        if (!m_ctx->m_tactic) {
+            #pragma omp critical (tactic2solver)
+            {
+                m_ctx->m_tactic = get_tactic(m_ctx->m(), m_params);
+            }
+
+            if (m_ctx->m_tactic) {
+                m_ctx->m_tactic->collect_param_descrs(r);
+            }
+
+            #pragma omp critical (tactic2solver)
+            {
+                m_ctx->m_tactic = 0;
+            }
+        }
+        else {
+            m_ctx->m_tactic->collect_param_descrs(r);
+        }
+    }
+}
+
+void tactic2solver::reset() {
+    SASSERT(m_ctx);
+    m_ctx->m_assertions.reset();
+    m_ctx->m_scopes.reset();
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver::assert_expr(expr * t) {
+    SASSERT(m_ctx);
+    m_ctx->m_assertions.push_back(t);
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver::push() {
+    SASSERT(m_ctx);
+    m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver::pop(unsigned n) {
+    SASSERT(m_ctx);
+    unsigned new_lvl = m_ctx->m_scopes.size() - n;
+    unsigned old_sz  = m_ctx->m_scopes[new_lvl];
+    m_ctx->m_assertions.shrink(old_sz);
+    m_ctx->m_scopes.shrink(new_lvl);
+    m_ctx->m_result = 0;
+}
+
+unsigned tactic2solver::get_scope_level() const {
+    SASSERT(m_ctx);
+    return m_ctx->m_scopes.size();
+}
+
+lbool tactic2solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    SASSERT(m_ctx);
+    ast_manager & m = m_ctx->m();
+    params_ref p = m_params;
+    if (m_fparams)
+        front_end_params2params(*m_fparams, p);
+    #pragma omp critical (tactic2solver)
+    {
+        m_ctx->m_tactic = get_tactic(m, p);
+        if (m_ctx->m_tactic) {
+            m_ctx->m_result = alloc(simple_check_sat_result, m);
+        }
+    }
+    if (!m_ctx->m_tactic)
+        return l_undef;
+    tactic & t                       = *(m_ctx->m_tactic);
+    simple_check_sat_result & result = *(m_ctx->m_result);
+    if (m_fparams)
+        t.set_front_end_params(*m_fparams);
+    goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
+    t.set_logic(m_ctx->m_logic);
+    unsigned sz = m_ctx->m_assertions.size();
+    for (unsigned i = 0; i < sz; i++) {
+        g->assert_expr(m_ctx->m_assertions.get(i));
+    }
+    for (unsigned i = 0; i < num_assumptions; i++) {
+        g->assert_expr(assumptions[i], m.mk_asserted(assumptions[i]), m.mk_leaf(assumptions[i]));
+    }
+
+    model_ref           md;
+    proof_ref           pr(m);
+    expr_dependency_ref core(m);
+    std::string         reason_unknown = "unknown";
+    try {
+        switch (::check_sat(t, g, md, pr, core, reason_unknown)) {
+        case l_true: 
+            result.set_status(l_true);
+            break;
+        case l_false: 
+            result.set_status(l_false);
+            break;
+        default: 
+            result.set_status(l_undef);
+            if (reason_unknown != "")
+                result.m_unknown = reason_unknown;
+            break;
+        }
+    }
+    catch (z3_error & ex) {
+        throw ex;
+    }
+    catch (z3_exception & ex) {
+        TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
+        result.set_status(l_undef);
+        result.m_unknown = ex.msg();
+    }
+    t.collect_statistics(result.m_stats);
+    result.m_model = md;
+    result.m_proof = pr;
+    if (m_produce_unsat_cores) {
+        ptr_vector<expr> core_elems;
+        m.linearize(core, core_elems);
+        result.m_core.append(core_elems.size(), core_elems.c_ptr());
+    }
+    
+    #pragma omp critical (tactic2solver)
+    {
+        m_ctx->m_tactic = 0;
+    }
+    return result.status();
+}
+
+void tactic2solver::set_cancel(bool f) {
+    #pragma omp critical (tactic2solver)
+    {
+        if (m_ctx && m_ctx->m_tactic)
+            m_ctx->m_tactic->set_cancel(f);
+    }
+}
+
+void tactic2solver::collect_statistics(statistics & st) const {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->collect_statistics(st);
+}
+
+void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->get_unsat_core(r);
+}
+
+void tactic2solver::get_model(model_ref & m) {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->get_model(m);
+}
+
+proof * tactic2solver::get_proof() {
+    if (m_ctx->m_result.get())
+        return m_ctx->m_result->get_proof();
+    else
+        return 0;
+}
+
+std::string tactic2solver::reason_unknown() const {
+    if (m_ctx->m_result.get())
+        return m_ctx->m_result->reason_unknown();
+    else
+        return std::string("unknown");
+}
+
+unsigned tactic2solver::get_num_assertions() const {
+    if (m_ctx) 
+        return m_ctx->m_assertions.size();
+    else
+        return 0;
+}
+
+expr * tactic2solver::get_assertion(unsigned idx) const {
+    SASSERT(m_ctx);
+    return m_ctx->m_assertions.get(idx);
+}
+
+void tactic2solver::display(std::ostream & out) const {
+    if (m_ctx) {
+        ast_manager & m = m_ctx->m_assertions.m();
+        unsigned num = m_ctx->m_assertions.size();
+        out << "(solver";
+        for (unsigned i = 0; i < num; i++) {
+            out << "\n  " << mk_ismt2_pp(m_ctx->m_assertions.get(i), m, 2);
+        }
+        out << ")";
+    }
+    else {
+        out << "(solver)";
+    }
+}
+
+void tactic2solver_cmd::set_tactic(tactic_factory * f) {
+    m_tactic_factory = f;
+}
+
+tactic * tactic2solver_cmd::get_tactic(ast_manager & m, params_ref const & p) {
+    if (m_tactic_factory == 0)
+        return 0;
+    return (*m_tactic_factory)(m, p);
+}
+
+tactic * tactic2solver_api::get_tactic(ast_manager & m, params_ref const & p) {
+    m_tactic->cleanup();
+    m_tactic->updt_params(p);
+    return m_tactic.get();
+}
+

src/framework/tactic2solver.h

@@ -0,0 +1,110 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic2solver.h
+
+Abstract:
+
+    Wrapper for implementing the external solver interface
+    using a tactic.
+
+    This is a light version of the strategic solver.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#ifndef _TACTIC2SOLVER_H_
+#define _TACTIC2SOLVER_H_
+
+#include"solver.h"
+#include"tactic.h"
+
+class tactic2solver : public solver {
+    struct ctx {
+        symbol                       m_logic;
+        expr_ref_vector              m_assertions;
+        unsigned_vector              m_scopes;
+        ref<simple_check_sat_result> m_result;
+        tactic_ref                   m_tactic;
+        ctx(ast_manager & m, symbol const & logic);
+        ast_manager & m() const { return m_assertions.m(); }
+    };
+    scoped_ptr<ctx>            m_ctx;
+    front_end_params *         m_fparams;
+    params_ref                 m_params;
+    bool                       m_produce_models;
+    bool                       m_produce_proofs;
+    bool                       m_produce_unsat_cores;
+public:
+    tactic2solver():m_ctx(0), m_fparams(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {}
+    virtual ~tactic2solver();
+
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p) = 0;
+    
+    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; } 
+
+    virtual void updt_params(params_ref const & p);
+    virtual void collect_param_descrs(param_descrs & r);
+
+    virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
+    virtual void set_produce_models(bool f) { m_produce_models = f; }
+    virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
+
+    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void reset();
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual unsigned get_scope_level() const;
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+
+    virtual void set_cancel(bool f);
+
+    virtual void collect_statistics(statistics & st) const;
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r) {}
+
+    virtual void set_progress_callback(progress_callback * callback) {}
+
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+
+    virtual void display(std::ostream & out) const;
+};
+
+/**
+   \brief Specialization for cmd_context
+*/
+class tactic2solver_cmd : public tactic2solver {
+    scoped_ptr<tactic_factory> m_tactic_factory;
+public:
+    virtual ~tactic2solver_cmd() {}
+    /**
+       \brief Set tactic that will be used to process the satisfiability queries.
+    */
+    void set_tactic(tactic_factory * f); 
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+/**
+   \brief Specialization for API
+*/
+class tactic2solver_api : public tactic2solver {
+    tactic_ref m_tactic;
+public:
+    tactic2solver_api(tactic * t):m_tactic(t) {}
+    virtual ~tactic2solver_api() {}
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+
+#endif