module Distinguish:`sig`

..`end`

Distinguish sets of structures by formulas.

`type `

logic =

`|` |
`FO` |

`|` |
`ExFO` |

`|` |
`GuardedFO` |

`|` |
`ExGuardedFO` |

`val predicates_partition : ``bool Pervasives.ref`

If set, predicates paritition the universe (are disjoint and total).

`val atoms : ``Structure.structure -> int array -> Formula.formula list`

The list of literals which hold for a tuple on a structure,
i.e. the atomic type of this tuple.

`val ntype : ``?existential:bool ->`

Structure.structure -> int -> int array -> Formula.formula

The

`?existential`

`qr`

-type in `length of tuple`

-variables
of `tuple`

in `struc`

.`val ntypes : ``?existential:bool ->`

Structure.structure -> qr:int -> k:int -> Formula.formula list

All

`?existential`

types of rank `qr`

of all `k`

-tuples in `struc`

.`val guards : ``Structure.structure ->`

int array ->

(int list * Formula.var list * int array * int array * Formula.formula) list

Generate all guarded substitutions of

`tuple`

with the guards.
A subst-tuple is a substitution of `tuple`

if it has the same length.
A subst-tuple is a guarded substitution of `tuple`

if a permuted
sub-tuple a of subst-tuple containig at least one element of
the original `tuple`

is in some relation R in the structure `struc`

.
The guard for subst-tuple is then the atomic formula R(x_i1, ..., x_iK)
such that a = (subst-tuple_i1, ..., subst-tuple_iK) and R(a) holds.
For every subst-tuple as above we return the quintuple:
<new elems in subst-tuple, their indices as vars, subst-tuple, a, guard>.
We do not generate subst-tuples with repeated new elements.`val guard_tuple_str : ``int list * Formula.var list * int array * int array * Formula.formula ->`

string

Print a guard tuple, as returned above, to string.

`val guarded_type : ``?existential:bool ->`

Structure.structure -> int -> int array -> Formula.formula

Guarded

`?existential`

`qr`

-type in `length of tuple`

-variables
of `tuple`

in `struc`

.`val guarded_types : ``?existential:bool ->`

Structure.structure -> qr:int -> k:int -> Formula.formula list

All guarded

`?existential`

types of rank `qr`

of
guarded `k`

-tuples in `struc`

.`val tc_max : ``Structure.structure -> Formula.formula -> ?from:int -> int -> int option`

Maximum n between

`from`

and `upto`

such that n-step TC of phi holds. *`val tc_atomic : ``?positive:bool ->`

?repeat_vars:bool ->

Structure.structure -> ?from:int -> int -> (int * Formula.formula) list

Pairs (n, phi) such that phi is a two-variable

`?positive`

atomic formula
and the n-step transitive closure of phi holds somewhere on `struc`

.
The n is between `?from`

- `upto`

, at least 1, phi has 2 free variables. *`val tc_atomic_distinguish : ``?positive:bool ->`

?repeat_vars:bool ->

Structure.structure list ->

Structure.structure list -> int -> Formula.formula option

Find a upto-

`n`

-step transitive closures of two-variable `?positive`

atomic
formulas that hold on all `pos_strucs`

and on no `neg_strucs`

. *`val distinguish_result_tc : ``(int * Formula.formula) list option Pervasives.ref`

Number of steps and base formula if distinguish returns a TC.

`val compare_types : ``(Formula.formula -> Formula.formula -> int) Pervasives.ref`

Order on types that we use to select the minimal ones.

`val min_type_omitting : ``?logic:logic ->`

qr:int ->

k:int ->

Formula.formula list -> Structure.structure -> Formula.formula option

Find the minimal

`logic`

-type of `struc`

not included in `neg_types`

and with at most `qr`

quantifiers and `k`

variables.`val distinguish_upto : ``?logic:logic ->`

qr:int ->

k:int ->

Structure.structure list ->

Structure.structure list -> Formula.formula option

Find a

`logic`

-formula with at most `qr`

quantifiers and `k`

variables
which holds on all `pos_strucs`

and on no `neg_strucs`

.
Leaves free variables which are implicitly quantified existentially.`val distinguish_guess : ``?positive:bool ->`

d1:int ->

d2:int ->

k:int ->

Structure.structure list ->

Structure.structure list -> Formula.formula option

Find a formula with at most

`d1`

unary and `d2`

binary definitions each with
`k`

quantified variables holding on all `pos_strucs`

and no `neg_strucs`

.`val distinguish : ``?use_tc:bool ->`

?skip_outer_exists:bool ->

?ex:bool ->

?guess:bool ->

Structure.structure list -> Structure.structure list -> Formula.formula

Find a formula holding on all

`pos_strucs`

and on no `neg_strucs`

.
Leaves free variables (existential) if `skip_outer_exists`

is set.