package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct