projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1e58294) | patch
Add proof for mult sign lemma (#5966)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 23 Feb 2021 18:31:28 +0000 (19:31 +0100)
committerGitHub <noreply@github.com>
Tue, 23 Feb 2021 18:31:28 +0000 (12:31 -0600)
commitf956c6b5cf9a4d836ebcd99ef57558b9b11f4d29
treee2fdba4a57678e56b90beab4913f5db129ee0a76tree
parent1e58294a927f8c3067ea0feaad0d891f82f42ebecommit | diff
Add proof for mult sign lemma (#5966)

This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/arith/nl/ext/monomial_check.cpp diff | blob | history
src/theory/arith/nl/ext/proof_checker.cpp diff | blob | history