Functor FeatureVector.Make

module Make (C : Index.CLAUSE) : sig .. end

Parameters:

C : Index.CLAUSE

type feature_vector = int list

a vector of feature

Features

module Feature: sig .. end

val compute_fv : Feature.t list ->
       FeatureVector.lits -> feature_vector

include Index.SUBSUMPTION_IDX

val retrieve_alpha_equiv : t -> FeatureVector.lits -> C.t Sequence.t

Retrieve clauses that are potentially alpha-equivalent to the given clause
Since 0.6

val retrieve_alpha_equiv_c : t -> C.t -> C.t Sequence.t

Since 0.6

val empty_with : Feature.t list -> t

val default_features : Feature.t list

val features_of_signature : ?ignore:(ID.t -> bool) -> Signature.t -> Feature.t list

Build a set of features from the given signature. IDs that satisfy ignore are not considered (default ignores connectives)

val of_signature : Signature.t -> t

val features : t -> Feature.t list