summaryrefslogtreecommitdiff
path: root/src/smt/logic_request.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/logic_request.h')
-rw-r--r--src/smt/logic_request.h10
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback