(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 12 Sep 2020 01:02:33 +0000 (20:02 -0500)
committerGitHub <noreply@github.com>
Sat, 12 Sep 2020 01:02:33 +0000 (20:02 -0500)
commit383d061be2bc8162d3379c98ad106555d21e5f86
tree56ae66e579cbadbe465a7f2617328df83ab9630b
parentb7bbe9a3bc30f41d1775a187ccc732aaeb41eaa1
(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/prop/theory_proxy.cpp
src/theory/combination_engine.cpp
src/theory/engine_output_channel.cpp
src/theory/shared_terms_database.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h