[sledge] Remove Funsym.Convert

Summary:
Conversions between types are uninterpreted, so use uninterpreted
function symbols for them.

Reviewed By: jvillard

Differential Revision: D24306077

fbshipit-source-id: 49937fdbb

sledge/src/fol.ml

@@ -1136,8 +1136,6 @@ let rec t_to_ses : trm -> Ses.Term.t = function
       Ses.Term.ashr (t_to_ses x) (t_to_ses y)
   | Apply (Signed n, Tuple [|x|]) -> Ses.Term.signed n (t_to_ses x)
   | Apply (Unsigned n, Tuple [|x|]) -> Ses.Term.unsigned n (t_to_ses x)
-  | Apply (Convert {src; dst}, Tuple [|x|]) ->
-      Ses.Term.convert src ~to_:dst (t_to_ses x)
   | Apply (sym, Tuple xs) ->
       Ses.Term.apply sym (IArray.of_array (Array.map ~f:t_to_ses xs))
   | (Apply _ | Tuple _ | Project _) as t ->
@@ -1229,7 +1227,6 @@ and of_ses : Ses.Term.t -> exp =
   | Rational {data} -> rational data
   | Ap1 (Signed {bits}, e) -> uap_tt (Signed bits) e
   | Ap1 (Unsigned {bits}, e) -> uap_tt (Unsigned bits) e
-  | Ap1 (Convert {src; dst}, e) -> uap_tt (Convert {src; dst}) e
   | Ap2 (Eq, d, e) -> ap2_f iff eq d e
   | Ap2 (Dq, d, e) -> ap2_f xor dq d e
   | Ap2 (Lt, d, e) -> ap2_f (fun p q -> and_ (not_ p) q) lt d e
@@ -1619,7 +1616,11 @@ module Term_of_Llair = struct
           | Some fml -> Formula.inject fml
           | _ -> uap1 (Unsigned bits) a
         else uap1 (Unsigned bits) a
-    | Ap1 (Convert {src}, dst, e) -> uap_te (Convert {src; dst}) e
+    | Ap1 (Convert {src}, dst, e) ->
+        let s =
+          Format.asprintf "convert_%a_%a" Llair.Typ.pp src Llair.Typ.pp dst
+        in
+        uap_te (Uninterp s) e
     | Ap2 (Eq, Integer {bits= 1; _}, p, q) -> ap_fff iff p q
     | Ap2 (Dq, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
     | Ap2 ((Gt | Ugt), Integer {bits= 1; _}, p, q)

sledge/src/ses/funsym.ml

@@ -21,7 +21,6 @@ type t =
   | BitAshr
   | Signed of int
   | Unsigned of int
-  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
   | Uninterp of string
 [@@deriving compare, equal, sexp]
 
@@ -41,5 +40,4 @@ let pp ppf f =
   | BitAshr -> pf "ashr"
   | Signed n -> pf "(s%i)" n
   | Unsigned n -> pf "(u%i)" n
-  | Convert {src; dst} -> pf "(%a)(%a)" Llair.Typ.pp dst Llair.Typ.pp src
   | Uninterp sym -> pf "%s" sym

sledge/src/ses/funsym.mli

@@ -33,7 +33,6 @@ type t =
       (** [Unsigned n] interprets its argument as an [n]-bit unsigned
           integer. That is, it unsigned-binary--decodes the low [n] bits of
           the infinite two's-complement encoding of the argument. *)
-  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
   | Uninterp of string  (** Uninterpreted function symbol *)
 [@@deriving compare, equal, sexp]
 

sledge/src/ses/term.ml

@@ -12,7 +12,6 @@
 type op1 =
   | Signed of {bits: int}
   | Unsigned of {bits: int}
-  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
   | Splat
   | Select of int
 [@@deriving compare, equal, hash, sexp]
@@ -208,13 +207,6 @@ let invariant e =
   | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       assert_sequence e
   | ApN (Record, elts) -> assert (not (IArray.is_empty elts))
-  | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false
-  | Ap1 (Convert {src; dst}, _) ->
-      assert (Llair.Typ.convertible src dst) ;
-      assert (
-        not
-          (Llair.Typ.equivalent src dst)
-          (* avoid redundant representations *) )
   | Rational {data} ->
       assert (Q.is_real data) ;
       assert (not (Z.equal Z.one (Q.den data)))
@@ -258,8 +250,6 @@ let rec ppx strength fs term =
     | Rational {data} -> Trace.pp_styled `Magenta "%a" fs Q.pp data
     | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg
     | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg
-    | Ap1 (Convert {src; dst}, arg) ->
-        pf "((%a)(%a)@ %a)" Llair.Typ.pp dst Llair.Typ.pp src pp arg
     | Ap2 (Eq, x, y) -> pf "(%a@ = %a)" pp x pp y
     | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y
     | Ap2 (Lt, x, y) -> pf "(%a@ < %a)" pp x pp y
@@ -365,8 +355,6 @@ let simp_unsigned bits arg =
   | Integer {data} -> integer (Z.extract data 0 bits)
   | _ -> Ap1 (Unsigned {bits}, arg)
 
-let simp_convert src dst arg = Ap1 (Convert {src; dst}, arg)
-
 (* arithmetic *)
 
 (* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of
@@ -555,9 +543,7 @@ let simp_cond cnd thn els =
 (* boolean / bitwise *)
 
 let rec is_boolean = function
-  | Ap1 ((Unsigned {bits= 1} | Convert {dst= Integer {bits= 1; _}; _}), _)
+  | Ap1 (Unsigned {bits= 1}, _) | Ap2 ((Eq | Dq | Lt | Le), _, _) -> true
-   |Ap2 ((Eq | Dq | Lt | Le), _, _) ->
-      true
   | Ap2 ((Div | Rem | Xor | Shl | Lshr | Ashr), x, y)
    |Ap3 (Conditional, _, x, y) ->
       is_boolean x || is_boolean y
@@ -911,7 +897,6 @@ let norm1 op x =
   ( match op with
   | Signed {bits} -> simp_signed bits x
   | Unsigned {bits} -> simp_unsigned bits x
-  | Convert {src; dst} -> simp_convert src dst x
   | Splat -> simp_splat x
   | Select idx -> simp_select idx x )
   |> check invariant
@@ -946,11 +931,6 @@ let normN op xs =
 
 let signed bits term = norm1 (Signed {bits}) term
 let unsigned bits term = norm1 (Unsigned {bits}) term
-
-let convert src ~to_:dst arg =
-  if Llair.Typ.equivalent src dst then arg
-  else norm1 (Convert {src; dst}) arg
-
 let eq = norm2 Eq
 let dq = norm2 Dq
 let lt = norm2 Lt

sledge/src/ses/term.mli

@@ -19,11 +19,6 @@ type op1 =
       (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit
           unsigned integer. That is, it unsigned-binary--decodes the low [n]
           bits of the infinite two's-complement encoding of [arg]. *)
-  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
-      (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src]
-          to type [dst], possibly with loss of information. The [src] and
-          [dst] types must be [Typ.convertible] and must not both be
-          [Integer] types. *)
   | Splat  (** Iterated concatenation of a single byte *)
   | Select of int  (** Select an index from a record *)
 [@@deriving compare, equal, sexp]
@@ -134,7 +129,6 @@ val rational : Q.t -> t
 (* type conversions *)
 val signed : int -> t -> t
 val unsigned : int -> t -> t
-val convert : Llair.Typ.t -> to_:Llair.Typ.t -> t -> t
 
 (* comparisons *)
 val eq : t -> t -> t