search

IagoAbal / haskell-z3

Haskell bindings to Microsoft's Z3 API (unofficial).
Other
57 stars 43 forks source link

Lift a few more functions from the tactics API and examples from the Z3 tutorial #62

Closed maurobringolf closed 3 years ago

maurobringolf commented 3 years ago

I looked a bit into the Z3 tutorial and thought the examples from there might make some good tests for us. So I added a few of them. I tried quite a few more, but sometimes failed because examples use features that are either not accessible through the API or result in slightly different behavior.

During this process I made some minor improvements in both Z3.Base and Z3.Monad:

  1. Added repeatTactic, applyResultToString, goalToString

  2. Removed an unused integer parameter from the API of mkSeqConcat. I presume this was used as the length of arguments in an earlier version, but marshalArrayLen takes care of that.