PLDI'18 | Program Synthesis using Conflict-Driven Learning

UniverseFly / Readings

Reading valuable research ideas while taking notes through GitHub Issues

0 stars 0 forks source link

Open UniverseFly opened 2 years ago

UniverseFly commented 2 years ago

UniverseFly commented 2 years ago

Decide: P is a partial program with holes. Decide which hole to fill with which component (production rule) such that P' satisfies the knowledge base (contains learned lemmas). Lemmas encode what the program structure should be like.
Deduce: check if P is feasible according to the DSL semantics.
Analyze conflict: Add new lemmas to the knowledge based according to the unsatisfiable core.