constraint solving based synthesis
原书第五章的内容
The key idea in applying constraint solving to program synthesis is encoding both the specification and the syntactic program restrictions in a single formula so that any true model corresponds to a correct program.
Basically, the variables in the formula corresponds to a choice of subexpression in the desired program (like production rule in a CFG, for example).
component based synthesis
A classical example of encoding the language and the spec into SAT/SMT constraints directly is component-based synthesis. blafpfwb use this method when introducing distinguishing input.
In component-based synthesis, our syntactic bias is a library of allowed components. Each component is a domain-specific function that may be used in the desired program. Usually there are no syntactic restrictions on their composition.
Assume every program uses all provided components, each exactly once (multiple uses of a component can be achieved by including multiple copies in the library).
to solve the problem, we need to encode that the program :
- is well-formed
- uses all components according to their semantics
- is consistent with the spec
Suppose the spec is a set of examples. For each input and output of a component, we introduce a variable encoding its line number. Also, for every example pair in the spec, we introduce a variable for every input/output of a component, encoding the dataflow.
solver-aided programming
the community built several frameworks for representing synthesis problem in a high-level programming language. solver-aided programming augment high-level programming languages with new constructs that require constraint solving to be materialized. See torlakLightweightSymbolicVirtual2013 for Rosette.