From 0d31d9d84ea71c20d461683ee61f20aef6725fba Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 17 Mar 2021 18:29:39 -0400 Subject: [PATCH] refactor(th-bool): parametrize bool_view by type of lists use iterator instead of a IArray.t on the view side --- src/smtlib/Form.ml | 20 +++++------ src/th-bool-static/Sidekick_th_bool_static.ml | 35 ++++++++++--------- src/util/IArray.ml | 5 +++ src/util/IArray.mli | 2 ++ 4 files changed, 36 insertions(+), 26 deletions(-) diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml index 60b8bebf..76faabc4 100644 --- a/src/smtlib/Form.ml +++ b/src/smtlib/Form.ml @@ -10,18 +10,18 @@ let id_imply = ID.make "=>" let view_id fid args = if ID.equal fid id_and then ( - B_and args + B_and (IArray.to_iter args) ) else if ID.equal fid id_or then ( - B_or args + B_or (IArray.to_iter args) ) else if ID.equal fid id_imply && IArray.length args >= 2 then ( (* conclusion is stored first *) let len = IArray.length args in - B_imply (IArray.sub args 1 (len-1), IArray.get args 0) + B_imply (IArray.to_iter_sub args 1 (len-1), IArray.get args 0) ) else ( raise_notrace Not_a_th_term ) -let view_as_bool (t:T.t) : T.t bool_view = +let view_as_bool (t:T.t) : (T.t, _) bool_view = match T.view t with | Bool b -> B_bool b | Not u -> B_not u @@ -47,13 +47,13 @@ module Funs = struct match view_id id args with | B_bool b -> Value.bool b | B_not (V_bool b) -> Value.bool (not b) - | B_and a when IArray.for_all Value.is_true a -> Value.true_ - | B_and a when IArray.exists Value.is_false a -> Value.false_ - | B_or a when IArray.exists Value.is_true a -> Value.true_ - | B_or a when IArray.for_all Value.is_false a -> Value.false_ + | B_and a when Iter.for_all Value.is_true a -> Value.true_ + | B_and a when Iter.exists Value.is_false a -> Value.false_ + | B_or a when Iter.exists Value.is_true a -> Value.true_ + | B_or a when Iter.for_all Value.is_false a -> Value.false_ | B_imply (_, V_bool true) -> Value.true_ - | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_ - | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_ + | B_imply (a,_) when Iter.exists Value.is_false a -> Value.true_ + | B_imply (a,b) when Iter.for_all Value.is_bool a && Value.is_bool b -> Value.false_ | B_ite(a,b,c) -> if Value.is_true a then b else if Value.is_false a then c diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 861a1326..e89a7c26 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -1,11 +1,11 @@ (** {2 Signatures for booleans} *) -type 'a bool_view = +type ('a, 'args) bool_view = | B_bool of bool | 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 'args + | B_or of 'args + | B_imply of 'args * 'a | B_equiv of 'a * 'a | B_eq of 'a * 'a | B_ite of 'a * 'a * 'a @@ -17,10 +17,10 @@ module type ARG = sig type term = S.T.Term.t - val view_as_bool : term -> term bool_view + val view_as_bool : term -> (term, term Iter.t) bool_view (** Project the term into the boolean view *) - val mk_bool : S.T.Term.state -> term bool_view -> term + val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term (** Make a term from the given boolean view *) val check_congruence_classes : bool @@ -95,18 +95,19 @@ module Make(A : ARG) : S with module A = A = struct | B_not _ -> None | B_opaque_bool _ -> None | B_and a -> - if IArray.exists is_false a then Some (T.bool tst false) - else if IArray.for_all is_true a then Some (T.bool tst true) + if Iter.exists is_false a then Some (T.bool tst false) + else if Iter.for_all is_true a then Some (T.bool tst true) else None | B_or a -> - if IArray.exists is_true a then Some (T.bool tst true) - else if IArray.for_all is_false a then Some (T.bool tst false) + if Iter.exists is_true a then Some (T.bool tst true) + else if Iter.for_all is_false a then Some (T.bool tst false) else None | B_imply (args, u) -> (* turn into a disjunction *) let u = - or_a tst @@ - IArray.append (IArray.map (not_ tst) args) (IArray.singleton u) + let args = + args |> Iter.map (not_ tst) |> IArray.of_iter in + or_a tst @@ IArray.append args (IArray.singleton u) in Some u | B_ite (a,b,c) -> @@ -176,14 +177,14 @@ module Make(A : ARG) : S with module A = A = struct let lit = get_lit u in Lit.neg lit | B_and l -> - let subs = IArray.to_list_map get_lit l in + let subs = l |> Iter.map get_lit |> Iter.to_list in let proxy = fresh_lit ~mk_lit ~pre:"and_" self in (* add clauses *) List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs; add_clause (proxy :: List.map Lit.neg subs); proxy | B_or l -> - let subs = IArray.to_list_map get_lit l in + let subs = l |> Iter.map get_lit |> Iter.to_list in let proxy = fresh_lit ~mk_lit ~pre:"or_" self in (* add clauses *) List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs; @@ -191,8 +192,10 @@ module Make(A : ARG) : S with module A = A = struct proxy | B_imply (args, u) -> let t' = - or_a self.tst @@ - IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in + let args = + args |> Iter.map (not_ self.tst) |> IArray.of_iter + in + or_a self.tst @@ IArray.append args (IArray.singleton u) in get_lit t' | B_ite _ | B_eq _ -> mk_lit t | B_equiv (a,b) -> diff --git a/src/util/IArray.ml b/src/util/IArray.ml index 9c898e2d..8884da4d 100644 --- a/src/util/IArray.ml +++ b/src/util/IArray.ml @@ -92,6 +92,11 @@ 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 diff --git a/src/util/IArray.mli b/src/util/IArray.mli index 64145f67..8aff9543 100644 --- a/src/util/IArray.mli +++ b/src/util/IArray.mli @@ -76,6 +76,8 @@ val of_array_unsafe : 'a array -> 'a t 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