package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = {
  1. name : string;
  2. f : LogtkIndex.lits -> int;
}

a function that computes a given feature on clauses

val name : t -> string
val compute : t -> LogtkIndex.lits -> int
val pp : Buffer.t -> t -> unit
val fmt : Format.formatter -> t -> unit
val sum_of_depths : t

sum of depths of symbols

val size_plus : t

sum of depths of symbols

size of positive clause

val size_minus : t

size of positive clause

size of negative clause

val count_symb_plus : LogtkSymbol.t -> t

size of negative clause

occurrences of symbol in positive clause

val count_symb_minus : LogtkSymbol.t -> t

occurrences of symbol in positive clause

occurrences of symbol in negative clause

val max_depth_plus : LogtkSymbol.t -> t

occurrences of symbol in negative clause

maximal depth of symb in positive clause

val max_depth_minus : LogtkSymbol.t -> t

maximal depth of symb in positive clause

maximal depth of symb in negative clause