expressions-z3: Encode and Decode expressions from Z3 ASTs

[ bsd3, data, library, logic, math ] [ Propose Tags ]

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

Downloads

Maintainer's Corner

Package maintainers

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.13), containers (>=0.5 && <0.7), expressions (>=0.5 && <0.6), list-t (>=1.0 && <1.1), singletons (>=2.2 && <2.6), 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 2019-04-30T21:47:13Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 5782 total (9 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 2019-04-30 [all 3 reports]