From 9e826c3454950065f3cf1739791f0f614c527e24 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 02:36:55 -0700 Subject: [PATCH] [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 | 9 +++++---- sledge/src/ses/funsym.ml | 2 -- sledge/src/ses/funsym.mli | 1 - sledge/src/ses/term.ml | 22 +--------------------- sledge/src/ses/term.mli | 6 ------ 5 files changed, 6 insertions(+), 34 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 01951ea79..02173cbdf 100644 --- a/sledge/src/fol.ml +++ b/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) diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml index 7875c13e3..4b52989be 100644 --- a/sledge/src/ses/funsym.ml +++ b/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 diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli index 0e3239303..62e247e14 100644 --- a/sledge/src/ses/funsym.mli +++ b/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] diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml index 209e46084..de0b1af82 100644 --- a/sledge/src/ses/term.ml +++ b/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; _}; _}), _) - |Ap2 ((Eq | Dq | Lt | Le), _, _) -> - true + | Ap1 (Unsigned {bits= 1}, _) | 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 diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli index eede4968f..d5a1caefb 100644 --- a/sledge/src/ses/term.mli +++ b/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