Introduction

Introduction

• deciding unrealizability of synthesis not solved
• synthesis wants to find goal, but what if it’s impossible?
• not much work on provability of SyGuS problems
• requires proving all programs in infinite space fails.
• unrealizability proved with finitely many input examples
• devise a way to encode SyGuS over a finite set of examples as a reachability problem in a recursive program.
• challenges
  • infinitely many terms
  • nondeterminism
  • complex specifications

Example

• encode program as..a program
• fig 1. in paper
• encode program as sequence of boolean expressions (true, false)
• generate new program for every new counterexample

SyGuS, Realizability, CEGIS

• RTG: typed regular-tree grammar
  • \[G = (N, \Sigma, S, a, \sigma)\]
  • N = finite set of symbols (e.g., x, y)
  • \(\Sigma\) = ranked alphabet
  • S = initial non-terminals
  • \(\sigma\) = finite set of productions
• sygus problems are on first order theories, ST solver can be used to verify satisfiability of a problem
• sygus on finite set of inputs is unrealizable, then whole problem is unrealizable
• if there is an unrealizable sygus problem from, then for every finite set of examples, a small set may be unrealizable

Unrealizability to unreachability

• reachability problem

Questions:

Summary

In this paper the authors present present a method for determining the unrealizability of a SyGuS problem - or more aptly, determining whether or not a solution to a particular SyGus problem exists. The authors achieve this by actually encoding the grammar of a SyGuS problem into a program itself. Each of the programs generated from the grammar contains an assertion. If the assertion in the program holds after execution, then the problem can be deemed unrealizable.

Programs representing the grammar are generated by creating a series of statements guarded by conditionals clauses with a non-deterministic value (nd()). non-terminal parts of the grammar are guarded by a conditional, but within the program represent a recursive call. At the end of the grammar-program an assertion statements containing a necessary condition for unrealizability is also generated. An execution of the program can then be series of true or false branches which allows for the decoding of the program. And the state of the program checked each time an assertion is reached.

Once the program is generated realizing the unrealizability of a problem means that we just have to search through the space of nd()’s for a program output state which satisfies (or doesn’t) the assertion in the grammar-program.

Strengths

• novelty..don’t need to explore the entire search space
• can be incorporated easily into existing synthesizers

Weaknesses

• limited to SyGuS grammars
• incomplete for proving unrealizability
• may not terminate depending on grammar
• need to limit recursion depth

Summary

Q’s

• What does Nope use as behavioral constraints? Structural constraint? Search strategy?

• behavioral
  • input/output examples/constraints (for checking)
  • assertions in generated grammar-program
• structural
  • SyGuS grammars
  • generated grammar-program
• search strategy
  • CEGIS loop
• Can you give an example of an unrealizable problem over the theory of bit vectors?

constraints:

• (0010 -> 0001)
• (0100 -> 1000)
• (1000 -> 0001)

• (0001 -> 1000)

• Why is unrealizability harder than synthesis?

Unrealizability is harder than synthesis because synthesis can come to a solution before needing to evaluate the infinite program space of a particular grammar. Unrealizability has to prove that no program in the entire infinite space cannot satisfy the given constraints.