remove veci32

This commit is contained in:
Simon Cruanes 2022-07-15 20:32:06 -04:00
parent ba4b4c0302
commit 5a559bec92
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
16 changed files with 105 additions and 207 deletions

View file

@ -51,8 +51,24 @@ type proof_rule = t -> proof_step
module Step_vec = struct module Step_vec = struct
type elt = proof_step type elt = proof_step
type t = elt Vec.t
include VecI32 let get = Vec.get
let size = Vec.size
let iter = Vec.iter
let iteri = Vec.iteri
let create ?cap:_ () = Vec.create ()
let clear = Vec.clear
let copy = Vec.copy
let is_empty = Vec.is_empty
let push = Vec.push
let fast_remove = Vec.fast_remove
let filter_in_place = Vec.filter_in_place
let ensure_size v len = Vec.ensure_size v ~elt:0l len
let pop = Vec.pop_exn
let set = Vec.set
let shrink = Vec.shrink
let to_iter = Vec.to_iter
end end
let disable (self : t) : unit = let disable (self : t) : unit =

View file

@ -30,8 +30,8 @@ end = struct
let del_clause self c = Vec.push self.ops (Delete c) let del_clause self c = Vec.push self.ops (Delete c)
let get self i = Vec.get self.ops i let get self i = Vec.get self.ops i
let size self = Vec.size self.ops let size self = Vec.size self.ops
let ops self = Vec.to_seq self.ops let ops self = Vec.to_iter self.ops
let iteri self ~f = Vec.iteri f self.ops let iteri self ~f = Vec.iteri ~f self.ops
let pp_op out = function let pp_op out = function
| Input c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c | Input c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c
@ -43,19 +43,17 @@ end = struct
let pp_c out c = let pp_c out c =
Clause.iter c ~f:(fun a -> fpf out "%d " (a : atom :> int)) Clause.iter c ~f:(fun a -> fpf out "%d " (a : atom :> int))
in in
Vec.iter Vec.iter self.ops ~f:(function
(function | Input c -> fpf oc "i %a0\n" pp_c c
| Input c -> fpf oc "i %a0\n" pp_c c | Redundant c -> fpf oc "%a0\n" pp_c c
| Redundant c -> fpf oc "%a0\n" pp_c c | Delete c -> fpf oc "d %a0\n" pp_c c)
| Delete c -> fpf oc "d %a0\n" pp_c c)
self.ops
end end
(** Forward checking. (** Forward checking.
Each event is checked by reverse-unit propagation on previous events. *) Each event is checked by reverse-unit propagation on previous events. *)
module Fwd_check : sig module Fwd_check : sig
type error = [ `Bad_steps of VecSmallInt.t | `No_empty_clause ] type error = [ `Bad_steps of Veci.t | `No_empty_clause ]
val pp_error : Trace.t -> error Fmt.printer val pp_error : Trace.t -> error Fmt.printer
@ -64,10 +62,10 @@ module Fwd_check : sig
success. In case of error it returns [Error idxs] where [idxs] are the success. In case of error it returns [Error idxs] where [idxs] are the
indexes in the trace of the steps that failed. *) indexes in the trace of the steps that failed. *)
end = struct end = struct
type t = { checker: Checker.t; errors: VecSmallInt.t } type t = { checker: Checker.t; errors: Veci.t }
let create cstore : t = let create cstore : t =
{ checker = Checker.create cstore; errors = VecSmallInt.create () } { checker = Checker.create cstore; errors = Veci.create () }
(* check event, return [true] if it's valid *) (* check event, return [true] if it's valid *)
let check_op (self : t) i (op : Trace.op) : bool = let check_op (self : t) i (op : Trace.op) : bool =
@ -87,15 +85,15 @@ end = struct
Checker.del_clause self.checker c; Checker.del_clause self.checker c;
true true
type error = [ `Bad_steps of VecSmallInt.t | `No_empty_clause ] type error = [ `Bad_steps of Veci.t | `No_empty_clause ]
let pp_error trace out = function let pp_error trace out = function
| `No_empty_clause -> Fmt.string out "no empty clause found" | `No_empty_clause -> Fmt.string out "no empty clause found"
| `Bad_steps bad -> | `Bad_steps bad ->
let n0 = VecSmallInt.get bad 0 in let n0 = Veci.get bad 0 in
Fmt.fprintf out Fmt.fprintf out
"@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]" "@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]"
(VecSmallInt.size bad) n0 Trace.pp_op (Trace.get trace n0) (Veci.size bad) n0 Trace.pp_op (Trace.get trace n0)
let check trace : _ result = let check trace : _ result =
let self = create (Trace.cstore trace) in let self = create (Trace.cstore trace) in
@ -116,13 +114,13 @@ end = struct
) else ( ) else (
Log.debugf 10 (fun k -> Log.debugf 10 (fun k ->
k "(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op); k "(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
VecSmallInt.push self.errors i Veci.push self.errors i
)); ));
Log.debugf 10 (fun k -> k "found %d errors" (VecSmallInt.size self.errors)); Log.debugf 10 (fun k -> k "found %d errors" (Veci.size self.errors));
if not !has_false then if not !has_false then
Error `No_empty_clause Error `No_empty_clause
else if VecSmallInt.size self.errors > 0 then else if Veci.size self.errors > 0 then
Error (`Bad_steps self.errors) Error (`Bad_steps self.errors)
else else
Ok () Ok ()

