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

remove iarray

Browse source
This commit is contained in:
Simon Cruanes 2022-07-15 21:06:46 -04:00
parent 801d0b3e45
commit 00dec7ced8
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
27 changed files with 149 additions and 393 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/base-solver/sidekick_base_solver.ml
View file

@ -44,24 +44,22 @@ module Th_data = Sidekick_th_data.Make (struct
match Term.view t with
| Term.App_fun ({ fun_view = Fun.Fun_cstor c; _ }, args) -> T_cstor (c, args)
| Term.App_fun ({ fun_view = Fun.Fun_select sel; _ }, args) ->
assert (IArray.length args = 1);
T_select (sel.select_cstor, sel.select_i, IArray.get args 0)
assert (CCArray.length args = 1);
T_select (sel.select_cstor, sel.select_i, CCArray.get args 0)
| Term.App_fun ({ fun_view = Fun.Fun_is_a c; _ }, args) ->
assert (IArray.length args = 1);
T_is_a (c, IArray.get args 0)
assert (CCArray.length args = 1);
T_is_a (c, CCArray.get args 0)
| _ -> T_other t
let mk_eq = Term.eq
let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
let mk_sel tst c i u =
Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u)
let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) [| u |]
let mk_is_a tst c u : Term.t =
if c.cstor_arity = 0 then
Term.eq tst u (Term.const tst (Fun.cstor c))
else
Term.app_fun tst (Fun.is_a c) (IArray.singleton u)
Term.app_fun tst (Fun.is_a c) [| u |]
let ty_is_finite = Ty.finite
let ty_set_is_finite = Ty.set_finite

83
src/base/Base_types.ml
View file

