From d2a97a6174c0f6290428564a3ac26ec9fe94ff1f Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 26 Apr 2019 12:03:15 -0700
Subject: [PATCH] [sledge] Use integer or float constants as needed in Exp
 normalization

Summary:
Some constants are used during Exp normalization, to encode
subtraction using addition, units of addition and multiplication,
etc. Previously these were unconditionally integers, but need to be
floats for float arithmetic.

Reviewed By: mbouaziz

Differential Revision: D15098815

fbshipit-source-id: 13d1be142
---
 sledge/src/llair/exp.ml | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 44fd72935..bd66ce88b 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -655,6 +655,15 @@ let null = integer Z.zero Typ.ptr
 let bool b = integer (Z.of_bool b) Typ.bool
 let float data = Float {data} |> check invariant
 
+let zero (typ : Typ.t) =
+  match typ with Float _ -> float "0" | _ -> integer Z.zero typ
+
+let one (typ : Typ.t) =
+  match typ with Float _ -> float "1" | _ -> integer Z.one typ
+
+let minus_one (typ : Typ.t) =
+  match typ with Float _ -> float "-1" | _ -> integer Z.minus_one typ
+
 let simp_convert signed (dst : Typ.t) src arg =
   match (dst, arg) with
   | _ when Typ.equal dst src -> arg
@@ -720,7 +729,7 @@ let sum_mul_const const sum =
 
 let rec sum_to_exp typ sum =
   match Qset.length sum with
-  | 0 -> integer Z.zero typ
+  | 0 -> zero typ
   | 1 -> (
     match Qset.min_elt sum with
     | Some (Integer _, q) -> rational q typ
@@ -817,7 +826,7 @@ let rec simp_add_ typ es poly =
   in
   Qset.fold ~f es ~init:poly
 
-let simp_add typ es = simp_add_ typ es (integer Z.zero typ)
+let simp_add typ es = simp_add_ typ es (zero typ)
 let simp_add2 typ e f = simp_add_ typ (Sum.singleton e) f
 
 (* Products of indeterminants represented by multisets. A product ∏ᵢ xᵢ^nᵢ
@@ -876,12 +885,12 @@ let simp_mul typ es =
     if Q.equal Q.zero pwr then exp
     else mul_pwr bas Q.(pwr - one) (simp_mul2 typ bas exp)
   in
-  let one = integer Z.one typ in
+  let one = one typ in
   Qset.fold es ~init:one ~f:(fun bas pwr exp ->
       if Q.sign pwr >= 0 then mul_pwr bas pwr exp
       else simp_div exp (mul_pwr bas (Q.neg pwr) one) )
 
-let simp_negate typ x = simp_mul2 typ (integer Z.minus_one typ) x
+let simp_negate typ x = simp_mul2 typ (minus_one typ) x
 
 let simp_sub typ x y =
   match (x, y) with
@@ -1345,7 +1354,7 @@ let solve e f =
           let d = rational (Q.neg q) typ in
           let r = div n d in
           Some (Map.add_exn s ~key:c ~data:r)
-      | e_f -> solve_uninterp e_f (integer Z.zero typ) )
+      | e_f -> solve_uninterp e_f (zero typ) )
     | Concat {args= ms}, Concat {args= ns} -> (
       match (concat_size ms, concat_size ns) with
       | Some p, Some q -> solve_uninterp e f >>= solve_ p q