Module Assignments

module Assignments: sig .. end

Handling partial assignments of elements to variables.

Basic Type Definition

type assignment_set =

`\|`	`Empty`
`\|`	`Any`
`\|`	`FO of string * (int * 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 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.

val compare_vars : string -> string -> int

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

List or Set Type

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

Join

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.

Equality

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.

Sum

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.

Projection

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.

Universality

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

Complement

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

Creating Assignments from Variables and Element Tuples

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.

Join a Relation with an Assignment

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

Basic univeral variable compression

val compress : int -> assignment_set -> assignment_set

Compress the given assignment set, use number of elements.