Module Term_attributes (.ml)

module Term_attributes: sig .. end

type term = Term.term 

type literal = Term.literal 

type clause = Term.clause 

type subst = Subst.subst 

type pureness 

a term is

• universal, if it contains no parameters,
• mixed, if it contains parameters and variables,
• parametric, if it contains parameters but no variables.

val get_pureness : term -> pureness

pureness of a term.

val is_universal : pureness -> bool

is the term universal?

val is_mixed : pureness -> bool

is the term mixed?

val is_parametric : pureness -> bool

is the term parametric?

val is_term_parametric : term -> bool

faster shortcut for Term_attributes.is_parametric (Term_attributes.get_pureness term).

val is_propositional : literal -> bool

is the literal propositional, i.e. a predicate symbol without arguments?

val cmp_pureness : pureness -> pureness -> int

cmp_pureness_universality pureness1 pureness2 returns

• -1, if pureness1 is universal but pureness2 is not,
• 1, if pureness2 is universal but pureness1 is not,
• 0, otherwise

val cmp_universality : pureness -> pureness -> int

cmp_pureness_universality pureness1 pureness2 returns -1, 0, or 1 and prefers first, terms with as few parameters as possible, and second, terms with as much universal variables as possible.

val depth_of_literal : literal -> int

depth of a literal, i.e. the deepest branch if the term is seen as a tree.

Examples:

• a -> 0
• f(a, b) -> 1
• f(a, g(b)) -> 2

val depth_of_term : term -> int

val depth_of_literal_subst : literal -> subst -> int -> int

depth_of_literal_subst subst literal offset is like Term_attributes.depth_of_literal, but variables in literal are replaced by their bindings in subst

val weight_of_literal : literal -> int

weight of a literal, i.e. the number of function/constant symbol occurrences in the term.

Examples:

• a -> 1
• f(a, a) -> 3
• f(x, g(b)) -> 3
• f(u, g(b)) -> 3

val weight_of_literal_subst : literal -> subst -> int -> int

weight_of_literal_subst subst literal offset is like Term_attributes.weight_of_literal, but variables in literal are replaced by their bindings in subst

val weight_of_clause : clause -> int

weight of a clause, i.e. the sum of the literal weights.