diff --git a/lib/pqtrees/pqRefinementOrder.ml b/lib/pqtrees/pqRefinementOrder.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3e95d7d79f9b338f862c626e61adcf5bf6e63582
--- /dev/null
+++ b/lib/pqtrees/pqRefinementOrder.ml
@@ -0,0 +1,122 @@
+open PqTree
+
+module Make = functor (S : Set.S) ->
+struct
+ type elt = S.elt
+ type pqtree = elt PqTree.t
+
+ (* type answer = *)
+ (* | Yes *)
+ (* | No of elt list *)
+
+
+ type intersection =
+ | Empty
+ | All
+ | Complete
+ | Compromised
+
+ let rec p_intersect = function
+ | []
+ | [ Empty ] -> Empty
+ | [ Complete ] -> Complete
+ | [ All ] | [All; All]-> All
+ | Empty :: Empty :: tail -> p_intersect (Empty :: tail)
+ | All :: All :: All :: tail -> p_intersect (All :: All :: tail)
+ | All :: All :: _ -> Compromised
+ | (All | Complete) :: tail
+ | Empty :: (All | Complete) :: tail ->
+ if List.for_all (fun elt -> elt = Empty) tail then Complete
+ else Compromised
+ | Compromised :: _
+ | _ :: Compromised :: _ -> Compromised
+
+ let rec q_intersect = function
+ | All :: All :: tail -> q_intersect (All :: tail)
+ | Empty :: Empty :: tail -> q_intersect (Empty :: tail)
+ | Empty :: All :: All :: tail -> q_intersect (Empty :: All :: tail)
+ | All :: Empty :: tail
+ | Empty :: All :: Empty :: tail
+ | Empty :: Complete :: tail
+ | Complete :: Empty :: tail -> q_intersect(Complete :: tail)
+ | [ All ] -> All
+ | [ Empty ] | [] -> Empty
+ | [ Complete ] | [Empty; All] -> Complete
+ | All :: Complete :: _
+ | Compromised :: _
+ | _ :: Compromised :: _
+ | Empty :: All :: (Complete | Compromised) :: _
+ | Complete :: All :: _
+ | Complete :: Complete :: _ -> Compromised
+ (* | _ -> Compromised *)
+
+
+
+ let rec intersect_block block = function
+ | P children ->
+ children
+ |> List.map (intersect_block block)
+ |> p_intersect
+ | Q children ->
+ children
+ |> List.map (intersect_block block)
+ |> q_intersect
+ | Leaf x when S.mem x block -> All
+ | Leaf _ -> Empty
+
+
+ let is_a_block tree block =
+ intersect_block block tree <> Compromised
+
+
+ let is_not_singleton set =
+ S.cardinal set <> 1
+
+ let rec blocks_and_block =
+ let recurse children =
+ List.to_seq children
+ |> Seq.map blocks_and_block
+ |> Seq.split
+ in
+ function
+ | Leaf x -> (Seq.empty, S.singleton x)
+ | P children ->
+ let (blocks, sets) = recurse children in
+ (blocks
+ |> Seq.concat
+ |> Seq.append (Seq.filter is_not_singleton sets),
+ Seq.fold_left S.union S.empty sets
+ )
+ | Q children ->
+ let n = List.length children in
+ let (blocks, sets) = recurse children in
+ let set = Seq.fold_left S.union S.empty sets in
+ let leftist_blocks =
+ Seq.scan S.union S.empty sets |> Seq.drop 2 |> Seq.take (n-2)
+ in
+ let rightist_blocks =
+ Seq.scan S.diff set sets |> Seq.drop 1 |> Seq.take (n-2)
+ in
+ (blocks
+ |> Seq.concat
+ |> Seq.append (Seq.filter is_not_singleton sets)
+ |> Seq.append leftist_blocks
+ |> Seq.append rightist_blocks,
+ set)
+
+ let enumerate_non_trivial_blocks tree =
+ fst (blocks_and_block tree)
+
+
+ let is_refinement tree1 tree2 =
+ Seq.for_all
+ (is_a_block tree1)
+ (enumerate_non_trivial_blocks tree2)
+
+
+ (* let is_refinement tree1 tree2 = *)
+ (* match certify_refinement tree1 tree2 with *)
+ (* | Yes -> true *)
+ (* | No _ -> false *)
+
+end
diff --git a/lib/pqtrees/pqRefinementOrder.mli b/lib/pqtrees/pqRefinementOrder.mli
new file mode 100644
index 0000000000000000000000000000000000000000..fae9bc4dbe46a77352c261fb494479a7ef4d9327
--- /dev/null
+++ b/lib/pqtrees/pqRefinementOrder.mli
@@ -0,0 +1,32 @@
+module Make : functor (S : Set.S) ->
+sig
+ type elt = S.elt
+ type pqtree = elt PqTree.t
+
+
+ val is_a_block : pqtree -> S.t -> bool
+
+ val enumerate_non_trivial_blocks : pqtree -> S.t Seq.t
+
+ val is_refinement : pqtree -> pqtree -> bool
+
+
+end
+
+
+
+(* type 'elt answer = *)
+(* | Yes *)
+(* | No of 'elt list (\** a certifying permutation *\) *)
+
+
+(* (\** [is_refinement tree1 tree2] checks whether all permutations *)
+(* represented by [tree1] are represented in [tree2]. *\) *)
+(* val is_refinement : 'elt PqTree.t -> 'elt PqTree.t -> bool *)
+
+
+(* (\** [certify_refinement tree1 tree2] returns [Yes] if [tree1] is a *)
+(* refinement of [tree2], or [No permut] where [permut] is *)
+(* represented in [tree1] but not in [tree2]. *\) *)
+(* val certify_refinement : 'elt PqTree.t -> 'elt PqTree.t -> 'elt answer *)
+
diff --git a/test/propertytest/chainInsertion.ml b/test/propertytest/chainInsertion.ml
index 90034d80fe296ccfaad9c59bc8354386f5cdbcc4..573d7a485338b4eed03839942aec7bd8ddd2229d 100644
--- a/test/propertytest/chainInsertion.ml
+++ b/test/propertytest/chainInsertion.ml
@@ -7,6 +7,7 @@ open QCheck2
module IntSet = Set.Make(Int)
+module Ref = PqRefinementOrder.Make(IntSet)
let insert_interval interval pqtree =
let f i = if IntSet.mem i interval then 0 else 1 in
@@ -38,7 +39,56 @@ let test_interval_insertion_does_not_fail =
+let rec zip list1 list2 = match list1, list2 with
+| hd1::tl1, hd2::tl2 -> (hd1,hd2)::zip tl1 tl2
+| _,_ -> []
+
+
+
+let print_tree_and_chain =
+ Print.(pair to_string (pair int (list (pair int int))))
+
+let gen_tree_and_chain =
+ let open Gen in
+ list_size (return 100) bool >>= fun bools ->
+ int_range 1 50 >>=
+ sized_shuffled_pair_gen >>= fun (shuffled, pqtree) ->
+ let elts = PqTree.frontier shuffled in
+ let n = List.length elts in
+ int_range 0 (n-1) >>= fun pivot_rank ->
+ let ints =
+ bools
+ |> List.fold_left (fun (accu,i) bool -> (i::accu, if bool then i else i+1)) ([],0)
+ |> fst
+ in
+ let pivot = List.nth elts pivot_rank in
+ let pivot_v = List.nth ints pivot_rank in
+ return (pqtree, (pivot, zip elts (List.map (fun i -> abs (i - pivot_v)) ints)))
+
+
+
+let new_valid_permutation_is_old_valid_permutation (pqtree, (source,distances)) =
+ let f i = List.assoc i distances in
+ match PqChainInsertion.refine_by_distances source f pqtree with
+ | None -> false
+| Some new_pqtree -> Ref.is_refinement new_pqtree pqtree
+
+let test_new_valid_permutation_is_old_valid_permutation =
+ Test.make
+ ~name:"Chain insertion returns a refinement of the original PQ-tree"
+ ~print:print_tree_and_chain
+ ~count:1000
+ gen_tree_and_chain
+ new_valid_permutation_is_old_valid_permutation
+
+
+
+
+
+
+
let tests =
[
- test_interval_insertion_does_not_fail
+ test_interval_insertion_does_not_fail;
+ test_new_valid_permutation_is_old_valid_permutation;
]
diff --git a/test/unit/refinementOrderTest.ml b/test/unit/refinementOrderTest.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a9c60f09161e5546b1455d9816445fad9096dbed
--- /dev/null
+++ b/test/unit/refinementOrderTest.ml
@@ -0,0 +1,107 @@
+open PqTreeLib
+open PqTree
+open RobinsonTest
+
+open IntPqTree
+
+module IntSet = Set.Make(Int)
+
+
+let pp_sep sep fmt () = Format.(fprintf fmt "%s@ " sep)
+
+let pp_delimiter left right inside_formatter fmt value =
+ Format.(fprintf fmt "%s%a%s" left inside_formatter value right)
+
+let pp_delimited_seq left sep right elt_formatter =
+ let open Format in
+ pp_delimiter left right
+ (pp_print_seq elt_formatter ~pp_sep:(pp_sep sep))
+
+let pp_block fmt block =
+ pp_delimited_seq "{" ";" "}" Format.pp_print_int fmt (IntSet.to_seq block)
+
+
+let pp_block_seq =
+ pp_delimited_seq "[" ";" "]" pp_block
+
+
+let output_blocks blocks =
+ Format.(printf "%a" pp_block_seq blocks)
+
+
+let output result =
+ result
+ |> Option.map Canonical.canonical
+ |> Option.map to_string
+ |> Option.value ~default:"not an interval"
+ |> print_endline
+
+module M = PqRefinementOrder.Make(IntSet)
+
+
+
+let tree0 = P [Leaf 1; Leaf 2; Leaf 3]
+
+let%expect_test _ =
+ M.enumerate_non_trivial_blocks tree0
+ |> output_blocks; [%expect{|
+ []|}]
+
+
+let tree1 = Q [Leaf 1; Leaf 2; Leaf 3]
+
+let%expect_test _ =
+ M.enumerate_non_trivial_blocks tree1
+ |> output_blocks; [%expect{|
+ [{2; 3}; {1;
+ 2}]|}]
+
+
+let tree2 = P [ Q [Leaf 1; Leaf 2; Leaf 3]; P [Leaf 4; Leaf 5]]
+
+let%expect_test _ =
+ M.enumerate_non_trivial_blocks tree2
+ |> output_blocks; [%expect{|
+ [{1; 2; 3}; {4; 5}; {2; 3}; {1;
+ 2}]|}]
+
+let tree3 =
+ Q [
+ P [Leaf 1; Leaf 2; Leaf 3];
+ Q [Leaf 4; Leaf 5; Leaf 6];
+ Leaf 7;
+ P [P [Leaf 8; Leaf 9]; Leaf 10; Leaf 11]
+ ]
+
+let%expect_test _ =
+ M.enumerate_non_trivial_blocks tree3
+ |> output_blocks; [%expect{|
+ [{4; 5; 6; 7; 8; 9; 10; 11}; {7; 8; 9; 10; 11}; {1; 2; 3; 4; 5; 6}; {1; 2; 3;
+ 4; 5; 6; 7}; {1; 2; 3}; {4; 5; 6}; {8; 9; 10; 11}; {5; 6}; {4; 5}; {8;
+ 9}]|}]
+
+let%expect_test _ =
+ [ ([1;2], tree1);
+ ([2;3], tree1);
+ ([4;5], tree2);
+ ([1;2;3;4;5], tree2);
+ ([1;2;3], tree2);
+ ([2], tree2);
+ ([4;5;6;7], tree3);
+ ([1;2;3;4;5;6], tree3);
+ ([8;9],tree3);
+ ([1;3], tree0);
+ ([1;3], tree1);
+ ([1;3], tree2);
+ ([1;2;4;5], tree2);
+ ([2;3;4;5;6], tree3);
+ ([1;2;3;7], tree3);
+ ([8;9;10], tree3);
+ ]
+ |> List.to_seq
+ |> Seq.map (fun (block, tree) -> M.is_a_block tree (IntSet.of_list block))
+ |> Format.printf "%a" (pp_delimited_seq "[" ";" "]" Format.pp_print_bool);
+ [%expect{|
+ [true; true; true; true; true; true; true; true; true; false; false; false;
+ false; false; false;
+ false] |}]