projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7a695fd) | patch
Add proof for monomial bounds check (#5965)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 23 Feb 2021 16:51:53 +0000 (17:51 +0100)
committerGitHub <noreply@github.com>
Tue, 23 Feb 2021 16:51:53 +0000 (17:51 +0100)
commitb4c832ab30dafe048334c6e47642aa12619357ef
treeb37829eb546c49fd2921a3bd841db12e6f066408tree
parent7a695fd7c29af97dbcc363eb277ffeae1617cffecommit | diff
Add proof for monomial bounds check (#5965)

This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.
src/expr/proof_rule.cpp diff | blob | history
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