Oriented Metrics for Bottom-Up Enumerative Synthesis

TL;DR

This paper tackles the challenge of vast search spaces in syntax-guided synthesis by introducing oriented metrics (orimetrics) that handle directional operations, such as string manipulation and bitwise operations. It presents a principled construction of orimetrics from operator inverse semantics and demonstrates how they enable four generic reductions—pruning, factorization, refinement, and learning—within a CEGAR-style loop. The authors implement these ideas in Merlin, achieving substantial speedups over state-of-the-art solvers on string and bitvector benchmarks. The framework is generic and can be instantiated with different orimetrics and enumeration orders, highlighting the practical impact of incorporating orientation-aware distance notions into bottom-up enumerative synthesis. Overall, the work provides a unified foundation for pruning and guiding search in SyGuS problems with oriented domains, with strong empirical validation.

Abstract

In syntax-guided synthesis, one of the challenges is to reduce the enormous size of the search space. We observe that most search spaces are not just flat sets of programs, but can be endowed with a structure that we call an oriented metric. Oriented metrics measure the distance between programs, like ordinary metrics do, but are designed for settings in which operations have an orientation. Our focus is on the string and the bitvector domains, where operations like concatenation and bitwise conjunction transform an input into an output in a way that is not symmetric. We develop several new oriented metrics for these domains. Oriented metrics are designed for search space reduction, and we present four techniques: (i) pruning the search space to a ball around the ground truth, (ii) factorizing the search space by an equivalence that is induced by the oriented metric, (iii) abstracting the oriented metric (and hence the equivalence) and refining it, and (iv) improving the enumeration order by learning from abstract information. We acknowledge that these techniques are inspired by developments in the literature. By understanding their roots in oriented metrics, we can substantially increase their applicability and efficiency. We have integrated these techniques into a new synthesis algorithm and implemented the algorithm in a new solver. Notably, our solver is generic in the oriented metric over which it computes. We conducted experiments in the string and the bitvector domains, and consistently improve the performance over the state-of-the-art by more than an order of magnitude.

Figures (4)

• Figure 1: CEGAR loop for synthesis.
• Figure 2: Example grammar $\mathcal{G}$.
• Figure 3: Input-output examples $(\mathit{I}, O)$.
• Figure 4: Search space and enumeration order.