refactor(sat): remove unused values, split code off main functor

src/sat/Solver.ml

@@ -14,21 +14,6 @@ module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
 let invalid_argf fmt =
   Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt
 
-module Make (Plugin : PLUGIN) = struct
-  module Step_vec = Proof_trace.Step_vec
-
-  type theory = Plugin.t
-
-  module Clause_pool_id : sig
-    type t = private int
-
-    val _unsafe_of_int : int -> t
-  end = struct
-    type t = int
-
-    let _unsafe_of_int x = x
-  end
-
 (* ### types ### *)
 
 (* a boolean variable (positive int) *)
@@ -48,7 +33,6 @@ module Make (Plugin : PLUGIN) = struct
   val sign : t -> bool
   val of_var : var -> t
   val var : t -> var
-    val abs : t -> t
   val pa : var -> t
   val na : var -> t
 
@@ -61,7 +45,6 @@ module Make (Plugin : PLUGIN) = struct
   let[@inline] sign i = i land 1 = 0
   let[@inline] pa v = (v : var :> int) lsl 1
   let of_var = pa
-    let[@inline] abs a = a land lnot 1
   let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
   let[@inline] na v = ((v : var :> int) lsl 1) lor 1
 
@@ -69,8 +52,6 @@ module Make (Plugin : PLUGIN) = struct
   module ATbl = CCHashtbl.Make (CCInt)
 end
 
-  type atom = Atom0.t
-
 module Clause0 : sig
   include Int_id.S
   module Tbl : Hashtbl.S with type key = t
@@ -81,6 +62,10 @@ module Make (Plugin : PLUGIN) = struct
   module CVec = Veci
 end
 
+module Step_vec = Proof_trace.Step_vec
+
+type atom = Atom0.t
+
 type clause = Clause0.t
 and reason = Decision | Bcp of clause | Bcp_lazy of clause lazy_t
 
@@ -171,9 +156,6 @@ module Make (Plugin : PLUGIN) = struct
         };
     }
 
-    (** Number of variables *)
-    let[@inline] n_vars self : int = Vec.size self.v_level
-
   (** iterate on variables *)
   let iter_vars self f =
     Vec.iteri self.v_level ~f:(fun i _ -> f (Var0.of_int_unsafe i))
@@ -184,10 +166,7 @@ module Make (Plugin : PLUGIN) = struct
     let[@inline] level self v = Vec.get self.v_level (v : var :> int)
     let[@inline] set_level self v l = Vec.set self.v_level (v : var :> int) l
     let[@inline] reason self v = Vec.get self.v_reason (v : var :> int)
-
+    let[@inline] set_reason self v r = Vec.set self.v_reason (v : var :> int) r
-      let[@inline] set_reason self v r =
-        Vec.set self.v_reason (v : var :> int) r
-
     let[@inline] weight self v = Vec_float.get self.v_weight (v : var :> int)
 
     let[@inline] set_weight self v w =
@@ -215,10 +194,7 @@ module Make (Plugin : PLUGIN) = struct
     let[@inline] lit self a = Vec.get self.a_form (a : atom :> int)
     let lit = lit
     let[@inline] mark self a = Bitvec.set self.a_seen (a : atom :> int) true
-
+    let[@inline] unmark self a = Bitvec.set self.a_seen (a : atom :> int) false
-      let[@inline] unmark self a =
-        Bitvec.set self.a_seen (a : atom :> int) false
-
     let[@inline] marked self a = Bitvec.get self.a_seen (a : atom :> int)
     let[@inline] watched self a = Vec.get self.a_watched (a : atom :> int)
     let[@inline] is_true self a = Bitvec.get self.a_is_true (a : atom :> int)
@@ -281,9 +257,6 @@ module Make (Plugin : PLUGIN) = struct
 
     let debug_a self out vec =
       Array.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) vec
-
-      let debug_l self out l =
-        List.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) l
   end
 
   module Clause : sig
