input-output examples [ 8 ] , among others .

Given a semantic constraint specified by a logical formula, and syntactic constraints specified by a context-free grammar, the SyntaxGuided Synthesis (SyGuS) problem is to find an expression that satisfies both the syntactic and semantic constraints. An enumerative approach to solve this problem is to systematically generate all expressions from the syntactic space with some pruning, and has proved to be surprisingly competitive in the newly started competition of SyGuS solvers. It performs well on small to medium sized benchmarks, produces succinct expressions, and has the ability to generalize from input-output examples. However, its performance degrades drastically with the size of the smallest solution. To overcome this limitation, in this paper we propose an alternative approach to solve SyGuS instances. The key idea is to employ a divide-and-conquer approach by separately enumerating (a) smaller expressions that are correct on subsets of inputs, and (b) predicates on inputs that distinguish these subsets. These smaller expressions and predicates are then combined using decision trees to obtain an expression that is correct on all inputs. We view the problem of combining expressions and predicates as a multi-label decision tree learning problem. We propose a novel technique of associating a probability distribution over the set of labels that a sample can be labeled with. This enables us to use standard information-gain based heuristics to learn a compact decision tree. We report a prototype implementation and evaluate it on the benchmarks from the SyGuS 2015 competition. Our tool is able to match the running times and the succinctness of solutions of both standard enumerative solver as well as the latest white-box solvers in most cases. Further, our solver is able to solve a large number of instances from the ICFP class of benchmarks, which were previously unsolved by all existing solvers. The experimental results in this report are outdated. The implementation has undergone several major improvements—the latest version of the tool can be found at https://bitbucket.org/abhishekudupa/eusolver/.