[sledge] Make API of Term constant destructors uniform

Reviewed By: jvillard

Differential Revision: D24549077

fbshipit-source-id: b8659ec86

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 e ~f:(fun e p ->
-            match Term.get_const e with
+            match Term.get_q e with
             | Some q -> Term.mulq q p
             | None -> (
-              match Term.get_const p with
+              match Term.get_q 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 e ~f:(fun e p ->
-            match Term.get_const e with
+            match Term.get_q 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/fol/exp.ml

@@ -253,13 +253,8 @@ module Term = struct
 
   (** Destruct *)
 
-  let d_int e = match (e : t) with `Trm (Z z) -> Some z | _ -> None
-
-  let get_const e =
-    match (e : t) with
-    | `Trm (Z z) -> Some (Q.of_z z)
-    | `Trm (Q q) -> Some q
-    | _ -> None
+  let get_z = function `Trm t -> Trm.get_z t | _ -> None
+  let get_q = function `Trm t -> Trm.get_q t | _ -> None
 
   (** Access *)
 

sledge/src/fol/exp.mli

@@ -71,10 +71,11 @@ module rec Term : sig
 
   (** Destruct *)
 
-  val d_int : t -> Z.t option
+  val get_z : t -> Z.t option
+  (** [get_z a] is [Some z] iff [equal a (integer z)] *)
 
-  val get_const : t -> Q.t option
-  (** [get_const a] is [Some q] iff [equal a (const q)] *)
+  val get_q : t -> Q.t option
+  (** [get_q a] is [Some q] iff [equal a (rational q)] *)
 
   (** Access *)
 

sledge/src/fol/trm.ml

@@ -108,6 +108,8 @@ and Trm : sig
   val sub : t -> t -> t
   val seq_size_exn : t -> t
   val seq_size : t -> t option
+  val get_z : t -> Z.t option
+  val get_q : t -> Q.t option
   val vars : t -> Var.t iter
 end = struct
   type t =

sledge/src/fol/trm.mli

@@ -86,6 +86,11 @@ val ancestor : int -> t
 (* uninterpreted *)
 val apply : Funsym.t -> t array -> t
 
+(** Destruct *)
+
+val get_z : t -> Z.t option
+val get_q : t -> Q.t option
+
 (** Transform *)
 
 val map_vars : t -> f:(Var.t -> Var.t) -> t

sledge/src/sh.ml

@@ -141,15 +141,15 @@ let pp_block x fs segs =
     | {loc; bas; len; _} :: _ -> (
         Term.equal loc bas
         &&
-        match Term.d_int len with
-        | Some data -> (
+        match Term.get_z len with
+        | Some z -> (
           match
             List.fold segs (Some Z.zero) ~f:(fun seg len ->
-                match (len, Term.d_int seg.siz) with
-                | Some len, Some data -> Some (Z.add len data)
+                match (len, Term.get_z seg.siz) with
+                | Some len, Some siz -> Some (Z.add len siz)
                 | _ -> None )
           with
-          | Some blk_len -> Z.equal data blk_len
+          | Some blk_len -> Z.equal z blk_len
           | _ -> false )
         | _ -> false )
     | [] -> false

sledge/src/solver.ml

@@ -142,7 +142,7 @@ let fresh_var name vs zs ~wrt =
   let v = Term.var v in
   (v, vs, zs, wrt)
 
-let difference x e f = Term.d_int (Context.normalize x (Term.sub e f))
+let difference x e f = Term.get_z (Context.normalize x (Term.sub e f))
 let excise (k : Trace.pf -> _) = [%Trace.infok k]
 let trace (k : Trace.pf -> _) = [%Trace.infok k]
 

sledge/src/test/fol_test.ml

@@ -56,7 +56,7 @@ let%test_module _ =
     let union r s = union wrt r s |> snd
     let inter r s = inter wrt r s |> snd
     let implies_eq r a b = implies r (Formula.eq a b)
-    let difference x e f = Term.d_int (normalize x (Term.sub e f))
+    let difference x e f = Term.get_z (normalize x (Term.sub e f))
 
     (** tests *)