[sledge] Refactor: Factor out accessor for polynomial constant as Term.const_of

Summary:
It is suboptimal for `Sh` to destruct terms with detailed knowledge of
their representation. So add `Term.const_of` to obtain the constant
summand of a polynomial term.

Reviewed By: jvillard

Differential Revision: D21721022

fbshipit-source-id: 4af858896

sledge/src/sh.ml

@@ -177,11 +177,10 @@ 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 = Term.Qset.count poly Term.one in
-        (Term.sub sum (Term.rational const), const)
-    | e -> (e, Q.zero)
+  let bas_off e =
+    match Term.const_of e with
+    | Some const -> (Term.sub e (Term.rational const), const)
+    | None -> (e, Q.zero)
   in
   let compare s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]

sledge/src/term.ml

@@ -1144,6 +1144,10 @@ end
 
 let d_int = function Integer {data} -> Some data | _ -> None
 
+(** Access *)
+
+let const_of = function Add poly -> Some (Qset.count poly one) | _ -> None
+
 (** Transform *)
 
 let map e ~f =

sledge/src/term.mli

@@ -241,6 +241,10 @@ val of_exp : Llair.Exp.t -> t
 
 val d_int : t -> Z.t option
 
+(** Access *)
+
+val const_of : t -> Q.t option
+
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t