Semantics-Guided Synthesis

1 INTRODUCTION

• Solver-aided languages cannot express infinite search spaces, while SyGuS is limited to semantics from fixed theories, leaving imperative programs with loops outside its scope.These limitations motivate a framework that can define synthesis problems across both settings.Source: §1 · p. 2
• SemGuS lets users define a program’s syntax and the semantics of its grammar constructs using inference rules.Its framework can specify synthesis problems over imperative programming languages.Source: §1 · pp. 2–3
• Regular-tree grammars specify SemGuS syntax, while Constrained Horn Clauses specify semantics expressible as recursive big-step rules.Unlike SyGuS, SemGuS gives semantics an explicit formalism.Source: §1 · p. 3
• Loops combine infinitely many possible syntactic elaborations with arbitrary execution counts, so SemGuS reasons about sets of loop bodies without an unrolling bound.Bounded unrolling can limit which synthesis problems constraint-based methods can define or solve.Source: §1 · p. 3
• CHC proof search can return a satisfying program when a proof exists or prove unrealizability when the specification is unsatisfiable under the supplied rules.The method encodes the syntax, semantics, and behavioral specification as CHCs.Source: §1 · p. 3
• MESSY implements the CHC-based solver, and SemGuS supports alternative semantics that can sometimes yield solutions more efficiently.The tool is reported as the first to synthesize programs and prove unrealizability for imperative problems with infinitely many programs.Source: §1 · p. 4

2.1 Defining a SemGuS Problem

• SemGuS defines a synthesis problem using a regular tree grammar, its semantics, and a specification of the desired program behavior.The example grammar describes single-loop programs using bitwise-and and bitwise-or assignments.Source: §2.1 · p. 4
• SemGuS expresses imperative semantics as CHCs, allowing recursively defined big-step rules for constructs such as loops.Each grammar production can have semantic rules expressed as CHCs.Source: §2.1 · pp. 4–5

2.2 Solving SemGuS Problems

• CHC proof search can return a satisfying program or prove that no program in the search space meets the specification.The query combines syntax and semantic relations for candidate terms against input-output examples.Source: §2.2 · pp. 5–6
• For the single example (6, 9) → 15, MESSY synthesizes a while-loop using bitwise-or, which matches xor on that input.The loop iterates once and sets x to 15.Source: Figure 2 · p. 6, §2.2 · p. 7
• For the full example set, Spacer proves unrealizability using an invariant that the third bit of x is always set for the example (14, 15) → 1.That invariant conflicts with the required output 1; it applies to all programs derived from Start, not just one program.Source: §2.1 · p. 5, §2.2 · p. 7

2.3 Instantiating SemGuS with Other Semantics

• The abstract domain B3 tracks only the third bit yet suffices to prove the xor synthesis problem unrealizable more efficiently than precise semantics.The abstract semantics uses true, false, and ⊤ for that bit.Source: §2.3 · pp. 7–8

3.1 Constrained Horn Clauses

• CHCs encode constraints and uninterpreted relations, and the paper uses them to formalize semantics and solve SemGuS problems.The proof-search encoding treats derivability of Realizable as synthesis and its non-derivability as unrealizability.Source: §3.1 · pp. 8–9

3.2 Trees, Tree Grammars, and Semantics

• A typed regular tree grammar specifies well-typed tree terms through nonterminals, ranked symbols, and productions.Terms generated from the initial nonterminal form the grammar's language.Source: §3.2 · p. 9
• SemGuS assigns each production semantics expressible as CHCs, allowing customized semantics that distinguish it from SyGuS's underlying-theory semantics.The semantics can flexibly track program state and returned values.Source: §3.2 · p. 10

4 SEMANTICS-GUIDED SYNTHESIS AND ITS PROPERTIES

• A SemGuS problem combines a regular tree grammar with production-based semantics and a behavioral formula, and is realizable when a grammar term satisfies that formula.Source: §4 · p. 10

4.1 Unrealizability of SemGuS Problems with Overapproximating Abstract Semantics

• If an overapproximating abstract semantics makes a SemGuS problem unrealizable, the original semantics also makes it unrealizable.The abstraction overapproximates values obtainable under the original semantics, so absence of a desired output establishes unrealizability soundly.Source: §4.1 · p. 11

4.2 Solving Realizable SemGuS Problems with Underapproximating Semantics

