AlleAlle: Bounded relational model finding with unbounded data
Relational model finding is a successful technique which has been used in a wide range of problems during the last decade. This success is partly due to the fact that many problems contain relational structures which can be explored using relational model finders. Although these model finders allow for the exploration of such structures they often struggle with incorporating the non-relational elements. In this paper we introduce AlleAlle, a method and language that integrates reasoning on both relational structure and non-relational elements —the data— of a problem. By combining first order logic with Codd’s relational algebra, transitive closure, and optimization criteria, we obtain a rich input language for expressing constraints on both relational and scalar values. We present the semantics of AlleAlle and the translation of AlleAlle specifications to SMT constraints, and use the off-the-shelf SMT solver Z3 to find solutions. We evaluate AlleAlle by comparing its performance with Kodkod, a state-of-the-art relational model finder, and by encoding a solution to the optimal package resolution problem. Initial benchmarking show that although the translation times of AlleAlle can be improved, the resulting SMT constraints can efficiently be solved by the underlying solver.
|First order logic, Relational algebra, SMT solvers, Model finding, Constraint problems, Constraint optimization problems|
|ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software|
|Organisation||Centrum Wiskunde & Informatica, Amsterdam, The Netherlands|
Stoel, J, van der Storm, T, & Vinju, J.J. (2019). AlleAlle: Bounded relational model finding with unbounded data. In Onward! 2019 - Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2019 (pp. 46–61). doi:10.1145/3359591.3359726