# Module Z3.Relation

`module Relation: `sig` .. `end``
Functions to manipulate Relation expressions

`val is_relation : `Expr.expr -> bool``
Indicates whether the term is of a relation sort.
`val is_store : `Expr.expr -> bool``
Indicates whether the term is an relation store

Insert a record into a relation. The function takes `n+1` arguments, where the first argument is the relation and the remaining `n` elements correspond to the `n` columns of the relation.

`val is_empty : `Expr.expr -> bool``
Indicates whether the term is an empty relation
`val is_is_empty : `Expr.expr -> bool``
Indicates whether the term is a test for the emptiness of a relation
`val is_join : `Expr.expr -> bool``
Indicates whether the term is a relational join
`val is_union : `Expr.expr -> bool``
Indicates whether the term is the union or convex hull of two relations. The function takes two arguments.
`val is_widen : `Expr.expr -> bool``
Indicates whether the term is the widening of two relations The function takes two arguments.
`val is_project : `Expr.expr -> bool``
Indicates whether the term is a projection of columns (provided as numbers in the parameters). The function takes one argument.
`val is_filter : `Expr.expr -> bool``
Indicates whether the term is a relation filter

Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation. So the first column in the relation has index 0.

`val is_negation_filter : `Expr.expr -> bool``
Indicates whether the term is an intersection of a relation with the negation of another.

Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with ( x : expr ) on the columns c1, d1, .., cN, dN.

`val is_rename : `Expr.expr -> bool``
Indicates whether the term is the renaming of a column in a relation

The function takes one argument. The parameters contain the renaming as a cycle.

`val is_complement : `Expr.expr -> bool``
Indicates whether the term is the complement of a relation
`val is_select : `Expr.expr -> bool``
Indicates whether the term is a relational select

Check if a record is an element of the relation. The function takes `n+1` arguments, where the first argument is a relation, and the remaining `n` arguments correspond to a record.

`val is_clone : `Expr.expr -> bool``
Indicates whether the term is a relational clone (copy)

Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind `Relation.is_union` to perform destructive updates to the first argument.

`val get_arity : `Sort.sort -> int``
The arity of the relation sort.
`val get_column_sorts : `Sort.sort -> Sort.sort list``
The sorts of the columns of the relation sort.