diff options
| author | Tim King <taking@cs.nyu.edu> | 2014-05-26 11:44:38 -0400 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2014-05-26 11:44:38 -0400 |
| commit | a4ca46db48f8ba450004dd96cce96efbc20b4362 (patch) | |
| tree | c8dfa11d6674b6de5bd26c40cdc4c45e024ad779 /src/smt/logic_request.h | |
| parent | 29744e3da7abba18ca58f6a21ff2f5c300fbe241 (diff) | |
Separating an implicit inclusion of smt_engine.h from theory.h.
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 */ |