[sledge] Add Term.is_constant

Reviewed By: jvillard

Differential Revision: D20863523

fbshipit-source-id: 4998d7376

sledge/lib/import/qset.ml

@@ -83,5 +83,6 @@ struct
   let to_list m = M.to_alist m
   let iter m ~f = M.iteri ~f:(fun ~key ~data -> f key data) m
   let exists m ~f = M.existsi ~f:(fun ~key ~data -> f key data) m
+  let for_all m ~f = M.for_alli ~f:(fun ~key ~data -> f key data) m
   let fold m ~f ~init = M.fold ~f:(fun ~key ~data -> f key data) m ~init
 end

sledge/lib/import/qset_intf.ml

@@ -79,6 +79,9 @@ module type S = sig
   val exists : t -> f:(elt -> Q.t -> bool) -> bool
   (** Search for an element satisfying a predicate. *)
 
+  val for_all : t -> f:(elt -> Q.t -> bool) -> bool
+  (** Test whether all elements satisfy a predicate. *)
+
   val fold : t -> f:(elt -> Q.t -> 's -> 's) -> init:'s -> 's
   (** Fold over the elements in ascending order. *)
 end

sledge/lib/term.ml

@@ -1186,6 +1186,15 @@ let exists e ~f =
   | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ -> false
 
+let for_all e ~f =
+  match e with
+  | Ap1 (_, x) -> f x
+  | Ap2 (_, x, y) -> f x && f y
+  | Ap3 (_, x, y, z) -> f x && f y && f z
+  | ApN (_, xs) | RecN (_, xs) -> IArray.for_all ~f xs
+  | Add args | Mul args -> Qset.for_all ~f:(fun arg _ -> f arg) args
+  | Var _ | Label _ | Nondet _ | Float _ | Integer _ | Rational _ -> true
+
 let fold e ~init:s ~f =
   match e with
   | Ap1 (_, x) -> f x s
@@ -1245,6 +1254,11 @@ 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 rec is_constant = function
+  | Var _ -> false
+  | Label _ | Nondet _ | Float _ | Integer _ | Rational _ -> true
+  | a -> for_all ~f:is_constant a
+
 let height e =
   let height_ height_ = function
     | Var _ -> 0

sledge/lib/term.mli

@@ -251,6 +251,10 @@ 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 is_constant : t -> bool
+(** Test if a term's semantics is independent of the values of variables. *)
+
 val height : t -> int
 
 (** Solve *)