From 5c7d51d9195d94edcf422f8f81b417077b2c460c Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 10 Feb 2020 10:50:28 -0800 Subject: [PATCH] Add more IntReal predicates (#3731) --- proofs/signatures/th_lira.plf | 10 ++++++++-- 1 file 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. -- 2.30.2