From f804220cd2e44ce2065b8b702b37d8453a0830d0 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 10 Oct 2019 06:17:31 -0700
Subject: [PATCH] [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  | 18 +++++++++---------
 sledge/src/llair/term.mli |  8 ++++----
 2 files changed, 13 insertions(+), 13 deletions(-)

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