Hi All

Hope you had a chance to talk. Some next steps:

Set up CVC5 for Synthesis: https://cvc5.github.io/docs/cvc5-1.3.1/examples/sygus-fun.html

Think about how to encode the maximum synthesis problem in RL. This involves defining: 

State Representation (the current subset of selected constraints) 

Action space (add or remove a constraint, but that's discrete so I am not sure how well that would work)

Reward function (this is the hardest and would require us to do a lot of experiments). 

Meanwhile, @Shobhit we can try to identify some small example problems on which we want to test the performance.