module AssignmentSet: Main type for partial assignments of elements to variables.
Basic type definition.
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 :
string list -> assignment_set -> int array list
List all tuples the first-order assignment
asg assigns to
in order in which
vars are given.
elems are are all elements.
val fo_assgn_to_list :
int list ->
Formula.fo_var list ->
(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.