Skip to main content

Functional Synthesis with Examples

Author(s): Fedyukovich, Grigory; Gupta, Aarti

To refer to this page use:
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.
Publication Date: 2019
Citation: Fedyukovich, Grigory, and Aarti Gupta. "Functional Synthesis with Examples." In International Conference on Principles and Practice of Constraint Programming (2019): pp. 547-564. doi:10.1007/978-3-030-30048-7_32
DOI: 10.1007/978-3-030-30048-7_32
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 547 - 564
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Principles and Practice of Constraint Programming
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.