CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1908.09481v1 |
| _version_ | 1819277781174845440 |
|---|---|
| author | Fadil Kallat Tristan Schäfer Anna Vasileva |
| author_facet | Fadil Kallat Tristan Schäfer Anna Vasileva |
| author_sort | Fadil Kallat |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-24T00:01:34Z |
| format | Article |
| id | doaj.art-9136cd5bcbe0401ab50c41c736710019 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-24T00:01:34Z |
| publishDate | 2019-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-9136cd5bcbe0401ab50c41c7367100192022-12-21T17:25:07ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-08-01301Proc. PxTP 2019516510.4204/EPTCS.301.7:1CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo TheoriesFadil Kallat0Tristan Schäfer1Anna Vasileva2 Technical University of Dortmund, Germany Technical University of Dortmund, Germany 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.http://arxiv.org/pdf/1908.09481v1 |
| spellingShingle | Fadil Kallat Tristan Schäfer Anna Vasileva CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories Electronic Proceedings in Theoretical Computer Science |
| title | CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories |
| title_full | CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories |
| title_fullStr | CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories |
| title_full_unstemmed | CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories |
| title_short | CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories |
| title_sort | cls smt bringing together combinatory logic synthesis and satisfiability modulo theories |
| url | http://arxiv.org/pdf/1908.09481v1 |
| work_keys_str_mv | AT fadilkallat clssmtbringingtogethercombinatorylogicsynthesisandsatisfiabilitymodulotheories AT tristanschafer clssmtbringingtogethercombinatorylogicsynthesisandsatisfiabilitymodulotheories AT annavasileva clssmtbringingtogethercombinatorylogicsynthesisandsatisfiabilitymodulotheories |