Synthesis with underspecified functions

[Calvin-L]

Sometimes it is useful to write "lenient" specifications, for instance:

return (any [c | c <- connections, c.writeable])

Cozy currently requires all specifications to be fully precise, in the sense that there is only one correct return value. This restricts how efficient its solutions can be when there are multiple possible correct answers and one answer is easier to compute than another.

One possible design that I endorse:

• a function to_relational_form that converts any expression into a relation that describes its set of legal outputs
• synthesis in core.py should be updated to use to_relational_form when checking correctness