Z3_OP_RA_* functions. Theory, use cases, worked examples

[DavidPratten]

Hi

I'm researching the connection between Z3 and the Relational Model. Could anyone point me to doco/references that unpack the motivation, theory, use cases, and worked examples for the built-in functions:

Z3_OP_RA_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.
Z3_OP_RA_EMPTY: Creates the empty relation.
Z3_OP_RA_IS_EMPTY: Tests if the relation is empty.
Z3_OP_RA_JOIN: Create the relational join.
Z3_OP_RA_UNION: Create the union or convex hull of two relations. The function takes two arguments.
Z3_OP_RA_WIDEN: Widen two relations. The function takes two arguments.
Z3_OP_RA_PROJECT: Project the columns (provided as numbers in the parameters). The function takes one argument.
Z3_OP_RA_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.
Z3_OP_RA_NEGATION_FILTER: 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 in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.
Z3_OP_RA_RENAME: rename columns in the relation. The function takes one argument. The parameters contain the renaming as a cycle.
Z3_OP_RA_COMPLEMENT: Complement the relation.
Z3_OP_RA_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.
Z3_OP_RA_CLONE: Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for Z3_OP_RA_UNION to perform destructive updates to the first argument.

C API

Thanks

David

[NikolajBjorner]

This is pretty old functionality. It was introduced for Datalog solving. It doesn't surface for standard uses.
The relevant paper is in CAV 2011.
https://link.springer.com/chapter/10.1007/978-3-642-22110-1_36

[DavidPratten]

Thanks Nikola, very exactly what I was looking for. David