Formulog: Datalog + SMT + FP
Proceedings of the 4th International Workshop on the Resurgence of Datalog in Academia and Industry (Datalog 2.0), September 2022.
Abstract.
Formulog extends Datalog with mechanisms for constructing logical terms and reasoning about them with satisfiability modulo theories (SMT) solving; a first-order functional language aids inspecting and manipulating complex terms. This combination of features makes it possible to write complex SMT-based program analyses in a way close to their formal specification, while being satisfactorily performant thanks to powerful Datalog optimizations and efficient evaluation techniques.