Datalog as a monotonic SMT theory, implemented as a Z3 user propagator.
The canonical version of this tool is in the Zenodo artifact for the POPL'23 paper "From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems" by Aaron Bembenek, Michael Greenberg, and Stephen Chong.