Functional Synthesis With Examples
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING, CP 2019(2019)
摘要
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 for all there exists-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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络