[sledge] Remove dead Domain.is_false

Reviewed By: jvillard

Differential Revision: D25756561

fbshipit-source-id: 9de9f97c2

sledge/src/domain_intf.ml

@@ -13,7 +13,6 @@ module type Dom = sig
   val report_fmt_thunk : t -> Format.formatter -> unit
   val init : Llair.GlobalDefn.t iarray -> t
   val join : t -> t -> t option
-  val is_false : t -> bool
   val dnf : t -> t list
   val exec_assume : t -> Llair.Exp.t -> t option
   val exec_kill : Llair.Reg.t -> t -> t

sledge/src/domain_relation.ml

@@ -40,8 +40,6 @@ module Make (State_domain : State_domain_sig) = struct
       (entry_a, next)
     else None
 
-  let is_false (_, curr) = State_domain.is_false curr
-
   let exec_assume (entry, current) cnd =
     let+ next = State_domain.exec_assume current cnd in
     (entry, next)

sledge/src/domain_sh.ml

@@ -41,7 +41,6 @@ let join p q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" pp)]
 
-let is_false = Sh.is_unsat
 let dnf = Sh.dnf
 let exec_assume q b = Exec.assume q (X.formula b) |> Option.map ~f:simplify
 let exec_kill r q = Exec.kill q (X.reg r) |> simplify

sledge/src/domain_unit.ml

@@ -13,7 +13,6 @@ let pp fs () = Format.pp_print_string fs "()"
 let report_fmt_thunk () fs = pp fs ()
 let init _ = ()
 let join () () = Some ()
-let is_false _ = false
 let exec_assume () _ = Some ()
 let exec_kill _ () = ()
 let exec_move _ () = ()

sledge/src/domain_used_globals.ml

@@ -20,7 +20,6 @@ let init globals =
 
 let join l r = Some (Llair.Global.Set.union l r)
 let recursion_beyond_bound = `skip
-let is_false _ = false
 let post _ _ state = state
 let retn _ _ from_call post = Llair.Global.Set.union from_call post
 let dnf t = [t]