Module `FeatureVector.Make`

module C = C

module Feature : sig ... end

module IntMap : sig ... end

module CSet : sig ... end

type trie = | TrieNode of trie IntMap.t map feature -> trie | TrieLeaf of CSet.t leaf with a set of clauses

val empty_trie : trie -> bool
val goto_leaf : trie -> IntMap.key list -> (CSet.t -> trie) -> trie: get/add/remove the leaf for the given list of ints. The continuation k takes the leaf, and returns a leaf that replaces the old leaf. This function returns the new trie.

val empty_with : Feature.t list -> t
val name : string
val features : t -> Feature.t list
val default_features : Feature.t list
val max_features : int: maximam number of features in addition to basic ones

val features_of_signature : ?⁠ignore:(ID.t -> bool) -> Signature.t -> Feature.t list
val of_signature : Signature.t -> t
val empty : unit -> t
val add : t -> C.t -> t
val add_seq : t -> C.t Iter.t -> t
val add_list : t -> C.t list -> t
val remove : t -> C.t -> t
val remove_seq : t -> C.t Iter.t -> t
val retrieve_subsuming : t -> lits -> 'a -> (CSet.elt -> unit) -> unit
val retrieve_subsumed : t -> lits -> 'a -> (CSet.elt -> unit) -> unit: clauses that are subsumed (potentially) by the given clause

val retrieve_alpha_equiv : t -> lits -> 'a -> (CSet.elt -> unit) -> unit: clauses that are potentially alpha-equivalent to the given clause

`\|` `TrieNode of trie IntMap.t`	map feature -> trie
`\|` `TrieLeaf of CSet.t`	leaf with a set of clauses