simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 20:25:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: use Var.mark and a pre-allocated vec for analyze

Browse source
This commit is contained in:
Simon Cruanes 2019-01-25 19:27:25 -06:00 • committed by Guillaume Bury
parent cf6147c500
commit a5ec88f2a7
1 changed files with 18 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/core/Internal.ml
View file

@ -152,9 +152,9 @@ module Make(Plugin : PLUGIN)
(v.lid+1) debug_assign v Term.pp v.term (v.lid+1) debug_assign v Term.pp v.term
end end
let seen_var = 0b1 let seen_var = 0x1
let seen_pos = 0b10 let seen_pos = 0x2
let seen_neg = 0b100 let seen_neg = 0x4
module Var = struct module Var = struct
type t = var type t = var
@ -762,6 +762,9 @@ module Make(Plugin : PLUGIN)
order : H.t; order : H.t;
(* Heap ordered by variable activity *) (* Heap ordered by variable activity *)
to_clear: var Vec.t;
(* variables to unmark *)
mutable var_incr : float; mutable var_incr : float;
(* increment for variables' activity *) (* increment for variables' activity *)
@ -787,6 +790,7 @@ module Make(Plugin : PLUGIN)
clauses_learnt = Vec.create(); clauses_learnt = Vec.create();
clauses_to_add = Stack.create (); clauses_to_add = Stack.create ();
to_clear=Vec.create();
th_head = 0; th_head = 0;
elt_head = 0; elt_head = 0;
@ -1285,24 +1289,26 @@ module Make(Plugin : PLUGIN)
cr_is_uip: bool; (* conflict is UIP? *) cr_is_uip: bool; (* conflict is UIP? *)
} }
let get_atom st i = let[@inline] get_atom st i =
match Vec.get st.trail i with match Vec.get st.trail i with
| Lit _ -> assert false | Atom x -> x | Atom x -> x
| Lit _ -> assert false
(* conflict analysis for SAT (* conflict analysis for SAT
Same idea as the mcsat analyze function (without semantic propagations), Same idea as the mcsat analyze function (without semantic propagations),
except we look the the Last UIP (TODO: check ?), and do it in an imperative except we look the the Last UIP (TODO: check ?), and do it in an imperative
and efficient manner. *) and efficient manner. *)
let analyze_sat st c_clause : conflict_res = let analyze st c_clause : conflict_res =
let pathC = ref 0 in let pathC = ref 0 in
let learnt = ref [] in let learnt = ref [] in
let cond = ref true in let cond = ref true in
let blevel = ref 0 in let blevel = ref 0 in
let seen = ref [] in (* for cleanup *) let seen = st.to_clear in (* for cleanup *)
let c = ref (Some c_clause) in let c = ref (Some c_clause) in
let tr_ind = ref (Vec.size st.trail - 1) in let tr_ind = ref (Vec.size st.trail - 1) in
let history = ref [] in let history = ref [] in
assert (decision_level st > 0); assert (decision_level st > 0);
Vec.clear seen;
let conflict_level = let conflict_level =
Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
in in
@ -1329,10 +1335,9 @@ module Make(Plugin : PLUGIN)
| Some Bcp cl -> history := cl :: !history | Some Bcp cl -> history := cl :: !history
| _ -> assert false | _ -> assert false
); );
if not (Var.seen_both q.var) then ( if not (Var.marked q.var) then (
Atom.mark q; Var.mark q.var;
Atom.mark q.neg; Vec.push seen q.var;
seen := q :: !seen;
if q.var.v_level > 0 then ( if q.var.v_level > 0 then (
var_bump_activity st q.var; var_bump_activity st q.var;
if q.var.v_level >= conflict_level then ( if q.var.v_level >= conflict_level then (
@ -1352,7 +1357,7 @@ module Make(Plugin : PLUGIN)
Log.debugf debug (fun k -> k " looking at: %a" Trail_elt.debug a); Log.debugf debug (fun k -> k " looking at: %a" Trail_elt.debug a);
match a with match a with
| Atom q -> | Atom q ->
(not (Var.seen_both q.var)) || (not (Var.marked q.var)) ||
(q.var.v_level < conflict_level) (q.var.v_level < conflict_level)
| Lit _ -> true | Lit _ -> true
do do
@ -1375,7 +1380,7 @@ module Make(Plugin : PLUGIN)
c := Some cl c := Some cl
| _ -> assert false | _ -> assert false
done; done;
List.iter (fun q -> Var.clear q.var) !seen; Vec.iter Var.clear seen;
(* put high-level literals first, so that: (* put high-level literals first, so that:
- they make adequate watch lits - they make adequate watch lits
- the first literal is the UIP, if any *) - the first literal is the UIP, if any *)
@ -1387,9 +1392,6 @@ module Make(Plugin : PLUGIN)
cr_is_uip = is_uip; cr_is_uip = is_uip;
} }
let[@inline] analyze st c_clause : conflict_res =
analyze_sat st c_clause
(* add the learnt clause to the clause database, propagate, etc. *) (* add the learnt clause to the clause database, propagate, etc. *)
let record_learnt_clause st (confl:clause) (cr:conflict_res): unit = let record_learnt_clause st (confl:clause) (cr:conflict_res): unit =
begin match cr.cr_learnt with begin match cr.cr_learnt with