sig
  val sort :
    int array -> 'a Cudd.Bdd.t array -> int array * 'a Cudd.Bdd.t array
  val is_equal : 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t array -> bool
  val post :
    'a Cudd.Bdd.t -> int array -> 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
  val postcondition : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
end