summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r--src/prop/theory_proxy.cpp7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 35602b8b3..8e54064e1 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -35,10 +35,9 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
DecisionEngine* decisionEngine,
context::Context* context,
context::UserContext* userContext,
- CnfStream* cnfStream,
ProofNodeManager* pnm)
: d_propEngine(propEngine),
- d_cnfStream(cnfStream),
+ d_cnfStream(nullptr),
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
d_queue(context),
@@ -50,6 +49,8 @@ TheoryProxy::~TheoryProxy() {
/* nothing to do for now */
}
+void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
+
void TheoryProxy::variableNotify(SatVariable var) {
d_theoryEngine->preRegister(getNode(SatLiteral(var)));
}
@@ -189,5 +190,7 @@ theory::TrustNode TheoryProxy::preprocess(
return pnode;
}
+void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback