mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-08 04:05:43 -05:00
refactor: use iter instead of sequence
This commit is contained in:
parent
6e8cedd790
commit
fb219fb415
7 changed files with 40 additions and 40 deletions
|
|
@ -29,7 +29,7 @@ opam pin add msat https://github.com/Gbury/mSAT.git
|
||||||
|
|
||||||
### Manual installation
|
### Manual installation
|
||||||
|
|
||||||
You will need `dune` and `sequence`. The command is:
|
You will need `dune` and `iter`. The command is:
|
||||||
|
|
||||||
```
|
```
|
||||||
$ make install
|
$ make install
|
||||||
|
|
|
||||||
|
|
@ -13,7 +13,7 @@ build: [
|
||||||
depends: [
|
depends: [
|
||||||
"ocaml" { >= "4.03" }
|
"ocaml" { >= "4.03" }
|
||||||
"dune" {build}
|
"dune" {build}
|
||||||
"sequence"
|
"iter" { >= "1.2" }
|
||||||
"containers" {with-test}
|
"containers" {with-test}
|
||||||
"mdx" {with-test}
|
"mdx" {with-test}
|
||||||
]
|
]
|
||||||
|
|
|
||||||
|
|
@ -365,7 +365,7 @@ module Make(Plugin : PLUGIN)
|
||||||
let[@inline] equal c1 c2 = c1.cid = c2.cid
|
let[@inline] equal c1 c2 = c1.cid = c2.cid
|
||||||
let[@inline] hash c = Hashtbl.hash c.cid
|
let[@inline] hash c = Hashtbl.hash c.cid
|
||||||
let[@inline] atoms c = c.atoms
|
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[@inline] atoms_l c = Array.to_list c.atoms
|
||||||
|
|
||||||
let flag_attached = 0b1
|
let flag_attached = 0b1
|
||||||
|
|
@ -473,11 +473,11 @@ module Make(Plugin : PLUGIN)
|
||||||
res
|
res
|
||||||
|
|
||||||
(* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *)
|
(* 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 =
|
let subset a b =
|
||||||
Sequence.iter Atom.mark b;
|
Iter.iter Atom.mark b;
|
||||||
let res = Sequence.for_all Atom.seen a in
|
let res = Iter.for_all Atom.seen a in
|
||||||
Sequence.iter clear_var_of_ b;
|
Iter.iter clear_var_of_ b;
|
||||||
res
|
res
|
||||||
in
|
in
|
||||||
subset c1 c2 && subset c2 c1
|
subset c1 c2 && subset c2 c1
|
||||||
|
|
@ -567,9 +567,9 @@ module Make(Plugin : PLUGIN)
|
||||||
(fun c ->
|
(fun c ->
|
||||||
let pivot =
|
let pivot =
|
||||||
match
|
match
|
||||||
Sequence.of_array c.atoms
|
Iter.of_array c.atoms
|
||||||
|> Sequence.filter (fun a -> Atom.seen (Atom.neg a))
|
|> Iter.filter (fun a -> Atom.seen (Atom.neg a))
|
||||||
|> Sequence.to_list
|
|> Iter.to_list
|
||||||
with
|
with
|
||||||
| [a] -> a
|
| [a] -> a
|
||||||
| [] ->
|
| [] ->
|
||||||
|
|
@ -608,11 +608,11 @@ module Make(Plugin : PLUGIN)
|
||||||
error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion
|
error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion
|
||||||
| History [c] ->
|
| History [c] ->
|
||||||
let duplicates, res = find_dups c in
|
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) }
|
{ conclusion; step = Duplicate (c, duplicates) }
|
||||||
| History (c :: r) ->
|
| History (c :: r) ->
|
||||||
let res, steps = find_pivots c r in
|
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}; }
|
{ conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; }
|
||||||
| Empty_premise -> raise Solver_intf.No_proof
|
| Empty_premise -> raise Solver_intf.No_proof
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -90,10 +90,10 @@ let[@inline] iteri f t =
|
||||||
|
|
||||||
let[@inline] to_seq a k = iter k a
|
let[@inline] to_seq a k = iter k a
|
||||||
|
|
||||||
let exists p t = Sequence.exists p @@ to_seq t
|
let exists p t = Iter.exists p @@ to_seq t
|
||||||
let for_all p t = Sequence.for_all p @@ to_seq t
|
let for_all p t = Iter.for_all p @@ to_seq t
|
||||||
let fold f acc a = Sequence.fold f acc @@ to_seq a
|
let fold f acc a = Iter.fold f acc @@ to_seq a
|
||||||
let to_list a = Sequence.to_list @@ 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 to_array a = Array.sub a.data 0 a.sz
|
||||||
|
|
||||||
let of_list l : _ t =
|
let of_list l : _ t =
|
||||||
|
|
|
||||||
|
|
@ -16,7 +16,7 @@ val to_array : 'a t -> 'a array
|
||||||
|
|
||||||
val of_list : 'a list -> 'a t
|
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
|
val clear : 'a t -> unit
|
||||||
(** Set size to 0, doesn't free elements *)
|
(** Set size to 0, doesn't free elements *)
|
||||||
|
|
|
||||||
|
|
@ -2,7 +2,7 @@
|
||||||
(library
|
(library
|
||||||
(name msat)
|
(name msat)
|
||||||
(public_name msat)
|
(public_name msat)
|
||||||
(libraries sequence)
|
(libraries iter)
|
||||||
(synopsis "core data structures and algorithms for msat")
|
(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)
|
(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
|
(ocamlopt_flags :standard -O3 -bin-annot
|
||||||
|
|
|
||||||
|
|
@ -36,13 +36,13 @@ module Grid : sig
|
||||||
val set : t -> int -> int -> Cell.t -> t
|
val set : t -> int -> int -> Cell.t -> t
|
||||||
|
|
||||||
(** A set of related cells *)
|
(** 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 rows : t -> set Iter.t
|
||||||
val cols : t -> set Sequence.t
|
val cols : t -> set Iter.t
|
||||||
val squares : t -> set Sequence.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 parse : string -> t
|
||||||
val is_full : t -> bool
|
val is_full : t -> bool
|
||||||
|
|
@ -60,9 +60,9 @@ end = struct
|
||||||
s'
|
s'
|
||||||
|
|
||||||
(** A set of related cells *)
|
(** 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) =
|
let all_cells (g:t) =
|
||||||
0 -- 8 >>= fun i ->
|
0 -- 8 >>= fun i ->
|
||||||
|
|
@ -90,17 +90,17 @@ end = struct
|
||||||
let is_valid g =
|
let is_valid g =
|
||||||
let all_distinct (s:set) =
|
let all_distinct (s:set) =
|
||||||
(s >|= fun (_,_,c) -> c)
|
(s >|= fun (_,_,c) -> c)
|
||||||
|> Sequence.diagonal
|
|> Iter.diagonal
|
||||||
|> Sequence.for_all (fun (c1,c2) -> Cell.neq c1 c2)
|
|> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2)
|
||||||
in
|
in
|
||||||
Sequence.for_all all_distinct @@ rows g &&
|
Iter.for_all all_distinct @@ rows g &&
|
||||||
Sequence.for_all all_distinct @@ cols g &&
|
Iter.for_all all_distinct @@ cols g &&
|
||||||
Sequence.for_all all_distinct @@ squares g
|
Iter.for_all all_distinct @@ squares g
|
||||||
|
|
||||||
let matches ~pat:g1 g2 : bool =
|
let matches ~pat:g1 g2 : bool =
|
||||||
all_cells g1
|
all_cells g1
|
||||||
|> Sequence.filter (fun (_,_,c) -> Cell.is_full c)
|
|> Iter.filter (fun (_,_,c) -> Cell.is_full c)
|
||||||
|> Sequence.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y)
|
|> Iter.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y)
|
||||||
|
|
||||||
let pp out g =
|
let pp out g =
|
||||||
Fmt.fprintf out "@[<v>";
|
Fmt.fprintf out "@[<v>";
|
||||||
|
|
@ -186,11 +186,11 @@ end = struct
|
||||||
let[@inline] all_diff kind f =
|
let[@inline] all_diff kind f =
|
||||||
let pairs =
|
let pairs =
|
||||||
f (grid self)
|
f (grid self)
|
||||||
|> Sequence.flat_map
|
|> Iter.flat_map
|
||||||
(fun set ->
|
(fun set ->
|
||||||
set
|
set
|
||||||
|> Sequence.filter (fun (_,_,c) -> Cell.is_full c)
|
|> Iter.filter (fun (_,_,c) -> Cell.is_full c)
|
||||||
|> Sequence.diagonal)
|
|> Iter.diagonal)
|
||||||
in
|
in
|
||||||
pairs
|
pairs
|
||||||
(fun ((x1,y1,c1),(x2,y2,c2)) ->
|
(fun ((x1,y1,c1),(x2,y2,c2)) ->
|
||||||
|
|
@ -208,7 +208,7 @@ end = struct
|
||||||
|
|
||||||
let trail_ (acts:_ Msat.acts) =
|
let trail_ (acts:_ Msat.acts) =
|
||||||
acts.acts_iter_assumptions
|
acts.acts_iter_assumptions
|
||||||
|> Sequence.map
|
|> Iter.map
|
||||||
(function
|
(function
|
||||||
| Assign _ -> assert false
|
| Assign _ -> assert false
|
||||||
| Lit f -> f)
|
| Lit f -> f)
|
||||||
|
|
@ -255,10 +255,10 @@ end = struct
|
||||||
let solve (self:t) : _ option =
|
let solve (self:t) : _ option =
|
||||||
let assumptions =
|
let assumptions =
|
||||||
Grid.all_cells self.grid0
|
Grid.all_cells self.grid0
|
||||||
|> Sequence.filter (fun (_,_,c) -> Cell.is_full c)
|
|> Iter.filter (fun (_,_,c) -> Cell.is_full c)
|
||||||
|> Sequence.map (fun (x,y,c) -> F.make true x y c)
|
|> Iter.map (fun (x,y,c) -> F.make true x y c)
|
||||||
|> Sequence.map (S.make_atom self.solver)
|
|> Iter.map (S.make_atom self.solver)
|
||||||
|> Sequence.to_rev_list
|
|> Iter.to_rev_list
|
||||||
in
|
in
|
||||||
Log.debugf 2
|
Log.debugf 2
|
||||||
(fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
|
(fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue