search

cvc5 / cvc5_pythonic_api

A Z3Py-compatible interface to cvc5
Other
6 stars 9 forks source link

Adding Strings and Sequences to the Pythonic API #86

Closed LaorS closed 1 year ago

LaorS commented 1 year ago

This PR follows z3's python API strings and sequences and adds support for them to cvc5's pythonic API. The signatures of the new functions as well as their documentation are copied from z3.

yoni206 commented 1 year ago

@alex-ozdemir @barrettcw FYI.

Also -- @alex-ozdemir -- Is it desirable to copy the examples from z3? Or should new examples be introduced? How is it done in the rest of the API? I am referring to the examples that appear as comments below the declaration of each function.

alex-ozdemir commented 1 year ago

I'll review this soon.

Is it desirable to copy the examples from z3? Or should new examples be introduced? How is it done in the rest of the API?

I always started with z3's doc-tests, but then modified them freely. For example, if one doc-test failed or didn't apply because of some small difference, I removed it. On the other hand, sometimes the doc-tests from z3 were obviously missing some key functionality, in which case I would add more.

alex-ozdemir commented 1 year ago

Just following up: let me know when you'd like me to take another look.

LaorS commented 1 year ago

I added doc-tests. Still have to fix the formatting- I'm not sure how, is there any tool I can use for that?

Some notes: The functions <,<=,> ,>= only work for string, which is why they are missing in the Sequence class. Also, in cvc5 there are kinds for string leq and lt but there are no corresponding kinds for > and >=. so > and >= are implemented using < and <=. For example, s > t is actually equivalent to t < s.

alex-ozdemir commented 1 year ago

I added doc-tests. Still have to fix the formatting- I'm not sure how, is there any tool I can use for that?

Yes. You should use the black formatter.

  1. Merge the latest main branch into your branch.
  2. Install black using your package manager or these instructions: https://black.readthedocs.io/en/stable/getting_started.html#installation
  3. In the repo, run make fmt to format the repo.

Also, in cvc5 there are kinds for string leq and lt but there are no corresponding kinds for > and >=. so > and >= are implemented using < and <=. For example, s > t is actually equivalent to t < s.

This makes sense.

LaorS commented 1 year ago

Just following up: let me know when you'd like me to take another look.

It's ready for you to take another look.

alex-ozdemir commented 1 year ago

It's ready for you to take another look.

This PR doesn't seem to be quite ready yet: you still need to merge the latest main into it. I'd recommend reverting your formatting commit first, so that the merge isn't too messy.

LaorS commented 1 year ago

Merged latest main. PR is ready for review.

LaorS commented 1 year ago
  • isString and isSequence appear undefined

They are implemented here https://github.com/cvc5/cvc5/blob/main/src/api/python/cvc5.pxi#L3084C6-L3084C6

alex-ozdemir commented 1 year ago

Okay, this is good to go. Nice work!

yoni206 commented 1 year ago

@barrettcw FYI