diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-10 10:50:28 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-10 12:50:28 -0600 |
| commit | 5c7d51d9195d94edcf422f8f81b417077b2c460c (patch) | |
| tree | 5c2e35568d24b2f49846a91a4b9d60647d592d76 /proofs/signatures/th_lira.plf | |
| parent | aa18f9e6a3ef18071af3636871dc62c8ec0227b2 (diff) | |
Add more IntReal predicates (#3731)
Diffstat (limited to 'proofs/signatures/th_lira.plf')
| -rw-r--r-- | proofs/signatures/th_lira.plf | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index 145980b24..a5b73d6b4 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -59,8 +59,14 @@ ((/_Real x y) (/_Real (reify_real_term x) (reify_real_term y))) )) -; Predicates of the form (term Integer) >= (term Real) or negations thereof -(declare >=_IntReal (! x (term Int) (! y (term Real) formula))) +; Predicates of the form (term Integer) (comparison) (term Real) +(define arithpred_IntReal (! x (term Int) + (! y (term Real) + formula))) +(declare >_IntReal arithpred_IntReal) +(declare >=_IntReal arithpred_IntReal) +(declare <_IntReal arithpred_IntReal) +(declare <=_IntReal arithpred_IntReal) ; From an arith predicate, compute the equivalent real predicate ; All arith predicates are (possibly negated) >='s with a real on the right. |