@ -170,7 +170,7 @@ type term = {
term view. *)
and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t (* full, first-order application *)
| App_fun of fun_ * 'a array (* full, first-order application *)
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
@ -186,12 +186,12 @@ and fun_view =
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp: 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
abs: self:term -> term IArray.t -> term * bool; (* remove the sign? *)
pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
abs: self:term -> term array -> term * bool; (* remove the sign? *)
do_cc: bool; (* participate in congruence closure? *)
relevant: 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
ty: ID.t -> term IArray.t -> ty; (* compute type *)
eval: value IArray.t -> value; (* evaluate term *)
relevant: 'a. ID.t -> 'a array -> int -> bool; (* relevant argument? *)
ty: ID.t -> term array -> ty; (* compute type *)
eval: value array -> value; (* evaluate term *)
}
(** Methods on the custom term view whose arguments are ['a].
Terms must be printable, and provide some additional theory handles.
@ -336,10 +336,9 @@ let pp_term_view_gen ~pp_id ~pp_t out = function
| Bool false -> Fmt.string out "false"
| App_fun ({ fun_view = Fun_def { pp = Some pp_custom; _ }; _ }, l) ->
pp_custom pp_t out l
| App_fun (c, a) when IArray.is_empty a -> pp_id out (id_of_fun c)
| App_fun (c, [||]) -> pp_id out (id_of_fun c)
| App_fun (f, l) ->
Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_fun f) (Util.pp_iarray pp_t)
l
Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_fun f) (Util.pp_array pp_t) l
| Eq (a, b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
| Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u
| Ite (a, b, c) ->
@ -547,13 +546,13 @@ module Fun : sig
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp: 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
abs: self:term -> term IArray.t -> term * bool; (* remove the sign? *)
pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
abs: self:term -> term array -> term * bool; (* remove the sign? *)
do_cc: bool; (* participate in congruence closure? *)
relevant: 'a. ID.t -> 'a IArray.t -> int -> bool;
relevant: 'a. ID.t -> 'a array -> int -> bool;
(* relevant argument? *)
ty: ID.t -> term IArray.t -> ty; (* compute type *)
eval: value IArray.t -> value; (* evaluate term *)
ty: ID.t -> term array -> ty; (* compute type *)
eval: value array -> value; (* evaluate term *)
}
(** user defined function symbol.
A good example can be found in {!Form} for boolean connectives. *)
@ -594,13 +593,13 @@ end = struct
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp: 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
abs: self:term -> term IArray.t -> term * bool; (* remove the sign? *)
pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
abs: self:term -> term array -> term * bool; (* remove the sign? *)
do_cc: bool; (* participate in congruence closure? *)
relevant: 'a. ID.t -> 'a IArray.t -> int -> bool;
relevant: 'a. ID.t -> 'a array -> int -> bool;
(* relevant argument? *)
ty: ID.t -> term IArray.t -> ty; (* compute type *)
eval: value IArray.t -> value; (* evaluate term *)
ty: ID.t -> term array -> ty; (* compute type *)
eval: value array -> value; (* evaluate term *)
}
type t = fun_ = { fun_id: ID.t; fun_view: fun_view }
@ -666,7 +665,7 @@ end
module Term_cell : sig
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| App_fun of fun_ * 'a array
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
@ -680,7 +679,7 @@ module Term_cell : sig
val true_ : t
val false_ : t
val const : fun_ -> t
val app_fun : fun_ -> term IArray.t -> t
val app_fun : fun_ -> term array -> t
val eq : term -> term -> t
val not_ : term -> t
val ite : term -> term -> term -> t
@ -710,7 +709,7 @@ module Term_cell : sig
end = struct
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| App_fun of fun_ * 'a array
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
@ -746,7 +745,7 @@ end = struct
match a, b with
| Bool b1, Bool b2 -> CCBool.equal b1 b2
| App_fun (f1, a1), App_fun (f2, a2) ->
Fun.equal f1 f2 && IArray.equal sub_eq a1 a2
Fun.equal f1 f2 && CCArray.equal sub_eq a1 a2
| Eq (a1, b1), Eq (a2, b2) -> sub_eq a1 a2 && sub_eq b1 b2
| Not a, Not b -> sub_eq a b
| Ite (a1, b1, c1), Ite (a2, b2, c2) ->
@ -770,7 +769,7 @@ end = struct
let true_ = Bool true
let false_ = Bool false
let app_fun f a = App_fun (f, a)
let const c = App_fun (c, IArray.empty)
let const c = App_fun (c, CCArray.empty)
let eq a b =
if term_equal_ a b then
@ -805,13 +804,13 @@ end = struct
| Fun_undef fty ->
let ty_args, ty_ret = Ty.Fun.unfold fty in
(* check arity *)
if List.length ty_args <> IArray.length args then
if List.length ty_args <> CCArray.length args then
Error.errorf "Term_cell.apply: expected %d args, got %d@ in %a"
(List.length ty_args) (IArray.length args) pp t;
(List.length ty_args) (CCArray.length args) pp t;
(* check types *)
List.iteri
(fun i ty_a ->
let a = IArray.get args i in
let a = CCArray.get args i in
if not @@ Ty.equal a.term_ty ty_a then
Error.errorf
"Term_cell.apply: %d-th argument mismatch:@ %a does not have \
@ -839,7 +838,7 @@ end = struct
let iter f view =
match view with
| Bool _ -> ()
| App_fun (_, a) -> IArray.iter f a
| App_fun (_, a) -> CCArray.iter f a
| Not u -> f u
| Eq (a, b) ->
f a;
@ -854,7 +853,7 @@ end = struct
let map f view =
match view with
| Bool b -> Bool b
| App_fun (fu, a) -> App_fun (fu, IArray.map f a)
| App_fun (fu, a) -> App_fun (fu, CCArray.map f a)
| Not u -> Not (f u)
| Eq (a, b) -> Eq (f a, f b)
| Ite (a, b, c) -> Ite (f a, f b, f c)
@ -872,7 +871,7 @@ module Term : sig
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| App_fun of fun_ * 'a array
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
@ -894,13 +893,13 @@ module Term : sig
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t IArray.t -> t
val app_fun : store -> fun_ -> t array -> t
val app_fun_l : store -> fun_ -> t list -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val app_undefined : store -> ID.t -> Ty.Fun.t -> t IArray.t -> t
val app_undefined : store -> ID.t -> Ty.Fun.t -> t array -> t
(** [app_undefined store f ty args] is [app store (Fun.mk_undef f ty) args].
It builds a function symbol and applies it into a term immediately *)
@ -910,7 +909,7 @@ module Term : sig
immediately. *)
val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t IArray.t -> t
val app_cstor : store -> cstor -> t array -> t
val is_a : store -> cstor -> t -> t
val lra : store -> t LRA_view.t -> t
val lia : store -> t LIA_view.t -> t
@ -980,7 +979,7 @@ end = struct
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| App_fun of fun_ * 'a array
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
@ -1039,13 +1038,13 @@ end = struct
let cell = Term_cell.app_fun f a in
make st cell
let app_fun_l st f l = app_fun st f (IArray.of_list l)
let[@inline] const st c = app_fun st c IArray.empty
let app_fun_l st f l = app_fun st f (CCArray.of_list l)
let[@inline] const st c = app_fun st c CCArray.empty
let[@inline] eq st a b = make st (Term_cell.eq a b)
let[@inline] not_ st a = make st (Term_cell.not_ a)
let ite st a b c : t = make st (Term_cell.ite a b c)
let select st sel t : t = app_fun st (Fun.select sel) (IArray.singleton t)
let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t)
let select st sel t : t = app_fun st (Fun.select sel) [| t |]
let is_a st c t : t = app_fun st (Fun.is_a c) [| t |]
let app_cstor st c args : t = app_fun st (Fun.cstor c) args
let[@inline] lra (st : store) (l : t LRA_view.t) : t =
@ -1133,7 +1132,7 @@ end = struct
let[@inline] is_const t =
match view t with
| App_fun (_, a) -> IArray.is_empty a
| App_fun (_, [||]) -> true
| _ -> false
let cc_view (t : t) =
@ -1141,7 +1140,7 @@ end = struct
match view t with
| Bool b -> C.Bool b
| App_fun (f, _) when not (Fun.do_cc f) -> C.Opaque t (* skip *)
| App_fun (f, args) -> C.App_fun (f, IArray.to_iter args)
| App_fun (f, args) -> C.App_fun (f, CCArray.to_iter args)
| Eq (a, b) -> C.Eq (a, b)
| Not u -> C.Not u
| Ite (a, b, c) -> C.If (a, b, c)
@ -1169,7 +1168,7 @@ end = struct
(* return [Some] iff the term is an undefined constant *)
let as_fun_undef (t : term) : (fun_ * Ty.Fun.t) option =
match view t with
| App_fun (c, a) when IArray.is_empty a -> Fun.as_undefined c
| App_fun (c, [||]) -> Fun.as_undefined c
| _ -> None
let as_bool t =
@ -1212,7 +1211,7 @@ end = struct
let map_shallow (tst : store) f (t : t) : t =
match view t with
| Bool _ -> t
| App_fun (hd, a) -> app_fun tst hd (IArray.map f a)
| App_fun (hd, a) -> app_fun tst hd (CCArray.map f a)
| Not u -> not_ tst (f u)
| Eq (a, b) -> eq tst (f a) (f b)
| Ite (a, b, c) -> ite tst (f a) (f b) (f c)

