diff options
Diffstat (limited to 'src/smt/logic_request.h')
-rw-r--r-- | src/smt/logic_request.h | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h index 4985b0e65..8aad440c6 100644 --- a/src/smt/logic_request.h +++ b/src/smt/logic_request.h @@ -27,10 +27,11 @@ #define __CVC4__LOGIC_REQUEST_H #include "expr/kind.h" -#include "smt/smt_engine.h" namespace CVC4 { +class SmtEngine; + class LogicRequest { /** The SmtEngine at play. */ SmtEngine& d_smt; @@ -39,12 +40,7 @@ public: LogicRequest(SmtEngine& smt) : d_smt(smt) { } /** Widen the logic to include the given theory. */ - void widenLogic(theory::TheoryId id) { - d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(id); - d_smt.d_logic.lock(); - } + void widenLogic(theory::TheoryId id); };/* class LogicRequest */ |