• A solution found using an underapproximating semantics is also a solution under the original semantics, but that semantics cannot establish unrealizability.It is exact where defined, while answers may exist outside its defined subset.Source: §4.2 · p. 11

5.1 Solving SemGuS Problems with Counterexample-Guided Inductive Synthesis

• For SemGuS-with-examples problems, the CHC query is sound and complete: a proof yields a grammar term satisfying the examples.General specifications can be handled by embedding this algorithm in a CEGIS loop.Source: §5.1 · p. 12
• CEGIS is sound but incomplete for unrealizability, and some unrealizable problems remain realizable on every finite example set.Thus finite-example unrealizability suffices for the general problem, but failure to prove it on finite examples is inconclusive.Source: §5.1 · p. 13

5.2 Using Flattened Representations of Terms to Solve SemGuS Problems

• Flattened listings encode terms as preorder production sequences to avoid solver difficulties with tree terms represented as algebraic datatypes.Semantic rules inspect the list head and process subterms from left to right.Source: §5.2 · pp. 13–14
• The listing semantics is correct when its input listing consists of the term's preorder listing followed by the output listing.The theorem equates listing-based semantic derivations with the corresponding tree-term derivations.Source: §5.2 · p. 14

6.1 Instantiating SemGuS with an Alternative Exact Semantics

• Vectorized semantics merges multiple examples into one semantic premise, and Theorem 6.1 states that its results match standard semantics example by example.For loops, valuations with false guards are projected to ⊥ while true-guard valuations execute the body; the results are then merged.Source: §6.1 · p. 15

6.2 Using Abstract Semantics in SemGuS to Prove Unrealizability

• The B_i abstract domain tracks one bit, so it often cannot resolve branch conditions and must approximate with ⊤ or evaluate both branches and join them.The same precision issue applies to conditionals and loops.Source: §6.2 · p. 16
• WTrueJoin is more precise and more expensive than WTrueHavoc; it proves bitwise-xor unrealizable where WTrueHavoc cannot.WTrueJoin preserves a known bit by joining loop outcomes, while WTrueHavoc assigns ⊤ when it cannot resolve the guard.Source: §6.2 · p. 17

6.3 Using Underapproximating Semantics in SemGuS for Program Synthesis

• A loop-iteration bound makes the semantics underapproximating: loops exceeding the bound have no proof, while loops executing fewer iterations match standard semantics.The bound is carried in the state and decremented at each iteration.Source: §6.3 · p. 17

6.4 Instantiating SemGuS to Synthesize Regular Expressions

• For regular expressions, deterministic matrix semantics handles nondeterminism that otherwise complicates negative examples.Matrices encode substring matches; concatenation uses Boolean matrix multiplication, and Kleene star combines repeated matches with pointwise logical-or.Source: §6.4 · p. 18
• Encoding strings as integer sequences makes the regular-expression semantics more solver-friendly, with acceptance determined by whether X_r[0,n] is true.Direct string encodings were problematic because string support in CHC solvers was poor and Z3 often segfaulted on CHCs containing strings.Source: §6.4 · p. 18

7.1 Implementing MESSY

• MESSY sends CHCs to Z3, which returns unrealizability or a proof from which MESSY extracts a solution; it also supports three term representations.The representations are algebraic datatypes for trees, and lists or arrays for listings; MESSY can also perform CEGIS for synthesis and unrealizability.Source: §7.1 · p. 19

7.2 Optimizing Imperative SemGuS Problems with Fused Semantics

• Fused semantics evaluates terms during construction, and Theorem 7.1 establishes the optimization's soundness and completeness.The fused syntax relations combine checking a term's validity with checking its semantic behavior.Source: §7.2 · pp. 20–21
• For productions containing loops, fused syntax rules need a separate procedure to ensure the same loop body is synthesized for every iteration.The syntax relations can synthesize the body on the first iteration and pass its representation to semantic relations for later iterations.Source: §7.2 · pp. 20–21
• Fused semantics performs better than ordinary SemGuS syntax relations, while syntax-relation-less CHCs perform similarly to ordinary syntax relations.The fused encoding modifies syntax relations to check semantic behavior as terms are constructed.Source: §7.2 · p. 20

8.1 Benchmarks

