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

sat: only re-internalize atoms of permanent clauses, on backtrack

Browse source
This commit is contained in:
Simon Cruanes 2018-05-25 19:35:06 -05:00
parent 6302d13fe8
commit b73e900839
1 changed files with 9 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/sat/Internal.ml
View file

@ -880,6 +880,9 @@ module Make (Th : Theory_intf.S) = struct
Vec.push st.backtrack_levels (Vec.size st.backtrack); (* save the current theory state *) Vec.push st.backtrack_levels (Vec.size st.backtrack); (* save the current theory state *)
() ()
let[@inline] internalize_atoms (self:t) (c:clause) : unit =
Array.iter (attach_atom self) c.atoms
(* Attach a clause. (* Attach a clause.
A clause is attached (to its watching lits) when it is first added, A clause is attached (to its watching lits) when it is first added,
either because it is assumed or learnt. either because it is assumed or learnt.
@ -891,8 +894,7 @@ module Make (Th : Theory_intf.S) = struct
Vec.push c.atoms.(0).neg.watched c; Vec.push c.atoms.(0).neg.watched c;
Vec.push c.atoms.(1).neg.watched c; Vec.push c.atoms.(1).neg.watched c;
Clause.set_attached c true; Clause.set_attached c true;
(* internalize atoms *) internalize_atoms self c;
Array.iter (attach_atom self) c.atoms;
) )
(* perform all backtracking actions down to level [l]. (* perform all backtracking actions down to level [l].
@ -1197,20 +1199,13 @@ module Make (Th : Theory_intf.S) = struct
(* 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 *)
and add_clause ~permanent st (c:clause) : unit = and add_clause ~permanent st (c:clause) : unit =
add_clause_ st c;
if permanent then ( if permanent then (
add_clause_ st c; (* need to re-internalize *)
redo_down_to_level_0 st (fun () -> attach_clause st c) redo_down_to_level_0 st (fun () -> internalize_atoms st c)
) else ( ) else (
(* kill clause once we backtrack *) (* kill clause on backtrack *)
on_backtrack st (fun () -> Clause.mark_dead c); on_backtrack st (fun () -> Clause.mark_dead c)
add_clause_ st c;
(* detach clause once we backtrack *)
if Clause.attached c then (
on_backtrack st
(fun () ->
Log.debugf 5 (fun k->k "(@[sat.detach_clause@ %a@])" Clause.debug c);
Clause.set_attached c false);
)
) )
(* process a conflict: (* process a conflict: