projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 27fb04b) | patch
Improve arithmetic proofs (#6106)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 10 Mar 2021 20:48:13 +0000 (21:48 +0100)
committerGitHub <noreply@github.com>
Wed, 10 Mar 2021 20:48:13 +0000 (20:48 +0000)
commitbd52deb7434b1b08a122db4513972644c11fc4aa
tree44cd11cde22fe7f20a281c8d9092de219547c6fbtree
parent27fb04bc96999e101b45458c549345e864e085e9commit | diff
Improve arithmetic proofs (#6106)

The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.
src/expr/proof_rule.h diff | blob | history
src/theory/arith/nl/ext/monomial_bounds_check.cpp diff | blob | history
src/theory/arith/nl/ext/proof_checker.cpp diff | blob | history