From 434c40e646473c9db9e90f04c0758140591eedde Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 17 Mar 2020 09:05:35 -0700 Subject: [PATCH] [sledge] Do not use Base.Map to implement Qset Reviewed By: ngorogiannis Differential Revision: D20482766 fbshipit-source-id: 9884fc6cf --- sledge/bin/domain_itv.ml | 4 +- sledge/lib/import/import.ml | 7 +- sledge/lib/import/import.mli | 7 +- sledge/lib/import/import0.ml | 1 + sledge/lib/import/qset.ml | 226 +++++++++++++++++++---------------- sledge/lib/import/qset.mli | 129 +++++++------------- sledge/lib/sh.ml | 2 +- sledge/lib/term.ml | 58 ++++----- sledge/lib/term.mli | 60 ++++++---- 9 files changed, 224 insertions(+), 270 deletions(-) diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml index 3d1ba2963..91755ae14 100644 --- a/sledge/bin/domain_itv.ml +++ b/sledge/bin/domain_itv.ml @@ -74,7 +74,7 @@ let rec pow base typ = function * (See sledge/src/llair/term.ml functions assert_(mono|poly)mial for details) *) let rec texpr_of_nary_term subtms typ q op = - assert (Qset.length subtms >= 2) ; + assert (Term.Qset.length subtms >= 2) ; let term_to_texpr (tm, coeff) = let* base = apron_texpr_of_llair_term tm q typ in match op with @@ -87,7 +87,7 @@ let rec texpr_of_nary_term subtms typ q op = Some (pow base typ (Q.to_int coeff)) | _ -> None in - match Qset.to_list subtms with + match Term.Qset.to_list subtms with | hd :: tl -> List.fold tl ~init:(term_to_texpr hd) ~f:(fun acc curr -> let* c = term_to_texpr curr in diff --git a/sledge/lib/import/import.ml b/sledge/lib/import/import.ml index 9e8f563e2..ddf6d2089 100644 --- a/sledge/lib/import/import.ml +++ b/sledge/lib/import/import.ml @@ -121,12 +121,7 @@ module Vector = Vector include Vector.Infix module Set = Set module Map = Map - -module Qset = struct - include Qset - - let pp sep pp_elt fs s = List.pp sep pp_elt fs (to_list s) -end +module Qset = Qset module Array = struct include Base.Array diff --git a/sledge/lib/import/import.mli b/sledge/lib/import/import.mli index cef8f6339..7007170f9 100644 --- a/sledge/lib/import/import.mli +++ b/sledge/lib/import/import.mli @@ -114,12 +114,7 @@ module Vector = Vector include module type of Vector.Infix module Set = Set module Map = Map - -module Qset : sig - include module type of Qset - - val pp : (unit, unit) fmt -> ('a * Q.t) pp -> ('a, _) t pp -end +module Qset = Qset module Array : sig include module type of Base.Array diff --git a/sledge/lib/import/import0.ml b/sledge/lib/import/import0.ml index 1bd3a0a41..8f13d9f27 100644 --- a/sledge/lib/import/import0.ml +++ b/sledge/lib/import/import0.ml @@ -11,6 +11,7 @@ type 'a pp = Format.formatter -> 'a -> unit (** Format strings. *) type ('a, 'b) fmt = ('a, 'b) Trace.fmt +module Hash = Ppx_hash_lib.Std.Hash module Sexp = Sexplib.Sexp module type Applicative_syntax = sig diff --git a/sledge/lib/import/qset.ml b/sledge/lib/import/qset.ml index 1110a5706..2e344668b 100644 --- a/sledge/lib/import/qset.ml +++ b/sledge/lib/import/qset.ml @@ -7,112 +7,134 @@ (** Qset - Set with (signed) rational multiplicity for each element *) -open Base +open Import0 -type ('elt, 'cmp) t = ('elt, Q.t, 'cmp) Map.t - -module M (Elt : sig +module type S = sig + type elt type t - type comparator_witness -end) = -struct - type nonrec t = (Elt.t, Elt.comparator_witness) t -end -module type Sexp_of_m = sig - type t [@@deriving sexp_of] -end + val compare : t -> t -> int + val equal : t -> t -> bool + val hash_fold_t : elt Hash.folder -> t Hash.folder + val sexp_of_t : t -> Sexp.t + val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t + val pp : (unit, unit) fmt -> (elt * Q.t) pp -> t pp + + val empty : t + (** The empty multiset over the provided order. *) + + val add : t -> elt -> Q.t -> t + (** Add to multiplicity of single element. [O(log n)] *) + + val remove : t -> elt -> t + (** Set the multiplicity of an element to zero. [O(log n)] *) + + val union : t -> t -> t + (** Sum multiplicities pointwise. [O(n + m)] *) + + val length : t -> int + (** Number of elements with non-zero multiplicity. [O(1)]. *) -module type M_of_sexp = sig - type t [@@deriving of_sexp] + val count : t -> elt -> Q.t + (** Multiplicity of an element. [O(log n)]. *) - include Comparator.S with type t := t + val map : t -> f:(elt -> Q.t -> elt * Q.t) -> t + (** Map over the elements in ascending order. Preserves physical equality + if [f] does. *) + + val map_counts : t -> f:(elt -> Q.t -> Q.t) -> t + (** Map over the multiplicities of the elements in ascending order. *) + + val fold : t -> f:(elt -> Q.t -> 's -> 's) -> init:'s -> 's + (** Fold over the elements in ascending order. *) + + val iter : t -> f:(elt -> Q.t -> unit) -> unit + (** Iterate over the elements in ascending order. *) + + val exists : t -> f:(elt -> Q.t -> bool) -> bool + (** Search for an element satisfying a predicate. *) + + val min_elt : t -> (elt * Q.t) option + (** Minimum element. *) + + val min_elt_exn : t -> elt * Q.t + (** Minimum element. *) + + val to_list : t -> (elt * Q.t) list + (** Convert to a list of elements in ascending order. *) end -module type Compare_m = sig end -module type Hash_fold_m = Hasher.S - -let sexp_of_q q = Sexp.Atom (Q.to_string q) -let q_of_sexp = function Sexp.Atom s -> Q.of_string s | _ -> assert false -let hash_fold_q state q = Hash.fold_int state (Hashtbl.hash q) - -let sexp_of_m__t (type elt) (module Elt : Sexp_of_m with type t = elt) t = - Map.sexp_of_m__t (module Elt) sexp_of_q t - -let m__t_of_sexp (type elt cmp) - (module Elt : M_of_sexp - with type t = elt - and type comparator_witness = cmp) sexp = - Map.m__t_of_sexp (module Elt) q_of_sexp sexp - -let compare_m__t (module Elt : Compare_m) = Map.compare_direct Q.compare -let equal_m__t (module Elt : Compare_m) = Map.equal Q.equal - -let hash_fold_m__t (type elt) (module Elt : Hash_fold_m with type t = elt) - state = - Map.hash_fold_m__t (module Elt) hash_fold_q state - -let hash_m__t (type elt) (module Elt : Hash_fold_m with type t = elt) = - Hash.of_fold (hash_fold_m__t (module Elt)) - -type ('elt, 'cmp) comparator = - (module Comparator.S with type t = 'elt and type comparator_witness = 'cmp) - -let empty cmp = Map.empty cmp -let if_nz q = if Q.equal Q.zero q then None else Some q - -let add m x i = - Map.change m x ~f:(function Some j -> if_nz Q.(i + j) | None -> if_nz i) - -let remove m x = Map.remove m x - -let union m n = - Map.merge m n ~f:(fun ~key:_ -> function - | `Both (i, j) -> if_nz Q.(i + j) | `Left i | `Right i -> Some i ) - -let length m = Map.length m -let count m x = match Map.find m x with Some q -> q | None -> Q.zero - -let count_and_remove m x = - let found = ref Q.zero in - let m = - Map.change m x ~f:(function - | None -> None - | Some i -> - found := i ; - None ) - in - if Q.equal !found Q.zero then None else Some (!found, m) - -let min_elt = Map.min_elt -let min_elt_exn = Map.min_elt_exn -let fold m ~f ~init = Map.fold m ~f:(fun ~key ~data s -> f key data s) ~init - -let map m ~f = - let m' = Map.empty (Map.comparator_s m) in - let m, m' = - fold m ~init:(m, m') ~f:(fun x i (m, m') -> - let x', i' = f x i in - if phys_equal x' x then - if Q.equal i' i then (m, m') else (Map.set m ~key:x ~data:i', m') - else (Map.remove m x, add m' x' i') ) - in - fold m' ~init:m ~f:(fun x i m -> add m x i) - -let fold_map m ~f ~init:s = - let m' = Map.empty (Map.comparator_s m) in - let m, m', s = - fold m ~init:(m, m', s) ~f:(fun x i (m, m', s) -> - let x', i', s = f x i s in - if phys_equal x' x then - if Q.equal i' i then (m, m', s) - else (Map.set m ~key:x ~data:i', m', s) - else (Map.remove m x, add m' x' i', s) ) - in - (fold m' ~init:m ~f:(fun x i m -> add m x i), s) - -let for_all m ~f = Map.for_alli m ~f:(fun ~key ~data -> f key data) -let map_counts m ~f = Map.mapi m ~f:(fun ~key ~data -> f key data) -let iter m ~f = Map.iteri m ~f:(fun ~key ~data -> f key data) -let exists m ~f = Map.existsi m ~f:(fun ~key ~data -> f key data) -let to_list m = Map.to_alist m +module Make (Elt : OrderedType) = struct + module M = Stdlib.Map.Make (Elt) + + type elt = Elt.t + type t = Q.t M.t + + let compare = M.compare Q.compare + let equal = M.equal Q.equal + + let hash_fold_t hash_fold_elt s m = + let hash_fold_q s q = Hash.fold_int s (Hashtbl.hash q) in + M.fold + (fun key data state -> hash_fold_q (hash_fold_elt state key) data) + m + (Hash.fold_int s (M.cardinal m)) + + let sexp_of_t s = + let sexp_of_q q = Sexp.Atom (Q.to_string q) in + List.sexp_of_t + (Sexplib.Conv.sexp_of_pair Elt.sexp_of_t sexp_of_q) + (M.bindings s) + + let t_of_sexp elt_of_sexp sexp = + let q_of_sexp = function + | Sexp.Atom s -> Q.of_string s + | _ -> assert false + in + List.fold_left + ~f:(fun m (k, v) -> M.add k v m) + ~init:M.empty + (List.t_of_sexp + (Sexplib.Conv.pair_of_sexp elt_of_sexp q_of_sexp) + sexp) + + let pp sep pp_elt fs s = List.pp sep pp_elt fs (M.bindings s) + let empty = M.empty + let if_nz q = if Q.equal Q.zero q then None else Some q + + let add m x i = + M.update x (function Some j -> if_nz Q.(i + j) | None -> if_nz i) m + + let remove m x = M.remove x m + + let union m n = + M.merge + (fun _ m_q n_q -> + match (m_q, n_q) with + | Some i, Some j -> if_nz Q.(i + j) + | Some i, None | None, Some i -> Some i + | None, None -> None ) + m n + + let length m = M.cardinal m + let count m x = try M.find x m with Not_found -> Q.zero + let fold m ~f ~init = M.fold (fun key data s -> f key data s) m init + + let map m ~f = + let m' = M.empty in + let m, m' = + fold m ~init:(m, m') ~f:(fun x i (m, m') -> + let x', i' = f x i in + if x' == x then + if Q.equal i' i then (m, m') else (M.add x i' m, m') + else (M.remove x m, add m' x' i') ) + in + fold m' ~init:m ~f:(fun x i m -> add m x i) + + let map_counts m ~f = M.mapi (fun key data -> f key data) m + let iter m ~f = M.iter (fun key data -> f key data) m + let exists m ~f = M.exists (fun key data -> f key data) m + let min_elt = M.min_binding_opt + let min_elt_exn = M.min_binding + let to_list m = M.bindings m +end diff --git a/sledge/lib/import/qset.mli b/sledge/lib/import/qset.mli index e681f7769..597d9b1c5 100644 --- a/sledge/lib/import/qset.mli +++ b/sledge/lib/import/qset.mli @@ -7,110 +7,61 @@ (** Qset - Set with (signed) rational multiplicity for each element *) -open Base +open Import0 -type ('elt, 'cmp) t - -type ('elt, 'cmp) comparator = - (module Comparator.S with type t = 'elt and type comparator_witness = 'cmp) - -module M (Elt : sig +module type S = sig + type elt type t - type comparator_witness -end) : sig - type nonrec t = (Elt.t, Elt.comparator_witness) t -end - -module type Sexp_of_m = sig - type t [@@deriving sexp_of] -end - -module type M_of_sexp = sig - type t [@@deriving of_sexp] - - include Comparator.S with type t := t -end - -module type Compare_m = sig end -module type Hash_fold_m = Hasher.S -val sexp_of_m__t : - (module Sexp_of_m with type t = 'elt) -> ('elt, 'cmp) t -> Sexp.t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash_fold_t : elt Hash.folder -> t Hash.folder + val sexp_of_t : t -> Sexp.t + val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t + val pp : (unit, unit) fmt -> (elt * Q.t) pp -> t pp -val m__t_of_sexp : - (module M_of_sexp with type t = 'elt and type comparator_witness = 'cmp) - -> Sexp.t - -> ('elt, 'cmp) t + val empty : t + (** The empty multiset over the provided order. *) -val compare_m__t : - (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> int + val add : t -> elt -> Q.t -> t + (** Add to multiplicity of single element. [O(log n)] *) -val equal_m__t : - (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> bool + val remove : t -> elt -> t + (** Set the multiplicity of an element to zero. [O(log n)] *) -val hash_fold_m__t : - (module Hash_fold_m with type t = 'elt) - -> Hash.state - -> ('elt, _) t - -> Hash.state + val union : t -> t -> t + (** Sum multiplicities pointwise. [O(n + m)] *) -val hash_m__t : - (module Hash_fold_m with type t = 'elt) -> ('elt, _) t -> Hash.hash_value + val length : t -> int + (** Number of elements with non-zero multiplicity. [O(1)]. *) -val empty : ('elt, 'cmp) comparator -> ('elt, 'cmp) t -(** The empty multiset over the provided order. *) + val count : t -> elt -> Q.t + (** Multiplicity of an element. [O(log n)]. *) -val add : ('a, 'c) t -> 'a -> Q.t -> ('a, 'c) t -(** Add to multiplicity of single element. [O(log n)] *) + val map : t -> f:(elt -> Q.t -> elt * Q.t) -> t + (** Map over the elements in ascending order. Preserves physical equality + if [f] does. *) -val remove : ('a, 'c) t -> 'a -> ('a, 'c) t -(** Set the multiplicity of an element to zero. [O(log n)] *) + val map_counts : t -> f:(elt -> Q.t -> Q.t) -> t + (** Map over the multiplicities of the elements in ascending order. *) -val union : ('a, 'c) t -> ('a, 'c) t -> ('a, 'c) t -(** Sum multiplicities pointwise. [O(n + m)] *) + val fold : t -> f:(elt -> Q.t -> 's -> 's) -> init:'s -> 's + (** Fold over the elements in ascending order. *) -val length : _ t -> int -(** Number of elements with non-zero multiplicity. [O(1)]. *) + val iter : t -> f:(elt -> Q.t -> unit) -> unit + (** Iterate over the elements in ascending order. *) -val count : ('a, _) t -> 'a -> Q.t -(** Multiplicity of an element. [O(log n)]. *) + val exists : t -> f:(elt -> Q.t -> bool) -> bool + (** Search for an element satisfying a predicate. *) -val count_and_remove : ('a, 'c) t -> 'a -> (Q.t * ('a, 'c) t) option -(** Multiplicity of an element, and remove it. [O(log n)]. *) + val min_elt : t -> (elt * Q.t) option + (** Minimum element. *) -val map : ('a, 'c) t -> f:('a -> Q.t -> 'a * Q.t) -> ('a, 'c) t -(** Map over the elements in ascending order. Preserves physical equality if - [f] does. *) + val min_elt_exn : t -> elt * Q.t + (** Minimum element. *) -val map_counts : ('a, 'c) t -> f:('a -> Q.t -> Q.t) -> ('a, 'c) t -(** Map over the multiplicities of the elements in ascending order. *) - -val fold : ('a, _) t -> f:('a -> Q.t -> 's -> 's) -> init:'s -> 's -(** Fold over the elements in ascending order. *) - -val fold_map : - ('a, 'c) t - -> f:('a -> Q.t -> 's -> 'a * Q.t * 's) - -> init:'s - -> ('a, 'c) t * 's -(** Folding map over the elements in ascending order. Preserves physical - equality if [f] does. *) - -val for_all : ('a, _) t -> f:('a -> Q.t -> bool) -> bool -(** Universal property test. [O(n)] but returns as soon as a violation is - found, in ascending order. *) - -val iter : ('a, _) t -> f:('a -> Q.t -> unit) -> unit -(** Iterate over the elements in ascending order. *) - -val exists : ('a, _) t -> f:('a -> Q.t -> bool) -> bool -(** Search for an element satisfying a predicate. *) - -val min_elt : ('a, _) t -> ('a * Q.t) option -(** Minimum element. *) - -val min_elt_exn : ('a, _) t -> 'a * Q.t -(** Minimum element. *) + val to_list : t -> (elt * Q.t) list + (** Convert to a list of elements in ascending order. *) +end -val to_list : ('a, _) t -> ('a * Q.t) list -(** Convert to a list of elements in ascending order. *) +module Make (Elt : OrderedType) : S with type elt = Elt.t diff --git a/sledge/lib/sh.ml b/sledge/lib/sh.ml index 02c9f40b4..d36ca44d6 100644 --- a/sledge/lib/sh.ml +++ b/sledge/lib/sh.ml @@ -180,7 +180,7 @@ let pp_block x fs segs = let pp_heap x ?pre cong fs heap = let bas_off = function | Term.Add poly as sum -> - let const = Qset.count poly Term.one in + let const = Term.Qset.count poly Term.one in (Term.sub sum (Term.rational const), const) | e -> (e, Q.zero) in diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml index 9fc81ab99..f41e3b268 100644 --- a/sledge/lib/term.ml +++ b/sledge/lib/term.ml @@ -40,38 +40,22 @@ type op3 = Conditional | Extract [@@deriving compare, equal, hash, sexp] type opN = Concat | Record [@@deriving compare, equal, hash, sexp] type recN = Record [@@deriving compare, equal, hash, sexp] -module rec T : sig - type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] +module rec Qset : sig + include Import.Qset.S with type elt := T.t - type t = - | Add of qset - | Mul of qset - | Var of {id: int; name: string} - | Ap1 of op1 * t - | Ap2 of op2 * t * t - | Ap3 of op3 * t * t * t - | ApN of opN * t vector - | RecN of recN * t vector (** NOTE: cyclic *) - | Label of {parent: string; name: string} - | Nondet of {msg: string} - | Float of {data: string} - | Integer of {data: Z.t} - [@@deriving compare, equal, hash, sexp] - - (* Note: solve (and invariant) requires Qset.min_elt to return a - non-coefficient, so Integer terms must compare higher than any valid - monomial *) - - type comparator_witness - - val comparator : (t, comparator_witness) Comparator.t + val hash : t -> int + val hash_fold_t : t Hash.folder + val t_of_sexp : Sexp.t -> t end = struct - include T0 include Comparator.Make (T0) + include Import.Qset.Make (T) + + let hash_fold_t = hash_fold_t T.hash_fold_t + let hash = Hash.of_fold hash_fold_t + let t_of_sexp = t_of_sexp T.t_of_sexp end -(* auxiliary definition for safe recursive module initialization *) -and T0 : sig - type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] +and T : sig + type qset = Qset.t [@@deriving compare, equal, hash, sexp] type t = | Add of qset @@ -81,14 +65,14 @@ and T0 : sig | Ap2 of op2 * t * t | Ap3 of op3 * t * t * t | ApN of opN * t vector - | RecN of recN * t vector + | RecN of recN * t vector (** NOTE: cyclic *) | Label of {parent: string; name: string} | Nondet of {msg: string} | Float of {data: string} | Integer of {data: Z.t} [@@deriving compare, equal, hash, sexp] end = struct - type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] + type qset = Qset.t [@@deriving compare, equal, hash, sexp] type t = | Add of qset @@ -98,13 +82,16 @@ end = struct | Ap2 of op2 * t * t | Ap3 of op3 * t * t * t | ApN of opN * t vector - | RecN of recN * t vector + | RecN of recN * t vector (** NOTE: cyclic *) | Label of {parent: string; name: string} | Nondet of {msg: string} | Float of {data: string} | Integer of {data: Z.t} [@@deriving compare, equal, hash, sexp] + (* Note: solve (and invariant) requires Qset.min_elt to return a + non-coefficient, so Integer terms must compare higher than any valid + monomial *) let compare x y = match (x, y) with | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> @@ -112,9 +99,6 @@ end = struct | _ -> compare x y end -(* suppress spurious "Warning 60: unused module T0." *) -type _t = T0.t - include T module Map = Map.Make (T) @@ -124,8 +108,6 @@ module Set = struct let t_of_sexp = t_of_sexp T.t_of_sexp end -let empty_qset = Qset.empty (module T) - let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a = let rec fix_f seen e = match e with @@ -462,7 +444,7 @@ let simp_convert src dst arg = elements are Xᵢ with multiplicities cᵢ. A constant is treated as the coefficient of the empty monomial, which is the unit of multiplication 1. *) module Sum = struct - let empty = empty_qset + let empty = Qset.empty let add coeff term sum = assert (not (Q.equal Q.zero coeff)) ; @@ -486,7 +468,7 @@ end of indeterminates xᵢ is represented by a multiset where the elements are xᵢ and the multiplicities are the exponents nᵢ. *) module Prod = struct - let empty = empty_qset + let empty = Qset.empty let add term prod = assert (match term with Integer _ -> false | _ -> true) ; diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli index 73da97c60..a14b13e10 100644 --- a/sledge/lib/term.mli +++ b/sledge/lib/term.mli @@ -60,37 +60,45 @@ type opN = type recN = Record (** Recursive record (array / struct) constant *) [@@deriving compare, equal, hash, sexp] -type comparator_witness - -type qset = (t, comparator_witness) Qset.t - -and t = private - | Add of qset (** Sum of terms with rational coefficients *) - | Mul of qset (** Product of terms with rational exponents *) - | Var of {id: int; name: string} (** Local variable / virtual register *) - | Ap1 of op1 * t (** Unary application *) - | Ap2 of op2 * t * t (** Binary application *) - | Ap3 of op3 * t * t * t (** Ternary application *) - | ApN of opN * t vector (** N-ary application *) - | RecN of recN * t vector - (** Recursive n-ary application, may recursively refer to itself - (transitively) from its args. NOTE: represented by cyclic values. *) - | Label of {parent: string; name: string} - (** Address of named code block within parent function *) - | Nondet of {msg: string} - (** Anonymous local variable with arbitrary value, representing - non-deterministic approximation of value described by [msg] *) - | Float of {data: string} (** Floating-point constant *) - | Integer of {data: Z.t} (** Integer constant *) -[@@deriving compare, equal, hash, sexp] +module rec Qset : sig + include Import.Qset.S with type elt := T.t + + val hash_fold_t : t Hash.folder + val t_of_sexp : Sexp.t -> t +end + +and T : sig + type qset = Qset.t [@@deriving compare, equal, hash, sexp] + + and t = private + | Add of qset (** Sum of terms with rational coefficients *) + | Mul of qset (** Product of terms with rational exponents *) + | Var of {id: int; name: string} + (** Local variable / virtual register *) + | Ap1 of op1 * t (** Unary application *) + | Ap2 of op2 * t * t (** Binary application *) + | Ap3 of op3 * t * t * t (** Ternary application *) + | ApN of opN * t vector (** N-ary application *) + | RecN of recN * t vector + (** Recursive n-ary application, may recursively refer to itself + (transitively) from its args. NOTE: represented by cyclic + values. *) + | Label of {parent: string; name: string} + (** Address of named code block within parent function *) + | Nondet of {msg: string} + (** Anonymous local variable with arbitrary value, representing + non-deterministic approximation of value described by [msg] *) + | Float of {data: string} (** Floating-point constant *) + | Integer of {data: Z.t} (** Integer constant *) + [@@deriving compare, equal, hash, sexp] +end + +include module type of T with type t = T.t (** Term.Var is re-exported as Var *) module Var : sig type term := t type t = private term [@@deriving compare, equal, hash, sexp] - - include Comparator.S with type t := t - type strength = t -> [`Universal | `Existential | `Anonymous] option module Map : Map.S with type key := t