diff options
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 4a95591b4..e509bf182 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -53,26 +53,16 @@ TheoryProxy::~TheoryProxy() { void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; } -void TheoryProxy::notifyPreprocessedAssertions( - const std::vector<Node>& assertions) -{ - d_theoryEngine->notifyPreprocessedAssertions(assertions); - for (const Node& assertion : assertions) - { - d_decisionEngine->addAssertion(assertion); - } -} - -void TheoryProxy::notifyAssertion(Node lem, TNode skolem) +void TheoryProxy::notifyAssertion(Node a, TNode skolem) { if (skolem.isNull()) { - d_decisionEngine->addAssertion(lem); + d_decisionEngine->addAssertion(a); } else { - d_skdm->notifySkolemDefinition(skolem, lem); - d_decisionEngine->addSkolemDefinition(lem, skolem); + d_skdm->notifySkolemDefinition(skolem, a); + d_decisionEngine->addSkolemDefinition(a, skolem); } } |