Module Weight

module Weight: sig .. end

Weighing Terms.

type term_weighing_method =

`\|`	`SymbolCount`	`(*`	`The size of the term, i.e. the number of occurences of predicate, function and constant symbols as well as variables in it is used.`	`*)`
`\|`	`Depth`	`(*`	`The depth of the term is used.`	`*)`

An object of this type specifies how the term weight value for a given term is computed. It is passed as argument to term_weight.

val term_weight : term_weighing_method -> Term.term -> int

Return the weight of the given term.