module Assignments:`sig`

..`end`

Handling partial assignments of elements to variables.

`type `

assignment_set =

`|` |
`Empty` |

`|` |
`Any` |

`|` |
`FO of ` |

`|` |
`Real of ` |

We represent assignment sets as trees. Below a variable we keep a
tree of all assignments which assign this variable the same value.
For real-valued variables, we keep disjunctions of polynomials.
If an assignment set is not Empty, then it cannot contain Empty leafs.

`val assigned_vars : ``Formula.var list -> assignment_set -> Formula.var list`

Variables assigned in an assignement set.

`val str : ``assignment_set -> string`

Print the given assignment as string.

`val named_str : ``Structure.structure -> assignment_set -> string`

Print the given assignment as string, using element names.

`val choose_fo : ``(string * int) list -> assignment_set -> (string * int) list`

Select an arbitrary assignment for first-order variables with the
given names and default values. Raise

`Not_found`

if the assignment
set is empty.`val assigned_elems : ``string -> assignment_set -> int list`

Elements assigned to a given FO variable. Assumes the variable appears.

`val tuples : ``Structure.Elems.t ->`

string list -> assignment_set -> int array list

List all tuples the first-order assignment

`asg`

assigns to `vars`

in order in which `vars`

are given. `elems`

are are all elements.`val fo_assgn_to_list : ``int list ->`

Formula.fo_var list ->

assignment_set ->

(Formula.fo_var * Structure.Elems.elt) list list

Convert the FO part of an assingment set into a list of substitutions.

`val fo_assgn_of_list : ``(string * int) list -> assignment_set`

Convert an association list into an assignment for FO variables.

`val compare_vars : ``string -> string -> int`

The order on variables we use; might differ from Formula.compare_vars!

`type `

set_list

Helper type to represent a set or a list of elements with length.

`val set_to_set_list : ``Structure.Elems.t -> set_list Pervasives.ref`

Create a set_list

`val list_to_set_list : ``int list -> set_list Pervasives.ref`

`val slist : ``set_list Pervasives.ref -> int list`

List a set or list ref; changes from set to list if required.

`val sset : ``set_list Pervasives.ref -> Structure.Elems.t`

`val sllen : ``set_list Pervasives.ref -> int`

`val join : ``assignment_set ->`

assignment_set -> assignment_set

This function joins two assignment sets, i.e. if these represent
valuations of two formulas, it computes one for the conjunction.

`val equal_vars : ``?unequal:bool ->`

set_list Pervasives.ref ->

string -> string -> assignment_set -> assignment_set

Enforce that in

`aset`

the variable `u`

is equal to `w`

.
If `unequal`

is set, enforce the opposite.`val sum : ``set_list Pervasives.ref ->`

assignment_set ->

assignment_set -> assignment_set

Sum of two assignments, assuming that

`elems`

are all assignable elements.
We assume that `elems`

are sorted. Corresponds to disjunction of formulas.`val project : ``set_list Pervasives.ref ->`

string -> assignment_set -> assignment_set

Project assignments on a given variable. We assume that

`elems`

are all
elements and are sorted. Corresponds to the existential quantifier.`val project_list : ``set_list Pervasives.ref ->`

assignment_set -> string list -> assignment_set

Projection on a list of variables.

`val universal : ``set_list Pervasives.ref ->`

string -> assignment_set -> assignment_set

Project assignments on a given universal variable. We assume that

`elems`

are all elements and are sorted. Corresponds to the for-all v quantifier.`val universal_list : ``set_list Pervasives.ref ->`

assignment_set -> string list -> assignment_set

`val complement : ``set_list Pervasives.ref ->`

assignment_set -> assignment_set

Complement an assignment set assuming

`elems`

are all assignable elements.
We assume `elems`

are sorted. This corresponds to negation of formulas.`val complement_join : ``set_list Pervasives.ref ->`

assignment_set ->

assignment_set -> assignment_set

Complement

`a`

and join with `aset`

; assumes `a`

is joined with `aset`

`val assignments_of_list : ``set_list Pervasives.ref ->`

string array -> int array list -> assignment_set

Create an assignment set out of an array of variables and a list of
assigned tuples. The first argument are elements of the structure.

`val join_rel : ``assignment_set ->`

string array ->

Structure.Tuples.t ->

Structure.Tuples.t array ->

set_list Pervasives.ref -> assignment_set

`val full_join_rel : ``assignment_set ->`

string array ->

Structure.Tuples.t ->

set_list Pervasives.ref -> assignment_set

`val compress : ``int -> assignment_set -> assignment_set`

Compress the given assignment set, use number of elements.