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.