Module Distinguish

module Distinguish: sig .. end

Distinguish sets of structures by formulas.

type logic =

`\|`	`FO`
`\|`	`ExFO`
`\|`	`GuardedFO`
`\|`	`ExGuardedFO`

Atoms and FO Types

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.

Guards and Guarded Types

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.

Transitive Closure Formulas

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.

Distinguishing Structure Sets

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.