mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-12 14:00:42 -05:00
refactor: simplify vec, remove the need to provide dummy elt
This commit is contained in:
Simon Cruanes
Guillaume Bury
parent
b3fc070d09
commit
e60aff60b6
14 changed files with 100 additions and 314 deletions
|
|
@ -34,7 +34,7 @@ module Make(St : Solver_types_intf.S) = struct
|
|||
|
||||
(* Dimacs & iCNF export *)
|
||||
let export_vec name fmt vec =
|
||||
Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.Clause.pp_dimacs) vec
|
||||
Format.fprintf fmt "c %s@,%a@," name (Vec.pp ~sep:"" St.Clause.pp_dimacs) vec
|
||||
|
||||
let export_assumption fmt vec =
|
||||
Format.fprintf fmt "c Local assumptions@,a %a@," St.Clause.pp_dimacs vec
|
||||
|
|
@ -66,7 +66,7 @@ module Make(St : Solver_types_intf.S) = struct
|
|||
end
|
||||
|
||||
let filter_vec learnt =
|
||||
let lemmas = Vec.make (Vec.size learnt) St.Clause.dummy in
|
||||
let lemmas = Vec.create() in
|
||||
Vec.iter (fun c ->
|
||||
match map_filter_learnt c with
|
||||
| None -> ()
|
||||
|
|
|
|||
|
|
@ -55,9 +55,6 @@ module type S = sig
|
|||
val print : Format.formatter -> t -> unit
|
||||
(** Printing function used among other thing for debugging. *)
|
||||
|
||||
val dummy : t
|
||||
(** Constant formula. A valid formula should never be physically equal to [dummy] *)
|
||||
|
||||
val neg : t -> t
|
||||
(** Formula negation *)
|
||||
|
||||
|
|
|
|||
|
|
@ -35,9 +35,6 @@ module type S = sig
|
|||
val print : Format.formatter -> t -> unit
|
||||
(** Printing function used among other thing for debugging. *)
|
||||
|
||||
val dummy : t
|
||||
(** Formula constant. A valid formula should never be physically equal to [dummy] *)
|
||||
|
||||
val neg : t -> t
|
||||
(** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should
|
||||
always hold. *)
|
||||
|
|
|
|||
|
|
@ -8,12 +8,12 @@ module Make(Elt : RANKED) = struct
|
|||
|
||||
type t = {
|
||||
heap : elt Vec.t;
|
||||
}
|
||||
} [@@unboxed]
|
||||
|
||||
let _absent_index = -1
|
||||
|
||||
let create () =
|
||||
{ heap = Vec.make_empty Elt.dummy; }
|
||||
{ heap = Vec.create(); }
|
||||
|
||||
let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
|
||||
let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
|
||||
|
|
@ -109,9 +109,6 @@ module Make(Elt : RANKED) = struct
|
|||
percolate_up s elt;
|
||||
)
|
||||
|
||||
let[@inline] grow_to_at_least s sz =
|
||||
Vec.grow_to_at_least s.heap sz
|
||||
|
||||
(*
|
||||
let update cmp s n =
|
||||
assert (heap_property cmp s);
|
||||
|
|
@ -130,10 +127,9 @@ module Make(Elt : RANKED) = struct
|
|||
if Vec.size heap=0 then raise Not_found;
|
||||
let x = Vec.get heap 0 in
|
||||
Elt.set_idx x _absent_index;
|
||||
let new_hd = Vec.last heap in (* heap.last() *)
|
||||
let new_hd = Vec.pop heap in (* new head *)
|
||||
Vec.set heap 0 new_hd;
|
||||
Elt.set_idx new_hd 0;
|
||||
Vec.pop heap; (* remove last *)
|
||||
(* enforce heap property again *)
|
||||
if Vec.size heap > 1 then (
|
||||
percolate_down s new_hd;
|
||||
|
|
|
|||
|
|
@ -3,7 +3,6 @@ module type RANKED = sig
|
|||
type t
|
||||
val idx: t -> int (** Index in heap. return -1 if never set *)
|
||||
val set_idx : t -> int -> unit (** Update index in heap *)
|
||||
val dummy : t
|
||||
val cmp : t -> t -> bool
|
||||
end
|
||||
|
||||
|
|
@ -36,10 +35,6 @@ module type S = sig
|
|||
val insert : t -> elt -> unit
|
||||
(** Insert a new element into the heap *)
|
||||
|
||||
val grow_to_at_least: t -> int -> unit
|
||||
(** Hint: augment the internal capacity of the heap until it reaches at
|
||||
least the given integer *)
|
||||
|
||||
(*val update : (int -> int -> bool) -> t -> int -> unit*)
|
||||
|
||||
val remove_min : t -> elt
|
||||
|
|
|
|||
|
|
@ -17,7 +17,6 @@ module Make
|
|||
module H = Heap.Make(struct
|
||||
type t = St.Elt.t
|
||||
let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *)
|
||||
let dummy = Elt.of_var St.Var.dummy
|
||||
let idx = Elt.idx
|
||||
let set_idx = Elt.set_idx
|
||||
end)
|
||||
|
|
@ -122,14 +121,14 @@ module Make
|
|||
}
|
||||
|
||||
(* Starting environment. *)
|
||||
let create_ ~st ~size_trail ~size_lvl () : t = {
|
||||
let create_ ~st () : t = {
|
||||
st;
|
||||
unsat_conflict = None;
|
||||
next_decision = None;
|
||||
|
||||
clauses_hyps = Vec.make 0 Clause.dummy;
|
||||
clauses_learnt = Vec.make 0 Clause.dummy;
|
||||
clauses_temp = Vec.make 0 Clause.dummy;
|
||||
clauses_hyps = Vec.create();
|
||||
clauses_learnt = Vec.create();
|
||||
clauses_temp = Vec.create();
|
||||
|
||||
clauses_root = Stack.create ();
|
||||
clauses_to_add = Stack.create ();
|
||||
|
|
@ -137,10 +136,10 @@ module Make
|
|||
th_head = 0;
|
||||
elt_head = 0;
|
||||
|
||||
trail = Vec.make size_trail (Trail_elt.of_atom Atom.dummy);
|
||||
elt_levels = Vec.make size_lvl (-1);
|
||||
th_levels = Vec.make size_lvl Plugin.dummy;
|
||||
user_levels = Vec.make 0 (-1);
|
||||
trail = Vec.create ();
|
||||
elt_levels = Vec.create();
|
||||
th_levels = Vec.create();
|
||||
user_levels = Vec.create();
|
||||
|
||||
order = H.create();
|
||||
|
||||
|
|
@ -153,13 +152,9 @@ module Make
|
|||
dirty=false;
|
||||
}
|
||||
|
||||
let create ?(size=`Big) ?st () : t =
|
||||
let st = match st with Some s -> s | None -> St.create ~size () in
|
||||
let size_trail, size_lvl = match size with
|
||||
| `Tiny -> 0, 0
|
||||
| `Small -> 32, 16
|
||||
| `Big -> 600, 50
|
||||
in create_ ~st ~size_trail ~size_lvl ()
|
||||
let create ?(size=`Big) () : t =
|
||||
let st = St.create ~size () in
|
||||
create_ ~st ()
|
||||
|
||||
(* Misc functions *)
|
||||
let to_float = float_of_int
|
||||
|
|
@ -504,8 +499,8 @@ module Make
|
|||
Log.debugf error
|
||||
(fun k ->
|
||||
k "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
|
||||
(Vec.print ~sep:"" Atom.debug)
|
||||
(Vec.from_list l Atom.dummy)
|
||||
(Vec.pp ~sep:"" Atom.debug)
|
||||
(Vec.of_list l)
|
||||
Clause.debug cl);
|
||||
assert false
|
||||
end
|
||||
|
|
@ -537,7 +532,6 @@ module Make
|
|||
let l = List.map (Lit.make st.st) terms in
|
||||
let lvl = List.fold_left (fun acc {l_level; _} ->
|
||||
assert (l_level > 0); max acc l_level) 0 l in
|
||||
H.grow_to_at_least st.order (St.nb_elt st.st);
|
||||
enqueue_bool st a ~level:lvl Semantic
|
||||
)
|
||||
|
||||
|
|
@ -864,8 +858,6 @@ module Make
|
|||
|
||||
let flush_clauses st =
|
||||
if not (Stack.is_empty st.clauses_to_add) then (
|
||||
let nbv = St.nb_elt st.st in
|
||||
H.grow_to_at_least st.order nbv;
|
||||
while not (Stack.is_empty st.clauses_to_add) do
|
||||
let c = Stack.pop st.clauses_to_add in
|
||||
add_clause st c
|
||||
|
|
@ -986,7 +978,6 @@ module Make
|
|||
else if p.neg.is_true then (
|
||||
Stack.push c st.clauses_to_add
|
||||
) else (
|
||||
H.grow_to_at_least st.order (St.nb_elt st.st);
|
||||
insert_subterms_order st p.var;
|
||||
let level = List.fold_left (fun acc a -> max acc a.var.v_level) 0 l in
|
||||
enqueue_bool st p ~level (Bcp c)
|
||||
|
|
@ -1033,7 +1024,6 @@ module Make
|
|||
if not @@ List.for_all (fun a -> a.neg.is_true) l then (
|
||||
raise (Invalid_argument "msat:core/internal: invalid conflict");
|
||||
);
|
||||
H.grow_to_at_least st.order (St.nb_elt st.st);
|
||||
List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l;
|
||||
(* Create the clause and return it. *)
|
||||
let c = St.Clause.make l (Lemma p) in
|
||||
|
|
@ -1215,14 +1205,14 @@ module Make
|
|||
cancel_until st (base_level st);
|
||||
Log.debugf debug
|
||||
(fun k -> k "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]"
|
||||
st.elt_head st.th_head (Vec.print ~sep:"" Trail_elt.debug) st.trail);
|
||||
st.elt_head st.th_head (Vec.pp ~sep:"" Trail_elt.debug) st.trail);
|
||||
begin match propagate st with
|
||||
| Some confl ->
|
||||
report_unsat st confl
|
||||
| None ->
|
||||
Log.debugf debug
|
||||
(fun k -> k "@[<v>Current trail:@,@[<hov>%a@]@]"
|
||||
(Vec.print ~sep:"" Trail_elt.debug) st.trail);
|
||||
(Vec.pp ~sep:"" Trail_elt.debug) st.trail);
|
||||
Log.debug info "Creating new user level";
|
||||
new_decision_level st;
|
||||
Vec.push st.user_levels (Vec.size st.clauses_temp);
|
||||
|
|
@ -1237,8 +1227,7 @@ module Make
|
|||
Log.debug info "Popping user level";
|
||||
assert (base_level st > 0);
|
||||
st.unsat_conflict <- None;
|
||||
let n = Vec.last st.user_levels in
|
||||
Vec.pop st.user_levels; (* before the [cancel_until]! *)
|
||||
let n = Vec.pop st.user_levels in (* before the [cancel_until]! *)
|
||||
(* Add the root clauses to the clauses to add *)
|
||||
Stack.iter (fun c -> Stack.push c st.clauses_to_add) st.clauses_root;
|
||||
Stack.clear st.clauses_root;
|
||||
|
|
@ -1263,9 +1252,6 @@ module Make
|
|||
(* conflict between assumptions: UNSAT *)
|
||||
report_unsat st c;
|
||||
) else (
|
||||
(* Grow the heap, because when the lit is backtracked,
|
||||
it will be added to the heap. *)
|
||||
H.grow_to_at_least st.order (St.nb_elt st.st);
|
||||
(* make a decision, propagate *)
|
||||
let level = decision_level st in
|
||||
enqueue_bool st a ~level (Bcp c);
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ module Make
|
|||
type t = S.t
|
||||
type solver = t
|
||||
|
||||
let[@inline] create ?size () = S.create ?size ()
|
||||
let create = S.create
|
||||
|
||||
(* Result type *)
|
||||
type res =
|
||||
|
|
@ -44,10 +44,10 @@ module Make
|
|||
"@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,\
|
||||
@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
|
||||
status
|
||||
(Vec.print ~sep:"" St.Trail_elt.debug) (S.trail st)
|
||||
(Vec.print ~sep:"" St.Clause.debug) (S.temp st)
|
||||
(Vec.print ~sep:"" St.Clause.debug) (S.hyps st)
|
||||
(Vec.print ~sep:"" St.Clause.debug) (S.history st)
|
||||
(Vec.pp ~sep:"" St.Trail_elt.debug) (S.trail st)
|
||||
(Vec.pp ~sep:"" St.Clause.debug) (S.temp st)
|
||||
(Vec.pp ~sep:"" St.Clause.debug) (S.hyps st)
|
||||
(Vec.pp ~sep:"" St.Clause.debug) (S.history st)
|
||||
)
|
||||
|
||||
let mk_sat (st:S.t) : (_,_) sat_state =
|
||||
|
|
|
|||
|
|
@ -24,8 +24,6 @@ module McMake (E : Expr_intf.S) = struct
|
|||
type formula = E.Formula.t
|
||||
type proof = E.proof
|
||||
|
||||
let pp_form = E.Formula.dummy
|
||||
|
||||
type seen =
|
||||
| Nope
|
||||
| Both
|
||||
|
|
@ -91,37 +89,6 @@ module McMake (E : Expr_intf.S) = struct
|
|||
| Lit of lit
|
||||
| Atom of atom
|
||||
|
||||
let rec dummy_var =
|
||||
{ vid = -101;
|
||||
pa = dummy_atom;
|
||||
na = dummy_atom;
|
||||
v_fields = Var_fields.empty;
|
||||
v_level = -1;
|
||||
v_weight = -1.;
|
||||
v_idx= -1;
|
||||
v_assignable = None;
|
||||
reason = None;
|
||||
}
|
||||
and dummy_atom =
|
||||
{ var = dummy_var;
|
||||
lit = E.Formula.dummy;
|
||||
watched = Obj.magic 0;
|
||||
(* should be [Vec.make_empty dummy_clause]
|
||||
but we have to break the cycle *)
|
||||
neg = dummy_atom;
|
||||
is_true = false;
|
||||
aid = -102 }
|
||||
let dummy_clause =
|
||||
{ name = -1;
|
||||
tag = None;
|
||||
atoms = [| |];
|
||||
activity = -1.;
|
||||
attached = false;
|
||||
visited = false;
|
||||
cpremise = History [] }
|
||||
|
||||
let () = dummy_atom.watched <- Vec.make_empty dummy_clause
|
||||
|
||||
(* Constructors *)
|
||||
module MF = Hashtbl.Make(E.Formula)
|
||||
module MT = Hashtbl.Make(E.Term)
|
||||
|
|
@ -136,21 +103,21 @@ module McMake (E : Expr_intf.S) = struct
|
|||
|
||||
type state = t
|
||||
|
||||
let create_ size_map size_vars () : t = {
|
||||
let create_ size_map () : t = {
|
||||
f_map = MF.create size_map;
|
||||
t_map = MT.create size_map;
|
||||
vars = Vec.make size_vars (E_var dummy_var);
|
||||
vars = Vec.create();
|
||||
cpt_mk_var = 0;
|
||||
cpt_mk_clause = 0;
|
||||
}
|
||||
|
||||
let create ?(size=`Big) () : t =
|
||||
let size_map, size_vars = match size with
|
||||
| `Tiny -> 8, 0
|
||||
| `Small -> 16, 10
|
||||
| `Big -> 4096, 128
|
||||
let size_map = match size with
|
||||
| `Tiny -> 8
|
||||
| `Small -> 16
|
||||
| `Big -> 4096
|
||||
in
|
||||
create_ size_map size_vars ()
|
||||
create_ size_map ()
|
||||
|
||||
let nb_elt st = Vec.size st.vars
|
||||
let get_elt st i = Vec.get st.vars i
|
||||
|
|
@ -200,7 +167,6 @@ module McMake (E : Expr_intf.S) = struct
|
|||
|
||||
module Var = struct
|
||||
type t = var
|
||||
let dummy = dummy_var
|
||||
let[@inline] level v = v.v_level
|
||||
let[@inline] pos v = v.pa
|
||||
let[@inline] neg v = v.na
|
||||
|
|
@ -228,14 +194,14 @@ module McMake (E : Expr_intf.S) = struct
|
|||
and pa =
|
||||
{ var = var;
|
||||
lit = lit;
|
||||
watched = Vec.make 10 dummy_clause;
|
||||
watched = Vec.create();
|
||||
neg = na;
|
||||
is_true = false;
|
||||
aid = cpt_double (* aid = vid*2 *) }
|
||||
and na =
|
||||
{ var = var;
|
||||
lit = E.Formula.neg lit;
|
||||
watched = Vec.make 10 dummy_clause;
|
||||
watched = Vec.create();
|
||||
neg = pa;
|
||||
is_true = false;
|
||||
aid = cpt_double + 1 (* aid = vid*2+1 *) } in
|
||||
|
|
@ -255,7 +221,6 @@ module McMake (E : Expr_intf.S) = struct
|
|||
|
||||
module Atom = struct
|
||||
type t = atom
|
||||
let dummy = dummy_atom
|
||||
let[@inline] level a = a.var.v_level
|
||||
let[@inline] var a = a.var
|
||||
let[@inline] neg a = a.neg
|
||||
|
|
@ -370,7 +335,6 @@ module McMake (E : Expr_intf.S) = struct
|
|||
|
||||
module Clause = struct
|
||||
type t = clause
|
||||
let dummy = dummy_clause
|
||||
|
||||
let make =
|
||||
let n = ref 0 in
|
||||
|
|
|
|||
|
|
@ -156,7 +156,6 @@ module type S = sig
|
|||
|
||||
module Var : sig
|
||||
type t = var
|
||||
val dummy : t
|
||||
|
||||
val pos : t -> atom
|
||||
val neg : t -> atom
|
||||
|
|
@ -180,7 +179,6 @@ module type S = sig
|
|||
|
||||
module Atom : sig
|
||||
type t = atom
|
||||
val dummy : t
|
||||
val level : t -> int
|
||||
val reason : t -> reason option
|
||||
val lit : t -> formula
|
||||
|
|
@ -227,7 +225,6 @@ module type S = sig
|
|||
|
||||
module Clause : sig
|
||||
type t = clause
|
||||
val dummy : t
|
||||
|
||||
val name : t -> string
|
||||
val equal : t -> t -> bool
|
||||
|
|
|
|||
|
|
@ -49,9 +49,6 @@ module type S = sig
|
|||
type level
|
||||
(** The type for levels to allow backtracking. *)
|
||||
|
||||
val dummy : level
|
||||
(** A dummy level. *)
|
||||
|
||||
val current_level : unit -> level
|
||||
(** Return the current level of the theory (either the empty/beginning state, or the
|
||||
last level returned by the [assume] function). *)
|
||||
|
|
@ -76,7 +73,6 @@ module Dummy(F: Formula_intf.S)
|
|||
type formula = F.t
|
||||
type proof = unit
|
||||
type level = unit
|
||||
let dummy = ()
|
||||
let current_level () = ()
|
||||
let assume _ = Sat
|
||||
let if_sat _ = Sat
|
||||
|
|
|
|||
204
src/core/Vec.ml
204
src/core/Vec.ml
|
|
@ -1,49 +1,12 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Cubicle *)
|
||||
(* Combining model checking algorithms and SMT solvers *)
|
||||
(* *)
|
||||
(* Mohamed Iguernelala *)
|
||||
(* Universite Paris-Sud 11 *)
|
||||
(* *)
|
||||
(* Copyright 2011. This file is distributed under the terms of the *)
|
||||
(* Apache Software License version 2.0 *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
type 'a t = {
|
||||
mutable dummy: 'a;
|
||||
mutable data : 'a array;
|
||||
mutable sz : int;
|
||||
}
|
||||
|
||||
let _size_too_big()=
|
||||
failwith "Vec: capacity exceeds maximum array size"
|
||||
let make n x = {data=Array.make n x; sz=0}
|
||||
|
||||
let make capa d =
|
||||
if capa > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.make capa d; sz = 0; dummy = d}
|
||||
|
||||
let[@inline] make_empty d = {data = [||]; sz=0; dummy=d }
|
||||
|
||||
let init capa f d =
|
||||
if capa > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
|
||||
|
||||
let from_array data sz d =
|
||||
assert (sz <= Array.length data);
|
||||
{data = data; sz = sz; dummy = d}
|
||||
|
||||
let from_list l d =
|
||||
let a = Array.of_list l in
|
||||
from_array a (Array.length a) d
|
||||
|
||||
let to_list s =
|
||||
let l = ref [] in
|
||||
for i = 0 to s.sz - 1 do
|
||||
l := s.data.(i) :: !l
|
||||
done;
|
||||
List.rev !l
|
||||
let[@inline] create () = {data = [||]; sz = 0}
|
||||
|
||||
let[@inline] clear s = s.sz <- 0
|
||||
|
||||
|
|
@ -54,159 +17,96 @@ let[@inline] shrink t i =
|
|||
|
||||
let[@inline] pop t =
|
||||
if t.sz = 0 then invalid_arg "vec.pop";
|
||||
t.sz <- t.sz - 1
|
||||
let x = Array.unsafe_get t.data (t.sz - 1) in
|
||||
t.sz <- t.sz - 1;
|
||||
x
|
||||
|
||||
let[@inline] size t = t.sz
|
||||
|
||||
let[@inline] is_empty t = t.sz = 0
|
||||
|
||||
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);
|
||||
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_exact t size
|
||||
|
||||
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
|
||||
let capa = ref (max (Array.length data) 1) in
|
||||
while !capa < new_capa do
|
||||
capa := min (2 * !capa + 1) Sys.max_array_length;
|
||||
done;
|
||||
if !capa > Array.length data then (
|
||||
grow_to_exact t !capa
|
||||
)
|
||||
|
||||
let[@inline] is_full t = Array.length t.data = t.sz
|
||||
|
||||
let[@inline] push t e =
|
||||
if is_full t then grow_to_double_size t;
|
||||
t.data.(t.sz) <- e;
|
||||
let[@inline] copy t : _ t =
|
||||
let data = Array.copy t.data in
|
||||
{t with data}
|
||||
|
||||
(* grow the array *)
|
||||
let[@inline never] grow_to_double_size t x : unit =
|
||||
if Array.length t.data = Sys.max_array_length then (
|
||||
failwith "vec: cannot resize";
|
||||
);
|
||||
let size =
|
||||
min Sys.max_array_length (max 4 (2 * Array.length t.data))
|
||||
in
|
||||
let arr' = Array.make size x in
|
||||
Array.blit t.data 0 arr' 0 (Array.length t.data);
|
||||
t.data <- arr';
|
||||
assert (Array.length t.data > t.sz);
|
||||
()
|
||||
|
||||
let[@inline] push t x : unit =
|
||||
if is_full t then grow_to_double_size t x;
|
||||
Array.unsafe_set t.data t.sz x;
|
||||
t.sz <- t.sz + 1
|
||||
|
||||
let[@inline] last t =
|
||||
if t.sz = 0 then invalid_arg "vec.last";
|
||||
t.data.(t.sz - 1)
|
||||
|
||||
let[@inline] pop_last t =
|
||||
if t.sz = 0 then invalid_arg "vec.pop_last";
|
||||
let x = t.data.(t.sz - 1) in
|
||||
t.sz <- t.sz - 1;
|
||||
x
|
||||
|
||||
let[@inline] get t i =
|
||||
if i < 0 || i >= t.sz then invalid_arg "vec.get";
|
||||
Array.unsafe_get t.data i
|
||||
|
||||
let[@inline] set t i v =
|
||||
if i < 0 || i > t.sz then invalid_arg "vec.set";
|
||||
if i = t.sz then
|
||||
if i = t.sz then (
|
||||
push t v
|
||||
else
|
||||
) else (
|
||||
Array.unsafe_set t.data i v
|
||||
|
||||
let[@inline] copy t =
|
||||
let data = Array.copy t.data in
|
||||
{t with data; }
|
||||
|
||||
let[@inline] move_to t t' =
|
||||
t'.data <- Array.copy t.data;
|
||||
t'.sz <- t.sz
|
||||
|
||||
let remove t e =
|
||||
let j = ref 0 in
|
||||
while (!j < t.sz && not (t.data.(!j) == e)) do incr j done;
|
||||
assert (!j < t.sz);
|
||||
for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done;
|
||||
pop t
|
||||
)
|
||||
|
||||
let[@inline] fast_remove t i =
|
||||
assert (i < t.sz);
|
||||
t.data.(i) <- t.data.(t.sz - 1);
|
||||
assert (i>= 0 && i < t.sz);
|
||||
Array.unsafe_set t.data i @@ Array.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 (get vec !i) then incr i else fast_remove vec !i
|
||||
if f (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i
|
||||
done
|
||||
|
||||
let sort t f =
|
||||
let sub_arr = Array.sub t.data 0 t.sz in
|
||||
let sort t f : unit =
|
||||
let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in
|
||||
Array.fast_sort f sub_arr;
|
||||
t.data <- sub_arr
|
||||
|
||||
let iter f t =
|
||||
let[@inline] iter f t =
|
||||
for i = 0 to size t - 1 do
|
||||
f (Array.unsafe_get t.data i)
|
||||
done
|
||||
|
||||
let append a b =
|
||||
grow_to_at_least a (size a + size b);
|
||||
iter (push a) b
|
||||
let[@inline] iteri f t =
|
||||
for i = 0 to size t - 1 do
|
||||
f i (Array.unsafe_get t.data i)
|
||||
done
|
||||
|
||||
let fold f acc t =
|
||||
let rec _fold f acc t i =
|
||||
if i=t.sz
|
||||
then acc
|
||||
else (
|
||||
let acc' = f acc (Array.unsafe_get t.data i) in
|
||||
_fold f acc' t (i+1)
|
||||
)
|
||||
in _fold f acc t 0
|
||||
let[@inline] to_seq a k = iter k a
|
||||
|
||||
exception ExitVec
|
||||
let exists p t = Sequence.exists p @@ to_seq t
|
||||
let for_all p t = Sequence.for_all p @@ to_seq t
|
||||
let fold f acc a = Sequence.fold f acc @@ to_seq a
|
||||
let to_list a = Sequence.to_list @@ to_seq a
|
||||
|
||||
let exists p t =
|
||||
try
|
||||
for i = 0 to t.sz - 1 do
|
||||
if p (Array.unsafe_get t.data i) then raise ExitVec
|
||||
done;
|
||||
false
|
||||
with ExitVec -> true
|
||||
let of_list l : _ t =
|
||||
match l with
|
||||
| [] -> create()
|
||||
| x :: tl ->
|
||||
let v = make (List.length tl+1) x in
|
||||
List.iter (push v) l;
|
||||
v
|
||||
|
||||
let for_all p t =
|
||||
try
|
||||
for i = 0 to t.sz - 1 do
|
||||
if not (p (Array.unsafe_get t.data i)) then raise ExitVec
|
||||
done;
|
||||
true
|
||||
with ExitVec -> false
|
||||
|
||||
let print ?(sep=", ") pp out v =
|
||||
let pp ?(sep=", ") pp out v =
|
||||
let first = ref true in
|
||||
iter
|
||||
(fun x ->
|
||||
if !first then first := false else Format.fprintf out "%s@," sep;
|
||||
pp out x)
|
||||
v
|
||||
|
||||
(*
|
||||
template<class V, class T>
|
||||
static inline void remove(V& ts, const T& t)
|
||||
{
|
||||
int j = 0;
|
||||
for (; j < ts.size() && ts[j] != t; j++);
|
||||
assert(j < ts.size());
|
||||
ts[j] = ts.last();
|
||||
ts.pop();
|
||||
}
|
||||
#endif
|
||||
|
||||
template<class V, class T>
|
||||
static inline bool find(V& ts, const T& t)
|
||||
{
|
||||
int j = 0;
|
||||
for (; j < ts.size() && ts[j] != t; j++);
|
||||
return j < ts.size();
|
||||
}
|
||||
|
||||
#endif
|
||||
*)
|
||||
|
|
|
|||
|
|
@ -1,15 +1,3 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Cubicle *)
|
||||
(* Combining model checking algorithms and SMT solvers *)
|
||||
(* *)
|
||||
(* Mohamed Iguernelala *)
|
||||
(* Universite Paris-Sud 11 *)
|
||||
(* *)
|
||||
(* Copyright 2011. This file is distributed under the terms of the *)
|
||||
(* Apache Software License version 2.0 *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
type 'a t
|
||||
(** Abstract type of vectors of 'a *)
|
||||
|
|
@ -19,22 +7,15 @@ val make : int -> 'a -> 'a t
|
|||
is initially empty but its underlying array has capacity [cap].
|
||||
[dummy] will stay alive as long as the vector *)
|
||||
|
||||
val make_empty : 'a -> 'a t
|
||||
(** Vector with an empty capacity. The only argument is the dummy. *)
|
||||
|
||||
val init : int -> (int -> 'a) -> 'a -> 'a t
|
||||
(** Same as {!Array.init}, but also with a dummy element *)
|
||||
|
||||
val from_array : 'a array -> int -> 'a -> 'a t
|
||||
(** [from_array arr size dummy] takes ownership of [data] (no copy)
|
||||
to create a vector. [size] is the length of the slice of [data] that is
|
||||
used ([size <= Array.length data] must hold) *)
|
||||
|
||||
val from_list : 'a list -> 'a -> 'a t
|
||||
val create : unit -> 'a t
|
||||
|
||||
val to_list : 'a t -> 'a list
|
||||
(** Returns the list of elements of the vector *)
|
||||
|
||||
val of_list : 'a list -> 'a t
|
||||
|
||||
val to_seq : 'a t -> 'a Sequence.t
|
||||
|
||||
val clear : 'a t -> unit
|
||||
(** Set size to 0, doesn't free elements *)
|
||||
|
||||
|
|
@ -42,37 +23,19 @@ val shrink : 'a t -> int -> unit
|
|||
(** [shrink vec sz] resets size of [vec] to [sz].
|
||||
Assumes [sz >=0 && sz <= size vec] *)
|
||||
|
||||
val pop : 'a t -> unit
|
||||
(** Pop last element
|
||||
val pop : 'a t -> 'a
|
||||
(** Pop last element and return it.
|
||||
@raise Invalid_argument if the vector is empty *)
|
||||
|
||||
val size : 'a t -> int
|
||||
|
||||
val is_empty : 'a t -> bool
|
||||
|
||||
val grow_to_exact : 'a t -> int -> unit
|
||||
|
||||
val grow_to_double_size : 'a t -> 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? *)
|
||||
|
||||
val push : 'a t -> 'a -> unit
|
||||
|
||||
val append : 'a t -> 'a t -> unit
|
||||
(** [append v1 v2] pushes all elements of [v2] into [v1] *)
|
||||
|
||||
val last : 'a t -> 'a
|
||||
(** Last element, or
|
||||
@raise Invalid_argument if the vector is empty *)
|
||||
|
||||
val pop_last : 'a t -> 'a
|
||||
(** Combine {!last} and {!pop}: remove last element and return it
|
||||
@raise Invalid_argument if empty *)
|
||||
(** Push element into the vector *)
|
||||
|
||||
val get : 'a t -> int -> 'a
|
||||
(** get the element at the given index, or
|
||||
|
|
@ -86,12 +49,6 @@ val set : 'a t -> int -> 'a -> unit
|
|||
val copy : 'a t -> 'a t
|
||||
(** Fresh copy *)
|
||||
|
||||
val move_to : 'a t -> 'a t -> unit
|
||||
(** [move_to a b] copies the content of [a] to [b], discarding [b]'s old content *)
|
||||
|
||||
val remove : 'a t -> 'a -> unit
|
||||
(** Uses [(==)] for comparison *)
|
||||
|
||||
val fast_remove : 'a t -> int -> unit
|
||||
(** Remove element at index [i] without preserving order
|
||||
(swap with last element) *)
|
||||
|
|
@ -106,6 +63,9 @@ val sort : 'a t -> ('a -> 'a -> int) -> unit
|
|||
val iter : ('a -> unit) -> 'a t -> unit
|
||||
(** Iterate on elements *)
|
||||
|
||||
val iteri : (int -> 'a -> unit) -> 'a t -> unit
|
||||
(** Iterate on elements with their index *)
|
||||
|
||||
val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
|
||||
(** Fold over elements *)
|
||||
|
||||
|
|
@ -115,7 +75,7 @@ val exists : ('a -> bool) -> 'a t -> bool
|
|||
val for_all : ('a -> bool) -> 'a t -> bool
|
||||
(** Do all elements satisfy the predicate? *)
|
||||
|
||||
val print :
|
||||
val pp :
|
||||
?sep:string ->
|
||||
(Format.formatter -> 'a -> unit) ->
|
||||
Format.formatter -> 'a t -> unit
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
(library
|
||||
(name msat)
|
||||
(public_name msat)
|
||||
(libraries sequence)
|
||||
(synopsis "core data structures and algorithms for msat")
|
||||
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
|
||||
(ocamlopt_flags :standard -O3 -bin-annot
|
||||
|
|
|
|||
|
|
@ -26,9 +26,6 @@ let _make i =
|
|||
end else
|
||||
raise Bad_atom
|
||||
|
||||
(** A dummy atom *)
|
||||
let dummy = 0
|
||||
|
||||
(** *)
|
||||
let neg a = - a
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue