solver methods, model, type-checker

cvc5 / cvc5_pythonic_api

A Z3Py-compatible interface to cvc5

Other

6 stars 9 forks source link

solver methods, model, type-checker #4

Closed alex-ozdemir closed 3 years ago

alex-ozdemir commented 3 years ago

Add solver methods, which include methods for getting a model.

One of these methods references the Boolean sort constructor function, which I added.

Also added the model class, which includes some machinery for finding all declared constants.

Finally, set up a type-checker, and added a few ignore annotations. I'll be able to remove some of these if we set up type stubs for the base library.

alex-ozdemir commented 3 years ago

Okay, I think I've addressed your comments. Thanks for the review! Let me know if you have other requests/comments/questions.