# 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