From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Sat, 18 Jan 2020 00:56:44 +0000 (-0800)
Subject: LIRA proof: Arithmetic predicates & reification thereof (#3612)
X-Git-Tag: cvc5-1.0.0~3731
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3bc4ac99c36029b78d866ffb89bd0d322821f34;p=cvc5.git

LIRA proof: Arithmetic predicates & reification thereof (#3612)

* Merge branch 'master' into lira-pf-arith-pred

* Shorten reify_arith_pred, thanks Yoni!

Use recursion!

* typo
---

diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf
index 5f6869051..25a7ac1fd 100644
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -33,7 +33,7 @@
     ((u-_Int x) (u-_Real (reify_int_term x)))
     ((*_Int x y) (*_Real (reify_int_term x) (reify_int_term y)))
     ; Reifying integer division is an error, since it changes the value!
-    ((/_Int x y) (fail Real))
+    ((/_Int x y) (fail (term Real)))
   ))
 
 ; This function recursively converts a real term to a real term.
@@ -52,3 +52,17 @@
     ((/_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)))
+
+; From an arith predicate, compute the equivalent real predicate
+; All arith predicates are (possibly negated) >='s with a real on the right.
+; Technically it's a real literal on the right, but we don't assume that here.
+(program reify_arith_pred ((p formula)) formula
+  (match p
+         ((not p') (not (reify_arith_pred p')))
+         ((>=_Real x y) (>=_Real (reify_real_term x) (reify_real_term y)))
+         ((>=_Int x y) (>=_Real (reify_int_term x) (reify_int_term y)))
+         ((>=_IntReal x y) (>=_Real (reify_int_term x) (reify_real_term y)))
+         (default (fail formula))
+         ))