Liquid Tree Automata

TL;DR

Liquid Tree Automata (LTA) is a novel tree automata approach that uses refinement types to efficiently explore logical similarities in component-based program synthesis, enabling the solution of complex queries.

Contribution

We introduce Liquid Tree Automata, a new automata variant that leverages refinement typing and subtyping to merge similar states, improving synthesis efficiency.

Findings

Hegel synthesizes solutions for complex queries beyond existing tools.

LTA effectively merges semantically similar states, reducing redundant exploration.

Our approach significantly improves synthesis performance on challenging benchmarks.

Abstract

Component-based synthesis (CBS) generates loop-free programs from library components to satisfy logical queries. While expressive specifications and precise queries simplify the solution space, they make finding feasible execution paths significantly more difficult for traditional CBS procedures. As constraints become more exact, the search must navigate an increasingly sparse space of valid paths. We address this challenge by reasoning about \emph{logical similarities} between exploration paths. We consider library methods equipped with refinement-type specifications, which enrich base types with logical qualifiers to precisely constrain the value space. To efficiently explore this space, we introduce Liquid Tree Automata (LTA), a novel tree automata variant whose construction is driven by refinement typing rules. LTAs leverage subtyping constraints to identify and eagerly merge semantically similar states during search. This merging avoids redundant exploration of equivalent paths, significantly improving synthesis efficiency. We implement this approach in a tool called Hegel. Our evaluation demonstrates that Hegel synthesizes solutions to complex queries that are beyond the reach of existing state-of-the-art tools.