search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

RegExp.All translates to re.allchar, not re.all as the docs would imply #616

Closed Torrencem closed 2 years ago

Torrencem commented 2 years ago

According to the docs for the UnicodeStrings theory, there are two SMT-Lib regexps:

        ; Constant denoting the set of all strings 
        (re.all RegLan)

        ; Constant denoting the set of all strings of length 1
        (re.allchar RegLan)

from the documentation of SBV, we'd expect All to translate into re.all (the regular expressioni that accepts every string). However, it is instead translated to re.allchar. It would make more sense if there were a function allchar that translated to re.allchar, and if All translated to re.all.

LeventErkok commented 2 years ago

Thanks! Looks like there's a couple of problems with the pull request (nothing big); if you could update those I'll merge the patch. (I added review comments)

Torrencem commented 2 years ago

That's odd, I'm having trouble finding the review comments (I know github has been kind of borked today)

LeventErkok commented 2 years ago

The build on the PR is failing, you can see it there. Or try: https://github.com/LeventErkok/sbv/pull/617

LeventErkok commented 2 years ago

Thanks!

I've also added everything, nothing, and anyChar to regexeps, which might come in handy:

https://github.com/LeventErkok/sbv/blob/b5e25f870b58997883f31b3e4d20d30b53672142/Data/SBV/RegExp.hs#L128-L147

Also added the Power constructor:

https://github.com/LeventErkok/sbv/blob/b5e25f870b58997883f31b3e4d20d30b53672142/Data/SBV/Core/Symbolic.hs#L364

where Power n r is shorthand for Loop n n r.