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:
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