logtk

Core types and algorithms for logic
IN THIS PACKAGE
type t = {
name : string;
f : lits -> int;
}

a function that computes a given feature on clauses

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

sum of depths of symbols

val size_plus : t

size of positive clause

val size_minus : t

size of negative clause

val count_symb_plus : ID.t -> t

occurrences of ID.t in positive clause

val count_symb_minus : ID.t -> t

occurrences of ID.t in negative clause

val max_depth_plus : ID.t -> t

maximal depth of symb in positive clause

val max_depth_minus : ID.t -> t

maximal depth of symb in negative clause