Add interface to cvc5 sygus bindings

[ndrwbrwn]

Hi!

I've been working on a project in OCaml that benefits from an interface to a SyGuS solver. Cvc5 is one of those solvers, and this project seems to be the best set of bindings out there, so the quickest and easiest option for me to get SyGuS support in OCaml was to hack it onto your bindings.

In this PR is a working, basic implementation of exactly as much SyGuS stuff as I needed:

• Creating and working with Grammars
• Querying SynthResults
• Declaring SyGuS variables
• Declaring synthesis functions (with and without grammars)
• Adding SyGuS constraints and assumptions

There's a couple other SyGuS-relevant functions here and there that I haven't bothered to add, mostly because I didn't need them. But this is easily enough to get started with Cvc5 SyGuS using these bindings, you can implement the examples from the Cvc5 docs and it all works.

Also, my system complained about the use of int in those original loops, so I switched it out for size_t. Since I first wrote these bindings, I see it's been changed for long unsigned int anyway (in 7d8a1a6), which fixes the compiler error, but AFAIK size_t is technically a more accurate type anyway, so I left my version in this PR. Happy to revert, up to you.

Hopefully someone else can benefit from the SyGuS interface :)

[joaomhmpereira]

Hi!

Thank you so much for the contribution! I’m glad these bindings were useful for your SyGuS project. Everything looks good to me, and I agree that size_t is more accurate here.

Assuming the build workflow finishes cleanly, I’m happy to merge this.

Thanks again!

[ndrwbrwn]

No worries, happy to contribute. Being able to lean on an existing implementation of the Term/TermManager refcounting stuff was super helpful. Thanks for the quick response, too!