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

sat: use an atom array for clauses again

Browse source 
allocator is not worth the complexity, and has a lot of double
indirections anyway.
This commit is contained in:
Simon Cruanes 2021-07-21 10:02:56 -04:00
parent 8b94e8404f
commit 3aa25cb2a2
5 changed files with 79 additions and 154 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

181
src/sat/Solver.ml
View file

@ -114,9 +114,7 @@ module Make(Plugin : PLUGIN)
(* variable/atom store *) (* variable/atom store *)
module Store = struct module Store = struct
type cstore = { type cstore = {
c_allocator : VecI32.t; (* storage for clause content *) c_lits: atom array Vec.t; (* storage for clause content *)
c_idx: VecI32.t; (* clause -> idx in [c_allocator] *)
c_len: VecI32.t; (* clause -> number of lits *)
c_activity: Vec_float.t; c_activity: Vec_float.t;
c_premise: premise Vec.t; c_premise: premise Vec.t;
c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *) c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *)
@ -154,10 +152,6 @@ module Make(Plugin : PLUGIN)
| `Tiny -> 8 | `Tiny -> 8
| `Small -> 16 | `Small -> 16
| `Big -> 4096 | `Big -> 4096
and size_alloc = match size with
| `Tiny -> 256
| `Small -> 4096
| `Big -> 4 * 1024 * 1024
in in
{ v_of_form = Form_tbl.create size_map; { v_of_form = Form_tbl.create size_map;
v_level = Vec.create(); v_level = Vec.create();
@ -172,9 +166,7 @@ module Make(Plugin : PLUGIN)
a_watched=Vec.create(); a_watched=Vec.create();
a_seen=Bitvec.create(); a_seen=Bitvec.create();
c_store={ c_store={
c_allocator=VecI32.create ~cap:size_alloc (); c_lits=Vec.create();
c_idx=VecI32.create ();
c_len=VecI32.create ();
c_activity=Vec_float.create(); c_activity=Vec_float.create();
c_premise=Vec.create(); c_premise=Vec.create();
c_recycle_idx=VecI32.create ~cap:0 (); c_recycle_idx=VecI32.create ~cap:0 ();
@ -293,8 +285,6 @@ module Make(Plugin : PLUGIN)
val premise : store -> t -> premise val premise : store -> t -> premise
val n_atoms : store -> t -> int val n_atoms : store -> t -> int
val atom : store -> t -> int -> atom
val set_atom : store -> t -> int -> atom -> unit
val visited : store -> t -> bool val visited : store -> t -> bool
val set_visited : store -> t -> bool -> unit val set_visited : store -> t -> bool -> unit
@ -302,8 +292,10 @@ module Make(Plugin : PLUGIN)
val set_attached : store -> t -> bool -> unit val set_attached : store -> t -> bool -> unit
val removable : store -> t -> bool val removable : store -> t -> bool
val set_removable : store -> t -> bool -> unit val set_removable : store -> t -> bool -> unit
val dead : store -> t -> bool val dead : store -> t -> bool
val set_dead : store -> t -> bool -> unit val dealloc : store -> t -> unit
(** Delete the clause *)
val activity : store -> t -> float val activity : store -> t -> float
val set_activity : store -> t -> float -> unit val set_activity : store -> t -> float -> unit
@ -313,19 +305,8 @@ module Make(Plugin : PLUGIN)
val for_all : store -> f:(atom -> bool) -> t -> bool val for_all : store -> f:(atom -> bool) -> t -> bool
val exists : store -> f:(atom -> bool) -> t -> bool val exists : store -> f:(atom -> bool) -> t -> bool
module Slice : sig val atoms_a : store -> t -> atom array
type t
val size : t -> int
val get : t -> int -> atom
val set : t -> int -> atom -> unit
val swap : t -> int -> int -> unit
val iteri : t -> (int -> atom -> unit) -> unit
end
val atoms_a : store -> t -> atom array (* allocates *)
val atoms_l : store -> t -> atom list (* allocates *) val atoms_l : store -> t -> atom list (* allocates *)
val atoms_slice : store -> t -> Slice.t
val atoms_iter : store -> t -> atom Iter.t val atoms_iter : store -> t -> atom Iter.t
val short_name : store -> t -> string val short_name : store -> t -> string
@ -336,24 +317,22 @@ module Make(Plugin : PLUGIN)
(* TODO: store watch lists inside clauses *) (* TODO: store watch lists inside clauses *)
let make_ (store:store) iter_atoms n_atoms premise : t = let make_a (store:store) (atoms:atom array) premise : t =
let { let {
c_allocator; c_recycle_idx; c_lits; c_activity; c_premise;
c_recycle_idx; c_idx; c_len; c_activity; c_premise;
c_attached; c_dead; c_removable; c_visited; c_attached; c_dead; c_removable; c_visited;
} = store.c_store in } = store.c_store in
(* allocate new ID *) (* allocate new ID *)
let cid = let cid =
if VecI32.is_empty c_recycle_idx then ( if VecI32.is_empty c_recycle_idx then (
VecI32.size c_idx Vec.size c_lits
) else VecI32.pop c_recycle_idx ) else VecI32.pop c_recycle_idx
in in
(* allocate space *) (* allocate space *)
begin begin
let new_len = cid + 1 in let new_len = cid + 1 in
VecI32.ensure_size c_idx new_len; Vec.ensure_size c_lits [||] new_len;
VecI32.ensure_size c_len new_len;
Vec_float.ensure_size c_activity new_len; Vec_float.ensure_size c_activity new_len;
Bitvec.ensure_size c_attached new_len; Bitvec.ensure_size c_attached new_len;
Bitvec.ensure_size c_dead new_len; Bitvec.ensure_size c_dead new_len;
@ -361,51 +340,24 @@ module Make(Plugin : PLUGIN)
Bitvec.ensure_size c_visited new_len; Bitvec.ensure_size c_visited new_len;
end; end;
(* copy atoms *) Vec.set c_lits cid atoms;
begin
let idx0 = VecI32.size c_allocator in
VecI32.ensure_size c_allocator (VecI32.size c_allocator + n_atoms + 1);
VecI32.set c_idx cid idx0;
VecI32.set c_len cid n_atoms;
let i = ref idx0 in
iter_atoms (fun a -> VecI32.set c_allocator !i (a:atom:>int); incr i);
end;
Vec.set c_premise cid premise; Vec.set c_premise cid premise;
let c = of_int_unsafe cid in let c = of_int_unsafe cid in
c c
let make_a store atoms premise : t =
let n = Array.length atoms in
make_ store (Iter.of_array atoms) n premise
let make_l store atoms premise : t = let make_l store atoms premise : t =
let n = List.length atoms in make_a store (Array.of_list atoms) premise
make_ store (Iter.of_list atoms) n premise
let make_vec store atoms premise : t = let make_vec store atoms premise : t =
let n = Vec.size atoms in make_a store (Vec.to_array atoms) premise
make_ store (Vec.to_seq atoms) n premise
let[@inline] n_atoms (store:store) (c:t) : int = let[@inline] n_atoms (store:store) (c:t) : int =
VecI32.get store.c_store.c_len (c:t:>int) Array.length (Vec.get store.c_store.c_lits (c:t:>int))
let[@inline] atom (store:store) (c:t) (i:int) : atom = let[@inline] iter (store:store) ~f c =
let idx0 = VecI32.get store.c_store.c_idx (c:t:>int) in let {c_lits; _} = store.c_store in
Atom0.of_int_unsafe (VecI32.get store.c_store.c_allocator (idx0 + i)) Array.iter f (Vec.get c_lits (c:t:>int))
let[@inline] set_atom store c i a : unit =
let idx0 = VecI32.get store.c_store.c_idx (c:t:>int) in
VecI32.set store.c_store.c_allocator (idx0 + i) (a:atom:>int)
let iter (store:store) ~f c =
let {c_len; c_idx; c_allocator; _} = store.c_store in
let idx0 = VecI32.get c_idx (c:t:>int) in
let len = VecI32.get c_len (c:t:>int) in
for i=0 to len-1 do
f (Atom.of_int_unsafe (VecI32.get c_allocator (idx0 + i)))
done
exception Early_exit exception Early_exit
@ -422,17 +374,8 @@ module Make(Plugin : PLUGIN)
with Early_exit -> true with Early_exit -> true
let fold (store:store) ~f acc c = let fold (store:store) ~f acc c =
let {c_len; c_idx; c_allocator; _} = store.c_store in let {c_lits; _} = store.c_store in
let idx0 = VecI32.get c_idx (c:t:>int) in Array.fold_left f acc (Vec.get c_lits (c:t:>int))
let len = VecI32.get c_len (c:t:>int) in
let rec fold acc i =
if i=len then acc
else (
let x = Atom.of_int_unsafe (VecI32.get c_allocator (idx0 + i)) in
fold (f acc x) (i+1)
)
in
fold acc 0
let[@inline] premise store c = Vec.get store.c_store.c_premise (c:t:>int) let[@inline] premise store c = Vec.get store.c_store.c_premise (c:t:>int)
let[@inline] visited store c = Bitvec.get store.c_store.c_visited (c:t:>int) let[@inline] visited store c = Bitvec.get store.c_store.c_visited (c:t:>int)
@ -444,6 +387,13 @@ module Make(Plugin : PLUGIN)
let[@inline] removable store c = Bitvec.get store.c_store.c_removable (c:t:>int) let[@inline] removable store c = Bitvec.get store.c_store.c_removable (c:t:>int)
let[@inline] set_removable store c b = Bitvec.set store.c_store.c_removable (c:t:>int) b let[@inline] set_removable store c b = Bitvec.set store.c_store.c_removable (c:t:>int) b
(* FIXME: actually GC the clause, recycle index, and remove it
somehow from the watch lists *)
let dealloc store c : unit =
set_dead store c true;
assert (dead store c);
()
let copy_flags store c1 c2 : unit = let copy_flags store c1 c2 : unit =
set_removable store c2 (removable store c1); set_removable store c2 (removable store c1);
() ()
@ -464,24 +414,9 @@ module Make(Plugin : PLUGIN)
assert (not (removable store c)); (* permanent by default *) assert (not (removable store c)); (* permanent by default *)
c c
module Slice = struct let[@inline] atoms_a store c : atom array =
include VecI32.Slice Vec.get store.c_store.c_lits (c:t:>int)
let[@inline] get self i = Atom.of_int_unsafe (VecI32.Slice.get self i) let atoms_l store c : _ list = Array.to_list (atoms_a store c)
let set = (VecI32.Slice.set :> t -> int -> atom -> unit)
let iteri self f =
for i=0 to size self-1 do f i (get self i) done
end
let atoms_slice store c : Slice.t =
let n = n_atoms store c in
let idx0 = VecI32.get store.c_store.c_idx (c:t:>int) in
VecI32.slice store.c_store.c_allocator ~off:idx0 ~len:n
let atoms_a store c : atom array =
Array.init (n_atoms store c) (fun i -> atom store c i)
let atoms_l store c : _ list =
CCList.init (n_atoms store c) (fun i -> atom store c i)
let atoms_iter store c = fun k -> iter store c ~f:k let atoms_iter store c = fun k -> iter store c ~f:k
let short_name store c = let short_name store c =
@ -1198,8 +1133,8 @@ module Make(Plugin : PLUGIN)
assert (not @@ Clause.attached store c); assert (not @@ Clause.attached store c);
Log.debugf 20 (fun k -> k "(@[sat.attach-clause@ %a@])" (Clause.debug store) c); Log.debugf 20 (fun k -> k "(@[sat.attach-clause@ %a@])" (Clause.debug store) c);
(* TODO: change when watchlist are updated *) (* TODO: change when watchlist are updated *)
Vec.push (Atom.watched store (Atom.neg (Clause.atom store c 0))) c; Vec.push (Atom.watched store (Atom.neg (Clause.atoms_a store c).(0))) c;
Vec.push (Atom.watched store (Atom.neg (Clause.atom store c 1))) c; Vec.push (Atom.watched store (Atom.neg (Clause.atoms_a store c).(1))) c;
Clause.set_attached store c true; Clause.set_attached store c true;
() ()
@ -1348,25 +1283,25 @@ module Make(Plugin : PLUGIN)
) )
(* move atoms assigned at high levels first *) (* move atoms assigned at high levels first *)
let put_high_level_atoms_first (store:store) (slice:Clause.Slice.t) : unit = let put_high_level_atoms_first (store:store) (arr:atom array) : unit =
let module CS = Clause.Slice in Array.iteri
CS.iteri slice
(fun i a -> (fun i a ->
if i>0 && Atom.level store a > Atom.level store (CS.get slice 0) then ( if i>0 && Atom.level store a > Atom.level store arr.(0) then (
(* move first to second, [i]-th to first, second to [i] *) (* move first to second, [i]-th to first, second to [i] *)
if i=1 then ( if i=1 then (
CS.swap slice 0 1; swap_arr arr 0 1;
) else ( ) else (
let tmp = CS.get slice 1 in let tmp = arr.(1) in
CS.set slice 1 (CS.get slice 0); arr.(1) <- arr.(0);
CS.set slice 0 (CS.get slice 1); arr.(0) <- arr.(i);
CS.set slice i tmp; arr.(i) <- tmp;
); );
) else if i>1 && ) else if i>1 &&
Atom.level store a > Atom.level store (Clause.Slice.get slice 1) Atom.level store a > Atom.level store arr.(1)
then ( then (
Clause.Slice.swap slice 1 i; swap_arr arr 1 i;
)) ))
arr
(* find which level to backtrack to, given a conflict clause (* find which level to backtrack to, given a conflict clause
and a boolean stating whether it is and a boolean stating whether it is
@ -1448,8 +1383,9 @@ module Make(Plugin : PLUGIN)
); );
Vec.push history clause; Vec.push history clause;
(* visit the current predecessors *) (* visit the current predecessors *)
for j = 0 to Clause.n_atoms store clause - 1 do let atoms = Clause.atoms_a store clause in
let q = Clause.atom store clause j in for j = 0 to Array.length atoms - 1 do
let q = atoms.(j) in
assert (Atom.is_true store q || assert (Atom.is_true store q ||
Atom.is_false store q && Atom.is_false store q &&
Atom.level store q >= 0); (* unsure? *) Atom.level store q >= 0); (* unsure? *)
@ -1589,7 +1525,8 @@ module Make(Plugin : PLUGIN)
let clause = let clause =
if history = [] then ( if history = [] then (
(* just update order of atoms *) (* just update order of atoms *)
List.iteri (fun i a -> Clause.set_atom store c i a) atoms; let c_atoms = Clause.atoms_a store c in
List.iteri (fun i a -> c_atoms.(i) <- a) atoms;
c c
) else ( ) else (
let proof = if self.store_proof then History (c::history) else Empty_premise in let proof = if self.store_proof then History (c::history) else Empty_premise in
@ -1621,7 +1558,7 @@ module Make(Plugin : PLUGIN)
if Atom.is_false store a then ( if Atom.is_false store a then (
(* Atom need to be sorted in decreasing order of decision level, (* Atom need to be sorted in decreasing order of decision level,
or we might watch the wrong literals. *) or we might watch the wrong literals. *)
put_high_level_atoms_first store (Clause.atoms_slice store clause); put_high_level_atoms_first store (Clause.atoms_a store clause);
attach_clause self clause; attach_clause self clause;
add_boolean_conflict self clause add_boolean_conflict self clause
) else ( ) else (
@ -1658,25 +1595,26 @@ module Make(Plugin : PLUGIN)
*) *)
let propagate_in_clause (self:t) (a:atom) (c:clause) (i:int): watch_res = let propagate_in_clause (self:t) (a:atom) (c:clause) (i:int): watch_res =
let store = self.store in let store = self.store in
let first = Clause.atom store c 0 in let atoms = Clause.atoms_a store c in
let first = atoms.(0) in
if first = Atom.neg a then ( if first = Atom.neg a then (
(* false lit must be at index 1 *) (* false lit must be at index 1 *)
Clause.set_atom store c 0 (Clause.atom store c 1); atoms.(0) <- atoms.(1);
Clause.set_atom store c 1 first; atoms.(1) <- first
) else ( ) else (
assert (Atom.neg a = Clause.atom store c 1) assert (Atom.neg a = atoms.(1))
); );
let first = Clause.atom store c 0 in let first = atoms.(0) in
if Atom.is_true store first then ( if Atom.is_true store first then (
Watch_kept (* true clause, keep it in watched *) Watch_kept (* true clause, keep it in watched *)
) else ( ) else (
try (* look for another watch lit *) try (* look for another watch lit *)
for k = 2 to Clause.n_atoms store c - 1 do for k = 2 to Array.length atoms - 1 do
let ak = Clause.atom store c k in let ak = atoms.(k) in
if not (Atom.is_false store ak) then ( if not (Atom.is_false store ak) then (
(* watch lit found: update and exit *) (* watch lit found: update and exit *)
Clause.set_atom store c 1 ak; atoms.(1) <- ak;
Clause.set_atom store c k (Atom.neg a); atoms.(k) <- Atom.neg a;
(* remove [c] from [a.watched], add it to [ak.neg.watched] *) (* remove [c] from [a.watched], add it to [ak.neg.watched] *)
Vec.push (Atom.watched store (Atom.neg ak)) c; Vec.push (Atom.watched store (Atom.neg ak)) c;
assert (Vec.get (Atom.watched store a) i == c); assert (Vec.get (Atom.watched store a) i == c);
@ -1933,8 +1871,7 @@ module Make(Plugin : PLUGIN)
while Vec.size v > n_of_learnts do while Vec.size v > n_of_learnts do
let c = Vec.pop_exn v in let c = Vec.pop_exn v in
assert (Clause.removable store c); assert (Clause.removable store c);
Clause.set_dead store c true; Clause.dealloc store c;
assert (Clause.dead store c);
incr n_collected; incr n_collected;
done; done;
Log.debugf 3 (fun k->k "(@[sat.gc.done :collected %d@])" !n_collected); Log.debugf 3 (fun k->k "(@[sat.gc.done :collected %d@])" !n_collected);

22
src/util/Vec.ml
View file

@ -45,15 +45,27 @@ let resize_ t x size =
t.data <- arr'; t.data <- arr';
() ()
let ensure_cap_ self x n =
if n > Array.length self.data then (
let new_size = max n (2 * Array.length self.data) in
resize_ self x new_size
)
let ensure_size self x n =
ensure_cap_ self x n;
if n > self.sz then (
self.sz <- n
)
(* grow the array *) (* grow the array *)
let[@inline never] grow_to_double_size t x : unit = let[@inline never] grow_to_double_size t x : unit =
if Array.length t.data = Sys.max_array_length then ( let new_size =
failwith "vec: cannot resize";
);
let size =
min Sys.max_array_length (max 4 (2 * Array.length t.data)) min Sys.max_array_length (max 4 (2 * Array.length t.data))
in in
resize_ t x size; if new_size = t.sz then (
failwith "vec: cannot resize";
);
resize_ t x new_size;
assert (Array.length t.data > t.sz); assert (Array.length t.data > t.sz);
() ()

3
src/util/Vec.mli
View file

@ -28,6 +28,9 @@ val to_seq : 'a t -> 'a Iter.t
val clear : 'a t -> unit val clear : 'a t -> unit
(** Set size to 0, doesn't free elements *) (** Set size to 0, doesn't free elements *)
val ensure_size : 'a t -> 'a -> int -> unit
(** ensure size is at least [n] *)
val shrink : 'a t -> int -> unit val shrink : 'a t -> int -> unit
(** [shrink vec sz] resets size of [vec] to [sz]. (** [shrink vec sz] resets size of [vec] to [sz].
Assumes [sz >=0 && sz <= size vec] *) Assumes [sz >=0 && sz <= size vec] *)

16
src/util/VecI32.ml
View file

@ -82,22 +82,6 @@ let[@inline] iteri ~f self =
let[@inline] to_iter self k = iter ~f:k self let[@inline] to_iter self k = iter ~f:k self
module Slice = struct
type t = int32arr
let size = A.dim
let[@inline] get self i = Int32.to_int (A.get self i)
let[@inline] set self i x = A.set self i (Int32.of_int x)
let[@inline] swap self i j =
let tmp = get self i in
set self i (get self j);
set self j tmp
end
let[@inline] slice self ~off ~len =
assert (off+len < self.sz);
A.sub self.data off len
let pp out self = let pp out self =
Format.fprintf out "[@["; Format.fprintf out "[@[";
iteri self ~f:(fun i x -> if i>0 then Format.fprintf out ",@ "; Format.pp_print_int out x); iteri self ~f:(fun i x -> if i>0 then Format.fprintf out ",@ "; Format.pp_print_int out x);

11
src/util/VecI32.mli
View file

@ -34,17 +34,6 @@ val shrink : t -> int -> unit
val iter : f:(int -> unit) -> t -> unit val iter : f:(int -> unit) -> t -> unit
val iteri : f:(int -> int -> unit) -> t -> unit val iteri : f:(int -> int -> unit) -> t -> unit
module Slice : sig
type t
val size : t -> int
val get : t -> int -> int
val set : t -> int -> int -> unit
val swap : t -> int -> int -> unit
end
val slice : t -> off:int -> len:int -> Slice.t
val to_iter : t -> int Iter.t val to_iter : t -> int Iter.t
val pp : t CCFormat.printer val pp : t CCFormat.printer