From 6be7e7c71a6b2861e6a333d3e82fa464a75742d3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 24 Nov 2016 14:11:58 +0100 Subject: [PATCH] rename a Vec function `grow_to_by_double` becomes `grow_to_at_least` so that it doesn't specify its own implementation's strategy --- src/core/internal.ml | 12 ++++++------ src/util/iheap.ml | 4 ++-- src/util/iheap.mli | 2 +- src/util/vec.ml | 13 +++++-------- src/util/vec.mli | 6 ++++-- 5 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index f7242410..766f69e6 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -783,9 +783,9 @@ module Make if not (Stack.is_empty env.clauses_to_add) then begin let nbv = St.nb_elt () in let nbc = env.nb_init_clauses + Stack.length env.clauses_to_add in - Iheap.grow_to_by_double env.order nbv; - Vec.grow_to_by_double env.clauses_hyps nbc; - Vec.grow_to_by_double env.clauses_learnt nbc; + Iheap.grow_to_at_least env.order nbv; + Vec.grow_to_at_least env.clauses_hyps nbc; + Vec.grow_to_at_least env.clauses_learnt nbc; env.nb_init_clauses <- nbc; while not (Stack.is_empty env.clauses_to_add) do let c = Stack.pop env.clauses_to_add in @@ -898,7 +898,7 @@ module Make let slice_propagate f lvl = let a = atom f in - Iheap.grow_to_by_double env.order (St.nb_elt ()); + Iheap.grow_to_at_least env.order (St.nb_elt ()); enqueue_bool a lvl (Semantic lvl) let current_slice (): (_,_,_) Plugin_intf.slice = { @@ -935,7 +935,7 @@ module Make | Plugin_intf.Unsat (l, p) -> (* conflict *) let l = List.rev_map new_atom l in - Iheap.grow_to_by_double env.order (St.nb_elt ()); + Iheap.grow_to_at_least env.order (St.nb_elt ()); List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in Some c @@ -1175,7 +1175,7 @@ module Make end else begin (* Grow the heap, because when the lit is backtracked, it will be added to the heap. *) - Iheap.grow_to_by_double env.order (St.nb_elt ()); + Iheap.grow_to_at_least env.order (St.nb_elt ()); (* make a decision, propagate *) let level = decision_level() in enqueue_bool a ~level (Bcp c); diff --git a/src/util/iheap.ml b/src/util/iheap.ml index a0e6603f..d23767cb 100644 --- a/src/util/iheap.ml +++ b/src/util/iheap.ml @@ -111,9 +111,9 @@ let insert cmp s n = percolate_up cmp s (V.get s.indices n) end -let grow_to_by_double s sz = +let grow_to_at_least s sz = V.resize s.indices sz; - Vec.grow_to_by_double s.heap sz + Vec.grow_to_at_least s.heap sz (* let update cmp s n = diff --git a/src/util/iheap.mli b/src/util/iheap.mli index c2825e41..6c1004a5 100644 --- a/src/util/iheap.mli +++ b/src/util/iheap.mli @@ -40,7 +40,7 @@ val clear : t -> unit val insert : (int -> int -> bool) -> t -> int -> unit (** Insert a new integer into the heap, according to the given comparison *) -val grow_to_by_double: t -> int -> unit +val grow_to_at_least: t -> int -> unit (** Hint: augment the internal capacity of the heap until it reaches at least the given integer *) diff --git a/src/util/vec.ml b/src/util/vec.ml index c9df846e..91177a34 100644 --- a/src/util/vec.ml +++ b/src/util/vec.ml @@ -57,22 +57,19 @@ let size t = t.sz let is_empty t = t.sz = 0 -let grow_to t new_capa = +let grow_to_exact t new_capa = assert (new_capa >= Array.length t.data); let new_data = Array.make new_capa t.dummy in assert (t.sz <= new_capa); - let old = t.data in - for i = 0 to t.sz - 1 do - Array.unsafe_set new_data i (Array.unsafe_get old i) - done; + Array.blit t.data 0 new_data 0 t.sz; t.data <- new_data let grow_to_double_size t = if Array.length t.data = Sys.max_array_length then _size_too_big(); let size = min Sys.max_array_length (2* Array.length t.data + 1) in - grow_to t size + grow_to_exact t size -let grow_to_by_double t new_capa = +let grow_to_at_least t new_capa = assert (new_capa >= 0); if new_capa > Sys.max_array_length then _size_too_big (); let data = t.data in @@ -80,7 +77,7 @@ let grow_to_by_double t new_capa = while !capa < new_capa do capa := min (2 * !capa + 1) Sys.max_array_length; done; - grow_to t !capa + grow_to_exact t !capa let is_full t = Array.length t.data = t.sz diff --git a/src/util/vec.mli b/src/util/vec.mli index a8017b06..d57b9cc3 100644 --- a/src/util/vec.mli +++ b/src/util/vec.mli @@ -49,11 +49,13 @@ val size : 'a t -> int val is_empty : 'a t -> bool -val grow_to : 'a t -> int -> unit +val grow_to_exact : 'a t -> int -> unit val grow_to_double_size : 'a t -> unit -val grow_to_by_double : 'a t -> int -> unit +val grow_to_at_least : 'a t -> int -> unit +(** [grow_to_at_least vec n] ensures that [capacity vec >= n] in + the most efficient way *) val is_full : 'a t -> bool (** Is the capacity of the vector equal to the number of its elements? *)