mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 03:35:38 -05:00
fix compilation error
This commit is contained in:
parent
c2b1bd038d
commit
c7511b2934
2 changed files with 13 additions and 6 deletions
|
|
@ -1169,18 +1169,18 @@ module Make(Plugin : PLUGIN)
|
||||||
(* minimize conflict by removing atoms whose propagation history
|
(* minimize conflict by removing atoms whose propagation history
|
||||||
is ultimately self-subsuming with [lits] *)
|
is ultimately self-subsuming with [lits] *)
|
||||||
let minimize_conflict (self:t) (_c_level:int)
|
let minimize_conflict (self:t) (_c_level:int)
|
||||||
(learnt: atom Vec.t) : unit =
|
(learnt: AVec.t) : unit =
|
||||||
let store = self.store in
|
let store = self.store in
|
||||||
|
|
||||||
(* abstraction of the levels involved in the conflict at all,
|
(* abstraction of the levels involved in the conflict at all,
|
||||||
as logical "or" of each literal's approximate level *)
|
as logical "or" of each literal's approximate level *)
|
||||||
let abstract_levels =
|
let abstract_levels =
|
||||||
Vec.fold (fun lvl a -> lvl lor abstract_level_ self (Atom.var a)) 0 learnt
|
AVec.fold_left (fun lvl a -> lvl lor abstract_level_ self (Atom.var a)) 0 learnt
|
||||||
in
|
in
|
||||||
|
|
||||||
let j = ref 1 in
|
let j = ref 1 in
|
||||||
for i=1 to Vec.size learnt - 1 do
|
for i=1 to AVec.size learnt - 1 do
|
||||||
let a = Vec.get learnt i in
|
let a = AVec.get learnt i in
|
||||||
let keep =
|
let keep =
|
||||||
begin match Atom.reason store a with
|
begin match Atom.reason store a with
|
||||||
| Some Decision -> true (* always keep decisions *)
|
| Some Decision -> true (* always keep decisions *)
|
||||||
|
|
@ -1190,13 +1190,13 @@ module Make(Plugin : PLUGIN)
|
||||||
end
|
end
|
||||||
in
|
in
|
||||||
if keep then (
|
if keep then (
|
||||||
Vec.set learnt !j a;
|
AVec.set learnt !j a;
|
||||||
incr j
|
incr j
|
||||||
) else (
|
) else (
|
||||||
Stat.incr self.n_minimized_away;
|
Stat.incr self.n_minimized_away;
|
||||||
)
|
)
|
||||||
done;
|
done;
|
||||||
Vec.shrink learnt !j;
|
AVec.shrink learnt !j;
|
||||||
()
|
()
|
||||||
|
|
||||||
(* result of conflict analysis, containing the learnt clause and some
|
(* result of conflict analysis, containing the learnt clause and some
|
||||||
|
|
|
||||||
|
|
@ -44,6 +44,8 @@ module type EXTENSIONS = sig
|
||||||
|
|
||||||
val to_array : t -> elt array
|
val to_array : t -> elt array
|
||||||
|
|
||||||
|
val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a
|
||||||
|
|
||||||
val pp : elt CCFormat.printer -> t CCFormat.printer
|
val pp : elt CCFormat.printer -> t CCFormat.printer
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
@ -69,6 +71,11 @@ module Make_extensions(B: BASE_RO)
|
||||||
a
|
a
|
||||||
)
|
)
|
||||||
|
|
||||||
|
let fold_left f acc self =
|
||||||
|
let r = ref acc in
|
||||||
|
iter self ~f:(fun x -> r := f !r x);
|
||||||
|
!r
|
||||||
|
|
||||||
let pp ppx out self =
|
let pp ppx out self =
|
||||||
Format.fprintf out "[@[";
|
Format.fprintf out "[@[";
|
||||||
iteri self
|
iteri self
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue