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 | |
| parent | 29744e3da7abba18ca58f6a21ff2f5c300fbe241 (diff) | |
Separating an implicit inclusion of smt_engine.h from theory.h.
| -rw-r--r-- | src/Makefile.am | 1 | ||||
| -rw-r--r-- | src/smt/logic_request.cpp | 17 | ||||
| -rw-r--r-- | src/smt/logic_request.h | 10 |
3 files changed, 21 insertions, 7 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 539afc781..ae7cb619a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -117,6 +117,7 @@ libcvc4_la_SOURCES = \ smt/boolean_terms.cpp \ smt/logic_exception.h \ smt/logic_request.h \ + smt/logic_request.cpp \ smt/simplification_mode.h \ smt/simplification_mode.cpp \ smt/options_handlers.h \ diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp new file mode 100644 index 000000000..a0b6d2bb9 --- /dev/null +++ b/src/smt/logic_request.cpp @@ -0,0 +1,17 @@ + + +#include "smt/logic_request.h" +#include "smt/smt_engine.h" + + +namespace CVC4 { + +/** Widen the logic to include the given theory. */ +void LogicRequest::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(); +} + +}/* CVC4 namespace */ 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 */ |