From 37fab88de006c6b625d9d67f4b94fff8da42716f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Aug 2022 18:16:43 -0700
Subject: [PATCH] respect dependencies, move proof_cmds to extra_cmds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/cmd_context/cmd_context.h | 6 ++----
src/shell/smtlib_frontend.cpp | 2 +-
2 files changed, 3 insertions(+), 5 deletions(-)
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 36ee3c1ca..512e367ef 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -39,7 +39,6 @@ Notes:
#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 @@ public:
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 @@ public:
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
index 7c81d2211..d0d0b452d 100644
--- 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"