@@ -293,28 +266,24 @@ module Make (Plugin : PLUGIN) = struct
 
     val make_a : store -> removable:bool -> atom array -> Proof_step.id -> t
     val make_l : store -> removable:bool -> atom list -> Proof_step.id -> t
-      val make_vec : store -> removable:bool -> atom Vec.t -> Proof_step.id -> t
     val n_atoms : store -> t -> int
     val marked : store -> t -> bool
     val set_marked : store -> t -> bool -> unit
     val attached : store -> t -> bool
     val set_attached : store -> t -> bool -> unit
     val removable : store -> t -> bool
-      val set_removable : store -> t -> bool -> unit
     val dead : store -> t -> bool
     val set_dead : store -> t -> bool -> unit
 
     val dealloc : store -> t -> unit
     (** Delete the clause *)
 
-      val set_proof_step : store -> t -> Proof_step.id -> unit
     val proof_step : store -> t -> Proof_step.id
     val activity : store -> t -> float
     val set_activity : store -> t -> float -> unit
     val iter : store -> f:(atom -> unit) -> t -> unit
     val fold : store -> f:('a -> atom -> 'a) -> 'a -> t -> 'a
     val for_all : store -> f:(atom -> bool) -> t -> bool
-      val exists : store -> f:(atom -> bool) -> t -> bool
     val atoms_a : store -> t -> atom array
     val lits_l : store -> t -> Lit.t list
     val lits_a : store -> t -> Lit.t array
@@ -327,8 +296,7 @@ module Make (Plugin : PLUGIN) = struct
 
     (* TODO: store watch lists inside clauses *)
 
-      let make_a (store : store) ~removable (atoms : atom array) proof_step : t
+    let make_a (store : store) ~removable (atoms : atom array) proof_step : t =
-          =
       let {
         c_recycle_idx;
         c_lits;
@@ -370,9 +338,6 @@ module Make (Plugin : PLUGIN) = struct
     let make_l store ~removable atoms proof_rule : t =
       make_a store ~removable (Array.of_list atoms) proof_rule
 
-      let make_vec store ~removable atoms proof_rule : t =
-        make_a store ~removable (Vec.to_array atoms) proof_rule
-
     let[@inline] n_atoms (store : store) (c : t) : int =
       Array.length (Vec.get store.c_store.c_lits (c : t :> int))
 
@@ -388,12 +353,6 @@ module Make (Plugin : PLUGIN) = struct
         true
       with Early_exit -> false
 
-      let exists store ~f c =
-        try
-          iter store c ~f:(fun x -> if f x then raise_notrace Early_exit);
-          false
-        with Early_exit -> true
-
     let fold (store : store) ~f acc c =
       let { c_lits; _ } = store.c_store in
       Array.fold_left f acc (Vec.get c_lits (c : t :> int))
@@ -418,12 +377,6 @@ module Make (Plugin : PLUGIN) = struct
     let[@inline] removable store c =
       Bitvec.get store.c_store.c_removable (c : t :> int)
 
-      let[@inline] set_removable store c b =
-        Bitvec.set store.c_store.c_removable (c : t :> int) b
-
-      let[@inline] set_proof_step store c p =
-        Step_vec.set store.c_store.c_proof (c : t :> int) p
-
     let[@inline] proof_step store c =
       Step_vec.get store.c_store.c_proof (c : t :> int)
 
@@ -455,28 +408,12 @@ module Make (Plugin : PLUGIN) = struct
       (* recycle idx *)
       ()
 
-      let copy_flags store c1 c2 : unit =
-        set_removable store c2 (removable store c1);
-        ()
-
     let[@inline] activity store c =
       Vec_float.get store.c_store.c_activity (c : t :> int)
 
     let[@inline] set_activity store c f =
       Vec_float.set store.c_store.c_activity (c : t :> int) f
 
-      let[@inline] make_removable store l proof_rule : t =
-        make_l store ~removable:true l proof_rule
-
-      let[@inline] make_removable_a store a proof_rule =
-        make_a store ~removable:true a proof_rule
-
-      let[@inline] make_permanent store l proof_rule : t =
-        let c = make_l store ~removable:false l proof_rule in
-        assert (not (removable store c));
-        (* permanent by default *)
-        c
-
     let[@inline] atoms_a store c : atom array =
       Vec.get store.c_store.c_lits (c : t :> int)
 
@@ -507,8 +444,7 @@ module Make (Plugin : PLUGIN) = struct
   end
 
   (* allocate new variable *)
-    let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var
+  let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var =
-        =
     let {
       v_count;
       v_of_lit;
@@ -587,6 +523,9 @@ module Make (Plugin : PLUGIN) = struct
     | exception Not_found -> None
 end
 
+module Make (Plugin : PLUGIN) = struct
+  type theory = Plugin.t
+  type clause = Clause0.t
   type store = Store.t
 
   module Atom = Store.Atom
@@ -665,8 +604,6 @@ module Make (Plugin : PLUGIN) = struct
     let descr = P.descr
     let add c = Vec.push clauses_ c
     let iter ~f = Vec.iter ~f clauses_
-    let push_level () = ()
-    let pop_levels _ = ()
     let size () = Vec.size clauses_
     let needs_gc () = size () > !P.max_size
 
@@ -699,7 +636,6 @@ module Make (Plugin : PLUGIN) = struct
               end)
               ())
 
