From c3bc4ac99c36029b78d866ffb89bd0d322821f34 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 17 Jan 2020 16:56:44 -0800 Subject: LIRA proof: Arithmetic predicates & reification thereof (#3612) * Merge branch 'master' into lira-pf-arith-pred * Shorten reify_arith_pred, thanks Yoni! Use recursion! * typo --- proofs/signatures/th_lira.plf | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) 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)) + )) -- cgit v1.2.3