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/theory/shared_terms_database.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/theory/shared_terms_database.cpp')
| -rw-r--r-- | src/theory/shared_terms_database.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index a196d0ed0..b01cef377 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -251,7 +251,8 @@ void SharedTermsDatabase::checkForConflict() { std::vector<TNode> assumptions; d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions); Node conflict = mkAnd(assumptions); - d_theoryEngine->conflict(conflict, THEORY_BUILTIN); + TrustNode tconf = TrustNode::mkTrustConflict(conflict); + d_theoryEngine->conflict(tconf, THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } } |