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
240 stars 33 forks source link

make extractModel work on strings #595

Closed eax- closed 3 years ago

eax- commented 3 years ago

Currently there seem to be no way to extract models if they contain strings or characters (e.g. extractModel <$> prove ( \x -> x .== (literal "") ) :: IO (Maybe String) fails) because SatModel has no appropriate instances defined. This PR is to create these instances. Tested with the latest z3 (4.8.12).

LeventErkok commented 3 years ago

@eax-

Thanks..

String constants are now settled in SMTLib, following https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml So, \x notation is no longer needed nor is supported in newer z3's.

If you can make a new pull request that drops the \x part, I'd be happy to merge.

eax- commented 3 years ago

Indeed, thank you, I was using the wrong z3 binary.

LeventErkok commented 3 years ago

@eax-

Great! If you can tell me your full name, I'd like to add it to the acknowledgements section.

eax- commented 3 years ago

Thanks, I'd like to just stay "eax" if you don't mind.

LeventErkok commented 3 years ago

No worries. Thanks for the contribution.