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

TL;DR

This paper presents CLS-SMT, a novel method that integrates SMT solvers with the CL S framework to incorporate domain-specific constraints into automatic software component synthesis.

Contribution

It introduces a translation of CL S tree grammars into SMT functions, enabling the inclusion of additional constraints in the synthesis process.

Findings

Enhanced synthesis with domain constraints demonstrated in experiments

Translation of tree grammars into SMT functions is effective

Framework supports more precise component composition

Abstract

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.