pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Remove Funsym.Label

Browse Source 
Summary:
Label values are uninterpreted, so use an uninterpreted function
symbol for them.

Reviewed By: jvillard

Differential Revision: D24306097

fbshipit-source-id: e139c70ba
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 2f4e3e17b6
commit fc841bcf0c
6 changed files with 15 additions and 26 deletions
Show Stats Download Patch File Download Diff File

5
sledge/src/fol.ml
Unescape View File

@ -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

8
sledge/src/ses/equality.ml
Unescape View File

@ -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

2
sledge/src/ses/funsym.ml
Unescape View File

@ -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 "%%"

1
sledge/src/ses/funsym.mli
Unescape View File

@ -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

22
sledge/src/ses/term.ml
Unescape View File

@ -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 *)

3
sledge/src/ses/term.mli
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save