From fc841bcf0ca71907afc2865f74660bd41330fc72 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 02:36:51 -0700 Subject: [PATCH] [sledge] Remove Funsym.Label Summary: Label values are uninterpreted, so use an uninterpreted function symbol for them. Reviewed By: jvillard Differential Revision: D24306097 fbshipit-source-id: e139c70ba --- sledge/src/fol.ml | 5 ++--- sledge/src/ses/equality.ml | 8 ++++---- sledge/src/ses/funsym.ml | 2 -- sledge/src/ses/funsym.mli | 1 - sledge/src/ses/term.ml | 22 +++++++++------------- sledge/src/ses/term.mli | 3 --- 6 files changed, 15 insertions(+), 26 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 9c75c4cfe..01951ea79 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -1119,7 +1119,6 @@ let rec t_to_ses : trm -> Ses.Term.t = function Ses.Term.update ~rcd:(t_to_ses rcd) ~idx:(to_int (t_to_ses idx)) ~elt:(t_to_ses elt) - | Apply (Label {parent; name}, Tuple [||]) -> Ses.Term.label ~parent ~name | Apply (Mul, Tuple [|x; y|]) -> Ses.Term.mul (t_to_ses x) (t_to_ses y) | Apply (Div, Tuple [|x; y|]) -> Ses.Term.div (t_to_ses x) (t_to_ses y) | Apply (Rem, Tuple [|x; y|]) -> Ses.Term.rem (t_to_ses x) (t_to_ses y) @@ -1228,7 +1227,6 @@ and of_ses : Ses.Term.t -> exp = | Var {id; name} -> var (Var.identified ~id ~name) | Integer {data} -> integer data | Rational {data} -> rational data - | Label {parent; name} -> uap0 (Label {parent; name}) | 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 @@ -1599,7 +1597,8 @@ module Term_of_Llair = struct let open Formula in match e with | Reg {name; global; typ= _} -> var (Var.program ~name ~global) - | Label {parent; name} -> uap0 (Label {parent; name}) + | Label {parent; name} -> + uap0 (Uninterp ("label_" ^ parent ^ "_" ^ name)) | Integer {typ= _; data} -> integer data | Float {data; typ= _} -> ( match Q.of_float (Float.of_string data) with diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml index 68809da5d..4f5e950d0 100644 --- a/sledge/src/ses/equality.ml +++ b/sledge/src/ses/equality.ml @@ -19,7 +19,7 @@ let classify e = | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | Apply _ | PosLit _ | NegLit _ |And _ | Or _ -> Uninterpreted - | Var _ | Integer _ | Rational _ | Label _ | RecRecord _ -> Atomic + | Var _ | Integer _ | Rational _ | RecRecord _ -> Atomic let interpreted e = equal_kind (classify e) Interpreted let non_interpreted e = not (interpreted e) @@ -101,7 +101,7 @@ end = struct (** compose a substitution with a mapping *) let compose1 ~key ~data s = match (key : Term.t) with - | Integer _ | Rational _ | Label _ -> s + | Integer _ | Rational _ -> s | _ -> if Term.equal key data then s else compose s (Term.Map.singleton key data) @@ -134,7 +134,7 @@ end = struct else let s = Term.Map.remove s key in match (key : Term.t) with - | Integer _ | Rational _ | Label _ -> s + | Integer _ | Rational _ -> s | _ -> Term.Map.add_exn ~key:key' ~data:data' s ) (** Holds only if [true ⊢ ∃xs. e=f]. Clients assume @@ -477,7 +477,7 @@ let rec canon r a = let rec extend_ a r = match (a : Term.t) with - | Integer _ | Rational _ | Label _ -> r + | Integer _ | Rational _ -> r | _ -> ( if interpreted a then Term.fold ~f:extend_ a ~init:r else diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml index 4e2d10637..7875c13e3 100644 --- a/sledge/src/ses/funsym.ml +++ b/sledge/src/ses/funsym.ml @@ -8,7 +8,6 @@ (** Function Symbols *) type t = - | Label of {parent: string; name: string} | Mul | Div | Rem @@ -29,7 +28,6 @@ type t = let pp ppf f = let pf fmt = Format.fprintf ppf fmt in match f with - | Label {name} -> pf "%s" name | Mul -> pf "@<1>×" | Div -> pf "/" | Rem -> pf "%%" diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli index cbc62a77b..0e3239303 100644 --- a/sledge/src/ses/funsym.mli +++ b/sledge/src/ses/funsym.mli @@ -12,7 +12,6 @@ applied to literal values of the expected sorts are reduced to literal values. *) type t = - | Label of {parent: string; name: string} | Mul (** Multiplication *) | Div (** Division, for integers result is truncated toward zero *) | Rem diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml index 4905e6513..209e46084 100644 --- a/sledge/src/ses/term.ml +++ b/sledge/src/ses/term.ml @@ -68,7 +68,6 @@ and T : sig | Or of set | Add of qset | Mul of qset - | Label of {parent: string; name: string} | Integer of {data: Z.t} | Rational of {data: Q.t} | RecRecord of int @@ -90,7 +89,6 @@ end = struct | Or of set | Add of qset | Mul of qset - | Label of {parent: string; name: string} | Integer of {data: Z.t} | Rational of {data: Q.t} | RecRecord of int @@ -258,7 +256,6 @@ let rec ppx strength fs term = | Var _ as v -> Var.ppx strength fs (Var.of_ v) | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data | Rational {data} -> Trace.pp_styled `Magenta "%a" fs Q.pp data - | Label {name} -> pf "%s" name | 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) -> @@ -355,7 +352,6 @@ let minus_one = integer Z.minus_one let bool b = integer (Z.of_bool b) let true_ = bool true let false_ = bool false -let label ~parent ~name = Label {parent; name} |> check invariant (* type conversions *) @@ -1040,7 +1036,7 @@ let map e ~f = | Apply (sym, xs) -> mapN (simp_apply sym) ~f xs | PosLit (sym, xs) -> mapN (simp_poslit sym) ~f xs | NegLit (sym, xs) -> mapN (simp_neglit sym) ~f xs - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> e + | Var _ | Integer _ | Rational _ | RecRecord _ -> e let fold_map e ~init ~f = let s = ref init in @@ -1095,7 +1091,7 @@ let iter e ~f = IArray.iter ~f xs | And args | Or args -> Set.iter ~f args | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> () + | Var _ | Integer _ | Rational _ | RecRecord _ -> () let exists e ~f = match e with @@ -1106,7 +1102,7 @@ let exists e ~f = IArray.exists ~f xs | And args | Or args -> Set.exists ~f args | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> false + | Var _ | Integer _ | Rational _ | RecRecord _ -> false let for_all e ~f = match e with @@ -1117,7 +1113,7 @@ let for_all e ~f = IArray.for_all ~f xs | And args | Or args -> Set.for_all ~f args | Add args | Mul args -> Qset.for_all ~f:(fun arg _ -> f arg) args - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> true + | Var _ | Integer _ | Rational _ | RecRecord _ -> true let fold e ~init:s ~f = match e with @@ -1128,7 +1124,7 @@ let fold e ~init:s ~f = IArray.fold ~f:(fun s x -> f x s) xs ~init:s | And args | Or args -> Set.fold ~f:(fun s e -> f e s) args ~init:s | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args ~init:s - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> s + | Var _ | Integer _ | Rational _ | RecRecord _ -> s let rec iter_terms e ~f = ( match e with @@ -1145,7 +1141,7 @@ let rec iter_terms e ~f = | And args | Or args -> Set.iter args ~f:(iter_terms ~f) | Add args | Mul args -> Qset.iter args ~f:(fun arg _ -> iter_terms ~f arg) - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> () ) ; + | Var _ | Integer _ | Rational _ | RecRecord _ -> () ) ; f e let rec fold_terms e ~init:s ~f = @@ -1161,7 +1157,7 @@ let rec fold_terms e ~init:s ~f = Set.fold args ~init:s ~f:(fun s x -> fold_terms f x s) | Add args | Mul args -> Qset.fold args ~init:s ~f:(fun arg _ s -> fold_terms f arg s) - | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> s + | Var _ | Integer _ | Rational _ | RecRecord _ -> s in f s e @@ -1184,7 +1180,7 @@ let is_false = function Integer {data} -> Z.is_false data | _ -> false let rec is_constant = function | Var _ -> false - | Label _ | Integer _ | Rational _ -> true + | Integer _ | Rational _ -> true | a -> for_all ~f:is_constant a let rec height = function @@ -1198,7 +1194,7 @@ let rec height = function 1 + Set.fold bs ~init:0 ~f:(fun m a -> max m (height a)) | Add qs | Mul qs -> 1 + Qset.fold qs ~init:0 ~f:(fun a _ m -> max m (height a)) - | Label _ | Integer _ | Rational _ | RecRecord _ -> 0 + | Integer _ | Rational _ | RecRecord _ -> 0 (** Solve *) diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli index 05ee94359..eede4968f 100644 --- a/sledge/src/ses/term.mli +++ b/sledge/src/ses/term.mli @@ -83,8 +83,6 @@ and T : sig | Or of set (** Disjunction, boolean or bitwise *) | Add of qset (** Sum of terms with rational coefficients *) | Mul of qset (** Product of terms with rational exponents *) - | Label of {parent: string; name: string} - (** Address of named code block within parent function *) | Integer of {data: Z.t} (** Integer constant *) | Rational of {data: Q.t} (** Rational constant *) | RecRecord of int (** Reference to ancestor recursive record *) @@ -124,7 +122,6 @@ val invariant : t -> unit val var : Var.t -> t (* constants *) -val label : parent:string -> name:string -> t val bool : bool -> t val true_ : t val false_ : t