sig
  module FixpointList :
    sig
      val check : Node.t -> Node.t list -> int list option
      val pure_smt_check : Node.t -> Node.t list -> int list option
    end
  module FixpointCertif :
    sig
      val useful_instances :
        Node.t -> Node.t list -> (Node.t * Variable.subst) list
    end
  module FixpointTrie :
    sig
      val easy_fixpoint : Node.t -> Node.t Cubetrie.t -> int list option
      val peasy_fixpoint : Node.t -> Node.t Cubetrie.t -> int list option
      val hard_fixpoint : Node.t -> Node.t Cubetrie.t -> int list option
      val check : Node.t -> Node.t Cubetrie.t -> int list option
    end
  module FixpointTrieNaive :
    sig val check : Node.t -> Node.t Cubetrie.t -> int list option end
end