package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.FeatureSource

Sourcetype t = {
  1. name : string;
  2. f : lits -> int;
}

a function that computes a given feature on clauses

Sourceval name : t -> string
Sourceval compute : t -> lits -> int
include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
Sourceval sum_of_depths : t

sum of depths of symbols

Sourceval size_plus : t

size of positive clause

Sourceval size_minus : t

size of negative clause

Sourceval count_symb_plus : ID.t -> t

occurrences of ID.t in positive clause

Sourceval count_symb_minus : ID.t -> t

occurrences of ID.t in negative clause

Sourceval max_depth_plus : ID.t -> t

maximal depth of symb in positive clause

Sourceval max_depth_minus : ID.t -> t

maximal depth of symb in negative clause