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.

翻译：基于组件的合成（Component-based Synthesis, CBS）通过从库组件生成无循环程序来满足逻辑查询。尽管表达性强的规格和精确的查询简化了求解空间，但这也使得传统CBS过程寻找可行执行路径的难度显著增加。随着约束条件愈发精确，搜索必须在日益稀疏的有效路径空间中导航。我们通过推理探索路径之间的\emph{逻辑相似性}应对这一挑战。我们考虑配备有精化类型（refinement-type）规格的库方法，这些规格为基础类型添加逻辑限定符以精确约束值空间。为高效探索该空间，我们提出液态树自动机（Liquid Tree Automata, LTA），这是一种新型树自动机变体，其构造由精化类型规则驱动。LTA利用子类型约束在搜索过程中识别并主动合并语义相似的状态。这种合并避免了等效路径的冗余探索，显著提升了合成效率。我们将该方法实现为名为Hegel的工具。评估表明，Hegel能够合成解决复杂查询的方案，而这些查询超出了现有最先进工具的能力范围。