| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
* Axioms for affine function bounds. Tests.
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Clarify descriptions of th_lira tests
Thanks, Yoni!
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
|
|
* 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
|
|
Used for proving that real terms are affine functions of their
variables.
|
|
This commit introduces types for linear combinations of arith variables
along with side conditions for their arithmetic.
It does the same for affine functions.
These primitives are ultimately used in our machinery for Farkas proofs.
|
|
* 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>
|
|
* Merge branch 'master' into lira-pf-arith-pred
* Shorten reify_arith_pred, thanks Yoni!
Use recursion!
* typo
|
|
* LIRA sig: int, real terms, and conversions
* Address Yoni's comments.
* Better description of "reify" functions
* explicit (rather than implicit) `fail` when reifying integer division
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
