respect dependencies, move proof_cmds to extra_cmds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 29, 2022 · 37fab88 · 37fab88
1 parent f65a244
commit 37fab88
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
@@ -39,7 +39,6 @@ Module Name:
 #include "solver/progress_callback.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
-#include "cmd_context/proof_cmds.h"
 #include "params/context_params.h"
 
 
@@ -94,8 +93,7 @@ class macro_decls {
 
 class proof_cmds {
 public:
-    proof_cmds(ast_manager& m);
-    virtual ~proof_cmds();
+    virtual ~proof_cmds() {}
     virtual void add_literal(expr* e) = 0;
     virtual void end_assumption() = 0;
     virtual void end_learned() = 0;
@@ -412,7 +410,7 @@ 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() { return m_proof_cmds; }
+    proof_cmds* get_proof_cmds() { return m_proof_cmds.get(); }
     void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
 
     void set_solver_factory(solver_factory * s);

diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
@@ -26,7 +26,7 @@ Revision History:
 #include "parsers/smt2/smt2parser.h"
 #include "muz/fp/dl_cmds.h"
 #include "cmd_context/extra_cmds/dbg_cmds.h"
-#include "cmd_context/proof_cmds.h"
+#include "cmd_context/extra_cmds/proof_cmds.h"
 #include "opt/opt_cmds.h"
 #include "cmd_context/extra_cmds/polynomial_cmds.h"
 #include "cmd_context/extra_cmds/subpaving_cmds.h"