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.cpp | |
parent | 29744e3da7abba18ca58f6a21ff2f5c300fbe241 (diff) |
Separating an implicit inclusion of smt_engine.h from theory.h.
Diffstat (limited to 'src/smt/logic_request.cpp')
-rw-r--r-- | src/smt/logic_request.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
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 */ |