diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 14:01:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 16:01:39 -0300 |
| commit | c17f9b25cac7c0d2941ef136466cb750cf4c3e7b (patch) | |
| tree | 95abb34573b6fd33e2215a7b2cfafc2f27281054 /src/theory/rewriter.cpp | |
| parent | a692d44ed5ba0107113df54d2654417bc9f9c345 (diff) | |
(proof-new) Add proof support in TheoryUF (#5002)
This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.
This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
Diffstat (limited to 'src/theory/rewriter.cpp')
0 files changed, 0 insertions, 0 deletions