Functional Synthesis with Examples

Grigory Fedyukovich, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Functional synthesis (FS) aims at generating an implementation from a declarative specification over sets of designated input and output variables. Traditionally, FS tasks are formulated as -formulas, where input variables are universally quantified and output variables are existentially quantified. State-of-the-art approaches to FS proceed by eliminating existential quantifiers and extracting Skolem functions, which are then turned into implementations. Related applications benefit from having concise (i.e., compact and comprehensive) Skolem functions. In this paper, we present an approach for extracting concise Skolem functions for FS tasks specified as examples, i.e., tuples of concrete values of integer variables. Our approach builds a decision tree from relationships between inputs and outputs and preconditions that classify all examples into subsets that share the same input-output relationship. We also present an extension that is applied to hybrid FS tasks, which are formulated in part by examples and in part by arbitrary declarative specifications. Our approach is implemented on top of a functional synthesizer AE-VAL and evaluated on a set of reactive synthesis benchmarks enhanced with examples. Solutions produced by our tool are an order of magnitude smaller than ones produced by the baseline AE-VAL.

Original languageEnglish (US)
Title of host publicationPrinciples and Practice of Constraint Programming - 25th International Conference, CP 2019, Proceedings
EditorsThomas Schiex, Simon de Givry
PublisherSpringer
Pages547-564
Number of pages18
ISBN (Print)9783030300470
DOIs
StatePublished - Jan 1 2019
Event25th International Conference on Principles and Practice of Constraint Programming, CP 2019 - Stamford , United States
Duration: Sep 30 2019Oct 4 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11802 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Principles and Practice of Constraint Programming, CP 2019
CountryUnited States
CityStamford
Period9/30/1910/4/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Functional Synthesis with Examples'. Together they form a unique fingerprint.

Cite this