View file

@ -169,7 +169,7 @@ module type SAT_PROOF = sig
type proof_step type proof_step
(** identifier for a proof *) (** identifier for a proof *)
module Step_vec : Vec_sig.S with type elt = proof_step module Step_vec : Vec_sig.BASE with type elt = proof_step
(** A vector of steps *) (** A vector of steps *)
type lit type lit

View file

@ -5,7 +5,7 @@
*) *)
module Fmt = CCFormat module Fmt = CCFormat
module VecSmallInt = VecSmallInt module Veci = Veci
(* TODO: resolution proof construction, optionally *) (* TODO: resolution proof construction, optionally *)
@ -130,7 +130,7 @@ module Make () : S = struct
end end
module Stack = struct module Stack = struct
include VecSmallInt include Veci
let create () = create () let create () = create ()
end end

View file

@ -4,10 +4,10 @@ module type S = Heap_intf.S
module Make (Elt : RANKED) = struct module Make (Elt : RANKED) = struct
type elt_store = Elt.store type elt_store = Elt.store
type elt = Elt.t type elt = Elt.t
type t = { store: elt_store; heap: VecSmallInt.t (* vec of elements *) } type t = { store: elt_store; heap: Veci.t (* vec of elements *) }
let _absent_index = -1 let _absent_index = -1
let create store : t = { store; heap = VecSmallInt.create () } let create store : t = { store; heap = Veci.create () }
let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *) let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *) let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
@ -16,17 +16,17 @@ module Make (Elt : RANKED) = struct
(* (*
let rec heap_property cmp ({heap=heap} as s) i = let rec heap_property cmp ({heap=heap} as s) i =
i >= (VecSmallInt.size heap) || i >= (Veci.size heap) ||
((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i)))) ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
&& heap_property cmp s (left i) && heap_property cmp s (right i)) && heap_property cmp s (left i) && heap_property cmp s (right i))
let heap_property cmp s = heap_property cmp s 1 let heap_property cmp s = heap_property cmp s 1
*) *)
let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecSmallInt.get self.heap i) let[@inline] get_elt_ self i = Elt.of_int_unsafe (Veci.get self.heap i)
let[@inline] set_elt_ self i elt = let[@inline] set_elt_ self i elt =
VecSmallInt.set self.heap i (elt : Elt.t :> int) Veci.set self.heap i (elt : Elt.t :> int)
(* [elt] is above or at its expected position. Move it up the heap (* [elt] is above or at its expected position. Move it up the heap
(towards high indices) to restore the heap property *) (towards high indices) to restore the heap property *)
@ -43,7 +43,7 @@ module Make (Elt : RANKED) = struct
Elt.set_heap_idx self.store elt !i Elt.set_heap_idx self.store elt !i
let percolate_down (self : t) (elt : Elt.t) : unit = let percolate_down (self : t) (elt : Elt.t) : unit =
let sz = VecSmallInt.size self.heap in let sz = Veci.size self.heap in
let li = ref (left (Elt.heap_idx self.store elt)) in let li = ref (left (Elt.heap_idx self.store elt)) in
let ri = ref (right (Elt.heap_idx self.store elt)) in let ri = ref (right (Elt.heap_idx self.store elt)) in
let i = ref (Elt.heap_idx self.store elt) in let i = ref (Elt.heap_idx self.store elt) in
@ -83,7 +83,7 @@ module Make (Elt : RANKED) = struct
let filter (self : t) filt : unit = let filter (self : t) filt : unit =
let j = ref 0 in let j = ref 0 in
let lim = VecSmallInt.size self.heap in let lim = Veci.size self.heap in
for i = 0 to lim - 1 do for i = 0 to lim - 1 do
if filt (get_elt_ self i) then ( if filt (get_elt_ self i) then (
set_elt_ self !j (get_elt_ self i); set_elt_ self !j (get_elt_ self i);
@ -92,24 +92,24 @@ module Make (Elt : RANKED) = struct
) else ) else
Elt.set_heap_idx self.store (get_elt_ self i) _absent_index Elt.set_heap_idx self.store (get_elt_ self i) _absent_index
done; done;
VecSmallInt.shrink self.heap (lim - !j); Veci.shrink self.heap (lim - !j);
for i = (lim / 2) - 1 downto 0 do for i = (lim / 2) - 1 downto 0 do
percolate_down self (get_elt_ self i) percolate_down self (get_elt_ self i)
done done
let[@inline] size s = VecSmallInt.size s.heap let[@inline] size s = Veci.size s.heap
let[@inline] is_empty s = VecSmallInt.is_empty s.heap let[@inline] is_empty s = Veci.is_empty s.heap
let clear self : unit = let clear self : unit =
VecSmallInt.iter self.heap ~f:(fun e -> Veci.iter self.heap ~f:(fun e ->
Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index); Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index);
VecSmallInt.clear self.heap; Veci.clear self.heap;
() ()
let insert self elt = let insert self elt =
if not (in_heap self elt) then ( if not (in_heap self elt) then (
Elt.set_heap_idx self.store elt (VecSmallInt.size self.heap); Elt.set_heap_idx self.store elt (Veci.size self.heap);
VecSmallInt.push self.heap (elt : Elt.t :> int); Veci.push self.heap (elt : Elt.t :> int);
percolate_up self elt percolate_up self elt
) )
@ -128,21 +128,21 @@ module Make (Elt : RANKED) = struct
*) *)
let remove_min self = let remove_min self =
match VecSmallInt.size self.heap with match Veci.size self.heap with
| 0 -> raise Not_found | 0 -> raise Not_found
| 1 -> | 1 ->
let x = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in let x = Elt.of_int_unsafe (Veci.pop self.heap) in
Elt.set_heap_idx self.store x _absent_index; Elt.set_heap_idx self.store x _absent_index;
x x
| _ -> | _ ->
let x = get_elt_ self 0 in let x = get_elt_ self 0 in
let new_hd = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in let new_hd = Elt.of_int_unsafe (Veci.pop self.heap) in
(* heap.last() *) (* heap.last() *)
set_elt_ self 0 new_hd; set_elt_ self 0 new_hd;
Elt.set_heap_idx self.store x _absent_index; Elt.set_heap_idx self.store x _absent_index;
Elt.set_heap_idx self.store new_hd 0; Elt.set_heap_idx self.store new_hd 0;
(* enforce heap property again *) (* enforce heap property again *)
if VecSmallInt.size self.heap > 1 then percolate_down self new_hd; if Veci.size self.heap > 1 then percolate_down self new_hd;
x x
end end
[@@inline] [@@inline]

