在线时间:8:00-16:00
迪恩网络APP
随时随地掌握行业动态
扫描二维码
关注迪恩网络微信公众号
开源软件名称(OpenSource Name):IagoAbal/haskell-z3开源软件地址(OpenSource Url):https://github.com/IagoAbal/haskell-z3开源编程语言(OpenSource Language):Haskell 99.6%开源软件介绍(OpenSource Introduction):Haskell bindings for Microsoft's Z3 (unofficial)These are Haskell bindings for the Z3 theorem prover. We don't provide any high-level interface (e.g. in the form of a Haskell eDSL) here, these bindings are targeted to those who want to build verification tools on top of Z3 in Haskell. State of maintenanceThe library is currently "maintained", meaning that I try to be responsive to new issues and pull requests. Unfortunately I do not have time to investigate issues or to do major work myself. I do try to help those who want to contribute. If someone demonstrates willingness to maintain the library more actively in the long run, then I will be very happy to give the required permissions to become a co-maintainer. In the meantime I will do my best to keep it alive. Supported versions and version policyZ3 releases come out often and sometimes introduce backwards incompatible changes.
In order to avoid churn and
The Z3-4.8.* compatibility
InstallationPreferably use the z3 package.
ExampleMost people use the import Control.Applicative
import Control.Monad ( join )
import Data.Maybe
import qualified Data.Traversable as T
import Z3.Monad
script :: Z3 (Maybe [Integer])
script = do
q1 <- mkFreshIntVar "q1"
q2 <- mkFreshIntVar "q2"
q3 <- mkFreshIntVar "q3"
q4 <- mkFreshIntVar "q4"
_1 <- mkInteger 1
_4 <- mkInteger 4
-- the ith-queen is in the ith-row.
-- qi is the column of the ith-queen
assert =<< mkAnd =<< T.sequence
[ mkLe _1 q1, mkLe q1 _4 -- 1 <= q1 <= 4
, mkLe _1 q2, mkLe q2 _4
, mkLe _1 q3, mkLe q3 _4
, mkLe _1 q4, mkLe q4 _4
]
-- different columns
assert =<< mkDistinct [q1,q2,q3,q4]
-- avoid diagonal attacks
assert =<< mkNot =<< mkOr =<< T.sequence
[ diagonal 1 q1 q2 -- diagonal line of attack between q1 and q2
, diagonal 2 q1 q3
, diagonal 3 q1 q4
, diagonal 1 q2 q3
, diagonal 2 q2 q4
, diagonal 1 q3 q4
]
-- check and get solution
fmap snd $ withModel $ \m ->
catMaybes <$> mapM (evalInt m) [q1,q2,q3,q4]
where mkAbs x = do
_0 <- mkInteger 0
join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x
diagonal d c c' =
join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkInteger d) In order to run this SMT script: main :: IO ()
main = evalZ3 script >>= \mbSol ->
case mbSol of
Nothing -> error "No solution found."
Just sol -> putStr "Solution: " >> print sol Garbage CollectionThis library automatically garbage collects all C objects created through its API. ConcurrencySince version Operations and objects in different |
2023-10-27
2022-08-15
2022-08-17
2022-09-23
2022-08-13
请发表评论