• The evaluation uses unrealizable and original LIA SyGuS benchmarks, imperative SemGuS problems, and textbook regular-expression problems.The imperative set includes hand-created problems and variants based on earlier templates; the evaluation also compares MESSY configurations with other tools.Source: §8.1 · pp. 21–22, Table 1 · p. 22

8.2 Q1: Evaluating MESSY on SyGuS Benchmarks

• With random examples, MESSY proved 66/132 SyGuS benchmarks unrealizable, compared with Nay’s 65/132 using standard CEGIS.MESSY and Nay each proved five additional benchmarks using the random-example technique; 67 benchmarks timed out for both.Source: §8.2 · p. 23
• On the 60 original LIA benchmarks, MESSY solved 4/60, ESolver 6/60, and CVC4 59/60; MESSY also solved one benchmark ESolver could not.For synthesis, ESolver solved its solvable benchmarks in under two minutes each, while MESSY took six minutes on two solved benchmarks.Source: §8.2 · p. 23

8.3 Q2: Evaluating MESSY on Imperative Synthesis Benchmarks

• MESSY solved 120/289 imperative benchmarks: 8/67 realizable and 112/222 unrealizable.Ten solved problems had infinite syntactic search spaces and possible infinite loops; another 15 had infinite search spaces without loops.Source: §8.3 · p. 24
• MESSY was more successful at proving unrealizability than synthesizing programs, and discovered lemmas can make even infinite-loop or infinite-space problems quick to solve.The authors suggest CHC-solving overhead makes synthesis relatively harder; without a lemma, even finite-space problems can take a long time.Source: §8.3 · pp. 24–25

8.4 Q3: Evaluating Optimized Methods for Solving SemGuS Problems

• The optimization evaluation compares tree, list, and array term representations, and individual, vectorized, and fused semantics.The semantics comparison uses array representations, while the representation comparison uses vectorized semantics with fused-semantic optimization.Source: §8.4 · p. 25

Effectiveness of Flattened Term Representations.

• For imperative benchmarks, arrays outperform lists and trees; lists solve a strict subset of array-solved benchmarks.Trees solve only one benchmark that arrays do not. Z3’s limited algebraic-datatype support may explain why tree and list encodings more often end in a “stuck on a lemma” error.Source: Effectiveness of Flattened Term… · pp. 25–26
• The three term representations perform similarly on SyGuS benchmarks.The comparison uses vectorized semantics with fused-semantic optimization enabled.Source: Effectiveness of Flattened Term… · p. 25
• Flattened representations are effective, especially arrays, which avoid algebraic datatypes altogether.The runtime figures compare representations on imperative benchmarks solved by at least one representation.Source: Effectiveness of Flattened Term… · p. 26, Figure 7 · p. 26

Effectiveness of the Vectorized and Fused Semantics.

• Imperative coverage rose from 3 realizable and 10 unrealizable benchmarks with individual semantics to 5 realizable and 62 unrealizable with non-fused vectorized semantics.Across SyGuS benchmarks, individual semantics solved 56 unrealizable cases, a strict subset of the 66 solved by vectorized semantics.Source: Effectiveness of the Vectorized and… · p. 26
• For imperative benchmarks, fused vectorized array semantics solved 6 realizable and 91 unrealizable benchmarks, versus 5 realizable and 56 unrealizable with non-fused vectorized arrays.The fused approach was effective, particularly on imperative benchmarks, but 11 unrealizable benchmarks were solvable only with non-fused semantics; list-representation gains were smaller, with Z3 datatype support remaining a bottleneck.Source: Effectiveness of the Vectorized and… · pp. 26–27

8.5 Q4: Evaluating SemGuS and MESSY with Approximate Semantics

• Abstract semantics solved 17 imperative unrealizable benchmarks that exact semantics could not, but added no new solved SyGuS benchmarks.Abstract semantics timed out on at most 15 benchmarks per domain variant, compared with over 200 for exact semantics; abstract realizability results have no meaning. The domains’ handling of addition also limited their usefulness on SyGuS benchmarks.Source: §8.5 · p. 27
• Bounded loop-unrolling semantics synthesized one more program than non-bounded semantics; the factorial program was synthesized at bound 100, but not at 10 or 50.The authors note that the small gain may reflect MESSY’s weaker synthesis performance and that proving candidate correctness through CHCs can be slower than direct execution.Source: §8.5 · pp. 27–28

