projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c3bc4ac) | patch
Axioms (and side conditions) for tightening bounds (#3613)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 21 Jan 2020 15:45:10 +0000 (07:45 -0800)
committerGitHub <noreply@github.com>
Tue, 21 Jan 2020 15:45:10 +0000 (07:45 -0800)
commit2f46d30ea76158dec2118e35086290ae7ddceedf
treecbb89afe1b25a1cac031bde2e454589e4e4a3a43tree
parentc3bc4ac99c36029b78d866ffb89bd0d322821f34commit | diff
Axioms (and side conditions) for tightening bounds (#3613)

* Axioms (and side conditions) for tightening bounds

* Side conditions for verifying floor/ceiling-like functions
* Axioms for their correct execution
* Axioms for bound tightening.

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Address Yoni's comments by addings documentation.

Thanks Yoni!

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
proofs/signatures/th_lira.plf diff | blob | history