[sledge] Use term height to avoid "pumpable" cyclic equations in Equality

Summary:
Equations of the form `a = b` where `a` is a proper subterm of `b` are
possible when uninterpreted functions are involved. Internally,
Equality does not eagerly substitute `b` for `a`, but external clients
can repeatedly `Equality.normalize` terms and thereby incrementally
blow up the sizes of terms.

This diff uses the heights of uninterpreted terms to choose equality
class representatives to avoid such blow-ups, by orienting equations
so that tall terms are represented by short terms, so that repeated
normalization cannot increase term height indefinitely.

Reviewed By: jvillard

Differential Revision: D20785632

fbshipit-source-id: ff4c5bacd

sledge/lib/equality.ml

@@ -189,18 +189,10 @@ let prefer e f =
     | ApN (Concat, _) -> 3
     | _ -> 4
   in
-  let rec height e =
-    match (e : Term.t) with
-    | Ap2 (Memory, _, x) -> 1 + height x
-    | Ap3 (Extract, x, _, _) -> 1 + height x
-    | ApN (Concat, xs) ->
-        1 + IArray.fold ~init:0 ~f:(fun h x -> max h (height x)) xs
-    | _ -> 0
-  in
   let o = compare (rank e) (rank f) in
   if o <> 0 then o
   else
-    let o = compare (height e) (height f) in
+    let o = compare (Term.height e) (Term.height f) in
     if o <> 0 then o else Term.compare e f
 
 (** orient equations based on representative preference *)

sledge/lib/term.ml

@@ -1178,6 +1178,20 @@ let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
 let is_true = function Integer {data} -> Z.is_true data | _ -> false
 let is_false = function Integer {data} -> Z.is_false data | _ -> false
 
+let height e =
+  let height_ height_ = function
+    | Var _ -> 0
+    | Ap1 (_, a) -> 1 + height_ a
+    | Ap2 (_, a, b) -> 1 + max (height_ a) (height_ b)
+    | Ap3 (_, a, b, c) -> 1 + max (height_ a) (max (height_ b) (height_ c))
+    | ApN (_, v) | RecN (_, v) ->
+        1 + IArray.fold v ~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 _ | Nondet _ | Float _ | Integer _ -> 0
+  in
+  fix height_ (fun _ -> 0) e
+
 (** Solve *)
 
 let solve_zero_eq ?for_ e =

sledge/lib/term.mli

@@ -250,6 +250,7 @@ val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a
 val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
+val height : t -> int
 
 (** Solve *)