wip: split VecI32 and VecSmallInt

- use VecSmallInt for small integers of type `int`
- use VecI32 to store actual int32 (in particular for proof steps)

src/base-solver/sidekick_base_solver.ml

@@ -14,7 +14,7 @@ module Solver_arg = struct
 
   let cc_view = Term.cc_view
   let is_valid_literal _ = true
-  module P = Proof_stub
+  module P = Proof_dummy
   type proof = P.t
   type proof_step = P.proof_step
 end
@@ -27,7 +27,7 @@ module Th_data = Sidekick_th_data.Make(struct
     module S = Solver
     open! Base_types
     open! Sidekick_th_data
-    module Proof = Proof_stub
+    module Proof = Proof_dummy
     module Cstor = Cstor
 
     let as_datatype ty = match Ty.view ty with
@@ -75,11 +75,11 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   module S = Solver
   type term = S.T.Term.t
   include Form
-  let lemma_bool_tauto = Proof_stub.lemma_bool_tauto
+  let lemma_bool_tauto = Proof_dummy.lemma_bool_tauto
-  let lemma_bool_c = Proof_stub.lemma_bool_c
+  let lemma_bool_c = Proof_dummy.lemma_bool_c
-  let lemma_bool_equiv = Proof_stub.lemma_bool_equiv
+  let lemma_bool_equiv = Proof_dummy.lemma_bool_equiv
-  let lemma_ite_true = Proof_stub.lemma_ite_true
+  let lemma_ite_true = Proof_dummy.lemma_ite_true
-  let lemma_ite_false = Proof_stub.lemma_ite_false
+  let lemma_ite_false = Proof_dummy.lemma_ite_false
 end)
 
 (** Theory of Linear Rational Arithmetic *)
@@ -102,7 +102,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   let ty_lra _st = Ty.real()
   let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
 
-  let lemma_lra = Proof_stub.lemma_lra
+  let lemma_lra = Proof_dummy.lemma_lra
 
   module Gensym = struct
     type t = {

src/base/Proof.ml

@@ -66,8 +66,6 @@ type proof_rule = t -> proof_step
 module Step_vec = struct
   type elt=proof_step
   include VecI32
-  let get = get_i32
-  let set = set_i32
 end
 
 let disable (self:t) : unit =
@@ -134,18 +132,18 @@ let[@inline] enabled (self:t) = self.enabled
 
 let begin_subproof _ = dummy_step
 let end_subproof _ = dummy_step
-let del_clause _ _ (_pr:t) = dummy_step
 let emit_redundant_clause _ ~hyps:_ _ = dummy_step
 let emit_input_clause _ _ = dummy_step
 let define_term _ _ _ = dummy_step
-let emit_unsat _ _ = dummy_step
 let proof_p1 _ _ (_pr:t) = dummy_step
-let emit_unsat_core _ (_pr:t) = dummy_step
 let lemma_preprocess _ _ ~using:_ (_pr:t) = dummy_step
 let lemma_true _ _ = dummy_step
 let lemma_cc _ _ = dummy_step
 let lemma_rw_clause _ ~using:_ (_pr:t) = dummy_step
 let with_defs _ _ (_pr:t) = dummy_step
+let del_clause _ _ (_pr:t) = ()
+let emit_unsat_core _ (_pr:t) = dummy_step
+let emit_unsat _ _ = ()
 
 let lemma_lra _ _ = dummy_step
 

src/checker/drup_check.ml

@@ -71,7 +71,7 @@ end
     Each event is checked by reverse-unit propagation on previous events. *)
 module Fwd_check : sig
   type error =
