Annotations

[alcides]

The goal is to allow the end-user to use annotations to guide program synthesis.

• [x] Create annotations library with:
  • [x] minimize/maximize annotations for single problem objectives
  • [x] multi_minimize/multi_maximize annotations for single problem objectives
  • [x] property annotation for single property-based testing
  • [x] properties annotation for multi-property-based testing
  • [x] modify PSB2 examples to work with annotations

[alcides]

Mattermost is down.

The initial goal with sugar vs core was to keep core clean of all the extra-information. The SoftRefinedType should not be part of the core (as we cannot synthesise it). Instead, it should be kept as metadata on the sugar layer, which can then be used to create the synthesis problem, but keep the synthesis only to the pure/core language.

Of course, this might not be possible. Did you find any use case that wouldn't allow this separation?

[eduardo-imadeira]

No, I didn't find a specific use case that wouldn't allow that separation.

So could a possible/potential approach be to convert the SoftRefinedType into some equivalent expression in the core language during the desugaring process? For example, convert that SoftRefinedType into a core let expression (i.e. let fitness( ): type = let_exprression_body )

[alcides]

If you can extract the logger infrastructure in a separate PR, I can merge it sooner (and use it in my other development).

[eduardo-imadeira]

I will do it now

[alcides]

I saw the branch, but I didn't see the PR. Can you create it and assign it to me?

[eduardo-imadeira]

@alcides requesting to review this PR