projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d99fc91) | patch
Types and side conditions for affine bounds (#3631)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 21 Jan 2020 23:05:52 +0000 (15:05 -0800)
committerGitHub <noreply@github.com>
Tue, 21 Jan 2020 23:05:52 +0000 (15:05 -0800)
commit3de5e8df6a6adcd0efe51db9d9eadad284ad3a64
tree0405a366343689b610e988841a924c29b9fd6841tree
parentd99fc9153d8260cfc6dd2aa7d2a2ea96ab5c4925commit | diff
Types and side conditions for affine bounds (#3631)

* Types and side conditions for affine bounds

Bounds (being positive, non-negative) actually have an arithmetic.
This PR defines that.

Useful b/c Farkas proofs are basically just sums of bounded affine
functions.

* Address Yoni's comments. Thanks!

* Moved a positivity-test to th_real
* Describe what an affine bound is in better detail
proofs/signatures/th_lira.plf diff | blob | history
proofs/signatures/th_real.plf diff | blob | history