8.6 Q5: Evaluating SemGuS and MESSY on Regular Expressions

• On regular-expression benchmarks, the CHC-solving approach solved none within 10 minutes, while enumeration solved 5; the authors attribute the difficulty to finding useful lemmas.They suggest the iterative Star rule, string behavior, and unrestricted grammar as likely factors; they also note AlphaRegex reported solving all 25 benchmarks, attributing the difference to CHC overhead and AlphaRegex’s enumeration optimizations.Source: §8.6 · p. 28

• Sketch, Rosette, and FlashMeta tie problem definition to their solving methods and disallow synthesis problems involving infinite search spaces.Sketch and Rosette use solver-aided languages; FlashMeta uses operator witness functions corresponding roughly to inverse semantics.Source: §9 · p. 28
• SyGuS provides a logical framework but cannot express arbitrary syntactic constructs outside a decidable SMT theory; SemGuS instead permits custom semantics and lets the solving procedure follow the problem definition.SyGuS customization is limited to formulas expressible in the background theory, restricting imperative synthesis; SemGuS allows arbitrary first-order constraints and additional relations or arguments.Source: §9 · pp. 28–29
• CVC4’s grammar encoding and SyGuS remain restricted to a background theory, whereas SemGuS uses CHCs for broader semantics and proof search rather than a universally quantified SMT formula.Source: §9 · p. 29
• Unlike imperative synthesizers that rely on templates, MESSY can synthesize from specified languages and prove unrealizability; its CHCs encode both syntax and semantics, unlike Nay’s encoding of possible outputs.The paper states that MESSY can extract a synthesized program when realizable, and identifies it as the only tool for synthesis and unrealizability in general SemGuS problems.Source: §9 · p. 29
• SYNGAR uses predicate abstraction to overapproximate term semantics, while SemGuS also accommodates infinite abstract domains and concrete programming-language semantics.Source: §9 · p. 30

• SemGuS specifies both syntax and semantics, supports imperative and alternative-semantics problems, and is solved by MESSY, which can synthesize programs or prove unrealizability.Source: §10 · p. 30
• MESSY relies on an external CHC solver to infer lemmas, and the authors identify uncertainty about how well CHC solvers can discover lemmas that prune syntactic search spaces.They suggest explicit lemma inference and pruning as a direction that could improve MESSY as a synthesizer.Source: §10 · p. 30
• The authors propose exploring efficient lemma inference with abstract domains and specialized solvers, including enumerative methods that validate proof trees without CHC solving.They report that the abstract domain B_i was inspired by a lemma that proved a benchmark unrealizable.Source: §10 · p. 30

• Both MESSY and Nay solved all easier LimitedConst benchmarks, with comparable runtimes below one second on most cases.Source: A A DETAILED COMPARISON OF MESSY AND… · p. 33
• Table 2 selects LimitedIf and LimitedPlus benchmarks that best distinguish the tools, alongside other benchmarks both tools solve quickly.Source: Table 2 · p. 33, A A DETAILED COMPARISON OF MESSY AND… · p. 33
• Table 2 reports grammar sizes, CEGIS example counts, and total runtimes for CEGIS and Oracle Examples modes; ✗ marks a timeout.Source: Table 2 · p. 33

• The CHC encoding is sound and complete for realizability when user-supplied semantic rules correctly encode the problem.Source: B PROOFS · p. 34
• The CHC representation of a grammar derives exactly the terms belonging to each nonterminal’s language.Source: B PROOFS · p. 34
• Flattened listing semantics corresponds to term-based semantics when the input listing is the term’s preorder listing followed by the output listing.The proof assumes finite derivation height, which assumes the program terminates.Source: B PROOFS · p. 35
• Vectorized semantics agrees with standard semantics exactly when each example’s input and output satisfy the standard term semantics.Source: B PROOFS · p. 35
• The bit-based semantics over B_i is an abstract semantics for G_impv with respect to its standard integer semantics.The proof uses a bit abstraction and concretization forming a Galois connection.Source: B PROOFS · p. 36
• The underapproximating semantics proves only behaviors also admitted by the standard semantics.It adds the constraint i > 0 to the standard semantics.Source: B PROOFS · p. 37
• Fused syntax rules are sound and complete with respect to grammar membership and the original semantic rules.The proof for loops relies on termination.Source: B PROOFS · p. 37