projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4f5abe1) | patch
(proof-new) Prove lemmas in Constraint (#5254)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 14 Oct 2020 04:15:25 +0000 (21:15 -0700)
committerGitHub <noreply@github.com>
Wed, 14 Oct 2020 04:15:25 +0000 (23:15 -0500)
commit9be90e37556d0654d7b7565ba6a62ba46eb44ccd
treea3761c17350681ee1bd8a86863cf19b04ad2856btree
parent4f5abe126235843cf17e83c7e1e29c91225573cacommit | 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 :).
src/theory/arith/constraint.cpp diff | blob | history
src/theory/arith/constraint.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.h diff | blob | history