-    [ `Bad_steps of VecI32.t
+    [ `Bad_steps of VecSmallInt.t
     | `No_empty_clause
     ]
 
@@ -84,11 +84,11 @@ module Fwd_check : sig
 end = struct
   type t = {
     checker: Checker.t;
-    errors: VecI32.t;
+    errors: VecSmallInt.t;
   }
   let create cstore : t = {
     checker=Checker.create cstore;
-    errors=VecI32.create();
+    errors=VecSmallInt.create();
   }
 
   (* check event, return [true] if it's valid *)
@@ -114,17 +114,17 @@ end = struct
     end
 
   type error =
-    [ `Bad_steps of VecI32.t
+    [ `Bad_steps of VecSmallInt.t
     | `No_empty_clause
     ]
 
   let pp_error trace out = function
     | `No_empty_clause -> Fmt.string out "no empty clause found"
     | `Bad_steps bad ->
-      let n0 = VecI32.get bad 0 in
+      let n0 = VecSmallInt.get bad 0 in
       Fmt.fprintf out
         "@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]"
-        (VecI32.size bad) n0
+        (VecSmallInt.size bad) n0
         Trace.pp_op (Trace.get trace n0)
 
   let check trace : _ result =
@@ -148,12 +148,12 @@ end = struct
           ) else (
             Log.debugf 10
               (fun k->k"(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
-            VecI32.push self.errors i
+            VecSmallInt.push self.errors i
           ));
 
-    Log.debugf 10 (fun k->k"found %d errors" (VecI32.size self.errors));
+    Log.debugf 10 (fun k->k"found %d errors" (VecSmallInt.size self.errors));
     if not !has_false then Error `No_empty_clause
-    else if VecI32.size self.errors > 0 then Error (`Bad_steps self.errors)
+    else if VecSmallInt.size self.errors > 0 then Error (`Bad_steps self.errors)
     else Ok ()
 end
 

src/drup/sidekick_drup.ml

@@ -6,7 +6,7 @@
 *)
 
 module Fmt = CCFormat
-module VecI32 = VecI32
+module VecSmallInt = VecSmallInt
 
 (* TODO: resolution proof construction, optionally *)
 
@@ -108,7 +108,7 @@ module Make() : S = struct
       let set = Vec.set
     end
     module Stack = struct
-      include VecI32
+      include VecSmallInt
       let create()=create()
     end
   end

src/sat/Heap.ml

@@ -9,14 +9,14 @@ module Make(Elt : RANKED) = struct
 
   type t = {
     store : elt_store;
-    heap : VecI32.t; (* vec of elements *)
+    heap : VecSmallInt.t; (* vec of elements *)
   }
 
   let _absent_index = -1
 
   let create store : t =
     { store;
-      heap = VecI32.create(); }
+      heap = VecSmallInt.create(); }
 
   let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
   let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
@@ -24,15 +24,15 @@ module Make(Elt : RANKED) = struct
 
   (*
   let rec heap_property cmp ({heap=heap} as s) i =
-    i >= (VecI32.size heap)  ||
+    i >= (VecSmallInt.size heap)  ||
       ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
        && heap_property cmp s (left i) && heap_property cmp s (right i))
 
   let heap_property cmp s = heap_property cmp s 1
   *)
 
-  let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecI32.get self.heap i)
+  let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecSmallInt.get self.heap i)
-  let[@inline] set_elt_ self i elt = VecI32.set self.heap i (elt:Elt.t:>int)
+  let[@inline] set_elt_ self i elt = VecSmallInt.set self.heap i (elt:Elt.t:>int)
 
   (* [elt] is above or at its expected position. Move it up the heap
      (towards high indices) to restore the heap property *)
@@ -49,7 +49,7 @@ module Make(Elt : RANKED) = struct
     Elt.set_heap_idx self.store elt !i
 
   let percolate_down (self:t) (elt:Elt.t): unit =
-    let sz = VecI32.size self.heap in
+    let sz = VecSmallInt.size self.heap in
     let li = ref (left (Elt.heap_idx self.store elt)) in
     let ri = ref (right (Elt.heap_idx self.store elt)) in
     let i = ref (Elt.heap_idx self.store elt) in
@@ -85,7 +85,7 @@ module Make(Elt : RANKED) = struct
 
   let filter (self:t) filt : unit =
     let j = ref 0 in
-    let lim = VecI32.size self.heap in
+    let lim = VecSmallInt.size self.heap in
     for i = 0 to lim - 1 do
       if filt (get_elt_ self i) then (
         set_elt_ self !j (get_elt_ self i);
@@ -95,24 +95,24 @@ module Make(Elt : RANKED) = struct
         Elt.set_heap_idx self.store (get_elt_ self i) _absent_index;
       );
     done;
-    VecI32.shrink self.heap (lim - !j);
+    VecSmallInt.shrink self.heap (lim - !j);
     for i = (lim / 2) - 1 downto 0 do
       percolate_down self (get_elt_ self i)
     done
 
-  let[@inline] size s = VecI32.size s.heap
+  let[@inline] size s = VecSmallInt.size s.heap
-  let[@inline] is_empty s = VecI32.is_empty s.heap
+  let[@inline] is_empty s = VecSmallInt.is_empty s.heap
 
   let clear self : unit =
-    VecI32.iter self.heap
+    VecSmallInt.iter self.heap
       ~f:(fun e -> Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index);
-    VecI32.clear self.heap;
+    VecSmallInt.clear self.heap;
     ()
 
   let insert self elt =
     if not (in_heap self elt) then (
-      Elt.set_heap_idx self.store elt (VecI32.size self.heap);
+      Elt.set_heap_idx self.store elt (VecSmallInt.size self.heap);
-      VecI32.push self.heap (elt:Elt.t:>int);
+      VecSmallInt.push self.heap (elt:Elt.t:>int);
       percolate_up self elt;
     )
 
@@ -131,20 +131,20 @@ module Make(Elt : RANKED) = struct
   *)
 
   let remove_min self =
-    match VecI32.size self.heap with
+    match VecSmallInt.size self.heap with
     | 0 -> raise Not_found
     | 1 ->
-      let x = Elt.of_int_unsafe (VecI32.pop self.heap) in
+      let x = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in
       Elt.set_heap_idx self.store x _absent_index;
       x
     | _ ->
       let x = get_elt_ self 0 in
-      let new_hd = Elt.of_int_unsafe (VecI32.pop self.heap) in (* heap.last() *)
+      let new_hd = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in (* heap.last() *)
       set_elt_ self 0 new_hd;
       Elt.set_heap_idx self.store x _absent_index;
       Elt.set_heap_idx self.store new_hd 0;
       (* enforce heap property again *)
-      if VecI32.size self.heap > 1 then (
+      if VecSmallInt.size self.heap > 1 then (
         percolate_down self new_hd;
       );
       x

src/sat/Solver.ml

@@ -58,7 +58,7 @@ module Make(Plugin : PLUGIN)
     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)
-    module AVec = VecI32
+    module AVec = VecSmallInt
   end
   type atom = Atom0.t
 
@@ -69,7 +69,7 @@ module Make(Plugin : PLUGIN)
   end = struct
     include Int_id.Make()
     module Tbl = Util.Int_tbl
-    module CVec = VecI32
+    module CVec = VecSmallInt
   end
   type clause = Clause0.t
 
@@ -93,7 +93,7 @@ module Make(Plugin : PLUGIN)
     type cstore = {
       c_lits: atom array Vec.t; (* storage for clause content *)
       c_activity: Vec_float.t;
-      c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *)
+      c_recycle_idx: VecSmallInt.t; (* recycle clause numbers that were GC'd *)
       c_proof: Step_vec.t; (* clause -> proof_rule for its proof *)
       c_attached: Bitvec.t;
       c_marked: Bitvec.t;
@@ -149,7 +149,7 @@ module Make(Plugin : PLUGIN)
         c_store={
           c_lits=Vec.create();
           c_activity=Vec_float.create();
-          c_recycle_idx=VecI32.create ~cap:0 ();
+          c_recycle_idx=VecSmallInt.create ~cap:0 ();
           c_proof=Step_vec.create ~cap:0 ();
           c_dead=Bitvec.create();
           c_attached=Bitvec.create();
@@ -302,9 +302,9 @@ module Make(Plugin : PLUGIN)
         } = store.c_store in
         (* allocate new ID *)
         let cid =
-          if VecI32.is_empty c_recycle_idx then (
+          if VecSmallInt.is_empty c_recycle_idx then (
             Vec.size c_lits
-          ) else VecI32.pop c_recycle_idx
+          ) else VecSmallInt.pop c_recycle_idx
         in
 
         (* allocate space *)
@@ -383,7 +383,7 @@ module Make(Plugin : PLUGIN)
         Vec.set c_lits cid [||];
         Vec_float.set c_activity cid 0.;
 
-        VecI32.push c_recycle_idx cid; (* recycle idx *)
+        VecSmallInt.push c_recycle_idx cid; (* recycle idx *)
         ()
 
       let copy_flags store c1 c2 : unit =
@@ -659,7 +659,7 @@ module Make(Plugin : PLUGIN)
     trail : AVec.t;
     (* decision stack + propagated elements (atoms or assignments). *)
 
-    var_levels : VecI32.t;
+    var_levels : VecSmallInt.t;
     (* decision levels in [trail]  *)
 
     mutable assumptions: AVec.t;
@@ -746,7 +746,7 @@ module Make(Plugin : PLUGIN)
     elt_head = 0;
 
     trail = AVec.create ();
-    var_levels = VecI32.create();
+    var_levels = VecSmallInt.create();
     assumptions= AVec.create();
 
     order = H.create store;
@@ -789,7 +789,7 @@ module Make(Plugin : PLUGIN)
     Vec.iter iter_pool self.clause_pools;
     ()
 
-  let[@inline] decision_level st = VecI32.size st.var_levels
+  let[@inline] decision_level st = VecSmallInt.size st.var_levels
   let[@inline] nb_clauses st = CVec.size st.clauses_hyps
   let stat self = self.stat
   let clause_pool_descr self (p:clause_pool_id) =
@@ -957,7 +957,7 @@ module Make(Plugin : PLUGIN)
   let new_decision_level st =
     assert (st.th_head = AVec.size st.trail);
     assert (st.elt_head = AVec.size st.trail);
-    VecI32.push st.var_levels (AVec.size st.trail);
+    VecSmallInt.push st.var_levels (AVec.size st.trail);
     Plugin.push_level st.th;
     ()
 
@@ -990,7 +990,7 @@ module Make(Plugin : PLUGIN)
     ) else (
       Log.debugf 5 (fun k -> k "(@[sat.cancel-until %d@])" lvl);
       (* We set the head of the solver and theory queue to what it was. *)
-      let head = ref (VecI32.get self.var_levels lvl) in
+      let head = ref (VecSmallInt.get self.var_levels lvl) in
       self.elt_head <- !head;
       self.th_head <- !head;
       (* Now we need to cleanup the vars that are not valid anymore
@@ -1023,7 +1023,7 @@ module Make(Plugin : PLUGIN)
       assert (n>0);
       (* Resize the vectors according to their new size. *)
       AVec.shrink self.trail !head;
-      VecI32.shrink self.var_levels lvl;
+      VecSmallInt.shrink self.var_levels lvl;
       Plugin.pop_levels self.th n;
       (* TODO: for scoped clause pools, backtrack them *)
       self.next_decisions <- [];

src/smtlib/Process.mli

@@ -7,7 +7,7 @@ module Solver
                             and type T.Term.store = Term.store
                             and type T.Ty.t = Ty.t
                             and type T.Ty.store = Ty.store
-                            and type proof = Proof_stub.t
+                            and type proof = Proof_dummy.t
 
 val th_bool : Solver.theory
 val th_data : Solver.theory

src/smtlib/Sidekick_smtlib.ml

@@ -6,7 +6,7 @@ module Process = Process
 module Solver = Process.Solver
 module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
-module Proof = Sidekick_base.Proof_stub
+module Proof = Sidekick_base.Proof_dummy
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Sidekick_smtlib.mli

@@ -10,7 +10,7 @@ module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
 module Process = Process
 module Solver = Process.Solver
-module Proof = Sidekick_base.Proof_stub (* FIXME: actual DRUP(T) proof *)
+module Proof = Sidekick_base.Proof_dummy (* FIXME: actual DRUP(T) proof *)
 
 val parse : Term.store -> string -> Stmt.t list or_error
 

src/util/Sidekick_util.ml

@@ -4,6 +4,7 @@ module Fmt = CCFormat
 module Util = Util
 
 module Vec = Vec
+module VecSmallInt = VecSmallInt
 module VecI32 = VecI32
 module Vec_float = Vec_float
 module Vec_unit = Vec_unit

src/util/VecI32.ml

@@ -35,7 +35,7 @@ let[@inline] fast_remove t i =
 let filter_in_place f vec =
   let i = ref 0 in
   while !i < size vec do
-    if f (Int32.to_int (A.unsafe_get vec.data !i)) then incr i else fast_remove vec !i
+    if f (A.unsafe_get vec.data !i) then incr i else fast_remove vec !i
   done
 
 (* ensure capacity is [new_cap] *)
@@ -59,7 +59,7 @@ let ensure_size self n =
 
 let[@inline] push (self:t) i : unit =
   ensure_cap self (self.sz+1);
-  self.data.{self.sz} <- Int32.of_int i;
+  self.data.{self.sz} <- i;
   self.sz <- 1 + self.sz
 
 let[@inline] push_i32 self i =
@@ -69,39 +69,35 @@ let[@inline] push_i32 self i =
 
 let[@inline] pop self =
   if self.sz > 0 then (
-    let x = Int32.to_int self.data.{self.sz-1} in
+    let x = self.data.{self.sz-1} in
     self.sz <- self.sz - 1;
     x
   ) else failwith "vecI32.pop: empty"
 
-let[@inline] get self i : int =
+let[@inline] get self i : int32 =
-  assert (i >= 0 && i < self.sz);
-  Int32.to_int (A.unsafe_get self.data i)
-
-let[@inline] get_i32 self i : int32 =
   assert (i >= 0 && i < self.sz);
   A.unsafe_get self.data i
 
 let[@inline] set self i x : unit =
   assert (i >= 0 && i < self.sz);
-  A.unsafe_set self.data i (Int32.of_int x)
+  A.unsafe_set self.data i x
 
-let[@inline] set_i32 self i x : unit =
+let[@inline] set self i x : unit =
   assert (i >= 0 && i < self.sz);
   A.unsafe_set self.data i x
 
 let[@inline] iter ~f self =
   for i=0 to self.sz - 1 do
-    f (Int32.to_int self.data.{i})
+    f self.data.{i}
   done
 
 let[@inline] iteri ~f self =
   for i=0 to self.sz - 1 do
-    f i (Int32.to_int self.data.{i})
+    f i self.data.{i}
   done
 
 include Vec_sig.Make_extensions(struct
-    type nonrec elt = int
+    type nonrec elt = int32
     type nonrec t = t
     let get = get
     let size = size

src/util/VecI32.mli

@@ -3,11 +3,4 @@
 
     These vectors are more optimized than {!Vec}. *)
 
-include Vec_sig.S with type elt := int
+include Vec_sig.S with type elt := int32
-
-val push_i32 : t -> int32 -> unit
-
-val get_i32 : t -> int -> int32
-
-val set_i32 : t -> int -> int32 -> unit
-

src/util/VecSmallInt.ml

@@ -0,0 +1,110 @@
+
+module A = Bigarray.Array1
+
+type int32arr = (int32, Bigarray.int32_elt, Bigarray.c_layout) A.t
+
+type t = {
+  mutable data: int32arr;
+  mutable sz: int;
+}
+
+let mk_arr_ sz : int32arr = A.create Bigarray.int32 Bigarray.c_layout sz
+
+let create ?(cap=16) () : t =
+  { sz=0; data=mk_arr_ cap }
+
+let[@inline] clear self = self.sz <- 0
+let[@inline] shrink self n = if n < self.sz then self.sz <- n
+let[@inline] size self = self.sz
+let[@inline] is_empty self = self.sz = 0
+
+let copy self =
+  if size self=0 then create ~cap:0 ()
+  else (
+    (* copy bigarray *)
+    let data = mk_arr_ (size self) in
+    A.blit self.data data;
+    {sz=self.sz; data}
+  )
+
+let[@inline] fast_remove t i =
+  assert (i>= 0 && i < t.sz);
+  A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);
+  t.sz <- t.sz - 1
+
+let filter_in_place f vec =
+  let i = ref 0 in
+  while !i < size vec do
+    if f (Int32.to_int (A.unsafe_get vec.data !i)) then incr i else fast_remove vec !i
+  done
+
+(* ensure capacity is [new_cap] *)
+let resize_cap_ self new_cap =
+  assert (A.dim self.data < new_cap);
+  let new_data = mk_arr_ new_cap in
+  A.blit self.data (A.sub new_data 0 (A.dim self.data));
+  self.data <- new_data
+
+let ensure_cap self (n:int) =
+  if n > A.dim self.data then (
+    let new_cap = max n (max 4 (A.dim self.data * 2)) in
+    resize_cap_ self new_cap;
+  )
+
+let ensure_size self n =
+  if n > self.sz then (
+    ensure_cap self n;
+    self.sz <- n
+  )
+
+let[@inline] push (self:t) i : unit =
+  ensure_cap self (self.sz+1);
+  self.data.{self.sz} <- Int32.of_int i;
+  self.sz <- 1 + self.sz
+
+let[@inline] push_i32 self i =
+  ensure_cap self (self.sz+1);
+  self.data.{self.sz} <- i;
+  self.sz <- 1 + self.sz
+
+let[@inline] pop self =
+  if self.sz > 0 then (
+    let x = Int32.to_int self.data.{self.sz-1} in
+    self.sz <- self.sz - 1;
+    x
+  ) else failwith "vecI32.pop: empty"
+
+let[@inline] get self i : int =
+  assert (i >= 0 && i < self.sz);
+  Int32.to_int (A.unsafe_get self.data i)
+
+let[@inline] get_i32 self i : int32 =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_get self.data i
+
+let[@inline] set self i x : unit =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_set self.data i (Int32.of_int x)
+
+let[@inline] set_i32 self i x : unit =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_set self.data i x
+
+let[@inline] iter ~f self =
+  for i=0 to self.sz - 1 do
+    f (Int32.to_int self.data.{i})
+  done
+
+let[@inline] iteri ~f self =
+  for i=0 to self.sz - 1 do
+    f i (Int32.to_int self.data.{i})
+  done
+
+include Vec_sig.Make_extensions(struct
+    type nonrec elt = int
+    type nonrec t = t
+    let get = get
+    let size = size
+    let iter = iter
+    let iteri = iteri
+  end)

src/util/VecSmallInt.mli

@@ -0,0 +1,13 @@
+
+(** Vectors of int32 integers
+
+    These vectors are more optimized than {!Vec}. *)
+
+include Vec_sig.S with type elt := int
+
+val push_i32 : t -> int32 -> unit
+
+val get_i32 : t -> int -> int32
+
+val set_i32 : t -> int -> int32 -> unit
+