Cubicle 1.1.2 documentation and source : Cubetrie.delete

let delete_subsumed ?(cpt=ref 0) p nodes =
  let vars, ap = Node.variables p, Node.array p in
  let substs = Variable.all_permutations vars vars in
  List.iter (fun ss ->
    let u = ArrayAtom.apply_subst ss ap in
    iter_subsumed (fun n ->
      if Node.has_deleted_ancestor n || not (Node.ancestor_of n p) then begin
        n.deleted <- true;
        if dot then Dot.delete_node_by n p;
        incr cpt;
      end
    ) (Array.to_list u) nodes;
  ) substs;
  (* iter (fun n -> if Node.has_deleted_ancestor n then *)
  (*       n.deleted <- true; *)
  (*       ) nodes; *)
  delete (fun n -> n.deleted || Node.has_deleted_ancestor n) nodes