move proof_cmds

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/cmd_context/CMakeLists.txt

@@ -11,7 +11,6 @@ z3_add_component(cmd_context
     simplify_cmd.cpp
     tactic_cmds.cpp
     tactic_manager.cpp
-    proof_cmds.cpp
   COMPONENT_DEPENDENCIES
     rewriter
     solver

src/cmd_context/cmd_context.h

@@ -91,6 +91,18 @@ class macro_decls {
     vector<macro_decl>::iterator end() const { return m_decls->end(); }
 };
 
+
+class proof_cmds {
+public:
+    proof_cmds(ast_manager& m);
+    virtual ~proof_cmds();
+    virtual void add_literal(expr* e) = 0;
+    virtual void end_assumption() = 0;
+    virtual void end_learned() = 0;
+    virtual void end_deleted() = 0;
+};
+
+
 /**
    \brief Generic wrapper.
 */
@@ -400,7 +412,8 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
 
-    proof_cmds& get_proof_cmds() { if (!m_proof_cmds) m_proof_cmds = proof_cmds::mk(m()); return *m_proof_cmds; }
+    proof_cmds* get_proof_cmds() { return m_proof_cmds; }
+    void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
 
     void set_solver_factory(solver_factory * s);
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }

src/cmd_context/extra_cmds/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(extra_cmds
     dbg_cmds.cpp
     polynomial_cmds.cpp
     subpaving_cmds.cpp
+    proof_cmds.cpp
   COMPONENT_DEPENDENCIES
     arith_tactics
     cmd_context

src/cmd_context/proof_cmds.cpp → src/cmd_context/extra_cmds/proof_cmds.cpp

@@ -24,9 +24,9 @@ Module Name:
 #include "util/small_object_allocator.h"
 #include "ast/ast_util.h"
 #include "cmd_context/cmd_context.h"
-#include "smt/smt_solver.h"
-#include "sat/sat_solver.h"
-#include "sat/sat_drat.h"
+// include "smt/smt_solver.h"
+// include "sat/sat_solver.h"
+// include "sat/sat_drat.h"
 #include "sat/smt/euf_proof_checker.h"
 #include <iostream>
 
@@ -57,7 +57,7 @@ class smt_checker {
         // sat_solver(m_params, m.limit()), 
         // m_drat(sat_solver) 
     {
-        m_solver = mk_smt_solver(m, m_params, symbol());
+//        m_solver = mk_smt_solver(m, m_params, symbol());
     }
 
     void check(expr_ref_vector const& clause, expr* proof_hint) {
@@ -94,22 +94,22 @@ class smt_checker {
     }
 };
 
-class proof_cmds::imp {
+class proof_cmds_imp : public proof_cmds {
     ast_manager& m;
     expr_ref_vector m_lits;
     expr_ref m_proof_hint;
     smt_checker m_checker;
 public:
-    imp(ast_manager& m): m(m), m_lits(m), m_proof_hint(m), m_checker(m) {}
+    proof_cmds_imp(ast_manager& m): m(m), m_lits(m), m_proof_hint(m), m_checker(m) {}
 
-    void add_literal(expr* e) {
+    void add_literal(expr* e) override {
         if (m.is_proof(e))
             m_proof_hint = e;
         else
             m_lits.push_back(e);
     }
 
-    void end_assumption() {
+    void end_assumption() override {
         m_checker.assume(m_lits);
         m_lits.reset();
         m_proof_hint.reset();
@@ -127,32 +127,11 @@ class proof_cmds::imp {
     }
 };
 
-proof_cmds* proof_cmds::mk(ast_manager& m) {
-    return alloc(proof_cmds, m);
-}
-
-proof_cmds::proof_cmds(ast_manager& m) {
-    m_imp = alloc(imp, m);
-}
-
-proof_cmds::~proof_cmds() {
-    dealloc(m_imp);
-}
-
-void proof_cmds::add_literal(expr* e) {
-    m_imp->add_literal(e);
-}
-
-void proof_cmds::end_assumption() {
-    m_imp->end_assumption();
-}
-
-void proof_cmds::end_learned() {
-    m_imp->end_learned();
-}
 
-void proof_cmds::end_deleted() {
-    m_imp->end_deleted();
+static proof_cmds& get(cmd_context& ctx) {
+    if (!ctx.get_proof_cmds())
+        ctx.set_proof_cmds(alloc(proof_cmds_imp, ctx.m()));
+    return *ctx.get_proof_cmds();
 }
 
 // assumption
@@ -166,8 +145,8 @@ class assume_cmd : public cmd {
     void finalize(cmd_context & ctx) override {}
     void failure_cleanup(cmd_context & ctx) override {}
     cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }    
-    void set_next_arg(cmd_context & ctx, expr * arg) override { ctx.get_proof_cmds().add_literal(arg); }
-    void execute(cmd_context& ctx) override { ctx.get_proof_cmds().end_assumption(); }
+    void set_next_arg(cmd_context & ctx, expr * arg) override { get(ctx).add_literal(arg); }
+    void execute(cmd_context& ctx) override { get(ctx).end_assumption(); }
 };
 
 // deleted clause
@@ -181,23 +160,23 @@ class del_cmd : public cmd {
     void finalize(cmd_context & ctx) override {}
     void failure_cleanup(cmd_context & ctx) override {}
     cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }    
-    void set_next_arg(cmd_context & ctx, expr * arg) override { ctx.get_proof_cmds().add_literal(arg); }
-    void execute(cmd_context& ctx) override { ctx.get_proof_cmds().end_deleted(); }
+    void set_next_arg(cmd_context & ctx, expr * arg) override { get(ctx).add_literal(arg); }
+    void execute(cmd_context& ctx) override { get(ctx).end_deleted(); }
 };
 
 // learned/redundant clause
 class learn_cmd : public cmd {
 public:
     learn_cmd():cmd("learn") {}
     char const* get_usage() const override { return "<expr>+"; }
-    char const * get_descr(cmd_context& ctx) const override { return "proof command for learned (redundant) clauses"; }
+    char const* get_descr(cmd_context& ctx) const override { return "proof command for learned (redundant) clauses"; }
     unsigned get_arity() const override { return VAR_ARITY; }
     void prepare(cmd_context & ctx) override {}
     void finalize(cmd_context & ctx) override {}
     void failure_cleanup(cmd_context & ctx) override {}
     cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }    
-    void set_next_arg(cmd_context & ctx, expr * arg) override { ctx.get_proof_cmds().add_literal(arg); }
-    void execute(cmd_context& ctx) override { ctx.get_proof_cmds().end_learned(); }
+    void set_next_arg(cmd_context & ctx, expr * arg) override { get(ctx).add_literal(arg); }
+    void execute(cmd_context& ctx) override { get(ctx).end_learned(); }
 };
 
 void install_proof_cmds(cmd_context & ctx) {

src/cmd_context/proof_cmds.h → src/cmd_context/extra_cmds/proof_cmds.h

@@ -31,19 +31,6 @@ Module Name:
 */
 
 
-class proof_cmds {
-    class imp;
-    imp* m_imp;
-public:
-    static proof_cmds* mk(ast_manager& m);
-    proof_cmds(ast_manager& m);
-    ~proof_cmds();
-    void add_literal(expr* e);
-    void end_assumption();
-    void end_learned();
-    void end_deleted();
-};
-
 class cmd_context;
 void install_proof_cmds(cmd_context & ctx);