From 128e7dceb8656524b9ccb7831c26865ec19d5e29 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 10 Jun 2019 10:46:16 -0500
Subject: [PATCH] refactor: move `Hash` to util/; fix some warnings

---
 src/msat-solver/Sidekick_msat_solver.ml | 9 ---------
 src/{base-term => util}/Hash.ml         | 0
 src/{base-term => util}/Hash.mli        | 0
 src/util/Sidekick_util.ml               | 2 +-
 4 files changed, 1 insertion(+), 10 deletions(-)
 rename src/{base-term => util}/Hash.ml (100%)
 rename src/{base-term => util}/Hash.mli (100%)

diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index ee5c100f..68fda661 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -31,8 +31,6 @@ module Make(A : ARG)
     let[@inline] sign t = t.lit_sign
     let[@inline] term (t:t): term = t.lit_term
 
-    let[@inline] abs t: t = {t with lit_sign=true}
-
     let make ~sign t = {lit_sign=sign; lit_term=t}
 
     let atom tst ?(sign=true) (t:term) : t =
@@ -40,8 +38,6 @@ module Make(A : ARG)
       let sign = if not sign' then not sign else sign in
       make ~sign t
 
-    let[@inline] as_atom (lit:t) = lit.lit_term, lit.lit_sign
-
     let equal a b =
       a.lit_sign = b.lit_sign &&
       T.equal a.lit_term b.lit_term
@@ -54,8 +50,6 @@ module Make(A : ARG)
       if l.lit_sign then T.pp out l.lit_term
       else Format.fprintf out "(@[@<1>¬@ %a@])" T.pp l.lit_term
 
-    let print = pp
-
     let apply_sign t s = if s then t else neg t
     let norm_sign l = if l.lit_sign then l, true else neg l, false
     let norm l = let l, sign = norm_sign l in l, if sign then Msat.Same_sign else Msat.Negated
@@ -365,9 +359,6 @@ module Make(A : ARG)
   (** the parametrized SAT Solver *)
   module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
 
-  let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
-    Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
-
   module Atom = Sat_solver.Atom
   module Proof = struct
     include Sat_solver.Proof
diff --git a/src/base-term/Hash.ml b/src/util/Hash.ml
similarity index 100%
rename from src/base-term/Hash.ml
rename to src/util/Hash.ml
diff --git a/src/base-term/Hash.mli b/src/util/Hash.mli
similarity index 100%
rename from src/base-term/Hash.mli
rename to src/util/Hash.mli
diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml
index 7b216231..7c656cba 100644
--- a/src/util/Sidekick_util.ml
+++ b/src/util/Sidekick_util.ml
@@ -1,4 +1,3 @@
-
 (* re-exports *)
 module Fmt = CCFormat
 module Vec = Msat.Vec
@@ -11,3 +10,4 @@ module IArray = IArray
 module Intf = Intf
 module Bag = Bag
 module Stat = Stat
+module Hash = Hash