search

alcides / GeneticEngine

Program Synthesis framework that features heuristics methods (e.g., Genetic Programming) and grammars are defined in Python dataclasses
36 stars 7 forks source link

Liquid Types #8

Open alcides opened 3 years ago

alcides commented 3 years ago

(Ab)use Annotated types to refer to the previous fields in the object, or place any SMT-encodable restriction on the field.

A corresponding metahandler will be needed to synthesize based on the previous value, using an SMTSolver

An example of a possible syntax:

class Range(object):
   start : AnnotatedType[int, "start > 0"]
   end : AnnotatedType[int,"end > start"]
alcides commented 1 year ago

Example in #53

alcides commented 1 month ago

Support for SMT-based meta handlers has been removed, to give way to Dependent Types.

You can encode dependencies in SMT meta handlers using dependent, but that will eagerly evaluate the left-hand side (dependant) first, and use its concrete value in the dependent SMT-expression, inlining it.

It would be interesting to aggregate the SMT-based restrictions and try to solve it at the end, as a secondary strategy (will work if "terminals" are ints or SMT-supported datatypes.