Module Sort_inference (.ml)

module Sort_inference: sig .. end

infers sorts based on a clause set

Implements sort inference, see the paper New Techniques that Improve MACE-style Finite Model Finding by Koen Classen and Niklas Soerensson.

For an unsorted first-order clause set, the sorts of each function and predicate symbol (arguments and results) are first assumed to be different. Then sorts are collapsed, if their occurrences in the clauses require two sorts to be identical. For example,

g(a) and g(b) requires a and b to have the same sort,
f(x, x) and f(a, b) requires a and b to have the same sort,
(a = b) requires a and b to have the same sort.

Sorts can be used for static symmetry reduction (Finite_domain).

Types

type symbol = Symbol.symbol

type clause = Term.clause

type sorts

the sorts of a clause set.

Functions

val infer : print:bool -> clause list -> sorts

infers the sorts for the clause set.

val add_constant : sorts ->
       symbol -> symbol -> unit

add_constant sorts constant existing registers the new constant symbol. Its sort is of the result sort of the symbol existing, which must already be registerd.

val constants_partition : sorts -> symbol list list

returns the constants partitioned by sorts.

val max_constant_partition_size : sorts -> int

returns the biggest partition in Sort_inference.constants_partition.

val print : sorts -> unit

prints the sorts.