diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-11 11:23:15 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-11 11:23:15 -0600 |
| commit | 8c04f1639607b34b56e3eaa8d3188b27e1454b41 (patch) | |
| tree | b4427f298b2fde0686b7fdd98008f2fdc0173321 /src/prop/theory_proxy.cpp | |
| parent | b8841e768a37131c492508cd0e12b9acd8bf4c2b (diff) | |
Merge theory registrar and theory proxy (#5758)
The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.
This merges the helper class TheoryRegistrar into TheoryProxy.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
| -rw-r--r-- | src/prop/theory_proxy.cpp | 7 |
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 */ |