From 383d061be2bc8162d3379c98ad106555d21e5f86 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Sep 2020 20:02:33 -0500 Subject: (proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056) This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node. This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR. --- src/theory/combination_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/combination_engine.cpp') diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index f1e977fe3..5c9e6713b 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -113,7 +113,7 @@ eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify() void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo) { - d_te.lemma(trn.getNode(), false, LemmaProperty::NONE, atomsTo); + d_te.lemma(trn, LemmaProperty::NONE, atomsTo); } void CombinationEngine::resetRound() -- cgit v1.2.3