Module AssignmentSet

module AssignmentSet: sig .. end

Main type for partial assignments of elements to variables.

Basic type definition.

type assignment_set =

`\|`	`Empty`
`\|`	`Any`
`\|`	`FO of string * (int * assignment_set) list`
`\|`	`MSO of string * ((Structure.Elems.t * Structure.Elems.t) * assignment_set) list`
`\|`	`Real of (Poly.polynomial * Formula.sign_op) list list`

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.

Printing and small helper functions.

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.