From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 10 Feb 2020 18:50:28 +0000 (-0800)
Subject: Add more IntReal predicates (#3731)
X-Git-Tag: cvc5-1.0.0~3665
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c7d51d9195d94edcf422f8f81b417077b2c460c;p=cvc5.git

Add more IntReal predicates (#3731)
---

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.