Datatypes. - Githubissues

cvc5 / cvc5_pythonic_api

A Z3Py-compatible interface to cvc5

Other

6 stars 9 forks source link

Datatypes. #36

Closed alex-ozdemir closed 3 years ago

alex-ozdemir commented 3 years ago

The idea it to use 5 new classes:

Datatype: for declaring new data-types.
DatatypeSortRef: for declared datatypes.
Datatype{Constructor,Selector,Recognizer}Ref: for {constructors, selectors, testers} of declared datatypes

The reason that the last three are not just standard functions is that they use a different kind of apply in the CVC4 API, and you get their domain/codomain/metadata in a different way.

alex-ozdemir commented 3 years ago

Thanks for reviewing! I think I have responded. Let me know if you have followup comments.