summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2020-03-05 13:21:43 -0800
committerAina Niemetz <aina.niemetz@gmail.com>2020-03-05 13:21:43 -0800
commit50f82fac417bc5b27ecaeb34d4e8034339c5982f (patch)
tree981c352e9aae8c96539374e98065101ee3835b28 /src/theory/theory_engine.h
parenta4151cb6755b9267cb90f7facc0ffd367aa7f0f2 (diff)
Move ownership of DecisionEngine into PropEngine. (#3850)
This is in preparation of fixing the issue we currently have with reset-assertions. This also removes a competition hack for QF_LRA.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h9
1 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1757d7a6d..e8223f1a1 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -101,7 +101,6 @@ namespace theory {
class EntailmentCheckSideEffects;
}/* CVC4::theory namespace */
-class DecisionEngine;
class RemoveTermFormulas;
/**
@@ -119,9 +118,6 @@ class TheoryEngine {
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
- /** Access to decision engine */
- DecisionEngine* d_decisionEngine;
-
/** Our context */
context::Context* d_context;
@@ -505,11 +501,6 @@ class TheoryEngine {
d_propEngine = propEngine;
}
- inline void setDecisionEngine(DecisionEngine* decisionEngine) {
- Assert(d_decisionEngine == NULL);
- d_decisionEngine = decisionEngine;
- }
-
/** Called when all initialization of options/logic is done */
void finishInit();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback