perf(sat): use Atom.Vec for temporary atom array

src/sat/Solver.ml

@@ -101,13 +101,13 @@ module Make(Plugin : PLUGIN)
 
     type t = {
       (* variables *)
-      v_of_lit: var Lit_tbl.t;
+      v_of_lit: var Lit_tbl.t; (* lit -> var *)
-      v_level: int Vec.t;
+      v_level: int Vec.t; (* decision/assignment level, or -1 *)
-      v_heap_idx: int Vec.t;
+      v_heap_idx: int Vec.t; (* index in priority heap *)
-      v_weight: Vec_float.t;
+      v_weight: Vec_float.t; (* heuristic activity *)
-      v_reason: reason option Vec.t;
+      v_reason: reason option Vec.t; (* reason for assignment *)
-      v_seen: Bitvec.t;
+      v_seen: Bitvec.t; (* generic temporary marker *)
-      v_default_polarity: Bitvec.t;
+      v_default_polarity: Bitvec.t; (* default polarity in decisions *)
       mutable v_count : int;
 
       (* atoms *)
@@ -679,7 +679,7 @@ module Make(Plugin : PLUGIN)
 
     (* temporaries *)
 
-    temp_atom_vec : atom Vec.t;
+    temp_atom_vec : AVec.t;
     temp_clause_vec : CVec.t;
 
     mutable var_incr : float;
@@ -728,7 +728,7 @@ module Make(Plugin : PLUGIN)
 
     to_clear=Vec.create();
     temp_clause_vec=CVec.create();
-    temp_atom_vec=Vec.create();
+    temp_atom_vec=AVec.create();
 
     th_head = 0;
     elt_head = 0;
@@ -1161,18 +1161,18 @@ module Make(Plugin : PLUGIN)
    (* minimize conflict by removing atoms whose propagation history
       is ultimately self-subsuming with [lits] *)
    let minimize_conflict (self:t) (_c_level:int)
-       (learnt: atom Vec.t) : unit =
+       (learnt: AVec.t) : unit =
      let store = self.store in
 
      (* abstraction of the levels involved in the conflict at all,
         as logical "or" of each literal's approximate level *)
      let abstract_levels =
-       Vec.fold (fun lvl a -> lvl lor abstract_level_ self (Atom.var a)) 0 learnt
+       AVec.fold_left (fun lvl a -> lvl lor abstract_level_ self (Atom.var a)) 0 learnt
      in
 
      let j = ref 1 in
-     for i=1 to Vec.size learnt - 1 do
+     for i=1 to AVec.size learnt - 1 do
-       let a = Vec.get learnt i in
+       let a = AVec.get learnt i in
        let keep =
          begin match Atom.reason store a with
            | Some Decision -> true (* always keep decisions *)
@@ -1182,13 +1182,13 @@ module Make(Plugin : PLUGIN)
          end
        in
        if keep then (
-         Vec.set learnt !j a;
+         AVec.set learnt !j a;
          incr j
        ) else (
          Stat.incr self.n_minimized_away;
        )
      done;
-     Vec.shrink learnt !j;
+     AVec.shrink learnt !j;
      ()
 
   (* result of conflict analysis, containing the learnt clause and some
@@ -1206,7 +1206,7 @@ module Make(Plugin : PLUGIN)
     let to_unmark = self.to_clear in (* for cleanup *)
     Vec.clear to_unmark;
     let learnt = self.temp_atom_vec in
-    Vec.clear learnt;
+    AVec.clear learnt;
 
     (* loop variables *)
     let pathC  = ref 0 in
@@ -1258,7 +1258,7 @@ module Make(Plugin : PLUGIN)
                 if Atom.level store q >= conflict_level then (
                   incr pathC;
                 ) else (
-                  Vec.push learnt q;
+                  AVec.push learnt q;
                   blevel := max !blevel (Atom.level store q)
                 )
               )
@@ -1282,7 +1282,7 @@ module Make(Plugin : PLUGIN)
       match !pathC, Atom.reason store p with
       | 0, _ ->
         continue := false;
-        Vec.push learnt (Atom.neg p)
+        AVec.push learnt (Atom.neg p)
       | n, Some (Bcp cl | Bcp_lazy (lazy cl)) ->
         assert (n > 0);
         assert (Atom.level store p >= conflict_level);
@@ -1300,8 +1300,8 @@ module Make(Plugin : PLUGIN)
     (* put high-level literals first, so that:
        - they make adequate watch lits
        - the first literal is the UIP, if any *)
-    let cr_learnt = Vec.to_array learnt in
+    let cr_learnt = AVec.to_array learnt in
-    Vec.clear learnt;
+    AVec.clear learnt;
     Array.sort (fun p q -> compare (Atom.level store q) (Atom.level store p)) cr_learnt;
 
     (* put_high_level_atoms_first a; *)
@@ -1750,7 +1750,7 @@ module Make(Plugin : PLUGIN)
   let reduce_clause_db (self:t) : unit =
     let store = self.store in
 
-    Log.debugf 3 (fun k->k "(@[sat.gc.start :max-learnt %d@])"
+    Log.debugf 3 (fun k->k "(@[sat.gc-clauses.start :max-learnt %d@])"
                      !(self.max_clauses_learnt));
 
     let to_be_gc = self.temp_clause_vec in (* clauses to collect *)
@@ -1759,14 +1759,14 @@ module Make(Plugin : PLUGIN)
     (* atoms whose watches will need to be rebuilt to filter out
        dead clauses *)
     let dirty_atoms = self.temp_atom_vec in
-    assert (Vec.is_empty dirty_atoms);
+    assert (AVec.is_empty dirty_atoms);
 
     (* [a] is watching at least one removed clause, we'll need to
        trim its watchlist *)
     let[@inline] mark_dirty_atom a =
       if not (Atom.marked store a) then (
         Atom.mark store a;
-        Vec.push dirty_atoms a;
+        AVec.push dirty_atoms a;
       )
     in
 
@@ -1774,13 +1774,12 @@ module Make(Plugin : PLUGIN)
        which we must therefore keep for now as they might participate in
        conflict resolution *)
     let iter_clauses_on_trail ~f : unit =
-      AVec.iter
+      AVec.iter self.trail
         ~f:(fun a ->
            match Atom.reason store a with
            | Some (Bcp c) -> f c
            | Some (Bcp_lazy lc) when Lazy.is_val lc -> f (Lazy.force lc)
-           | _ -> ())
+           | _ -> ());
-        self.trail;
     in
 
     iter_clauses_on_trail ~f:(fun c -> Clause.set_marked store c true);
@@ -1835,14 +1834,13 @@ module Make(Plugin : PLUGIN)
     let n_collected = CVec.size to_be_gc in
 
     (* update watchlist of dirty atoms *)
-    Vec.iter
+    AVec.iter dirty_atoms
-      (fun a ->
+      ~f:(fun a ->
          assert (Atom.marked store a);
          Atom.unmark store a;
          let w = Atom.watched store a in
-         CVec.filter_in_place (fun c -> not (Clause.dead store c)) w)
+         CVec.filter_in_place (fun c -> not (Clause.dead store c)) w);
-      dirty_atoms;
+    AVec.clear dirty_atoms;
-    Vec.clear dirty_atoms;
 
     (* actually remove the clauses now that they are detached *)
     CVec.iter ~f:(Clause.dealloc store) to_be_gc;

src/util/Vec_sig.ml

@@ -44,6 +44,8 @@ module type EXTENSIONS = sig
 
   val to_array : t -> elt array
 
+  val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a
+
   val pp : elt CCFormat.printer -> t CCFormat.printer
 end
 
@@ -69,6 +71,11 @@ module Make_extensions(B: BASE_RO)
       a
     )
 
+  let fold_left f acc self =
+    let r = ref acc in
+    iter self ~f:(fun x -> r := f !r x);
+    !r
+
   let pp ppx out self =
     Format.fprintf out "[@[";
     iteri self