Total: 1
Two fundamental challenges in program synthesis, i.e. learning programs from specifications, are (1) program correctness and (2) search efficiency. We claim logical constraints can address both: (1) by expressing strong requirements on solutions and (2) due to being effective at eliminating non-solutions. When learning from examples, a hypothesis failing on an example means that (a class of) related programs fail as well. We encode these classes into constraints, thereby pruning away many a failing hypothesis. We are expanding this method with failure explanation: identify failing sub-programs the related programs of which can be eliminated as well. In addition to reasoning about examples, programming involves ensuring general properties are not violated. Inspired by the synthesis of functional programs, we intend to encode correctness properties as well as runtime complexity bounds into constraints.