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.