logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
type t = {
name : string;
f : lits -> int;
}

a function that computes a given feature on clauses

val compute : t -> lits -> int
val name : t -> string
val pp : CCFormat.t -> t -> unit
val to_string : t -> string
val size_plus : t
val size_minus : t
val _depth_term : int -> T.t -> int
val sum_of_depths : t
val _select_sign : sign:bool -> 'a SLiteral.t Iter.t -> 'a SLiteral.t Iter.t
val _symbols : sign:bool -> InnerTerm.t SLiteral.t Iter.t -> ID.t Iter.t
val count_symb_plus : ID.t -> t
val count_symb_minus : ID.t -> t
val max_depth_term : ID.t -> InnerTerm.t -> int
val _max_depth_lits : sign:bool -> ID.t -> InnerTerm.t SLiteral.t Iter.t -> int
val max_depth_plus : ID.t -> t
val max_depth_minus : ID.t -> t