-  let[@inline] cp_descr_ (module P : CLAUSE_POOL) : string = P.descr ()
   let[@inline] cp_size_ (module P : CLAUSE_POOL) : int = P.size ()
   let[@inline] cp_needs_gc_ (module P : CLAUSE_POOL) : bool = P.needs_gc ()
   let[@inline] cp_add_ (module P : CLAUSE_POOL) c : unit = P.add c
@@ -718,10 +654,8 @@ module Make (Plugin : PLUGIN) = struct
 
     val create : unit -> t
     val is_empty : t -> bool
-    val clear : t -> unit
     val clear_on_backtrack : t -> unit
     val add_clause_learnt : t -> clause -> unit
-    val add_clause_pool : t -> clause -> clause_pool -> unit
     val propagate_atom : t -> atom -> lvl:int -> clause lazy_t -> unit
     val add_decision : t -> atom -> unit
 
@@ -794,9 +728,6 @@ module Make (Plugin : PLUGIN) = struct
       && CVec.is_empty clauses_to_add_learnt
       && Vec.is_empty decisions && Vec.is_empty propagate
 
-    let add_clause_pool (self : t) c pool =
-      Vec.push self.clauses_to_add_in_pool (c, pool)
-
     let add_clause_learnt (self : t) c = CVec.push self.clauses_to_add_learnt c
 
     let propagate_atom self p ~lvl c =
@@ -1027,13 +958,6 @@ module Make (Plugin : PLUGIN) = struct
   *)
   exception Trivial
 
-  (* [arr_to_list a i] converts [a.(i), ... a.(length a-1)] into a list *)
-  let arr_to_list arr i : _ list =
-    if i >= Array.length arr then
-      []
-    else
-      Array.to_list (Array.sub arr i (Array.length arr - i))
-
   (* get/build the proof for [a], which must be an atom true at level 0.
      This uses a global cache to avoid repeated computations, as many clauses
      might resolve against a given 0-level atom. *)
@@ -1259,35 +1183,6 @@ module Make (Plugin : PLUGIN) = struct
       Format.fprintf out "(@[unsat-cause@ :false %a@])"
         (Clause.debug self.store) c
 
