diff --git a/sidekick.opam b/sidekick.opam index 9659bf9d..bb62b9b1 100644 --- a/sidekick.opam +++ b/sidekick.opam @@ -13,7 +13,7 @@ build: [ depends: [ "dune" {build} "containers" - "sequence" + "iter" "zarith" "menhir" "msat" { >= "0.8" < "0.9" } diff --git a/src/cc/CC_types.ml b/src/cc/CC_types.ml index f0ff2363..2b75cd7d 100644 --- a/src/cc/CC_types.ml +++ b/src/cc/CC_types.ml @@ -49,7 +49,7 @@ module type TERM = sig val bool : state -> bool -> t (** View the term through the lens of the congruence closure *) - val cc_view : t -> (Fun.t, t, t Sequence.t) view + val cc_view : t -> (Fun.t, t, t Iter.t) view end end diff --git a/src/cc/Congruence_closure.ml b/src/cc/Congruence_closure.ml index 5a12f6fb..33ddee83 100644 --- a/src/cc/Congruence_closure.ml +++ b/src/cc/Congruence_closure.ml @@ -206,7 +206,7 @@ module Make(A: ARG) = struct let[@inline] is_root (n:node) : bool = n.n_root == n (* traverse the equivalence class of [n] *) - let iter_class_ (n:node) : node Sequence.t = + let iter_class_ (n:node) : node Iter.t = fun yield -> let rec aux u = yield u; @@ -218,7 +218,7 @@ module Make(A: ARG) = struct assert (is_root n); iter_class_ n - let[@inline] iter_parents (n:node) : node Sequence.t = + let[@inline] iter_parents (n:node) : node Iter.t = assert (is_root n); Bag.to_seq n.n_parents @@ -461,9 +461,9 @@ module Make(A: ARG) = struct let c = List.rev_map A.Lit.neg e in acts.Msat.acts_raise_conflict c A.Proof.default - let[@inline] all_classes cc : repr Sequence.t = + let[@inline] all_classes cc : repr Iter.t = T_tbl.values cc.tbl - |> Sequence.filter N.is_root + |> Iter.filter N.is_root (* TODO: use markers and lockstep iteration instead *) (* distance from [t] to its root in the proof forest *) @@ -634,12 +634,12 @@ module Make(A: ARG) = struct return @@ Eq (a,b) | Not u -> return @@ Not (deref_sub u) | App_fun (f, args) -> - let args = args |> Sequence.map deref_sub |> Sequence.to_list in + let args = args |> Iter.map deref_sub |> Iter.to_list in if args<>[] then ( return @@ App_fun (f, args) ) else None | App_ho (f, args) -> - let args = args |> Sequence.map deref_sub |> Sequence.to_list in + let args = args |> Iter.map deref_sub |> Iter.to_list in return @@ App_ho (deref_sub f, args) | If (a,b,c) -> return @@ If (deref_sub a, deref_sub b, deref_sub c) @@ -987,7 +987,7 @@ module Make(A: ARG) = struct end let[@inline] assert_lits cc lits : unit = - Sequence.iter (assert_lit cc) lits + Iter.iter (assert_lit cc) lits let assert_eq cc t1 t2 (e:lit list) : unit = let expl = Expl.mk_list @@ List.rev_map Expl.mk_lit e in @@ -1052,7 +1052,7 @@ module Make(A: ARG) = struct (* find a value in the class, if any *) let v = N.iter_class r - |> Sequence.find_map (fun n -> Model.eval m n.n_term) + |> Iter.find_map (fun n -> Model.eval m n.n_term) in let v = match v with | Some v -> v @@ -1066,7 +1066,7 @@ module Make(A: ARG) = struct (* now map every term to its representative's value *) let pairs = T_tbl.values cc.tbl - |> Sequence.map + |> Iter.map (fun n -> let r = find_ n in let v = @@ -1076,7 +1076,7 @@ module Make(A: ARG) = struct in n.n_term, v) in - let m = Sequence.fold (fun m (t,v) -> Model.add t v m) m pairs in + let m = Iter.fold (fun m (t,v) -> Model.add t v m) m pairs in Log.debugf 5 (fun k->k "(@[cc.model@ %a@])" Model.pp m); m end diff --git a/src/cc/Congruence_closure_intf.ml b/src/cc/Congruence_closure_intf.ml index aa99fc96..dc444544 100644 --- a/src/cc/Congruence_closure_intf.ml +++ b/src/cc/Congruence_closure_intf.ml @@ -73,11 +73,11 @@ module type S = sig val is_root : t -> bool (** Is the node a root (ie the representative of its class)? *) - val iter_class : t -> t Sequence.t + val iter_class : t -> t Iter.t (** Traverse the congruence class. Invariant: [is_root n] (see {!find} below) *) - val iter_parents : t -> t Sequence.t + val iter_parents : t -> t Iter.t (** Traverse the parents of the class. Invariant: [is_root n] (see {!find} below) *) end @@ -173,10 +173,10 @@ module type S = sig (** Current representative of the term. @raise Not_found if the term is not already {!add}-ed. *) - val add_seq : t -> term Sequence.t -> unit + val add_seq : t -> term Iter.t -> unit (** Add a sequence of terms to the congruence closure *) - val all_classes : t -> repr Sequence.t + val all_classes : t -> repr Iter.t (** All current classes. This is costly, only use if there is no other solution *) val assert_lit : t -> lit -> unit @@ -185,7 +185,7 @@ module type S = sig Useful for the theory combination or the SAT solver's functor *) - val assert_lits : t -> lit Sequence.t -> unit + val assert_lits : t -> lit Iter.t -> unit (** Addition of many literals *) val assert_eq : t -> term -> term -> lit list -> unit diff --git a/src/cc/Mini_cc.ml b/src/cc/Mini_cc.ml index c7ab15b5..f968ba07 100644 --- a/src/cc/Mini_cc.ml +++ b/src/cc/Mini_cc.ml @@ -183,8 +183,8 @@ module Make(A: TERM) = struct (* does this list contain a duplicate? *) let has_dups (l:node list) : bool = - Sequence.diagonal (Sequence.of_list l) - |> Sequence.exists (fun (n1,n2) -> Node.equal n1 n2) + Iter.diagonal (Iter.of_list l) + |> Iter.exists (fun (n1,n2) -> Node.equal n1 n2) exception E_unsat @@ -205,12 +205,12 @@ module Make(A: TERM) = struct return @@ Eq (a,b) | Not u -> return @@ Not (find_t_ self u) | App_fun (f, args) -> - let args = args |> Sequence.map (find_t_ self) |> Sequence.to_list in + let args = args |> Iter.map (find_t_ self) |> Iter.to_list in if args<>[] then ( return @@ App_fun (f, args) ) else None | App_ho (f, args) -> - let args = args |> Sequence.map (find_t_ self) |> Sequence.to_list in + let args = args |> Iter.map (find_t_ self) |> Iter.to_list in return @@ App_ho (find_t_ self f, args) | If (a,b,c) -> return @@ If(find_t_ self a, find_t_ self b, find_t_ self c) diff --git a/src/cc/dune b/src/cc/dune index 9c089050..0fa44a8f 100644 --- a/src/cc/dune +++ b/src/cc/dune @@ -3,7 +3,7 @@ (library (name Sidekick_cc) (public_name sidekick.cc) - (libraries containers containers.data msat sequence sidekick.util) + (libraries containers containers.data msat iter sidekick.util) (flags :standard -warn-error -a+8 -color always -safe-string -short-paths -open Sidekick_util) (ocamlopt_flags :standard -O3 -color always diff --git a/src/main/dune b/src/main/dune index 948a0873..8d9cf100 100644 --- a/src/main/dune +++ b/src/main/dune @@ -4,7 +4,7 @@ (name main) (public_name sidekick) (package sidekick) - (libraries containers sequence result msat sidekick.smt sidekick.smtlib + (libraries containers iter result msat sidekick.smt sidekick.smtlib sidekick.smt.th-ite sidekick.dimacs) (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always -open Sidekick_util) diff --git a/src/smt/Ast.ml b/src/smt/Ast.ml index 55f3731f..db9f3470 100644 --- a/src/smt/Ast.ml +++ b/src/smt/Ast.ml @@ -487,7 +487,7 @@ let env_add_statement env st = -> env let env_of_statements seq = - Sequence.fold env_add_statement env_empty seq + Iter.fold env_add_statement env_empty seq let env_find_def env id = try Some (ID.Map.find id env.defs) diff --git a/src/smt/Ast.mli b/src/smt/Ast.mli index 778671d3..4d61162d 100644 --- a/src/smt/Ast.mli +++ b/src/smt/Ast.mli @@ -208,7 +208,7 @@ val env_empty : env val env_add_statement : env -> statement -> env -val env_of_statements: statement Sequence.t -> env +val env_of_statements: statement Iter.t -> env val env_find_def : env -> ID.t -> env_entry option diff --git a/src/smt/Hash.mli b/src/smt/Hash.mli index 5e5a1dd2..bed155ca 100644 --- a/src/smt/Hash.mli +++ b/src/smt/Hash.mli @@ -14,7 +14,7 @@ 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 seq : 'a t -> 'a Sequence.t t +val seq : 'a t -> 'a Iter.t t val combine2 : int -> int -> int val combine3 : int -> int -> int -> int diff --git a/src/smt/Hashcons.ml b/src/smt/Hashcons.ml index 44a9fa66..ec9fa59c 100644 --- a/src/smt/Hashcons.ml +++ b/src/smt/Hashcons.ml @@ -10,7 +10,7 @@ module Make(A : ARG): sig type t val create : ?size:int -> unit -> t val hashcons : t -> A.t -> A.t - val to_seq : t -> A.t Sequence.t + val to_seq : t -> A.t Iter.t end = struct module W = Weak.Make(A) diff --git a/src/smt/Model.ml b/src/smt/Model.ml index 1c97ab05..791b26a6 100644 --- a/src/smt/Model.ml +++ b/src/smt/Model.ml @@ -41,7 +41,7 @@ module Fun_interpretation = struct } let default fi = fi.default - let cases_list fi = Val_map.to_seq fi.cases |> Sequence.to_rev_list + let cases_list fi = Val_map.to_seq fi.cases |> Iter.to_rev_list let make ~default l : t = let m = List.fold_left (fun m (k,v) -> Val_map.add k v m) Val_map.empty l in diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index f190107c..0a50d2b0 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -72,7 +72,7 @@ let flush_progress (): unit = module Top_goals: sig val push : term -> unit - val to_seq : term Sequence.t + val to_seq : term Iter.t val check: unit -> unit end = struct (* list of terms to fully evaluate *) @@ -147,9 +147,9 @@ type res = (** {2 Main} *) (* convert unsat-core *) -let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Sequence.t = - Sequence.of_list core - |> Sequence.map clause_of_mclause +let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t = + Iter.of_list core + |> Iter.map clause_of_mclause (* print all terms reachable from watched literals *) let pp_term_graph _out (_:t) = @@ -173,12 +173,12 @@ let do_on_exit ~on_exit = (* map boolean subterms to literals *) let add_bool_subterms_ (self:t) (t:Term.t) : unit = Term.iter_dag t - |> Sequence.filter (fun t -> Ty.is_prop @@ Term.ty t) - |> Sequence.filter + |> Iter.filter (fun t -> Ty.is_prop @@ Term.ty t) + |> Iter.filter (fun t -> match Term.view t with | Term.Not _ -> false (* will process the subterm just later *) | _ -> true) - |> Sequence.iter + |> Iter.iter (fun sub -> Log.debugf 5 (fun k->k "(@[solver.map-to-lit@ :subterm %a@])" Term.pp sub); ignore (mk_atom_t self sub : Sat_solver.atom)) @@ -250,8 +250,8 @@ let solve ?(on_exit=[]) ?(check=true) () = (* assume all literals [expanded t] are false *) let assumptions = Terms_to_expand.to_seq - |> Sequence.map (fun {Terms_to_expand.lit; _} -> Lit.neg lit) - |> Sequence.to_rev_list + |> Iter.map (fun {Terms_to_expand.lit; _} -> Lit.neg lit) + |> Iter.to_rev_list in incr n_iter; Log.debugf 2 diff --git a/src/smt/Term.mli b/src/smt/Term.mli index bd079892..5fefbaf3 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -42,10 +42,10 @@ val abs : state -> t -> t * bool module Iter_dag : sig type t val create : unit -> t - val iter_dag : t -> term -> term Sequence.t + val iter_dag : t -> term -> term Iter.t end -val iter_dag : t -> t Sequence.t +val iter_dag : t -> t Iter.t val pp : t Fmt.printer @@ -55,7 +55,7 @@ val is_true : t -> bool val is_false : t -> bool val is_const : t -> bool -val cc_view : t -> (cst,t,t Sequence.t) Sidekick_cc.view +val cc_view : t -> (cst,t,t Iter.t) Sidekick_cc.view (* return [Some] iff the term is an undefined constant *) val as_cst_undef : t -> (cst * Ty.Fun.t) option diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index 99c9ca89..d387e730 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -66,14 +66,14 @@ module type S = sig val on_merge: t -> actions -> CC_eq_class.t -> CC_eq_class.t -> CC_expl.t -> unit (** Called when two classes are merged *) - val partial_check : t -> actions -> Lit.t Sequence.t -> unit + val partial_check : t -> actions -> Lit.t Iter.t -> unit (** Called when a literal becomes true *) - val final_check: t -> actions -> Lit.t Sequence.t -> unit + val final_check: t -> actions -> Lit.t Iter.t -> unit (** Final check, must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) *) - val mk_model : t -> Lit.t Sequence.t -> Model.t -> Model.t + val mk_model : t -> Lit.t Iter.t -> Model.t -> Model.t (** Make a model for this theory's terms *) val push_level : t -> unit diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index fa7692c4..1cce41b5 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -33,13 +33,13 @@ type t = { let[@inline] cc (t:t) = Lazy.force t.cc let[@inline] tst t = t.tst -let[@inline] theories (self:t) : theory_state Sequence.t = +let[@inline] theories (self:t) : theory_state Iter.t = fun k -> List.iter k self.theories (** {2 Interface with the SAT solver} *) (* handle a literal assumed by the SAT solver *) -let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit = +let assert_lits_ ~final (self:t) acts (lits:Lit.t Iter.t) : unit = Msat.Log.debugf 2 (fun k->k "(@[@{th_combine.assume_lits@}%s@ %a@])" (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits); @@ -69,7 +69,7 @@ let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit = if final then Th.final_check st acts lits else Th.partial_check st acts lits); () -let[@inline] iter_atoms_ acts : _ Sequence.t = +let[@inline] iter_atoms_ acts : _ Iter.t = fun f -> acts.Msat.acts_iter_assumptions (function @@ -80,7 +80,7 @@ let[@inline] iter_atoms_ acts : _ Sequence.t = let check_ ~final (self:t) (acts:_ Msat.acts) = let iter = iter_atoms_ acts in (* TODO if Config.progress then print_progress(); *) - Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Sequence.length iter)); + Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Iter.length iter)); assert_lits_ ~final self acts iter let add_formula (self:t) (lit:Lit.t) = @@ -108,7 +108,7 @@ let pop_levels (self:t) n : unit = let mk_model (self:t) lits : Model.t = let m = - Sequence.fold + Iter.fold (fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m) Model.empty (theories self) in diff --git a/src/smt/Theory_combine.mli b/src/smt/Theory_combine.mli index 8d723954..532f20e2 100644 --- a/src/smt/Theory_combine.mli +++ b/src/smt/Theory_combine.mli @@ -19,9 +19,9 @@ val tst : t -> Term.state type theory_state = | Th_state : ('a Theory.t1 * 'a) -> theory_state -val theories : t -> theory_state Sequence.t +val theories : t -> theory_state Iter.t -val mk_model : t -> Lit.t Sequence.t -> Model.t +val mk_model : t -> Lit.t Iter.t -> Model.t val add_theory : t -> Theory.t -> unit (** How to add new theories *) diff --git a/src/smt/dune b/src/smt/dune index 2f7f98ec..0d2c2890 100644 --- a/src/smt/dune +++ b/src/smt/dune @@ -2,7 +2,7 @@ (library (name Sidekick_smt) (public_name sidekick.smt) - (libraries containers containers.data sequence + (libraries containers containers.data iter sidekick.util sidekick.cc msat zarith) (flags :standard -warn-error -a+8 -color always -safe-string -short-paths -open Sidekick_util) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 8f474c88..66ff2d12 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -506,7 +506,7 @@ end = struct let rhs = conv_term_rec env' rhs in let depends_on_vars = Term.to_seq_depth rhs - |> Sequence.exists + |> Iter.exists (fun (t,k) -> match t.term_cell with | DB db -> DB.level db < n_vars + k (* [k]: number of intermediate binders *) @@ -521,9 +521,9 @@ end = struct (* TODO: do the closedness check during conversion, above *) let rhs_l = ID.Map.values m - |> Sequence.map snd - |> Sequence.sort_uniq ~cmp:Term.compare - |> Sequence.to_rev_list + |> Iter.map snd + |> Iter.sort_uniq ~cmp:Term.compare + |> Iter.to_rev_list in begin match rhs_l with | [x] when not (!any_rhs_depends_vars) -> diff --git a/src/th-bool/Th_dyn_tseitin.ml b/src/th-bool/Th_dyn_tseitin.ml index 9cbc9f2e..a86fe8a2 100644 --- a/src/th-bool/Th_dyn_tseitin.ml +++ b/src/th-bool/Th_dyn_tseitin.ml @@ -86,10 +86,10 @@ module Make(Term : ARG) = struct | B_atom _ -> () | v -> tseitin ~final self acts lit t v) - let partial_check (self:t) acts (lits:Lit.t Sequence.t) = + let partial_check (self:t) acts (lits:Lit.t Iter.t) = check_ ~final:false self acts lits - let final_check (self:t) acts (lits:Lit.t Sequence.t) = + let final_check (self:t) acts (lits:Lit.t Iter.t) = check_ ~final:true self acts lits let th = diff --git a/src/th-distinct/Sidekick_th_distinct.ml b/src/th-distinct/Sidekick_th_distinct.ml index 2169b22e..48690df3 100644 --- a/src/th-distinct/Sidekick_th_distinct.ml +++ b/src/th-distinct/Sidekick_th_distinct.ml @@ -9,7 +9,7 @@ module type ARG = sig val pp : t Fmt.printer val equal : t -> t -> bool val hash : t -> int - val as_distinct : t -> t Sequence.t option + val as_distinct : t -> t Iter.t option val mk_eq : state -> t -> t -> t end module Lit : sig @@ -113,7 +113,7 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t module CC = Sidekick_smt.CC - let process_lit (st:st) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (subs:term Sequence.t) : unit = + let process_lit (st:st) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (subs:term Iter.t) : unit = let (module A) = acts in Log.debugf 5 (fun k->k "(@[th_distinct.process@ %a@])" Lit.pp lit); let add_axiom c = A.add_persistent_axiom c in @@ -129,11 +129,11 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t ) else if not @@ T_tbl.mem st.expanded lit_t then ( (* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *) T_tbl.add st.expanded lit_t (); - let l = Sequence.to_list subs in + let l = Iter.to_list subs in let c = - Sequence.diagonal_l l - |> Sequence.map (fun (t,u) -> Lit.atom st.tst @@ T.mk_eq st.tst t u) - |> Sequence.to_rev_list + Iter.diagonal_l l + |> Iter.map (fun (t,u) -> Lit.atom st.tst @@ T.mk_eq st.tst t u) + |> Iter.to_rev_list in let c = Lit.neg lit :: c in Log.debugf 5 (fun k->k "(@[tseitin.distinct.case-split@ %a@])" pp_c c); @@ -182,8 +182,8 @@ module Arg = struct let eval args = let module Value = Sidekick_smt.Value in if - Sequence.diagonal (IArray.to_seq args) - |> Sequence.for_all (fun (x,y) -> not @@ Value.equal x y) + Iter.diagonal (IArray.to_seq args) + |> Iter.for_all (fun (x,y) -> not @@ Value.equal x y) then Value.true_ else Value.false_ diff --git a/src/th-distinct/Sidekick_th_distinct.mli b/src/th-distinct/Sidekick_th_distinct.mli index eff7ca06..c5578bf4 100644 --- a/src/th-distinct/Sidekick_th_distinct.mli +++ b/src/th-distinct/Sidekick_th_distinct.mli @@ -14,7 +14,7 @@ module type ARG = sig val pp : t Fmt.printer val equal : t -> t -> bool val hash : t -> int - val as_distinct : t -> t Sequence.t option + val as_distinct : t -> t Iter.t option val mk_eq : state -> t -> t -> t end module Lit : sig diff --git a/src/util/Bag.mli b/src/util/Bag.mli index b7787f4f..9995abdb 100644 --- a/src/util/Bag.mli +++ b/src/util/Bag.mli @@ -21,7 +21,7 @@ val cons : 'a -> 'a t -> 'a t val append : 'a t -> 'a t -> 'a t -val to_seq : 'a t -> 'a Sequence.t +val to_seq : 'a t -> 'a Iter.t val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a diff --git a/src/util/IArray.ml b/src/util/IArray.ml index 48c650df..8f1352d0 100644 --- a/src/util/IArray.ml +++ b/src/util/IArray.ml @@ -100,8 +100,8 @@ let of_seq s = (*$Q Q.(list int) (fun l -> \ - let g = Sequence.of_list l in \ - of_seq g |> to_seq |> Sequence.to_list = l) + let g = Iter.of_list l in \ + of_seq g |> to_seq |> Iter.to_list = l) *) let rec gen_to_list_ acc g = match g() with diff --git a/src/util/Util.mli b/src/util/Util.mli index c268212a..c3849151 100644 --- a/src/util/Util.mli +++ b/src/util/Util.mli @@ -7,7 +7,7 @@ type 'a printer = 'a CCFormat.printer val pp_list : ?sep:string -> 'a printer -> 'a list printer -val pp_seq : ?sep:string -> 'a printer -> 'a Sequence.t printer +val pp_seq : ?sep:string -> 'a printer -> 'a Iter.t printer val pp_array : ?sep:string -> 'a printer -> 'a array printer diff --git a/src/util/dune b/src/util/dune index dc285068..34504bb6 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,7 +1,7 @@ (library (name sidekick_util) (public_name sidekick.util) - (libraries containers sequence msat) + (libraries containers iter msat) (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) (ocamlopt_flags :standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)