E3Solver: decision tree unification by enumeration

TL;DR

E3Solver is a decision tree-based solver for programming-by-example that unifies individual example solutions into a comprehensive decision tree, efficiently solving all instances in its category during the SyGuS Competition.

Contribution

It introduces a novel unification approach using enumeration and decision trees for PBE, achieving fast solutions for complex instances.

Findings

Solved all 750 instances in the bitvector sub-track

Operates in a few seconds per instance

Provides publicly available implementation

Abstract

We introduce E3Solver, a unification-based solver for programming-by-example (PBE) participating in the 2017 edition of the SyGuS Competition. Our tool proceeds in two phases. First, for each individual example, we enumerate a terminal expression consistent with it. Then, we unify these expressions using conditional expressions in a decision tree. To this end, a suitable condition is enumerated for each pair of conflicting examples. This incremental method terminates after fitting all examples in the decision tree. E3Solver solves all 750 instances in the bitvector sub-track in an average time of few seconds each. We make our contributions publicly available (https://github.com/sygus-tools)