From bbe366989c3fda490ea9e2289036b520097160a8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 26 Sep 2021 21:35:14 -0400 Subject: [PATCH] perf(sat): use Atom.Vec for temporary atom array --- src/sat/Solver.ml | 60 ++++++++++++++++++++++----------------------- src/util/Vec_sig.ml | 7 ++++++ 2 files changed, 36 insertions(+), 31 deletions(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 91399678..23acc373 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -101,13 +101,13 @@ module Make(Plugin : PLUGIN) type t = { (* variables *) - v_of_lit: var Lit_tbl.t; - v_level: int Vec.t; - v_heap_idx: int Vec.t; - v_weight: Vec_float.t; - v_reason: reason option Vec.t; - v_seen: Bitvec.t; - v_default_polarity: Bitvec.t; + v_of_lit: var Lit_tbl.t; (* lit -> var *) + v_level: int Vec.t; (* decision/assignment level, or -1 *) + v_heap_idx: int Vec.t; (* index in priority heap *) + v_weight: Vec_float.t; (* heuristic activity *) + v_reason: reason option Vec.t; (* reason for assignment *) + v_seen: Bitvec.t; (* generic temporary marker *) + 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 - let a = Vec.get learnt i in + for i=1 to AVec.size learnt - 1 do + 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 - Vec.clear learnt; + let cr_learnt = AVec.to_array learnt in + 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 - (fun a -> + AVec.iter dirty_atoms + ~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) - dirty_atoms; - Vec.clear dirty_atoms; + CVec.filter_in_place (fun c -> not (Clause.dead store c)) w); + AVec.clear dirty_atoms; (* actually remove the clauses now that they are detached *) CVec.iter ~f:(Clause.dealloc store) to_be_gc; diff --git a/src/util/Vec_sig.ml b/src/util/Vec_sig.ml index e1e21f63..8f3a0025 100644 --- a/src/util/Vec_sig.ml +++ b/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