module Class:`sig`

..`end`

Represent regular classes of structures.

`type `

struct_sum =

`|` |
`Struct of ` |

`|` |
`Sum of ` |

Sum of structures or specified classes with relation replacements.

type`structure_class =`

`(string * struct_sum list) list`

Class of regular structures.

`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.

`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) ...

`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.

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