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

reset some record accesses, for perf

Browse source
This commit is contained in:
Simon Cruanes 2017-12-29 18:53:26 +01:00
parent 38b670ebc0
commit 70fcded713
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/core/Internal.ml
View file

@ -396,11 +396,11 @@ module Make
*) *)
let attach_clause c = let attach_clause c =
assert (not @@ Clause.attached c); assert (not c.attached);
Log.debugf debug (fun k -> k "Attaching %a" Clause.debug c); Log.debugf debug (fun k -> k "Attaching %a" Clause.debug c);
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; c.attached <- true;
() ()
(* Backtracking. (* Backtracking.
@ -888,7 +888,7 @@ module Make
atoms.(1) <- first atoms.(1) <- first
) else assert (a.neg == atoms.(1)); ) else assert (a.neg == atoms.(1));
let first = atoms.(0) in let first = atoms.(0) in
if Atom.is_true first if first.is_true
then Watch_kept (* true clause, keep it in watched *) then Watch_kept (* true clause, keep it in watched *)
else ( else (
try (* look for another watch lit *) try (* look for another watch lit *)
@ -936,7 +936,7 @@ module Make
if i >= Vec.size watched then () if i >= Vec.size watched then ()
else ( else (
let c = Vec.get watched i in let c = Vec.get watched i in
assert (Clause.attached c); assert c.attached;
let j = match propagate_in_clause st a c i with let j = match propagate_in_clause st a c i with
| Watch_kept -> i+1 | Watch_kept -> i+1
| Watch_removed -> i (* clause at this index changed *) | Watch_removed -> i (* clause at this index changed *)
@ -994,7 +994,7 @@ module Make
let current_slice st : (_,_,_) Plugin_intf.slice = { let current_slice st : (_,_,_) Plugin_intf.slice = {
Plugin_intf.start = st.th_head; Plugin_intf.start = st.th_head;
length = (Vec.size st.trail) - st.th_head; length = Vec.size st.trail - st.th_head;
get = slice_get st; get = slice_get st;
push = slice_push st; push = slice_push st;
propagate = slice_propagate st; propagate = slice_propagate st;
@ -1111,7 +1111,7 @@ module Make
might 'forget' the initial conflict clause, and only add the might 'forget' the initial conflict clause, and only add the
analyzed backtrack clause. So in those case, we use add_clause analyzed backtrack clause. So in those case, we use add_clause
to make sure the initial conflict clause is also added. *) to make sure the initial conflict clause is also added. *)
if Clause.attached confl then if confl.attached then
add_boolean_conflict st confl add_boolean_conflict st confl
else else
add_clause st confl add_clause st confl