[sledge] Revise order of Term constructors for polynomial normalization

Summary: Integer terms need to compare higher than any monomial.

Reviewed By: bennostein

Differential Revision: D17725607

fbshipit-source-id: c64fd52d5

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
 

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 *)
+  | Label of {parent: string; name: string}
-  | Float of {data: string}  (** Floating-point constant *)
+      (** 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}
+  | Float of {data: string}  (** Floating-point constant *)
-      (** Address of named code block within parent function *)
+  | Integer of {data: Z.t}  (** Integer constant *)
 [@@deriving compare, equal, hash, sexp]
 
 val comparator : (t, comparator_witness) Comparator.t