diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 20:02:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-11 20:02:33 -0500 |
commit | 383d061be2bc8162d3379c98ad106555d21e5f86 (patch) | |
tree | 56ae66e579cbadbe465a7f2617328df83ab9630b /src/prop/theory_proxy.cpp | |
parent | b7bbe9a3bc30f41d1775a187ccc732aaeb41eaa1 (diff) |
(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.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d0ba4ca71..8165c5d8a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -76,7 +76,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - Node theoryExplanation = d_theoryEngine->getExplanation(lNode); + theory::TrustNode texp = d_theoryEngine->getExplanation(lNode); + Node theoryExplanation = texp.getNode(); if (options::unsatCores()) { |