module AssignmentSet:Main type for partial assignments of elements to variables.`sig`

..`end`

`type `

assignment_set =

`|` |
`Empty` |

`|` |
`Any` |

`|` |
`FO of ` |

`|` |
`MSO 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 an MSO variable X, we keep a list of elements which must be and
which must not be in X. 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.