Support check_sat statement for Alt-Ergo language

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

BSD 2-Clause "Simplified" License

80 stars 17 forks source link

Support check_sat statement for Alt-Ergo language #140

Closed Halbaroth closed 1 year ago

Halbaroth commented 1 year ago

This PR adds the keyword check_sat for the native language of Alt-Ergo.

Besides, I modified the Prove description for statement. Now, the payload of Prove can extend the assumptions and the goals of the current sequent.

Halbaroth commented 1 year ago

Done :)

Halbaroth commented 1 year ago

Done. I also tested the PR still works with my PR on Alt-Ergo ;)