View file

@ -61,7 +61,7 @@ module Make (Plugin : PLUGIN) = struct
let[@inline] var a = Var0.of_int_unsafe (a lsr 1) let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
let[@inline] na v = ((v : var :> int) lsl 1) lor 1 let[@inline] na v = ((v : var :> int) lsl 1) lor 1
module AVec = VecSmallInt module AVec = Veci
module ATbl = CCHashtbl.Make (CCInt) module ATbl = CCHashtbl.Make (CCInt)
end end
@ -74,7 +74,7 @@ module Make (Plugin : PLUGIN) = struct
end = struct end = struct
include Int_id.Make () include Int_id.Make ()
module Tbl = Util.Int_tbl module Tbl = Util.Int_tbl
module CVec = VecSmallInt module CVec = Veci
end end
type clause = Clause0.t type clause = Clause0.t
@ -98,7 +98,7 @@ module Make (Plugin : PLUGIN) = struct
type cstore = { type cstore = {
c_lits: atom array Vec.t; (* storage for clause content *) c_lits: atom array Vec.t; (* storage for clause content *)
c_activity: Vec_float.t; c_activity: Vec_float.t;
c_recycle_idx: VecSmallInt.t; (* recycle clause numbers that were GC'd *) c_recycle_idx: Veci.t; (* recycle clause numbers that were GC'd *)
c_proof: Step_vec.t; (* clause -> proof_rule for its proof *) c_proof: Step_vec.t; (* clause -> proof_rule for its proof *)
c_attached: Bitvec.t; c_attached: Bitvec.t;
c_marked: Bitvec.t; c_marked: Bitvec.t;
@ -158,7 +158,7 @@ module Make (Plugin : PLUGIN) = struct
{ {
c_lits = Vec.create (); c_lits = Vec.create ();
c_activity = Vec_float.create (); c_activity = Vec_float.create ();
c_recycle_idx = VecSmallInt.create ~cap:0 (); c_recycle_idx = Veci.create ~cap:0 ();
c_proof = Step_vec.create ~cap:0 (); c_proof = Step_vec.create ~cap:0 ();
c_dead = Bitvec.create (); c_dead = Bitvec.create ();
c_attached = Bitvec.create (); c_attached = Bitvec.create ();
@ -172,7 +172,7 @@ module Make (Plugin : PLUGIN) = struct
(** iterate on variables *) (** iterate on variables *)
let iter_vars self f = let iter_vars self f =
Vec.iteri (fun i _ -> f (Var0.of_int_unsafe i)) self.v_level Vec.iteri self.v_level ~f:(fun i _ -> f (Var0.of_int_unsafe i))
module Var = struct module Var = struct
include Var0 include Var0
@ -339,10 +339,10 @@ module Make (Plugin : PLUGIN) = struct
in in
(* allocate new ID *) (* allocate new ID *)
let cid = let cid =
if VecSmallInt.is_empty c_recycle_idx then if Veci.is_empty c_recycle_idx then
Vec.size c_lits Vec.size c_lits
else else
VecSmallInt.pop c_recycle_idx Veci.pop c_recycle_idx
in in
(* allocate space *) (* allocate space *)
@ -447,7 +447,7 @@ module Make (Plugin : PLUGIN) = struct
Vec.set c_lits cid [||]; Vec.set c_lits cid [||];
Vec_float.set c_activity cid 0.; Vec_float.set c_activity cid 0.;
VecSmallInt.push c_recycle_idx cid; Veci.push c_recycle_idx cid;
(* recycle idx *) (* recycle idx *)
() ()
@ -659,7 +659,7 @@ module Make (Plugin : PLUGIN) = struct
let descr = P.descr let descr = P.descr
let add c = Vec.push clauses_ c let add c = Vec.push clauses_ c
let iter ~f = Vec.iter f clauses_ let iter ~f = Vec.iter ~f clauses_
let push_level () = () let push_level () = ()
let pop_levels _ = () let pop_levels _ = ()
let size () = Vec.size clauses_ let size () = Vec.size clauses_
@ -816,10 +816,10 @@ module Make (Plugin : PLUGIN) = struct
} = } =
self self
in in
Vec.iter (fun (c, p) -> add_clause_pool c p) clauses_to_add_in_pool; Vec.iter clauses_to_add_in_pool ~f:(fun (c, p) -> add_clause_pool c p);
CVec.iter ~f:add_clause_learnt clauses_to_add_learnt; CVec.iter ~f:add_clause_learnt clauses_to_add_learnt;
Vec.iter decision decisions; Vec.iter ~f:decision decisions;
Vec.iter (fun (p, lvl, c) -> propagate p ~lvl c) prop; Vec.iter prop ~f:(fun (p, lvl, c) -> propagate p ~lvl c);
clear self; clear self;
() ()
end end
@ -847,7 +847,7 @@ module Make (Plugin : PLUGIN) = struct
store them here. *) store them here. *)
trail: AVec.t; trail: AVec.t;
(* decision stack + propagated elements (atoms or assignments). *) (* decision stack + propagated elements (atoms or assignments). *)
var_levels: VecSmallInt.t; (* decision levels in [trail] *) var_levels: Veci.t; (* decision levels in [trail] *)
assumptions: AVec.t; (* current assumptions *) assumptions: AVec.t; (* current assumptions *)
mutable th_head: int; mutable th_head: int;
(* Start offset in the queue {!trail} of (* Start offset in the queue {!trail} of
@ -911,7 +911,7 @@ module Make (Plugin : PLUGIN) = struct
th_head = 0; th_head = 0;
elt_head = 0; elt_head = 0;
trail = AVec.create (); trail = AVec.create ();
var_levels = VecSmallInt.create (); var_levels = Veci.create ();
assumptions = AVec.create (); assumptions = AVec.create ();
order = H.create store; order = H.create store;
var_incr = 1.; var_incr = 1.;
@ -944,10 +944,10 @@ module Make (Plugin : PLUGIN) = struct
let iter_clauses_learnt_ (self : t) ~f : unit = let iter_clauses_learnt_ (self : t) ~f : unit =
let[@inline] iter_pool (module P : CLAUSE_POOL) = P.iter ~f in let[@inline] iter_pool (module P : CLAUSE_POOL) = P.iter ~f in
iter_pool self.clauses_learnt; iter_pool self.clauses_learnt;
Vec.iter iter_pool self.clause_pools; Vec.iter ~f:iter_pool self.clause_pools;
() ()
let[@inline] decision_level st = VecSmallInt.size st.var_levels let[@inline] decision_level st = Veci.size st.var_levels
let[@inline] nb_clauses st = CVec.size st.clauses_hyps let[@inline] nb_clauses st = CVec.size st.clauses_hyps
let stat self = self.stat let stat self = self.stat
@ -1172,7 +1172,7 @@ module Make (Plugin : PLUGIN) = struct
let new_decision_level st = let new_decision_level st =
assert (st.th_head = AVec.size st.trail); assert (st.th_head = AVec.size st.trail);
assert (st.elt_head = AVec.size st.trail); assert (st.elt_head = AVec.size st.trail);
VecSmallInt.push st.var_levels (AVec.size st.trail); Veci.push st.var_levels (AVec.size st.trail);
Plugin.push_level st.th; Plugin.push_level st.th;
() ()
@ -1206,7 +1206,7 @@ module Make (Plugin : PLUGIN) = struct
else ( else (
Log.debugf 5 (fun k -> k "(@[sat.cancel-until %d@])" lvl); Log.debugf 5 (fun k -> k "(@[sat.cancel-until %d@])" lvl);
(* We set the head of the solver and theory queue to what it was. *) (* We set the head of the solver and theory queue to what it was. *)
let head = ref (VecSmallInt.get self.var_levels lvl) in let head = ref (Veci.get self.var_levels lvl) in
self.elt_head <- !head; self.elt_head <- !head;
self.th_head <- !head; self.th_head <- !head;
(* Now we need to cleanup the vars that are not valid anymore (* Now we need to cleanup the vars that are not valid anymore
@ -1239,7 +1239,7 @@ module Make (Plugin : PLUGIN) = struct
assert (n > 0); assert (n > 0);
(* Resize the vectors according to their new size. *) (* Resize the vectors according to their new size. *)
AVec.shrink self.trail !head; AVec.shrink self.trail !head;
VecSmallInt.shrink self.var_levels lvl; Veci.shrink self.var_levels lvl;
Plugin.pop_levels self.th n; Plugin.pop_levels self.th n;
Delayed_actions.clear_on_backtrack self.delayed_actions; Delayed_actions.clear_on_backtrack self.delayed_actions;
(* TODO: for scoped clause pools, backtrack them *) (* TODO: for scoped clause pools, backtrack them *)
@ -1598,7 +1598,7 @@ module Make (Plugin : PLUGIN) = struct
Step_vec.clear self.temp_step_vec; Step_vec.clear self.temp_step_vec;
(* cleanup marks *) (* cleanup marks *)
Vec.iter (Store.clear_var store) to_unmark; Vec.iter ~f:(Store.clear_var store) to_unmark;
Vec.clear to_unmark; Vec.clear to_unmark;
(* put high-level literals first, so that: (* put high-level literals first, so that:
@ -2213,7 +2213,7 @@ module Make (Plugin : PLUGIN) = struct
in in
gc_pool self.clauses_learnt; gc_pool self.clauses_learnt;
Vec.iter gc_pool self.clause_pools; Vec.iter ~f:gc_pool self.clause_pools;
let n_collected = CVec.size to_be_gc in let n_collected = CVec.size to_be_gc in

View file

@ -353,23 +353,21 @@ module Make (Arg : ARG) :
(Fmt.iter ~sep:(Fmt.return "@ ") ppi) (Fmt.iter ~sep:(Fmt.return "@ ") ppi)
CCInt.(0 -- (n_cols self - 1)); CCInt.(0 -- (n_cols self - 1));
Vec.iteri Vec.iteri self.rows ~f:(fun i row ->
(fun i row ->
let hd = let hd =
CCString.pad ~side:`Left 6 CCString.pad ~side:`Left 6
@@ Printf.sprintf "r%d (v%d)" i row.vs.idx @@ Printf.sprintf "r%d (v%d)" i row.vs.idx
in in
Fmt.fprintf out "@,{@[<hov2>%9s: %a@]}" hd Fmt.fprintf out "@,{@[<hov2>%9s: %a@]}" hd
(Fmt.iter ~sep:(Fmt.return "@ ") (Q.pp_approx 6)) (Fmt.iter ~sep:(Fmt.return "@ ") (Q.pp_approx 6))
(Vec.to_seq row.cols)) (Vec.to_iter row.cols));
self.rows;
Fmt.fprintf out "@;<0 -1>}@]" Fmt.fprintf out "@;<0 -1>}@]"
let to_string = Fmt.to_string pp let to_string = Fmt.to_string pp
let add_column self = let add_column self =
self.n_cols <- 1 + self.n_cols; self.n_cols <- 1 + self.n_cols;
Vec.iter (fun r -> Vec.push r.cols Q.zero) self.rows Vec.iter self.rows ~f:(fun r -> Vec.push r.cols Q.zero)
let add_row_and_column self ~f : var_state = let add_row_and_column self ~f : var_state =
let n = n_rows self in let n = n_rows self in
@ -393,7 +391,7 @@ module Make (Arg : ARG) :
Vec.set r.cols j n Vec.set r.cols j n
let[@inline] iter_rows ?(skip = ~-1) (self : t) f : unit = let[@inline] iter_rows ?(skip = ~-1) (self : t) f : unit =
Vec.iteri (fun i row -> if i <> skip then f i row.vs) self.rows Vec.iteri self.rows ~f:(fun i row -> if i <> skip then f i row.vs)
let[@inline] iter_cols ?(skip = ~-1) (self : t) f : unit = let[@inline] iter_cols ?(skip = ~-1) (self : t) f : unit =
for i = 0 to n_cols self - 1 do for i = 0 to n_cols self - 1 do
@ -498,7 +496,7 @@ module Make (Arg : ARG) :
(* for debug purposes *) (* for debug purposes *)
let _check_invariants self : unit = let _check_invariants self : unit =
Vec.iteri (fun i v -> assert (v.idx = i)) self.vars; Vec.iteri self.vars ~f:(fun i v -> assert (v.idx = i));
let n = Vec.size self.vars in let n = Vec.size self.vars in
assert (Matrix.n_rows self.matrix = 0 || Matrix.n_cols self.matrix = n); assert (Matrix.n_rows self.matrix = 0 || Matrix.n_cols self.matrix = n);
Matrix.iter_rows self.matrix (fun i x_i -> Matrix.iter_rows self.matrix (fun i x_i ->
@ -507,12 +505,10 @@ module Make (Arg : ARG) :
assert (Q.(Matrix.get self.matrix x_i.basic_idx x_i.idx = minus_one)); assert (Q.(Matrix.get self.matrix x_i.basic_idx x_i.idx = minus_one));
(* basic vars are only defined in terms of non-basic vars *) (* basic vars are only defined in terms of non-basic vars *)
Vec.iteri Vec.iteri self.vars ~f:(fun j x_j ->
(fun j x_j ->
if Var_state.(x_i != x_j) && Q.(Matrix.get self.matrix i j <> zero) if Var_state.(x_i != x_j) && Q.(Matrix.get self.matrix i j <> zero)
then then
assert (Var_state.is_n_basic x_j)) assert (Var_state.is_n_basic x_j));
self.vars;
(* sum of each row must be 0 *) (* sum of each row must be 0 *)
let sum = let sum =
@ -786,8 +782,7 @@ module Make (Arg : ARG) :
assert (Var_state.is_basic x_i); assert (Var_state.is_basic x_i);
let map_res = ref [] in let map_res = ref [] in
let bounds = ref V_map.empty in let bounds = ref V_map.empty in
Vec.iteri Vec.iteri self.vars ~f:(fun j x_j ->
(fun j x_j ->
if j <> x_i.idx then ( if j <> x_i.idx then (
let c = Matrix.get self.matrix x_i.basic_idx j in let c = Matrix.get self.matrix x_i.basic_idx j in
if Q.(c <> zero) then ( if Q.(c <> zero) then (
@ -817,8 +812,7 @@ module Make (Arg : ARG) :
bounds := V_map.add x_j.var (op, u) !bounds bounds := V_map.add x_j.var (op, u) !bounds
| None -> assert false (* we could increase [x_j]?! *)) | None -> assert false (* we could increase [x_j]?! *))
) )
)) ));
self.vars;
!map_res, !bounds !map_res, !bounds
let add_constraint ?(is_int = false) ~on_propagate (self : t) let add_constraint ?(is_int = false) ~on_propagate (self : t)
@ -1159,7 +1153,7 @@ module Make (Arg : ARG) :
| _ -> eps | _ -> eps
in in
eps) eps)
default_eps (Vec.to_seq self.vars) default_eps (Vec.to_iter self.vars)
in in
if Q.(eps >= one) then if Q.(eps >= one) then
Q.one Q.one
@ -1171,7 +1165,7 @@ module Make (Arg : ARG) :
Log.debugf 50 (fun k -> Log.debugf 50 (fun k ->
k "(@[simplex.model@ :epsilon-val %a@])" pp_q_dbg eps); k "(@[simplex.model@ :epsilon-val %a@])" pp_q_dbg eps);
let subst = let subst =
Vec.to_seq self.vars Vec.to_iter self.vars
|> Iter.fold |> Iter.fold
(fun subst x -> (fun subst x ->
let { base; eps_factor } = x.value in let { base; eps_factor } = x.value in

View file

@ -2,8 +2,7 @@
module Fmt = CCFormat module Fmt = CCFormat
module Util = Util module Util = Util
module Vec = Vec module Vec = Vec
module VecSmallInt = VecSmallInt module Veci = Veci
module VecI32 = VecI32
module Vec_float = Vec_float module Vec_float = Vec_float
module Vec_unit = Vec_unit module Vec_unit = Vec_unit
module Vec_sig = Vec_sig module Vec_sig = Vec_sig

View file

@ -53,7 +53,7 @@ let ensure_size_with self f n =
self.sz <- n self.sz <- n
) )
let ensure_size self x n = ensure_size_with self (fun () -> x) n let ensure_size self ~elt:x n = ensure_size_with self (fun () -> x) 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 =
@ -125,22 +125,21 @@ let sort t f : unit =
Array.fast_sort f sub_arr; Array.fast_sort f sub_arr;
t.data <- sub_arr t.data <- sub_arr
let[@inline] iter f t = let iter ~f t =
for i = 0 to size t - 1 do for i = 0 to size t - 1 do
f (Array.unsafe_get t.data i) f (Array.unsafe_get t.data i)
done done
let[@inline] iteri f t = let iteri ~f t =
for i = 0 to size t - 1 do for i = 0 to size t - 1 do
f i (Array.unsafe_get t.data i) f i (Array.unsafe_get t.data i)
done done
let[@inline] to_seq a k = iter k a let to_iter v k = iter ~f:k v
let to_iter v k = iter k v let exists p t = Iter.exists p @@ to_iter t
let exists p t = Iter.exists p @@ to_seq t let for_all p t = Iter.for_all p @@ to_iter t
let for_all p t = Iter.for_all p @@ to_seq t let fold f acc a = Iter.fold f acc @@ to_iter a
let fold f acc a = Iter.fold f acc @@ to_seq a let to_list a = Iter.to_list @@ to_iter a
let to_list a = Iter.to_list @@ to_seq a
let to_array a = Array.sub a.data 0 a.sz let to_array a = Array.sub a.data 0 a.sz
let of_list l : _ t = let of_list l : _ t =
@ -153,11 +152,9 @@ let of_list l : _ t =
let pp ?(sep = ", ") pp out v = let pp ?(sep = ", ") pp out v =
let first = ref true in let first = ref true in
iter iter v ~f:(fun x ->
(fun x ->
if !first then if !first then
first := false first := false
else else
Format.fprintf out "%s@," sep; Format.fprintf out "%s@," sep;
pp out x) pp out x)
v

View file

@ -20,12 +20,11 @@ val to_list : 'a t -> 'a list
val to_array : 'a t -> 'a array val to_array : 'a t -> 'a array
val of_list : 'a list -> 'a t val of_list : 'a list -> 'a t
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 val ensure_size : 'a t -> elt:'a -> int -> unit
(** ensure size is at least [n] *) (** ensure size is at least [n] *)
val ensure_size_with : 'a t -> (unit -> 'a) -> int -> unit val ensure_size_with : 'a t -> (unit -> 'a) -> int -> unit
@ -79,12 +78,12 @@ val filter_in_place : ('a -> bool) -> 'a t -> unit
val sort : 'a t -> ('a -> 'a -> int) -> unit val sort : 'a t -> ('a -> 'a -> int) -> unit
(** Sort in place the array *) (** Sort in place the array *)
val iter : ('a -> unit) -> 'a t -> unit val iter : f:('a -> unit) -> 'a t -> unit
(** Iterate on elements *) (** Iterate on elements *)
val to_iter : 'a t -> 'a Iter.t val to_iter : 'a t -> 'a Iter.t
val iteri : (int -> 'a -> unit) -> 'a t -> unit val iteri : f:(int -> 'a -> unit) -> 'a t -> unit
(** Iterate on elements with their index *) (** Iterate on elements with their index *)
val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b

View file

@ -1,104 +0,0 @@
module A = Bigarray.Array1
type int32arr = (int32, Bigarray.int32_elt, Bigarray.c_layout) A.t
type t = { mutable data: int32arr; mutable sz: int }
let mk_arr_ sz : int32arr = A.create Bigarray.int32 Bigarray.c_layout sz
let create ?(cap = 16) () : t = { sz = 0; data = mk_arr_ cap }
let[@inline] clear self = self.sz <- 0
let[@inline] shrink self n = if n < self.sz then self.sz <- n
let[@inline] size self = self.sz
let[@inline] is_empty self = self.sz = 0
let copy self =
if size self = 0 then
create ~cap:0 ()
else (
(* copy bigarray *)
let data = mk_arr_ (size self) in
A.blit (A.sub self.data 0 (size self)) data;
{ sz = self.sz; data }
)
let[@inline] fast_remove t i =
assert (i >= 0 && i < t.sz);
A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);
t.sz <- t.sz - 1
let filter_in_place f vec =
let i = ref 0 in
while !i < size vec do
if f (A.unsafe_get vec.data !i) then
incr i
else
fast_remove vec !i
done
(* ensure capacity is [new_cap] *)
let resize_cap_ self new_cap =
assert (A.dim self.data < new_cap);
let new_data = mk_arr_ new_cap in
A.blit self.data (A.sub new_data 0 (A.dim self.data));
self.data <- new_data
let ensure_cap self (n : int) =
if n > A.dim self.data then (
let new_cap = max n (max 4 (A.dim self.data * 2)) in
resize_cap_ self new_cap
)
let ensure_size self n =
if n > self.sz then (
ensure_cap self n;
self.sz <- n
)
let[@inline] push (self : t) i : unit =
ensure_cap self (self.sz + 1);
self.data.{self.sz} <- i;
self.sz <- 1 + self.sz
let[@inline] push_i32 self i =
ensure_cap self (self.sz + 1);
self.data.{self.sz} <- i;
self.sz <- 1 + self.sz
let[@inline] pop self =
if self.sz > 0 then (
let x = self.data.{self.sz - 1} in
self.sz <- self.sz - 1;
x
) else
failwith "vecI32.pop: empty"
let[@inline] get self i : int32 =
assert (i >= 0 && i < self.sz);
A.unsafe_get self.data i
let[@inline] set self i x : unit =
assert (i >= 0 && i < self.sz);
A.unsafe_set self.data i x
let[@inline] set self i x : unit =
assert (i >= 0 && i < self.sz);
A.unsafe_set self.data i x
let[@inline] iter ~f self =
for i = 0 to self.sz - 1 do
f self.data.{i}
done
let[@inline] iteri ~f self =
for i = 0 to self.sz - 1 do
f i self.data.{i}
done
include Vec_sig.Make_extensions (struct
type nonrec elt = int32
type nonrec t = t
let get = get
let size = size
let iter = iter
let iteri = iteri
end)

View file

@ -1,5 +0,0 @@
(** Vectors of int32 integers
These vectors are more optimized than {!Vec}. *)
include Vec_sig.S with type elt := int32

View file

@ -84,10 +84,13 @@ let[@inline] iteri ~f self =
f i self.data.{i} f i self.data.{i}
done done
let to_iter v k = iter ~f:k v
include Vec_sig.Make_extensions (struct include Vec_sig.Make_extensions (struct
type nonrec elt = float type nonrec elt = float
type nonrec t = t type nonrec t = t
let to_iter = to_iter
let get = get let get = get
let size = size let size = size
let iter = iter let iter = iter

View file

@ -7,6 +7,7 @@ module type BASE_RO = sig
val get : t -> int -> elt val get : t -> int -> elt
val iter : f:(elt -> unit) -> t -> unit val iter : f:(elt -> unit) -> t -> unit
val iteri : f:(int -> elt -> unit) -> t -> unit val iteri : f:(int -> elt -> unit) -> t -> unit
val to_iter : t -> elt Iter.t
end end
module type BASE = sig module type BASE = sig
@ -33,7 +34,6 @@ module type EXTENSIONS = sig
type elt type elt
type t type t
val to_iter : t -> elt Iter.t
val to_array : t -> elt array val to_array : t -> elt array
val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a 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
@ -48,8 +48,6 @@ module Make_extensions (B : BASE_RO) :
EXTENSIONS with type t := B.t and type elt := B.elt = struct EXTENSIONS with type t := B.t and type elt := B.elt = struct
include B include B
let[@inline] to_iter self k = iter ~f:k self
let to_array self = let to_array self =
if size self = 0 then if size self = 0 then
[||] [||]

View file

@ -97,10 +97,13 @@ let[@inline] iteri ~f self =
f i (Int32.to_int self.data.{i}) f i (Int32.to_int self.data.{i})
done done
let[@inline] to_iter self k = iter ~f:k self
include Vec_sig.Make_extensions (struct include Vec_sig.Make_extensions (struct
type nonrec elt = int type nonrec elt = int
type nonrec t = t type nonrec t = t
let to_iter = to_iter
let get = get let get = get
let size = size let size = size
let iter = iter let iter = iter