Relations, sort-erased

A relation is a set of tuples — (Set (Tuple T₁ … Tⱼ)) — and not a sort of its own: there is no RELATION_SORT. So a relation term is built with the set and tuple constructors, and the operators here are what treat one as a relation.

Tables, in Cvc.Untyped.Theory.Table, are bags of tuples, where duplicates are significant; they have the product, projection, join, grouping and aggregation, but none of the other operators.

cvc5 marks every kind here experimental, "may be changed or removed in future versions".

relAggregate takes its folding function as a term, which Term.lambda builds.

Operators taking no index

def Cvc.Untyped.Term.relJoin [Ω] (lft rgt : Term) : Env Term

Composition: pairs the two relations on lft's last component and rgt's first, dropping it.

Joining (Set (Tuple Int Bool)) with (Set (Tuple Bool String)) gives (Set (Tuple Int String)).

Equations

• lft.relJoin rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.RELATION_JOIN #[lft, rgt]

def Cvc.Untyped.Term.relProduct [Ω] (lft rgt : Term) : Env Term

Cartesian product: every pairing, with the components appended.

(Set (Tuple Int Bool)) and (Set (Tuple Bool String)) give (Set (Tuple Int Bool Bool String)).

Equations

• lft.relProduct rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.RELATION_PRODUCT #[lft, rgt]

def Cvc.Untyped.Term.relTranspose [Ω] (rel : Term) : Env Term

Reverses each tuple's components, so (Set (Tuple Int Bool)) becomes (Set (Tuple Bool Int)).

Equations

• rel.relTranspose = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.RELATION_TRANSPOSE #[rel]

def Cvc.Untyped.Term.relTclosure [Ω] (rel : Term) : Env Term

Transitive closure of a homogeneous binary relation, (Set (Tuple α α)).

Equations

• rel.relTclosure = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.RELATION_TCLOSURE #[rel]

def Cvc.Untyped.Term.relIden [Ω] (rel : Term) : Env Term

The identity relation over a unary relation's elements.

Takes (Set (Tuple α)) and answers (Set (Tuple α α)). cvc5 rejects anything else with Identity operates on non-unary relations.

Equations

• rel.relIden = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.RELATION_IDEN #[rel]

def Cvc.Untyped.Term.relJoinImage [Ω] (rel size : Term) : Env Term

The elements of a binary relation related to at least size others.

Takes (Set (Tuple α β)) and an integer term, and answers the unary relation (Set (Tuple α)).

Equations

• rel.relJoinImage size = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.RELATION_JOIN_IMAGE #[rel, size]

Operators carrying indices

Indices count components from zero, as tupleProject's do, and are what SMT-LIB writes inside (_ rel.project 2 0).

def Cvc.Untyped.Term.relProject [Ω] (indices : Array Nat) (rel : Term) : Env Term

Projects every tuple onto the given components, in the order given.

Tuple projection lifted to a relation, so it reorders and duplicates as readily as it selects.

Equations

• Cvc.Untyped.Term.relProject indices rel = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.RELATION_PROJECT indices tm.mkTermOfOp __do_lift #[rel]

def Cvc.Untyped.Term.relGroup [Ω] (indices : Array Nat) (rel : Term) : Env Term

Partitions the relation, putting tuples that agree on the given components in the same part.

Answers a set of relations: (Set (Tuple Int Bool)) grouped gives (Set (Set (Tuple Int Bool))). SQL's GROUP BY.

Equations

• Cvc.Untyped.Term.relGroup indices rel = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.RELATION_GROUP indices tm.mkTermOfOp __do_lift #[rel]

def Cvc.Untyped.Term.relTableJoin [Ω] (indices : Array (Nat × Nat)) (lft rgt : Term) : Env Term

Equi-join: the product of the two relations, keeping the pairings agreeing on the given pairs.

Each pair is a component of lft and one of rgt that must be equal. The result's sort is the product's, since the indices only filter.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.relAggregate [Ω] (indices : Array Nat) (f init rel : Term) : Env Term

Folds each group of tuples that agree on the given components.

f is a term of function sort (Tuple T₁ … Tⱼ) → T → T — a Term.lambda over a tuple bound variable and an accumulator — and init is the accumulator's starting value. The answer is a (Set T): one entry per group, of the accumulator's sort rather than the relation's.

With no index every tuple is in one group, which is an ordinary fold over the whole relation.

Equations

• One or more equations did not get rendered due to their size.