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

[sledge] Remove Funsym.Float

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

Reviewed By: jvillard

Differential Revision: D24306096

fbshipit-source-id: 8c10dd3fd
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 70a7224543
commit 2f4e3e17b6
6 changed files with 15 additions and 28 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 (Float s, Tuple [||]) -> Ses.Term.float s
| 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)
@ -1229,7 +1228,6 @@ and of_ses : Ses.Term.t -> exp =
| Var {id; name} -> var (Var.identified ~id ~name)
| Integer {data} -> integer data
| Rational {data} -> rational data
| Float {data} -> uap0 (Float 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
@ -1606,7 +1604,8 @@ module Term_of_Llair = struct
| Float {data; typ= _} -> (
match Q.of_float (Float.of_string data) with
| q when Q.is_real q -> rational q
| _ | (exception Invalid_argument _) -> uap0 (Float data) )
| _ | (exception Invalid_argument _) ->
uap0 (Uninterp ("float_" ^ data)) )
| Ap1 (Signed {bits}, _, e) ->
let a = exp e in
if bits = 1 then

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

@ -19,8 +19,7 @@ let classify e =
| Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | Apply _ | PosLit _ | NegLit _
|And _ | Or _ ->
Uninterpreted
| Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ ->
Atomic
| Var _ | Integer _ | Rational _ | Label _ | RecRecord _ -> Atomic
let interpreted e = equal_kind (classify e) Interpreted
let non_interpreted e = not (interpreted e)
@ -102,7 +101,7 @@ end = struct
(** compose a substitution with a mapping *)
let compose1 ~key ~data s =
match (key : Term.t) with
| Integer _ | Rational _ | Float _ | Label _ -> s
| Integer _ | Rational _ | Label _ -> s
| _ ->
if Term.equal key data then s
else compose s (Term.Map.singleton key data)
@ -135,7 +134,7 @@ end = struct
else
let s = Term.Map.remove s key in
match (key : Term.t) with
| Integer _ | Rational _ | Float _ | Label _ -> s
| Integer _ | Rational _ | Label _ -> s
| _ -> Term.Map.add_exn ~key:key' ~data:data' s )
(** Holds only if [true ⊢ ∃xs. e=f]. Clients assume
@ -478,7 +477,7 @@ let rec canon r a =
let rec extend_ a r =
match (a : Term.t) with
| Integer _ | Rational _ | Float _ | Label _ -> r
| Integer _ | Rational _ | Label _ -> 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 =
| Float of string
| Label of {parent: string; name: string}
| Mul
| Div
@ -30,7 +29,6 @@ type t =
let pp ppf f =
let pf fmt = Format.fprintf ppf fmt in
match f with
| Float s -> pf "%s" s
| Label {name} -> pf "%s" name
| Mul -> pf "@<1>×"
| Div -> 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 =
| Float of string
| Label of {parent: string; name: string}
| Mul (** Multiplication *)
| Div (** Division, for integers result is truncated toward zero *)

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

@ -69,7 +69,6 @@ and T : sig
| Add of qset
| Mul of qset
| Label of {parent: string; name: string}
| Float of {data: string}
| Integer of {data: Z.t}
| Rational of {data: Q.t}
| RecRecord of int
@ -92,7 +91,6 @@ end = struct
| Add of qset
| Mul of qset
| Label of {parent: string; name: string}
| Float of {data: string}
| Integer of {data: Z.t}
| Rational of {data: Q.t}
| RecRecord of int
@ -260,7 +258,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
| Float {data} -> pf "%s" 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
@ -358,7 +355,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 float data = Float {data} |> check invariant
let label ~parent ~name = Label {parent; name} |> check invariant
(* type conversions *)
@ -1044,7 +1040,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> e
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> e
let fold_map e ~init ~f =
let s = ref init in
@ -1099,7 +1095,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> ()
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> ()
let exists e ~f =
match e with
@ -1110,8 +1106,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ ->
false
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> false
let for_all e ~f =
match e with
@ -1122,7 +1117,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> true
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> true
let fold e ~init:s ~f =
match e with
@ -1133,7 +1128,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> s
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> s
let rec iter_terms e ~f =
( match e with
@ -1150,8 +1145,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> ()
) ;
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> () ) ;
f e
let rec fold_terms e ~init:s ~f =
@ -1167,7 +1161,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> s
| Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> s
in
f s e
@ -1190,7 +1184,7 @@ let is_false = function Integer {data} -> Z.is_false data | _ -> false
let rec is_constant = function
| Var _ -> false
| Label _ | Float _ | Integer _ | Rational _ -> true
| Label _ | Integer _ | Rational _ -> true
| a -> for_all ~f:is_constant a
let rec height = function
@ -1204,7 +1198,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 _ | Float _ | Integer _ | Rational _ | RecRecord _ -> 0
| Label _ | Integer _ | Rational _ | RecRecord _ -> 0
(** Solve *)

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

@ -85,7 +85,6 @@ and T : sig
| Mul of qset (** Product of terms with rational exponents *)
| Label of {parent: string; name: string}
(** Address of named code block within parent function *)
| Float of {data: string} (** Floating-point constant *)
| Integer of {data: Z.t} (** Integer constant *)
| Rational of {data: Q.t} (** Rational constant *)
| RecRecord of int (** Reference to ancestor recursive record *)
@ -134,7 +133,6 @@ val zero : t
val one : t
val minus_one : t
val rational : Q.t -> t
val float : string -> t
(* type conversions *)
val signed : int -> t -> t

Write Preview
Loading…
Cancel
Save