expressions-z3: Encode and Decode expressions from Z3 ASTs
A simple interface for converting expressions back and forth between pure representation and an AST within a Z3 context.
Assume
λ> :m + Control.Monad Data.Expression Data.Expression.Z3 Z3.Monad Data.Singletons λ> :t f f :: MonadZ3 z3 => AST -> z3 AST
Then
λ> let g :: ( MonadZ3 z3, IFromZ3 f, IToZ3 f, SingI s ) => IFix f s -> z3 (IFix f s); g = fromZ3 <=< f <=< toZ3 λ> :t g (var "a" :: Lia 'BooleanSort) g (var "a" :: Lia 'BooleanSort) :: MonadZ3 z3 => z3 (Lia 'BooleanSort)
For example
λ> let f b = mkStringSymbol "a" >>= mkIntVar >>= toApp >>= \a' -> mkForallConst [] [a'] b λ> let g :: ( MonadZ3 z3, IFromZ3 f, IToZ3 f ) => IFix f 'BooleanSort -> z3 (IFix f 'BooleanSort); g = fromZ3 <=< g <=< toZ3 λ> evalZ3 $ g (var "a" .+. cnst 1 .=. var "b" :: Lia 'BooleanSort) (forall ((a : int)) (= (+ 1 (a : int)) (b : int)))
Or more interestingly
λ> :{ | let f :: ( MonadZ3 z3, IFromZ3 f, IToZ3 f, SingI s ) => IFix f s -> z3 (IFix f s) | f a = do | a' <- toZ3 a | r <- getModel | case r of | (Sat, Just m) -> do | v <- modelEval m a' True | case v of | Just v' -> fromZ3 v' | _ -> error "..." | _ -> error "..." :} λ> evalZ3 $ f (var "a" :: Lia 'BooleanSort) false λ> evalZ3 $ f (var "a" :: Lia 'IntegralSort) 0 λ> evalZ3 $ f (var "a" .+. cnst 1:: Lia 'IntegralSort) 1
Modules
- Data
- Expression
- Data.Expression.Z3
- Expression
Downloads
- expressions-z3-0.1.6.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 0.1.0, 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.1.5, 0.1.6, 0.2, 0.3, 0.4, 0.5 |
---|---|
Change log | ChangeLog.md |
Dependencies | base (>=4.9 && <4.12), containers (>=0.5 && <0.7), expressions (>=0.1.7 && <0.2), list-t (>=1.0 && <1.1), singletons (>=2.2 && <2.5), transformers (>=0.5.2 && <0.6), z3 (>=4.1.2 && <4.4) [details] |
License | BSD-3-Clause |
Copyright | Copyright (C) 2017 Jakub Daniel |
Author | Jakub Daniel |
Maintainer | jakub.daniel@protonmail.com |
Category | Data, Logic, Math |
Source repo | head: git clone https://github.com/jakubdaniel/expressions-z3.git |
Uploaded | by jakubdaniel at 2018-06-21T20:01:47Z |
Distributions | |
Reverse Dependencies | 1 direct, 0 indirect [details] |
Downloads | 5775 total (12 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs not available [build log] All reported builds failed as of 2018-06-21 [all 3 reports] |