CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories

Fadil Kallat
(Technical University of Dortmund, Germany)
Tristan Schäfer
(Technical University of Dortmund, Germany)
Anna Vasileva
(Technical University of Dortmund, Germany)

We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified repository. The framework yields a tree grammar that contains all composed terms that comply with a target type. Type specifications for (CL)S are based on combinatory logic with intersection types. Our approach translates the tree grammar into SMT functions, which allows the consideration of additional domain-specific constraints. We demonstrate the usefulness of our approach in several experiments.

In Giselle Reis and Haniel Barbosa: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving (PxTP 2019), Natal, Brazil, August 26, 2019, Electronic Proceedings in Theoretical Computer Science 301, pp. 51–65.
Published: 23rd August 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.301.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org