wip: refactor

src/core/Sidekick_core.ml

@@ -957,10 +957,11 @@ module type SOLVER = sig
 
     val equal : t -> t -> bool
     val hash : t -> int
-    val pp : t CCFormat.printer
+
+    val pp : solver -> t CCFormat.printer
+    val formula : solver -> t -> lit
 
     val neg : t -> t
-    val formula : t -> lit
     val sign : t -> bool
   end
 

src/sat/Solver.ml

@@ -13,6 +13,24 @@ 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 type INT_ID = sig
+  type t = private int
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val hash : t -> int
+  val to_int : t -> int
+  val of_int_unsafe : int -> t
+end
+
+module Mk_int_id() = struct
+  type t = int
+  let equal : t -> t -> bool = (=)
+  let compare : t -> t -> int = compare
+  let hash = CCHash.int
+  let[@inline] to_int i = i
+  let[@inline] of_int_unsafe i = i
+end
+
 module Make(Plugin : PLUGIN)
 = struct
   module Formula = Plugin.Formula
@@ -21,27 +39,28 @@ module Make(Plugin : PLUGIN)
   type theory = Plugin.t
   type lemma = Plugin.proof
 
-  type var = {
+  (* ### types ### *)
-    vid : int;
-    pa : atom;
-    na : atom;
-    mutable v_fields : int;
-    mutable v_level : int;
-    mutable v_idx: int; (** position in heap *)
-    mutable v_weight : float; (** Weight (for the heap), tracking activity *)
-    mutable reason : reason option;
-  }
 
-  and atom = {
+  (* a boolean variable (positive int) *)
-    aid : int;
+  module Var : INT_ID = Mk_int_id()
-    var : var;
+  type var = Var.t
-    neg : atom;
-    lit : formula;
-    mutable is_true : bool;
-    watched : clause Vec.t;
-  }
 
-  and clause = {
+  (* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *)
+  module Atom : sig
+    include INT_ID
+    val of_var : var -> t
+    val neg : t -> t
+    val sign : t -> bool
+  end = struct
+    include Mk_int_id()
+    let[@inline] of_var v = (v:var:>int) lsl 1
+    let[@inline] neg i = (i lxor 1)
+    let[@inline] sign i = (i land 1) = 0
+  end
+  type atom = Atom.t
+
+  (* TODO: special clause allocator *)
+  type clause = {
     cid: int;
     atoms : atom array;
     mutable cpremise : premise;
@@ -49,11 +68,6 @@ module Make(Plugin : PLUGIN)
     mutable flags: int; (* bitfield *)
   }
 
-  and reason =
-    | Decision
-    | Bcp of clause
-    | Bcp_lazy of clause lazy_t
-
   (* TODO: remove, replace with user-provided proof trackng device?
      for pure SAT, [reason] is sufficient *)
   and premise =
@@ -63,98 +77,124 @@ module Make(Plugin : PLUGIN)
     | History of clause list
     | Empty_premise
 
-  (* Constructors *)
+  and reason =
-  module MF = Hashtbl.Make(Formula)
+    | Decision
+    | Bcp of clause
+    | Bcp_lazy of clause lazy_t
 
-  (* state for variables. declared separately because it simplifies our
+  (* ### stores ### *)
+
+  module Form_tbl = Hashtbl.Make(Formula)
+
+  (* variable store. declared separately because it simplifies our
      life below, as it's required to construct new atoms/variables *)
-  type st = {
+  module Vars = struct
-    f_map: var MF.t;
+    type t = {
-    vars: var Vec.t;
+      of_form: var Form_tbl.t;
-    mutable cpt_mk_var: int;
+      level: int Vec.t;
-    mutable cpt_mk_clause: int;
+      heap_idx: int Vec.t;
-  }
+      weight: float Vec.t;
-
+      reason: reason option Vec.t;
-  let create_st ?(size=`Big) () : st =
+      seen: Bitvec.t;
-    let size_map = match size with
+      default_polarity: Bitvec.t;
-      | `Tiny -> 8
+      mutable count : int;
-      | `Small -> 16
-      | `Big -> 4096
-    in
-    { f_map = MF.create size_map;
-      vars = Vec.create();
-      cpt_mk_var = 0;
-      cpt_mk_clause = 0;
     }
 
-  let nb_elt st = Vec.size st.vars
+    let create ?(size=`Big) () : t =
-  let get_elt st i = Vec.get st.vars i
+      let size_map = match size with
-  let iter_elt st f = Vec.iter f st.vars
+        | `Tiny -> 8
+        | `Small -> 16
+        | `Big -> 4096
+      in
+      { of_form = Form_tbl.create size_map;
+        level = Vec.create();
+        heap_idx = Vec.create();
+        weight = Vec.create();
+        reason = Vec.create();
+        seen = Bitvec.create();
+        default_polarity = Bitvec.create();
+        count = 1;
+      }
 
-  let kind_of_clause c = match c.cpremise with
+    (* allocate new variable *)
-    | Hyp _ -> "H"
+    let alloc ?default_pol:(pol=true) self (form:formula) : var =
-    | Lemma _ -> "T"
+      let {count; of_form; level; heap_idx; weight;
-    | Local -> "L"
+           reason; seen; default_polarity; } = self in
-    | History _ -> "C"
+      let v_idx = count in
-    | Empty_premise -> ""
+      let var = Var.of_int_unsafe v_idx in
+      self.count <- 1 + count;
+      Form_tbl.add of_form form var;
+      Vec.push level (-1);
+      Vec.push heap_idx (-1);
+      Vec.push reason None;
+      Vec.push weight 0.;
+      Bitvec.ensure_size seen v_idx;
+      Bitvec.ensure_size default_polarity v_idx;
+      Bitvec.set default_polarity v_idx pol;
+      var
 
-  (* some boolean flags for variables, used as masks *)
+    let[@inline] level self v = Vec.get self.level (v:var:>int)
-  let seen_var = 0b1
+    let[@inline] reason self v = Vec.get self.reason (v:var:>int)
-  let seen_pos = 0b10
+    let[@inline] weight self v = Vec.get self.weight (v:var:>int)
-  let seen_neg = 0b100
+    let[@inline] set_weight self v w = Vec.set self.weight (v:var:>int) w
-  let default_pol_true = 0b1000
+    let[@inline] mark self v = Bitvec.set self.seen (v:var:>int) true
+    let[@inline] unmark self v = Bitvec.set self.seen (v:var:>int) false
+    let[@inline] marked self v = Bitvec.get self.seen (v:var:>int)
+    let[@inline] set_default_pol self v b = Bitvec.set self.default_polarity (v:var:>int) b
+    let[@inline] default_pol self v = Bitvec.get self.default_polarity (v:var:>int)
+    let[@inline] heap_idx self v = Vec.get self.heap_idx (v:var:>int)
+    let[@inline] set_idx self v i = Vec.set self.heap_idx (v:var:>int) i
+  end
 
-  module Var = struct
+  module Atoms = struct
-    let[@inline] level v = v.v_level
+    type t = {
-    let[@inline] pos v = v.pa
+      positive: bool; (* is this for positive atoms *)
-    let[@inline] neg v = v.na
+      is_true: Bitvec.t;
-    let[@inline] reason v = v.reason
+      seen: Bitvec.t;
-    let[@inline] weight v = v.v_weight
+      form: formula Vec.t;
-    let[@inline] set_weight v w = v.v_weight <- w
+      (* TODO: store watches in clauses instead *)
-    let[@inline] mark v = v.v_fields <- v.v_fields lor seen_var
+      watched: clause Vec.t Vec.t;
-    let[@inline] unmark v = v.v_fields <- v.v_fields land (lnot seen_var)
+    }
-    let[@inline] marked v = (v.v_fields land seen_var) <> 0
-    let[@inline] set_default_pol_true v = v.v_fields <- v.v_fields lor default_pol_true
-    let[@inline] set_default_pol_false v = v.v_fields <- v.v_fields land (lnot default_pol_true)
-    let[@inline] default_pol v = (v.v_fields land default_pol_true) <> 0
-    let[@inline] idx v = v.v_idx
-    let[@inline] set_idx v i = v.v_idx <- i
 
-    let make ?(default_pol=true) (st:st) (t:formula) : var * Solver_intf.negated =
+    let create ~positive () : t =
-      let lit, negated = Formula.norm t in
+      { positive;
-      try
+        is_true=Bitvec.create();
-        MF.find st.f_map lit, negated
+        form=Vec.create();
-      with Not_found ->
+        watched=Vec.create();
-        let cpt_double = st.cpt_mk_var lsl 1 in
+        seen=Bitvec.create();
-        let rec var  =
+      }
-          { vid = st.cpt_mk_var;
+
-            pa = pa;
+    let of_var (self:t) (v:Var.t) : atom =
-            na = na;
+      let a = Atom.of_var v in
-            v_fields = 0;
+      if self.positive then a else Atom.neg a
-            v_level = -1;
+
-            v_idx= -1;
+    let alloc (self:t) (v:Var.t) (f:formula) : unit =
-            v_weight = 0.;
+      let {positive; is_true; seen; watched; form; } = self in
-            reason = None;
+      assert (Vec.size form = (v:var:>int) - 1);
-          }
+      Bitvec.ensure_size is_true (v:var:>int);
-        and pa =
+      Bitvec.ensure_size seen (v:var:>int);
-          { var = var;
+      Vec.push form f;
-            lit = lit;
+      ()
-            watched = Vec.create();
+  end
-            neg = na;
+
-            is_true = false;
+  (* state holding variables *)
-            aid = cpt_double (* aid = vid*2 *) }
+  type st = {
-        and na =
+    vars: Vars.t;
-          { var = var;
+    pa: Atoms.t;
-            lit = Formula.neg lit;
+    na: Atoms.t;
-            watched = Vec.create();
+  }
-            neg = pa;
+
-            is_true = false;
+  (* create new variable *)
-            aid = cpt_double + 1 (* aid = vid*2+1 *) } in
+  let mk_var (self:st) ?default_pol (t:formula) : var * Solver_intf.negated =
-        MF.add st.f_map lit var;
+    let form, negated = Formula.norm t in
-        st.cpt_mk_var <- st.cpt_mk_var + 1;
+    try Form_tbl.find self.vars.Vars.of_form form, negated
-        if default_pol then set_default_pol_true var;
+    with Not_found ->
-        Vec.push st.vars var;
+      let v = Vars.alloc ?default_pol self.vars form in
-        var, negated
+      Atoms.alloc self.pa v form;
+      Atoms.alloc self.na v (Formula.neg form);
+      v, negated
+
+  (* FIXME
 
     (* Marking helpers *)
     let[@inline] clear v =
@@ -163,7 +203,20 @@ module Make(Plugin : PLUGIN)
     let[@inline] seen_both v =
       (seen_pos land v.v_fields <> 0) &&
       (seen_neg land v.v_fields <> 0)
-  end
+     *)
+
+  (*
+  let nb_elt st = Vec.size st.vars
+  let get_elt st i = Vec.get st.vars i
+  let iter_elt st f = Vec.iter f st.vars
+     *)
+
+  let kind_of_clause c = match c.cpremise with
+    | Hyp _ -> "H"
+    | Lemma _ -> "T"
+    | Local -> "L"
+    | History _ -> "C"
+    | Empty_premise -> ""
 
   module Atom = struct
     type t = atom

src/sat/Solver_intf.ml

@@ -335,8 +335,9 @@ module type S = sig
     val neg : t -> t
     val sign : t -> bool
     val abs : t -> t
-    val formula : t -> formula
+
-    val pp : t printer
+    val formula : solver -> t -> formula
+    val pp : solver -> t printer
   end
 
   module Clause : sig