diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-10-13 21:15:25 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-13 23:15:25 -0500 |
| commit | 9be90e37556d0654d7b7565ba6a62ba46eb44ccd (patch) | |
| tree | a3761c17350681ee1bd8a86863cf19b04ad2856b /src/prop/proof_cnf_stream.cpp | |
| parent | 4f5abe126235843cf17e83c7e1e29c91225573ca (diff) | |
(proof-new) Prove lemmas in Constraint (#5254)
Includes:
T/F splitting lemmas for any arith constraint
Unate lemmas produced early on
The hard part is proving the unate lemmas. In general, they are all implied by 2-constraint farkas proofs, so we ultimately map them all down to proveOr, which constructs that proof.
make check was happy with this change. Hopefully the CI agrees :).
Diffstat (limited to 'src/prop/proof_cnf_stream.cpp')
0 files changed, 0 insertions, 0 deletions