Support for reasoning with sets and relational algebras: union, intersection, transpose, join, transitive closure

[vladi7]

Dear Z3 Community,

I am working on an access control research project which involves sets (for the past 6 months). Currently, I am trying to use CVC4 due to the out-of-box support of the Theory of Sets. I would very much like to try to use Z3 to compare the performance and choose the best one for my research problem.

As I currently understand, the way to implement sets in Z3 is to use an array of ints mapped to booleans. But I really need intersection, union, transpose, and join. Another big thing that I need is a transitive closure, and tclosure is actually what got me stuck for a while now.

Is there any example of how I can either use/implement the above set operations in Z3? I would really appreciate any suggestion and am sorry if that is the wrong place to ask questions.

A little information about my use-case: I am attempting to perform bounded model checking and my state-space can be huge and gets bigger each step k. I am currently using smtlibv2 standard, but can use APIs in c++, java, python, or scala, depending on performance.

Thank you,
Vlad

[vladi7]

I appreciate moving this question to the right place for questions.

[vladi7]

I found everything in python except join, is relational join available in Python API?

[NikolajBjorner]

It isn't. There is no first-class support for relational algebra. Some fragments are considered in various places.
For example, https://arxiv.org/abs/1802.07508, and in newer work on solving database queries with aggregates that relies on indirect encodings, such as https://dblp.org/pid/202/8941.html.

[vladi7]

Thanks!