diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 07c6014ac..8c7bbe896 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -59,10 +59,10 @@ module rec T : sig | Ap3 of op3 * t * t * t | ApN of opN * t vector | RecN of recN * t vector (** NOTE: cyclic *) - | Integer of {data: Z.t} - | Float of {data: string} - | Nondet of {msg: string} | 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 @@ -119,10 +119,10 @@ and T0 : sig | Ap3 of op3 * t * t * t | ApN of opN * t vector | RecN of recN * t vector - | Integer of {data: Z.t} - | Float of {data: string} - | Nondet of {msg: string} | 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] @@ -166,10 +166,10 @@ end = struct | Ap3 of op3 * t * t * t | ApN of opN * t vector | RecN of recN * t vector - | Integer of {data: Z.t} - | Float of {data: string} - | Nondet of {msg: string} | 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 diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index e25e2b777..b74558223 100644 --- a/sledge/src/llair/term.mli +++ b/sledge/src/llair/term.mli @@ -69,13 +69,13 @@ and t = private | RecN of recN * t vector (** Recursive n-ary application, may recursively refer to itself (transitively) from its args. NOTE: represented by cyclic values. *) - | Integer of {data: Z.t} (** Integer constant *) - | Float of {data: string} (** Floating-point constant *) + | 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] *) - | 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 *) [@@deriving compare, equal, hash, sexp] val comparator : (t, comparator_witness) Comparator.t