[sledge] Add Term.split_const and use instead of const_of

Summary:
Term.const_of is misleading as it is easy to expect it checks if a
term is a constant, or to expect that it returns the constant part of
a term. Instead, Term.split_const is clearer:
```
  val split_const : t -> t * Q.t
  (** Splits a term into the sum of its constant and non-constant parts.
      That is, [split_const a] is [(b, c)] such that [a = b + c] and the
      absolute value of [c] is maximal. *)
```

Reviewed By: ngorogiannis

Differential Revision: D24306065

fbshipit-source-id: ba15958ad

sledge/cli/smtlib.ml

@@ -67,10 +67,10 @@ and x_trm : var_env -> Smt.Ast.term -> Term.t =
     match List.map ~f:(x_trm n) es with
     | e :: es ->
         List.fold es ~init:e ~f:(fun p e ->
-            match Term.const_of e with
+            match Term.get_const e with
             | Some q -> Term.mulq q p
             | None -> (
-              match Term.const_of p with
+              match Term.get_const p with
               | Some q -> Term.mulq q e
               | None -> fail "nonlinear: %a" Smt.Ast.pp_term term () ) )
     | [] -> fail "malformed: %a" Smt.Ast.pp_term term () )
@@ -78,7 +78,7 @@ and x_trm : var_env -> Smt.Ast.term -> Term.t =
     match List.map ~f:(x_trm n) es with
     | e :: es ->
         List.fold es ~init:e ~f:(fun p e ->
-            match Term.const_of e with
+            match Term.get_const e with
             | Some q -> Term.mulq (Q.inv q) p
             | None -> fail "nonlinear: %a" Smt.Ast.pp_term term () )
     | [] -> fail "malformed: %a" Smt.Ast.pp_term term () )

sledge/src/arithmetic.ml

@@ -234,6 +234,11 @@ module Representation (Trm : INDETERMINATE) = struct
 
     (* transform *)
 
+    let split_const poly =
+      match Sum.find_and_remove poly Mono.one with
+      | Some (c, p_c) -> (p_c, c)
+      | None -> (poly, Q.zero)
+
     let map poly ~f =
       let p, p' = (poly, Sum.empty) in
       let p, p' =

sledge/src/arithmetic_intf.ml

@@ -48,6 +48,11 @@ module type S = sig
 
   (** Transform *)
 
+  val split_const : t -> t * Q.t
+  (** Splits an arithmetic term into the sum of its constant and
+      non-constant parts. That is, [split_const a] is [(b, c)] such that
+      [a = b + c] and the absolute value of [c] is maximal. *)
+
   val map : t -> f:(trm -> trm) -> t
   (** [map ~f a] is [a] with each indeterminate transformed by [f]. Viewing
       [a] as a polynomial,

sledge/src/fol.ml

@@ -855,13 +855,21 @@ module Term = struct
 
   let d_int = function `Trm (Z z) -> Some z | _ -> None
 
-  (** Access *)
-
-  let const_of = function
+  let get_const = function
     | `Trm (Z z) -> Some (Q.of_z z)
     | `Trm (Q q) -> Some q
     | _ -> None
 
+  (** Access *)
+
+  let split_const = function
+    | `Trm (Z z) -> (zero, Q.of_z z)
+    | `Trm (Q q) -> (zero, q)
+    | `Trm (Arith a) ->
+        let a_c, c = Arith.split_const a in
+        (`Trm (_Arith a_c), c)
+    | e -> (e, Q.zero)
+
   (** Traverse *)
 
   let fold_vars = fold_vars

sledge/src/fol.mli

@@ -60,9 +60,15 @@ module rec Term : sig
 
   val d_int : t -> Z.t option
 
+  val get_const : t -> Q.t option
+  (** [get_const a] is [Some q] iff [equal a (const q)] *)
+
   (** Access *)
 
-  val const_of : t -> Q.t option
+  val split_const : t -> t * Q.t
+  (** Splits a term into the sum of its constant and non-constant parts.
+      That is, [split_const a] is [(b, c)] such that [a = b + c] and the
+      absolute value of [c] is maximal. *)
 
   (** Query *)
 

sledge/src/sh.ml

@@ -170,11 +170,7 @@ let pp_block x fs segs =
   | [] -> ()
 
 let pp_heap x ?pre ctx fs heap =
-  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 bas_off = Term.split_const in
   let cmp s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]
       (Context.normalize ctx s1.bas, bas_off (Context.normalize ctx s1.loc))