package logtk

  1. Overview
  2. Docs

Module FeatureVector.Make

Parameters

module C : Index.CLAUSE

Signature

module C = C
type feature_vector = int list

a vector of feature

Features

module Feature : sig ... end
val compute_fv : Feature.t list -> lits -> int list

Feature Trie

module IntMap : sig ... end
module CSet : sig ... end
type trie =
  1. | TrieNode of trie IntMap.t
    (*

    map feature -> trie

    *)
  2. | 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.

Subsumption Index

type t = {
  1. trie : trie;
  2. features : Feature.t list;
}
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

val retrieve_subsuming_c : t -> C.t -> (CSet.elt -> unit) -> unit
val retrieve_subsumed_c : t -> C.t -> (CSet.elt -> unit) -> unit
val retrieve_alpha_equiv_c : t -> C.t -> (CSet.elt -> unit) -> unit
val iter : t -> (CSet.elt -> unit) -> unit
val fold : ('a -> CSet.elt -> 'a) -> 'a -> t -> 'a