logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
Module Logtk . 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 =
| 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.

Subsumption Index

type t = {
trie : trie;
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