31
src/base/Form.ml
View file

@ -21,13 +21,14 @@ let id_imply = ID.make "=>"
let view_id fid args =
if ID.equal fid id_and then
B_and (IArray.to_iter args)
B_and (CCArray.to_iter args)
else if ID.equal fid id_or then
B_or (IArray.to_iter args)
else if ID.equal fid id_imply && IArray.length args >= 2 then (
B_or (CCArray.to_iter args)
else if ID.equal fid id_imply && CCArray.length args >= 2 then (
(* conclusion is stored last *)
let len = IArray.length args in
B_imply (IArray.to_iter_sub args 0 (len - 1), IArray.get args (len - 1))
let len = CCArray.length args in
B_imply
(Iter.of_array args |> Iter.take (len - 1), CCArray.get args (len - 1))
) else
raise_notrace Not_a_th_term
@ -92,7 +93,7 @@ module Funs = struct
let ite = T.ite
end
let as_id id (t : T.t) : T.t IArray.t option =
let as_id id (t : T.t) : T.t array option =
match T.view t with
| App_fun ({ fun_id; _ }, args) when ID.equal id fun_id -> Some args
| _ -> None
@ -102,7 +103,7 @@ let flatten_id op sign (l : T.t list) : T.t list =
CCList.flat_map
(fun t ->
match as_id op t with
| Some args -> IArray.to_list args
| Some args -> CCArray.to_list args
| None when (sign && T.is_true t) || ((not sign) && T.is_false t) ->
[] (* idempotent *)
| None -> [ t ])
@ -113,19 +114,19 @@ let and_l st l =
| [] -> T.true_ st
| l when List.exists T.is_false l -> T.false_ st
| [ x ] -> x
| args -> T.app_fun st Funs.and_ (IArray.of_list args)
| args -> T.app_fun st Funs.and_ (CCArray.of_list args)
let or_l st l =
match flatten_id id_or false l with
| [] -> T.false_ st
| l when List.exists T.is_true l -> T.true_ st
| [ x ] -> x
| args -> T.app_fun st Funs.or_ (IArray.of_list args)
| args -> T.app_fun st Funs.or_ (CCArray.of_list args)
let and_ st a b = and_l st [ a; b ]
let or_ st a b = or_l st [ a; b ]
let and_a st a = and_l st (IArray.to_list a)
let or_a st a = or_l st (IArray.to_list a)
let and_a st a = and_l st (CCArray.to_list a)
let or_a st a = or_l st (CCArray.to_list a)
let eq = T.eq
let not_ = T.not_
@ -155,17 +156,17 @@ let equiv st a b =
let neq st a b = not_ st @@ eq st a b
let imply_a st xs y =
if IArray.is_empty xs then
if Array.length xs = 0 then
y
else
T.app_fun st Funs.imply (IArray.append xs (IArray.singleton y))
T.app_fun st Funs.imply (CCArray.append xs [| y |])
let imply_l st xs y =
match xs with
| [] -> y
| _ -> imply_a st (IArray.of_list xs) y
| _ -> imply_a st (CCArray.of_list xs) y
let imply st a b = imply_a st (IArray.singleton a) b
let imply st a b = imply_a st [| a |] b
let xor st a b = not_ st (equiv st a b)
let distinct_l tst l =

8
src/base/Model.ml
View file

@ -170,12 +170,12 @@ let eval (m : t) (t : Term.t) : Value.t option =
*)
| LIA _l -> assert false (* TODO *)
| App_fun (c, args) ->
(match Fun.view c, (args : _ IArray.t :> _ array) with
(match Fun.view c, (args : _ array :> _ array) with
| Fun_def udef, _ ->
(* use builtin interpretation function *)
let args = IArray.map aux args in
let args = CCArray.map aux args in
udef.eval args
| Fun_cstor c, _ -> Value.cstor_app c (IArray.to_list_map aux args)
| Fun_cstor c, _ -> Value.cstor_app c (Util.array_to_list_map aux args)
| Fun_select s, [| u |] ->
(match aux u with
| V_cstor { c; args } when Cstor.equal c s.select_cstor ->
@ -194,7 +194,7 @@ let eval (m : t) (t : Term.t) : Value.t option =
with Not_found ->
(match Fun.Map.find c m.funs with
| fi ->
let args = IArray.map aux args |> IArray.to_list in
let args = CCArray.map aux args |> CCArray.to_list in
(match Val_map.find args fi.FI.cases with
| None -> fi.FI.default
| Some v -> v)

6
src/base/Proof.ml
View file

@ -151,14 +151,14 @@ let rec emit_term_ (self : t) (t : Term.t) : term_id =
PS.Step_view.Expr_if { PS.Expr_if.cond = a; then_ = b; else_ = c }
| Term_cell.Not a -> PS.Step_view.Expr_not { PS.Expr_not.f = a }
| Term_cell.App_fun ({ fun_view = Fun.Fun_is_a c; _ }, args) ->
assert (IArray.length args = 1);
assert (CCArray.length args = 1);
let c = emit_fun_ self (Fun.cstor c) in
let arg = IArray.get args 0 in
let arg = CCArray.get args 0 in
PS.Step_view.Expr_isa { PS.Expr_isa.c; arg }
| Term_cell.App_fun (f, arr) ->
let f = emit_fun_ self f in
PS.Step_view.Expr_app
{ PS.Expr_app.f; args = (arr : _ IArray.t :> _ array) }
{ PS.Expr_app.f; args = (arr : _ array :> _ array) }
| Term_cell.Eq (a, b) ->
PS.Step_view.Expr_eq { PS.Expr_eq.lhs = a; rhs = b }
| LRA _ | LIA _ -> assert false

2
src/core/Sidekick_core.ml
View file

@ -1279,7 +1279,7 @@ module type SOLVER = sig
The proof of [|- lit = lit'] is directly added to the solver's proof. *)
val add_clause : t -> lit IArray.t -> proof_step -> unit
val add_clause : t -> lit array -> proof_step -> unit
(** [add_clause solver cs] adds a boolean clause to the solver.
Subsequent calls to {!solve} will need to satisfy this clause. *)

2
src/mini-cc/tests/sidekick_test_minicc.ml
View file

@ -24,7 +24,7 @@ module Setup () = struct
let false_ = Term.false_ tst
let const c = Term.const tst c
let app_a f l = Term.app_fun tst f l
let app_l f l = Term.app_fun tst f (IArray.of_list l)
let app_l f l = Term.app_fun tst f (CCArray.of_list l)
let not_ x = Term.not_ tst x
let eq a b = Term.eq tst a b
let neq a b = Term.not_ tst (eq a b)

16
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -508,7 +508,7 @@ module Make (A : ARG) :
[@@inline]
module PC_list = Preprocess_clause (CCList)
module PC_arr = Preprocess_clause (IArray)
module PC_arr = Preprocess_clause (CCArray)
let preprocess_clause_ = PC_list.top
let preprocess_clause_iarray_ = PC_arr.top
@ -966,8 +966,8 @@ module Make (A : ARG) :
let reset_last_res_ self = self.last_res <- None
(* preprocess clause, return new proof *)
let preprocess_clause_ (self : t) (c : lit IArray.t) (pr : proof_step) :
lit IArray.t * proof_step =
let preprocess_clause_ (self : t) (c : lit array) (pr : proof_step) :
lit array * proof_step =
Solver_internal.preprocess_clause_iarray_ self.si c pr
let mk_lit_t (self : t) ?sign (t : term) : lit =
@ -980,18 +980,18 @@ module Make (A : ARG) :
let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self)
(* add [c], without preprocessing its literals *)
let add_clause_nopreproc_ (self : t) (c : lit IArray.t) (proof : proof_step) :
let add_clause_nopreproc_ (self : t) (c : lit array) (proof : proof_step) :
unit =
Stat.incr self.count_clause;
reset_last_res_ self;
Log.debugf 50 (fun k ->
k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Lit.pp) c);
k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c);
let pb = Profile.begin_ "add-clause" in
Sat_solver.add_clause_a self.solver (c :> lit array) proof;
Profile.exit pb
let add_clause_nopreproc_l_ self c p =
add_clause_nopreproc_ self (IArray.of_list c) p
add_clause_nopreproc_ self (CCArray.of_list c) p
module Perform_delayed_ = Solver_internal.Perform_delayed (struct
type nonrec t = t
@ -1003,14 +1003,14 @@ module Make (A : ARG) :
Sat_solver.add_lit solver.solver ?default_pol lit
end)
let add_clause (self : t) (c : lit IArray.t) (proof : proof_step) : unit =
let add_clause (self : t) (c : lit array) (proof : proof_step) : unit =
let c, proof = preprocess_clause_ self c proof in
add_clause_nopreproc_ self c proof;
Perform_delayed_.top self.si self;
(* finish preproc *)
()
let add_clause_l self c p = add_clause self (IArray.of_list c) p
let add_clause_l self c p = add_clause self (CCArray.of_list c) p
let assert_terms self c =
let c = CCList.map (fun t -> Lit.atom (tst self) t) c in

4
src/smtlib/Process.ml
View file

@ -280,7 +280,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
| Statement.Stmt_assert t ->
if pp_cnf then Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t;
let lit = Solver.mk_lit_t solver t in
Solver.add_clause solver (IArray.singleton lit)
Solver.add_clause solver [| lit |]
(Solver.P.emit_input_clause (Iter.singleton lit) (Solver.proof solver));
E.return ()
| Statement.Stmt_assert_clause c_ts ->
@ -297,7 +297,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) proof
in
Solver.add_clause solver (IArray.of_list c) pr;
Solver.add_clause solver (CCArray.of_list c) pr;
E.return ()
| Statement.Stmt_get_model ->
(match Solver.last_res solver with

2
src/smtlib/Typecheck.ml
View file

@ -237,7 +237,7 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t =
| PA.App (f, args) ->
let args = List.map (conv_term ctx) args in
(match find_id_ ctx f with
| _, Ctx.K_fun f -> T.app_fun tst f (IArray.of_list args)
| _, Ctx.K_fun f -> T.app_fun tst f (CCArray.of_list args)
| _, Ctx.K_ty _ ->
errorf_ctx ctx "expected function, got type `%s` instead" f)
| PA.If (a, b, c) ->

18
src/th-bool-dyn/Sidekick_th_bool_dyn.ml
View file

@ -4,9 +4,9 @@
module View = struct
type 'a t =
| B_not of 'a
| B_and of 'a IArray.t
| B_or of 'a IArray.t
| B_imply of 'a IArray.t * 'a
| B_and of 'a array
| B_or of 'a array
| B_imply of 'a array * 'a
| B_atom of 'a
end
@ -58,35 +58,35 @@ struct
| B_and subs ->
if Lit.sign lit then
(* propagate [lit => subs_i] *)
IArray.iter
CCArray.iter
(fun sub ->
let sublit = SI.mk_lit solver sub in
SI.propagate_l solver sublit [ lit ])
subs
else if final && (not @@ expanded ()) then (
(* axiom [¬lit => ∨_i ¬ subs_i] *)
let subs = IArray.to_list subs in
let subs = CCArray.to_list subs in
let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:false) subs in
add_axiom c
)
| B_or subs ->
if not @@ Lit.sign lit then
(* propagate [¬lit => ¬subs_i] *)
IArray.iter
CCArray.iter
(fun sub ->
let sublit = SI.mk_lit solver ~sign:false sub in
SI.add_local_axiom solver [ Lit.neg lit; sublit ])
subs
else if final && (not @@ expanded ()) then (
(* axiom [lit => ∨_i subs_i] *)
let subs = IArray.to_list subs in
let subs = CCArray.to_list subs in
let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:true) subs in
add_axiom c
)
| B_imply (guard, concl) ->
if Lit.sign lit && final && (not @@ expanded ()) then (
(* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
let guard = IArray.to_list guard in
let guard = CCArray.to_list guard in
let c =
SI.mk_lit solver concl :: Lit.neg lit
:: List.map (SI.mk_lit solver ~sign:false) guard
@ -96,7 +96,7 @@ struct
(* propagate [¬lit => ¬concl] *)
SI.propagate_l solver (SI.mk_lit solver ~sign:false concl) [ lit ];
(* propagate [¬lit => ∧_i guard_i] *)
IArray.iter
CCArray.iter
(fun sub ->
let sublit = SI.mk_lit solver ~sign:true sub in
SI.propagate_l solver sublit [ lit ])

2
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -50,7 +50,7 @@ module type ARG = sig
val view_as_bool : term -> (term, term Iter.t) bool_view
(** Project the term into the boolean view. *)
val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term
val mk_bool : S.T.Term.store -> (term, term array) bool_view -> term
(** Make a term from the given boolean view. *)
include

10
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -1,6 +1,6 @@
(** {1 Theory for constructors} *)
type ('c, 't) cstor_view = T_cstor of 'c * 't IArray.t | T_other of 't
type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't
let name = "th-cstor"
@ -29,7 +29,7 @@ module Make (A : ARG) : S with module A = A = struct
module SI = SI
(* associate to each class a unique constructor term in the class (if any) *)
type t = { t: T.t; n: N.t; cstor: Fun.t; args: N.t IArray.t }
type t = { t: T.t; n: N.t; cstor: Fun.t; args: N.t array }
let name = name
@ -40,7 +40,7 @@ module Make (A : ARG) : S with module A = A = struct
let of_term cc n (t : T.t) : _ option * _ =
match A.view_as_cstor t with
| T_cstor (cstor, args) ->
let args = IArray.map (SI.CC.add_term cc) args in
let args = CCArray.map (SI.CC.add_term cc) args in
Some { n; t; cstor; args }, []
| _ -> None, []
@ -57,8 +57,8 @@ module Make (A : ARG) : S with module A = A = struct
in
if Fun.equal v1.cstor v2.cstor then (
(* same function: injectivity *)
assert (IArray.length v1.args = IArray.length v2.args);
IArray.iter2 (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) v1.args v2.args;
assert (CCArray.length v1.args = CCArray.length v2.args);
CCArray.iter2 (fun u1 u2 -> SI.CC.merge cc u1 u2 expl) v1.args v2.args;
Ok v1
) else
(* different function: disjointness *)

31
src/th-data/Sidekick_th_data.ml
View file

@ -172,17 +172,17 @@ module Make (A : ARG) : S with module A = A = struct
let name = "th-data.cstor"
(* associate to each class a unique constructor term in the class (if any) *)
type t = { c_n: N.t; c_cstor: A.Cstor.t; c_args: N.t IArray.t }
type t = { c_n: N.t; c_cstor: A.Cstor.t; c_args: N.t array }
let pp out (v : t) =
Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@ :args [@[%a@]]@])" name
A.Cstor.pp v.c_cstor N.pp v.c_n (Util.pp_iarray N.pp) v.c_args
A.Cstor.pp v.c_cstor N.pp v.c_n (Util.pp_array N.pp) v.c_args
(* attach data to constructor terms *)
let of_term cc n (t : T.t) : _ option * _ list =
match A.view_as_data t with
| T_cstor (cstor, args) ->
let args = IArray.map (SI.CC.add_term cc) args in
let args = CCArray.map (SI.CC.add_term cc) args in
Some { c_n = n; c_cstor = cstor; c_args = args }, []
| _ -> None, []
@ -209,10 +209,9 @@ module Make (A : ARG) : S with module A = A = struct
mk_expl t1 t2 @@ A.P.lemma_cstor_inj t1 t2 i (SI.CC.proof cc)
in
assert (IArray.length c1.c_args = IArray.length c2.c_args);
IArray.iteri2
(fun i u1 u2 -> SI.CC.merge cc u1 u2 (expl_merge i))
c1.c_args c2.c_args;
assert (CCArray.length c1.c_args = CCArray.length c2.c_args);
Util.array_iteri2 c1.c_args c2.c_args ~f:(fun i u1 u2 ->
SI.CC.merge cc u1 u2 (expl_merge i));
Ok c1
) else (
(* different function: disjointness *)
@ -342,7 +341,7 @@ module Make (A : ARG) : S with module A = A = struct
let sel_args =
A.Cstor.ty_args cstor
|> Iter.mapi (fun i ty -> A.mk_sel self.tst cstor i t)
|> Iter.to_array |> IArray.of_array_unsafe
|> Iter.to_array
in
A.mk_cstor self.tst cstor sel_args
in
@ -421,8 +420,8 @@ module Make (A : ARG) : S with module A = A = struct
Log.debugf 5 (fun k ->
k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" name
N.pp n i A.Cstor.pp c_t);
assert (i < IArray.length cstor.c_args);
let u_i = IArray.get cstor.c_args i in
assert (i < CCArray.length cstor.c_args);
let u_i = CCArray.get cstor.c_args i in
let pr =
A.P.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc)
in
@ -473,12 +472,12 @@ module Make (A : ARG) : S with module A = A = struct
Log.debugf 5 (fun k ->
k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name
N.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
assert (sel2.sel_idx < IArray.length c1.c_args);
assert (sel2.sel_idx < CCArray.length c1.c_args);
let pr =
A.P.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n)
self.proof
in
let u_i = IArray.get c1.c_args sel2.sel_idx in
let u_i = CCArray.get c1.c_args sel2.sel_idx in
SI.CC.merge cc sel2.sel_n u_i
(Expl.mk_theory (N.term sel2.sel_n) (N.term u_i)
[
@ -545,7 +544,7 @@ module Make (A : ARG) : S with module A = A = struct
let mk_graph (self : t) cc : graph =
let g : graph = N_tbl.create ~size:32 () in
let traverse_sub cstor : _ list =
IArray.to_list_map
Util.array_to_list_map
(fun sub_n -> sub_n, SI.CC.find cc sub_n)
cstor.Monoid_cstor.c_args
in
@ -625,7 +624,7 @@ module Make (A : ARG) : S with module A = A = struct
let args =
A.Cstor.ty_args c
|> Iter.mapi (fun i _ty -> A.mk_sel self.tst c i u)
|> Iter.to_list |> IArray.of_list
|> Iter.to_list |> CCArray.of_list
in
A.mk_cstor self.tst c args
in
@ -725,7 +724,7 @@ module Make (A : ARG) : S with module A = A = struct
let args =
A.Cstor.ty_args base_cstor
|> Iter.mapi (fun i _ -> A.mk_sel self.tst base_cstor i t)
|> IArray.of_iter
|> Iter.to_array
in
A.mk_cstor self.tst base_cstor args
in
@ -746,7 +745,7 @@ module Make (A : ARG) : S with module A = A = struct
| Some c ->
Log.debugf 5 (fun k ->
k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c);
let args = IArray.map (recurse si) c.c_args in
let args = CCArray.map (recurse si) c.c_args in
let t = A.mk_cstor self.tst c.c_cstor args in
Some t

4
src/th-data/th_intf.ml
View file

@ -4,7 +4,7 @@
- ['t] is the representation of terms
*)
type ('c, 't) data_view =
| T_cstor of 'c * 't IArray.t
| T_cstor of 'c * 't array
| T_select of 'c * int * 't
| T_is_a of 'c * 't
| T_other of 't
@ -82,7 +82,7 @@ module type ARG = sig
val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
(** Try to view term as a datatype term *)
val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t array -> S.T.Term.t
(** Make a constructor application term *)
val mk_is_a : S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t

10
src/th-data/types.ml
View file

@ -11,8 +11,8 @@ and datatype = {
(* a constructor *)
and data_cstor = {
cstor_ty: ty;
cstor_args: ty IArray.t; (* argument types *)
cstor_proj: cst IArray.t lazy_t; (* projectors *)
cstor_args: ty array; (* argument types *)
cstor_proj: cst array lazy_t; (* projectors *)
cstor_test: cst lazy_t; (* tester *)
cstor_cst: cst; (* the cstor itself *)
cstor_card: ty_card; (* cardinality of the constructor('s args) *)
@ -43,10 +43,10 @@ let if_ a b c =
If (a,b,c)
let cstor_test cstor t =
app_cst (Lazy.force cstor.cstor_test) (IArray.singleton t)
app_cst (Lazy.force cstor.cstor_test) (CCArray.singleton t)
let cstor_proj cstor i t =
let p = IArray.get (Lazy.force cstor.cstor_proj) i in
app_cst p (IArray.singleton t)
let p = CCArray.get (Lazy.force cstor.cstor_proj) i in
app_cst p (CCArray.singleton t)
*)

4
src/util/Bitvec.ml
View file

@ -1,7 +1,7 @@
type t = { mutable chunks: bytes (* TODO: use a in32vec with bigarray *) }
type t = { mutable chunks: bytes }
let create () : t = { chunks = Bytes.make 32 '\x00' }
let i2c = Char.chr
let i2c = Char.unsafe_chr
let c2i = Char.code
(* from index to offset in bytes *)

5
src/util/Bitvec.mli
View file

@ -1,4 +1,7 @@
(** Bitvector *)
(** Bitvector.
This provides compact storage with O(1) access to a range of bits,
like [bool Vec.t] but packed better. *)
type t

2
src/util/Hash.ml
View file

@ -77,7 +77,7 @@ let bool b =
let list f l = List.fold_left (combine f) 0x42 l
let array f = Array.fold_left (combine f) 0x43
let iarray f = IArray.fold (combine f) 0x44
let iarray f = CCArray.fold (combine f) 0x44
let string : string t = Hashtbl.hash
let seq f seq =

2
src/util/Hash.mli
View file

@ -10,7 +10,7 @@ val pair : 'a t -> 'b t -> ('a * 'b) t
val opt : 'a t -> 'a option t
val list : 'a t -> 'a list t
val array : 'a t -> 'a array t
val iarray : 'a t -> 'a IArray.t t
val iarray : 'a t -> 'a array t
val seq : 'a t -> 'a Iter.t t
val combine2 : int -> int -> int
val combine3 : int -> int -> int -> int

175
src/util/IArray.ml
View file

@ -1,175 +0,0 @@
(* This file is free software. See file "license" for more details. *)
type 'a t = 'a array
let empty = [||]
let is_empty a = Array.length a = 0
let length = Array.length
let singleton x = [| x |]
let doubleton x y = [| x; y |]
let make n x = Array.make n x
let init n f = Array.init n f
let sub = Array.sub
let get = Array.get
let unsafe_get = Array.unsafe_get
let set a n x =
let a' = Array.copy a in
a'.(n) <- x;
a'
let map = Array.map
let mapi = Array.mapi
let append a b =
let na = length a in
Array.init
(na + length b)
(fun i ->
if i < na then
a.(i)
else
b.(i - na))
let iter = Array.iter
let iteri = Array.iteri
let fold = Array.fold_left
let foldi f acc a =
let n = ref 0 in
Array.fold_left
(fun acc x ->
let acc = f acc !n x in
incr n;
acc)
acc a
exception ExitNow
let for_all p a =
try
Array.iter (fun x -> if not (p x) then raise ExitNow) a;
true
with ExitNow -> false
let exists p a =
try
Array.iter (fun x -> if p x then raise ExitNow) a;
false
with ExitNow -> true
(** {2 Conversions} *)
type 'a iter = ('a -> unit) -> unit
type 'a gen = unit -> 'a option
let of_list = Array.of_list
let to_list = Array.to_list
let of_list_map f l =
match l with
| [] -> empty
| x :: _ ->
let arr = make (List.length l) (f x) in
List.iteri (fun i x -> Array.unsafe_set arr i (f x)) l;
arr
let to_list_map f a = CCArray.fold_right (fun x acc -> f x :: acc) a []
let of_array_map = Array.map
let to_array_map = Array.map
let of_array_unsafe a = a (* careful with that axe, Eugene *)
let to_iter a k = iter k a
let to_iter_sub a i len k =
if i < 0 || i + len > Array.length a then invalid_arg "IArray.iter_sub";
for j = i to i + len - 1 do
k (Array.unsafe_get a j)
done
let of_iter s =
let l = ref [] in
s (fun x -> l := x :: !l);
Array.of_list (List.rev !l)
(*$Q
Q.(list int) (fun l -> \
let g = Iter.of_list l in \
of_iter g |> to_iter |> Iter.to_list = l)
*)
let rec gen_to_list_ acc g =
match g () with
| None -> List.rev acc
| Some x -> gen_to_list_ (x :: acc) g
let of_gen g =
let l = gen_to_list_ [] g in
Array.of_list l
let to_gen a =
let i = ref 0 in
fun () ->
if !i < Array.length a then (
let x = a.(!i) in
incr i;
Some x
) else
None
(*$Q
Q.(list int) (fun l -> \
let g = Gen.of_list l in \
of_gen g |> to_gen |> Gen.to_list = l)
*)
(** {2 IO} *)
type 'a printer = Format.formatter -> 'a -> unit
let print ?(start = "[|") ?(stop = "|]") ?(sep = ";") pp_item out a =
Format.pp_print_string out start;
for k = 0 to Array.length a - 1 do
if k > 0 then (
Format.pp_print_string out sep;
Format.pp_print_cut out ()
);
pp_item out a.(k)
done;
Format.pp_print_string out stop;
()
(** {2 Binary} *)
let equal = CCArray.equal
let compare = CCArray.compare
let for_all2 = CCArray.for_all2
let exists2 = CCArray.exists2
let map2 f a b =
if length a <> length b then invalid_arg "map2";
init (length a) (fun i -> f (unsafe_get a i) (unsafe_get b i))
let iter2 f a b =
if length a <> length b then invalid_arg "iter2";
for i = 0 to length a - 1 do
f (unsafe_get a i) (unsafe_get b i)
done
let iteri2 f a b =
if length a <> length b then invalid_arg "iteri2";
for i = 0 to length a - 1 do
f i (unsafe_get a i) (unsafe_get b i)
done
let fold2 f acc a b =
if length a <> length b then invalid_arg "fold2";
let rec aux acc i =
if i = length a then
acc
else (
let acc = f acc (unsafe_get a i) (unsafe_get b i) in
aux acc (i + 1)
)
in
aux acc 0

80
src/util/IArray.mli
View file

@ -1,80 +0,0 @@
(* This file is free software. See file "license" for more details. *)
type 'a t = private 'a array
(** Array of values of type 'a. The underlying type really is
an array, but it will never be modified.
It should be covariant but OCaml will not accept it. *)
val empty : 'a t
val is_empty : _ t -> bool
val length : _ t -> int
val sub : 'a t -> int -> int -> 'a t
val singleton : 'a -> 'a t
val doubleton : 'a -> 'a -> 'a t
val make : int -> 'a -> 'a t
(** [make n x] makes an array of [n] times [x] *)
val init : int -> (int -> 'a) -> 'a t
(** [init n f] makes the array [[| f 0; f 1; ... ; f (n-1) |]].
@raise Invalid_argument if [n < 0] *)
val get : 'a t -> int -> 'a
(** Access the element *)
val unsafe_get : 'a t -> int -> 'a
(** Unsafe access, not bound-checked. Use with caution *)
val set : 'a t -> int -> 'a -> 'a t
(** Copy the array and modify its copy *)
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t
val append : 'a t -> 'a t -> 'a t
val iter : ('a -> unit) -> 'a t -> unit
val iteri : (int -> 'a -> unit) -> 'a t -> unit
val foldi : ('a -> int -> 'b -> 'a) -> 'a -> 'b t -> 'a
val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
val for_all : ('a -> bool) -> 'a t -> bool
val exists : ('a -> bool) -> 'a t -> bool
(** {2 Conversions} *)
type 'a iter = ('a -> unit) -> unit
type 'a gen = unit -> 'a option
val of_list : 'a list -> 'a t
val to_list : 'a t -> 'a list
val of_list_map : ('a -> 'b) -> 'a list -> 'b t
val to_list_map : ('a -> 'b) -> 'a t -> 'b list
val of_array_map : ('a -> 'b) -> 'a array -> 'b t
val to_array_map : ('a -> 'b) -> 'a t -> 'b array
val of_array_unsafe : 'a array -> 'a t
(** Take ownership of the given array. Careful, the array must {b NOT}
be modified afterwards! *)
val to_iter : 'a t -> 'a iter
val to_iter_sub : 'a t -> int -> int -> 'a iter
val of_iter : 'a iter -> 'a t
val of_gen : 'a gen -> 'a t
val to_gen : 'a t -> 'a gen
(** {2 IO} *)
type 'a printer = Format.formatter -> 'a -> unit
val print :
?start:string -> ?stop:string -> ?sep:string -> 'a printer -> 'a t printer
(** {2 Binary} *)
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val for_all2 : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val exists2 : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val fold2 : ('acc -> 'a -> 'b -> 'acc) -> 'acc -> 'a t -> 'b t -> 'acc
val iteri2 : (int -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
val iter2 : ('a -> 'b -> unit) -> 'a t -> 'b t -> unit

3
src/util/Int_id.ml
View file

@ -1,3 +1,5 @@
(** Integer-based identifiers. *)
module type S = sig
type t = private int
@ -8,6 +10,7 @@ module type S = sig
val of_int_unsafe : int -> t
end
(** Generate a new type for integer identifiers *)
module Make () = struct
type t = int

6
src/util/Profile.mli
View file

@ -1,4 +1,8 @@
(** {1 Profiling probes} *)
(** Profiling probes.
This basic library can produce Catapult traces (a json file)
that can be read at [http://ui.perfetto.dev].
*)
type probe

11
src/util/Util.ml
View file

@ -14,11 +14,14 @@ let pp_pair ?(sep = " ") pp1 pp2 out t =
Fmt.pair ~sep:(pp_sep sep) pp1 pp2 out t
let pp_array ?(sep = " ") pp out l = Fmt.array ~sep:(pp_sep sep) pp out l
let flat_map_l_arr f l = CCList.flat_map (fun x -> CCArray.to_list @@ f x) l
let pp_iarray ?(sep = " ") pp out a =
Fmt.iter ~sep:(pp_sep sep) pp out (IArray.to_iter a)
let flat_map_l_ia f l = CCList.flat_map (fun x -> IArray.to_list @@ f x) l
let array_iteri2 ~f a b =
let open Array in
if length a <> length b then invalid_arg "iteri2";
for i = 0 to length a - 1 do
f i (unsafe_get a i) (unsafe_get b i)
done
let array_of_list_map f l =
match l with

7
src/util/Util.mli
View file

@ -8,11 +8,7 @@ val pp_list : ?sep:string -> 'a printer -> 'a list printer
val pp_iter : ?sep:string -> 'a printer -> 'a Iter.t printer
val pp_array : ?sep:string -> 'a printer -> 'a array printer
val pp_pair : ?sep:string -> 'a printer -> 'b printer -> ('a * 'b) printer
val pp_iarray :
?sep:string -> 'a CCFormat.printer -> 'a IArray.t CCFormat.printer
val flat_map_l_ia : ('a -> 'b IArray.t) -> 'a list -> 'b list
val flat_map_l_arr : ('a -> 'b array) -> 'a list -> 'b list
val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
(** [array_of_list_map f l] is the same as [Array.of_list @@ List.map f l] *)
@ -20,6 +16,7 @@ val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
val lazy_map : ('a -> 'b) -> 'a lazy_t -> 'b lazy_t
val lazy_map2 : ('a -> 'b -> 'c) -> 'a lazy_t -> 'b lazy_t -> 'c lazy_t
val array_iteri2 : f:(int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
val setup_gc : unit -> unit
(** Change parameters of the GC *)

4
src/util/Vec_unit.mli
View file

@ -1 +1,5 @@
(** Fake vector of unit.
This just retains the size, as 0 bits of actual storage are required. *)
include Vec_sig.S with type elt = unit