diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-03 19:15:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 19:15:30 -0500 |
commit | a5b834d5af88e372d9c6340653f831a09daf1d39 (patch) | |
tree | 13b998f9887589f9f9d5f0619a0139d982d7e3b8 /src/theory/bv/theory_bv.cpp | |
parent | 0fe081a56db369372584a5fcd35a4c4e4fb1c23f (diff) |
Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)
This gives theories a finer grained control over explained lemmas and conflicts.
A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma.
This is required for the new strings inference manager on proof-new.
This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer.
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
0 files changed, 0 insertions, 0 deletions