Module Class

module Class: sig .. end

Represent regular classes of structures.

Basic Type Definition.

type struct_sum =

`\|`	`Struct of Structure.structure`
`\|`	`Sum of ((string * string) list * (string * (Formula.fo_var list * Formula.formula)) list)`

Sum of structures or specified classes with relation replacements.

type structure_class = (string * struct_sum list) list

Class of regular structures.

Printing functions

val struct_sum_str : struct_sum -> string

Print a class definition (right hand side) as string.

val str : structure_class -> string

Print a regular structure class as a string, using its definition.

Split with atom replacing.

val split : Formula.formula -> struct_sum -> Formula.formula

Split of a sentence on a class definition is either true/false if the class definition is a Struct s (depending on whether s |= phi or not), or a new sentence psi such that, e.g. for the sum A:c + B:d, following is replaced:

each exists x (phi) by (exists "A:c:x" phi) or (exists "B:d:x" phi)
each exists X (phi) by exists "A:c:X" "B:d:X" (phi), x in X-> x in X1 or X2
dually the forall quantifiers
each resulting atom, say R(A:c:x, B:d:y), as given in WITH reldefs.

val split_simplify : ?get_ids:bool -> Formula.formula -> struct_sum -> Formula.formula

Split the formula as above and simplify by replacing trivially true or false atoms such as L(x:R) ...

Decomposing a formula for a class definition.

val decompose : ?get_ids:bool ->
       Formula.formula -> struct_sum -> (string * Formula.formula) list list

Compute a decomposition of a formula on a given class definition.

WMSO model checking on inductive structures

val check : string -> structure_class -> Formula.formula -> bool