diff --git a/README.md b/README.md index 9ceb0d81..c741988b 100644 --- a/README.md +++ b/README.md @@ -29,7 +29,7 @@ opam pin add msat https://github.com/Gbury/mSAT.git ### Manual installation -You will need `dune` and `sequence`. The command is: +You will need `dune` and `iter`. The command is: ``` $ make install diff --git a/msat.opam b/msat.opam index c2fca559..698d0cd4 100644 --- a/msat.opam +++ b/msat.opam @@ -13,7 +13,7 @@ build: [ depends: [ "ocaml" { >= "4.03" } "dune" {build} - "sequence" + "iter" { >= "1.2" } "containers" {with-test} "mdx" {with-test} ] diff --git a/src/core/Internal.ml b/src/core/Internal.ml index fad444d3..2342f42d 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -365,7 +365,7 @@ module Make(Plugin : PLUGIN) let[@inline] equal c1 c2 = c1.cid = c2.cid let[@inline] hash c = Hashtbl.hash c.cid let[@inline] atoms c = c.atoms - let[@inline] atoms_seq c = Sequence.of_array c.atoms + let[@inline] atoms_seq c = Iter.of_array c.atoms let[@inline] atoms_l c = Array.to_list c.atoms let flag_attached = 0b1 @@ -473,11 +473,11 @@ module Make(Plugin : PLUGIN) res (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *) - let same_lits (c1:atom Sequence.t) (c2:atom Sequence.t): bool = + let same_lits (c1:atom Iter.t) (c2:atom Iter.t): bool = let subset a b = - Sequence.iter Atom.mark b; - let res = Sequence.for_all Atom.seen a in - Sequence.iter clear_var_of_ b; + Iter.iter Atom.mark b; + let res = Iter.for_all Atom.seen a in + Iter.iter clear_var_of_ b; res in subset c1 c2 && subset c2 c1 @@ -567,9 +567,9 @@ module Make(Plugin : PLUGIN) (fun c -> let pivot = match - Sequence.of_array c.atoms - |> Sequence.filter (fun a -> Atom.seen (Atom.neg a)) - |> Sequence.to_list + Iter.of_array c.atoms + |> Iter.filter (fun a -> Atom.seen (Atom.neg a)) + |> Iter.to_list with | [a] -> a | [] -> @@ -608,11 +608,11 @@ module Make(Plugin : PLUGIN) error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion | History [c] -> let duplicates, res = find_dups c in - assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion)); + assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion)); { conclusion; step = Duplicate (c, duplicates) } | History (c :: r) -> let res, steps = find_pivots c r in - assert (same_lits (Sequence.of_list res) (Clause.atoms_seq conclusion)); + assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion)); { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; } | Empty_premise -> raise Solver_intf.No_proof diff --git a/src/core/Vec.ml b/src/core/Vec.ml index 0f2fb07b..782a8b6a 100644 --- a/src/core/Vec.ml +++ b/src/core/Vec.ml @@ -90,10 +90,10 @@ let[@inline] iteri f t = let[@inline] to_seq a k = iter k a -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 = Iter.exists p @@ to_seq t +let for_all p t = Iter.for_all p @@ to_seq t +let fold f acc a = Iter.fold f acc @@ to_seq a +let to_list a = Iter.to_list @@ to_seq a let to_array a = Array.sub a.data 0 a.sz let of_list l : _ t = diff --git a/src/core/Vec.mli b/src/core/Vec.mli index 74919698..d51a2b69 100644 --- a/src/core/Vec.mli +++ b/src/core/Vec.mli @@ -16,7 +16,7 @@ val to_array : 'a t -> 'a array val of_list : 'a list -> 'a t -val to_seq : 'a t -> 'a Sequence.t +val to_seq : 'a t -> 'a Iter.t val clear : 'a t -> unit (** Set size to 0, doesn't free elements *) diff --git a/src/core/dune b/src/core/dune index 6ec93b3a..85a23d9a 100644 --- a/src/core/dune +++ b/src/core/dune @@ -2,7 +2,7 @@ (library (name msat) (public_name msat) - (libraries sequence) + (libraries iter) (synopsis "core data structures and algorithms for msat") (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) (ocamlopt_flags :standard -O3 -bin-annot diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml index 389fce6a..616b02a4 100644 --- a/src/sudoku/sudoku_solve.ml +++ b/src/sudoku/sudoku_solve.ml @@ -36,13 +36,13 @@ module Grid : sig val set : t -> int -> int -> Cell.t -> t (** A set of related cells *) - type set = (int*int*Cell.t) Sequence.t + type set = (int*int*Cell.t) Iter.t - val rows : t -> set Sequence.t - val cols : t -> set Sequence.t - val squares : t -> set Sequence.t + val rows : t -> set Iter.t + val cols : t -> set Iter.t + val squares : t -> set Iter.t - val all_cells : t -> (int*int*Cell.t) Sequence.t + val all_cells : t -> (int*int*Cell.t) Iter.t val parse : string -> t val is_full : t -> bool @@ -60,9 +60,9 @@ end = struct s' (** A set of related cells *) - type set = (int*int*Cell.t) Sequence.t + type set = (int*int*Cell.t) Iter.t - open Sequence.Infix + open Iter.Infix let all_cells (g:t) = 0 -- 8 >>= fun i -> @@ -90,17 +90,17 @@ end = struct let is_valid g = let all_distinct (s:set) = (s >|= fun (_,_,c) -> c) - |> Sequence.diagonal - |> Sequence.for_all (fun (c1,c2) -> Cell.neq c1 c2) + |> Iter.diagonal + |> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2) in - Sequence.for_all all_distinct @@ rows g && - Sequence.for_all all_distinct @@ cols g && - Sequence.for_all all_distinct @@ squares g + Iter.for_all all_distinct @@ rows g && + Iter.for_all all_distinct @@ cols g && + Iter.for_all all_distinct @@ squares g let matches ~pat:g1 g2 : bool = all_cells g1 - |> Sequence.filter (fun (_,_,c) -> Cell.is_full c) - |> Sequence.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y) + |> Iter.filter (fun (_,_,c) -> Cell.is_full c) + |> Iter.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y) let pp out g = Fmt.fprintf out "@["; @@ -186,11 +186,11 @@ end = struct let[@inline] all_diff kind f = let pairs = f (grid self) - |> Sequence.flat_map + |> Iter.flat_map (fun set -> set - |> Sequence.filter (fun (_,_,c) -> Cell.is_full c) - |> Sequence.diagonal) + |> Iter.filter (fun (_,_,c) -> Cell.is_full c) + |> Iter.diagonal) in pairs (fun ((x1,y1,c1),(x2,y2,c2)) -> @@ -208,7 +208,7 @@ end = struct let trail_ (acts:_ Msat.acts) = acts.acts_iter_assumptions - |> Sequence.map + |> Iter.map (function | Assign _ -> assert false | Lit f -> f) @@ -255,10 +255,10 @@ end = struct let solve (self:t) : _ option = let assumptions = Grid.all_cells self.grid0 - |> Sequence.filter (fun (_,_,c) -> Cell.is_full c) - |> Sequence.map (fun (x,y,c) -> F.make true x y c) - |> Sequence.map (S.make_atom self.solver) - |> Sequence.to_rev_list + |> Iter.filter (fun (_,_,c) -> Cell.is_full c) + |> Iter.map (fun (x,y,c) -> F.make true x y c) + |> Iter.map (S.make_atom self.solver) + |> Iter.to_rev_list in Log.debugf 2 (fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);