-  let prove_unsat self (us : clause) : clause =
-    if Proof_trace.enabled self.proof && Clause.n_atoms self.store us > 0 then (
-      (* reduce [c] to an empty clause, all its literals should be false at level 0 *)
-      Log.debugf 1 (fun k ->
-          k "(@[sat.prove-unsat@ :from %a@])" (Clause.debug self.store) us);
-
-      (* accumulate proofs of all level-0 lits *)
-      let pvec = self.temp_step_vec in
-      assert (Step_vec.is_empty pvec);
-      Clause.iter self.store us ~f:(fun a ->
-          assert (Atom.is_false self.store a && Atom.level self.store a = 0);
-          match Atom.reason self.store a with
-          | Some (Bcp c | Bcp_lazy (lazy c)) ->
-            let p = Clause.proof_step self.store c in
-            Step_vec.push pvec p
-          | _ -> assert false);
-
-      let p_empty =
-        Proof_trace.add_step self.proof
-        @@ Proof_sat.sat_redundant_clause Iter.empty
-             ~hyps:(Step_vec.to_iter pvec)
-      in
-      Step_vec.clear pvec;
-      let c_empty = Clause.make_l self.store [] ~removable:false p_empty in
-
-      c_empty
-    ) else
-      us
-
   (* Unsatisfiability is signaled through an exception, since it can happen
      in multiple places (adding new clauses, or solving for instance). *)
   let report_unsat self (us : unsat_cause) : _ =
@@ -1836,8 +1731,6 @@ module Make (Plugin : PLUGIN) = struct
 
   exception Th_conflict of Clause.t
 
-  let[@inline] slice_get st i = AVec.get st.trail i
-
   let acts_add_clause self ?(keep = false) (l : Lit.t list) (p : Proof_step.id)
       : unit =
     let atoms = List.rev_map (make_atom_ self) l in
@@ -1848,18 +1741,6 @@ module Make (Plugin : PLUGIN) = struct
     (* will be added later, even if we backtrack *)
     Delayed_actions.add_clause_learnt self.delayed_actions c
 
-  let acts_add_clause_in_pool self ~pool (l : Lit.t list) (p : Proof_step.id) :
-      unit =
-    let atoms = List.rev_map (make_atom_ self) l in
-    let removable = true in
-    let c = Clause.make_l self.store ~removable atoms p in
-    let pool = Vec.get self.clause_pools (pool : Clause_pool_id.t :> int) in
-    Log.debugf 5 (fun k ->
-        k "(@[sat.th.add-clause-in-pool@ %a@ :pool %s@])"
-          (Clause.debug self.store) c (cp_descr_ pool));
-    (* will be added later, even if we backtrack *)
-    Delayed_actions.add_clause_pool self.delayed_actions c pool
-
   let acts_add_decision_lit (self : t) (f : Lit.t) (sign : bool) : unit =
     let store = self.store in
     let a = make_atom_ self f in
@@ -2328,7 +2209,6 @@ module Make (Plugin : PLUGIN) = struct
       raise UndecidedLit
 
   let[@inline] eval st lit = fst @@ eval_level st lit
-  let[@inline] unsat_conflict st = st.unsat_at_0
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
@@ -2439,8 +2319,6 @@ module Make (Plugin : PLUGIN) = struct
     pp_all self 99 "SAT";
     let t = self.trail in
     let module M = struct
-      type lit = Lit.t
-
       let iter_trail f = AVec.iter ~f:(fun a -> f (Atom.lit self.store a)) t
       let[@inline] eval f = eval self (make_atom_ self f)
       let[@inline] eval_level f = eval_level self (make_atom_ self f)
@@ -2684,4 +2562,4 @@ module Pure_sat = Make (struct
   let final_check () _ = ()
   let has_theory = false
 end)
-[@@inline] [@@specialise]
+[@@specialise]

src/sat/dune

@@ -2,5 +2,6 @@
  (name sidekick_sat)
  (public_name sidekick.sat)
  (synopsis "Pure OCaml SAT solver implementation for sidekick")
+ (private_modules heap heap_intf)
  (libraries iter sidekick.util sidekick.core)
  (flags :standard -w +32 -open Sidekick_util))