From 0879afe950a244d1b45a8d2e31bd5849545b3716 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:24:59 -0800
Subject: [PATCH] [sledge] Remove dead Domain.is_false

Reviewed By: jvillard

Differential Revision: D25756561

fbshipit-source-id: 9de9f97c2
---
 sledge/src/domain_intf.ml         | 1 -
 sledge/src/domain_relation.ml     | 2 --
 sledge/src/domain_sh.ml           | 1 -
 sledge/src/domain_unit.ml         | 1 -
 sledge/src/domain_used_globals.ml | 1 -
 5 files changed, 6 deletions(-)

diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index de84026e1..03b4de3c1 100644
--- a/sledge/src/domain_intf.ml
+++ b/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
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index 88e7c64ce..5736e0c6f 100644
--- a/sledge/src/domain_relation.ml
+++ b/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)
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 396ec1501..4d637c291 100644
--- a/sledge/src/domain_sh.ml
+++ b/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
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index 0c5f11f06..36bb89895 100644
--- a/sledge/src/domain_unit.ml
+++ b/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 _ () = ()
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 9f2ced8d1..5ff7c806f 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/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]