simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 20:34:53 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: return an array from conflict analysis

Browse source
This commit is contained in:
Simon Cruanes 2019-02-10 16:58:49 -06:00 • committed by Guillaume Bury
parent 110eda2f05
commit ea98f6f027
1 changed files with 19 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/core/Internal.ml
View file

@ -366,6 +366,7 @@ module Make(Plugin : PLUGIN)
let flag_dead = 0b1000 let flag_dead = 0b1000
let[@inline] make_removable l premise = make ~flags:flag_removable l premise let[@inline] make_removable l premise = make ~flags:flag_removable l premise
let[@inline] make_removable_a l premise = make_a ~flags:flag_removable l premise
let[@inline] make_permanent l premise = make ~flags:0 l premise let[@inline] make_permanent l premise = make ~flags:0 l premise
let[@inline] visited c = (c.flags land flag_visited) <> 0 let[@inline] visited c = (c.flags land flag_visited) <> 0
@ -1280,10 +1281,12 @@ module Make(Plugin : PLUGIN)
and a boolean stating whether it is and a boolean stating whether it is
a UIP ("Unique Implication Point") a UIP ("Unique Implication Point")
precond: the atom list is sorted by decreasing decision level *) precond: the atom list is sorted by decreasing decision level *)
let backtrack_lvl _st : atom list -> int * bool = function let backtrack_lvl _st (arr: atom array) : int * bool =
| [] | [_] -> if Array.length arr <= 1 then (
0, true 0, true
| a :: b :: _ -> ) else (
let a = arr.(0) in
let b = arr.(1) in
assert(a.var.v_level > 0); assert(a.var.v_level > 0);
if a.var.v_level > b.var.v_level then ( if a.var.v_level > b.var.v_level then (
(* backtrack below [a], so we can propagate [not a] *) (* backtrack below [a], so we can propagate [not a] *)
@ -1293,6 +1296,7 @@ module Make(Plugin : PLUGIN)
assert (a.var.v_level >= 0); assert (a.var.v_level >= 0);
max (a.var.v_level - 1) 0, false max (a.var.v_level - 1) 0, false
) )
)
(* result of conflict analysis, containing the learnt clause and some (* result of conflict analysis, containing the learnt clause and some
additional info. additional info.
@ -1302,7 +1306,7 @@ module Make(Plugin : PLUGIN)
(boolean conflict i.e hypothesis, or theory lemma) *) (boolean conflict i.e hypothesis, or theory lemma) *)
type conflict_res = { type conflict_res = {
cr_backtrack_lvl : int; (* level to backtrack to *) cr_backtrack_lvl : int; (* level to backtrack to *)
cr_learnt: atom list; (* lemma learnt from conflict *) cr_learnt: atom array; (* lemma learnt from conflict *)
cr_history: clause list; (* justification *) cr_history: clause list; (* justification *)
cr_is_uip: bool; (* conflict is UIP? *) cr_is_uip: bool; (* conflict is UIP? *)
} }
@ -1403,10 +1407,12 @@ module Make(Plugin : PLUGIN)
(* 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 *)
let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in let a = Array.of_list !learnt in
let level, is_uip = backtrack_lvl st l in Array.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) a;
(* put_high_level_atoms_first a; *)
let level, is_uip = backtrack_lvl st a in
{ cr_backtrack_lvl = level; { cr_backtrack_lvl = level;
cr_learnt = l; cr_learnt = a;
cr_history = List.rev !history; cr_history = List.rev !history;
cr_is_uip = is_uip; cr_is_uip = is_uip;
} }
@ -1415,19 +1421,20 @@ module Make(Plugin : PLUGIN)
let record_learnt_clause st (confl:clause) (cr:conflict_res): unit = let record_learnt_clause st (confl:clause) (cr:conflict_res): unit =
let proof = if st.store_proof then History cr.cr_history else Empty_premise in let proof = if st.store_proof then History cr.cr_history else Empty_premise in
begin match cr.cr_learnt with begin match cr.cr_learnt with
| [] -> assert false | [| |] -> assert false
| [fuip] -> | [|fuip|] ->
assert (cr.cr_backtrack_lvl = 0 && decision_level st = 0); assert (cr.cr_backtrack_lvl = 0 && decision_level st = 0);
if fuip.neg.is_true then ( if fuip.neg.is_true then (
(* incompatible at level 0 *) (* incompatible at level 0 *)
report_unsat st (US_false confl) report_unsat st (US_false confl)
) else ( ) else (
let uclause = Clause.make_removable cr.cr_learnt proof in let uclause = Clause.make_removable_a cr.cr_learnt proof in
(* no need to attach [uclause], it is true at level 0 *) (* no need to attach [uclause], it is true at level 0 *)
enqueue_bool st fuip ~level:0 (Bcp uclause) enqueue_bool st fuip ~level:0 (Bcp uclause)
) )
| fuip :: _ -> | _ ->
let lclause = Clause.make_removable cr.cr_learnt proof in let fuip = cr.cr_learnt.(0) in
let lclause = Clause.make_removable_a cr.cr_learnt proof in
if Array.length lclause.atoms > 2 then ( if Array.length lclause.atoms > 2 then (
Vec.push st.clauses_learnt lclause; (* potentially gc'able *) Vec.push st.clauses_learnt lclause; (* potentially gc'able *)
); );