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

refactor(sat): improve code

Browse source
This commit is contained in:
Simon Cruanes 2021-11-28 16:34:43 -05:00
parent e9b395b643
commit 15e16a515d
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 18 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/sat/Solver.ml
View file

@ -950,7 +950,7 @@ module Make(Plugin : PLUGIN)
let preprocess_clause_ (self:t) (c:Clause.t) : Clause.t = let preprocess_clause_ (self:t) (c:Clause.t) : Clause.t =
let store = self.store in let store = self.store in
let res0_proofs = ref [] in (* steps of resolution at level 0 *) let res0_proofs = ref [] in (* steps of resolution at level 0 *)
let add_proof_ p = res0_proofs := p :: !res0_proofs in let add_proof_lvl0_ p = res0_proofs := p :: !res0_proofs in
let trues = Vec.create () in let trues = Vec.create () in
let unassigned = Vec.create() in let unassigned = Vec.create() in
@ -987,7 +987,7 @@ module Make(Plugin : PLUGIN)
(Atom.debug store) a); (Atom.debug store) a);
let p = proof_of_atom_lvl0_ self (Atom.neg a) in let p = proof_of_atom_lvl0_ self (Atom.neg a) in
add_proof_ p; add_proof_lvl0_ p;
) else ( ) else (
Vec.push falses a; Vec.push falses a;
) )
@ -1334,7 +1334,7 @@ module Make(Plugin : PLUGIN)
} }
(* conflict analysis, starting with top of trail and conflict clause *) (* conflict analysis, starting with top of trail and conflict clause *)
let analyze (self:t) c_clause : conflict_res = let analyze (self:t) (c_clause:clause) : conflict_res =
let store = self.store in let store = self.store in
let to_unmark = self.to_clear in (* for cleanup *) let to_unmark = self.to_clear in (* for cleanup *)
@ -1389,13 +1389,13 @@ module Make(Plugin : PLUGIN)
assert (Atom.has_value store q); assert (Atom.has_value store q);
assert (Atom.level store q >= 0); assert (Atom.level store q >= 0);
if Atom.level store q = 0 then ( if Atom.level store q = 0 then (
(* skip [q] entirely, resolved away at level 0 *)
assert (Atom.is_false store q); assert (Atom.is_false store q);
if Proof.enabled self.proof then ( if Proof.enabled self.proof then (
let step = proof_of_atom_lvl0_ self (Atom.neg q) in let step = proof_of_atom_lvl0_ self (Atom.neg q) in
Step_vec.push steps step; Step_vec.push steps step;
) )
); ) else if not (Var.marked store (Atom.var q)) then (
if not (Var.marked store (Atom.var q)) then (
Var.mark store (Atom.var q); Var.mark store (Atom.var q);
Vec.push to_unmark (Atom.var q); Vec.push to_unmark (Atom.var q);
if Atom.level store q > 0 then ( if Atom.level store q > 0 then (
@ -1477,16 +1477,13 @@ module Make(Plugin : PLUGIN)
) )
(* add the learnt clause to the clause database, propagate, etc. *) (* add the learnt clause to the clause database, propagate, etc. *)
let record_learnt_clause (self:t) ~pool (confl:clause) (cr:conflict_res): unit = let record_learnt_clause (self:t) ~pool (cr:conflict_res): unit =
let store = self.store in let store = self.store 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 self = 0); assert (cr.cr_backtrack_lvl = 0 && decision_level self = 0);
if Atom.is_false store fuip then (
(* incompatible at level 0 *)
report_unsat self (US_false confl)
) else (
let p = let p =
Proof.emit_redundant_clause Proof.emit_redundant_clause
(Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
@ -1494,8 +1491,12 @@ module Make(Plugin : PLUGIN)
self.proof self.proof
in in
let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in
(match self.on_learnt with Some f -> f self uclause | None -> ()); (match self.on_learnt with Some f -> f self uclause | None -> ());
if Atom.is_false store fuip then (
(* incompatible at level 0 *)
report_unsat self (US_false uclause)
) else (
(* no need to attach [uclause], it is true at level 0 *) (* no need to attach [uclause], it is true at level 0 *)
enqueue_bool self fuip ~level:0 (Bcp uclause) enqueue_bool self fuip ~level:0 (Bcp uclause)
) )
@ -1536,7 +1537,7 @@ module Make(Plugin : PLUGIN)
); );
let cr = analyze self confl in let cr = analyze self confl in
cancel_until self (max cr.cr_backtrack_lvl 0); cancel_until self (max cr.cr_backtrack_lvl 0);
record_learnt_clause ~pool:self.clauses_learnt self confl cr record_learnt_clause ~pool:self.clauses_learnt self cr
(* Add a new clause, simplifying, propagating, and backtracking if (* Add a new clause, simplifying, propagating, and backtracking if
the clause is false in the current trail *) the clause is false in the current trail *)