expressions-z3 (empty) → 0.1.0
raw patch · 5 files changed
+478/−0 lines, 5 filesdep +basedep +containersdep +expressionssetup-changed
Dependencies added: base, containers, expressions, singletons, transformers, z3
Files
- ChangeLog.md +5/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- expressions-z3.cabal +73/−0
- src/Data/Expression/Z3.hs +368/−0
+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for expressions-z3++## 0.1.0++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2017, Jakub Daniel++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Jakub Daniel nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ expressions-z3.cabal view
@@ -0,0 +1,73 @@+name: expressions-z3+version: 0.1.0+synopsis: Encode and Decode expressions from Z3 ASTs+description:+ 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++license: BSD3+license-file: LICENSE+author: Jakub Daniel+maintainer: jakub.daniel@protonmail.com+copyright: Copyright (C) 2017 Jakub Daniel+category: Data, Logic, Math+build-type: Simple+extra-source-files: ChangeLog.md+cabal-version: >=1.10++source-repository head+ type: git+ location: https://github.com/jakubdaniel/expressions-z3.git++library+ exposed-modules: Data.Expression.Z3+ build-depends: base >=4.9 && <4.11,+ containers >=0.5 && <0.5.11,+ expressions >=0.1 && <0.2,+ singletons >=2.2 && <2.4,+ transformers >=0.5.2 && <0.5.5,+ z3 >=4.1.2 && <4.2+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall
+ src/Data/Expression/Z3.hs view
@@ -0,0 +1,368 @@+{-# LANGUAGE DataKinds+ , FlexibleContexts+ , FlexibleInstances+ , GADTs+ , GeneralizedNewtypeDeriving+ , KindSignatures+ , MultiParamTypeClasses+ , RankNTypes+ , ScopedTypeVariables+ , TypeOperators+ , UndecidableInstances #-}++module Data.Expression.Z3 ( IToZ3, toZ3, IFromZ3, fromZ3 ) where++import Control.Applicative hiding (Const)+import Control.Monad+import Control.Monad.IO.Class+import Control.Monad.Trans.Class+import Control.Monad.Trans.List+import Control.Monad.Trans.State+import Data.Expression+import Data.List hiding (and, or)+import Data.Maybe+import Data.Proxy+import Data.Singletons+import Data.Singletons.Decide+import Prelude hiding (and, or, not)++import qualified Data.Functor.Const as F+import qualified Data.Map as M+import qualified Z3.Monad as Z3++type Cache g = M.Map Z3.AST (DynamicallySorted g)++newtype Decoder g a b = Decoder { unwrap :: StateT (Cache g) (ListT a) b } deriving ( Functor, Applicative, Alternative, Monad, MonadIO )++instance Z3.MonadZ3 z3 => Z3.MonadZ3 (Decoder f z3) where+ getSolver = Decoder . lift . lift $ Z3.getSolver+ getContext = Decoder . lift . lift $ Z3.getContext++class IFunctor f => IToZ3 f where+ itoZ3 :: forall (s :: Sort) z3. Z3.MonadZ3 z3 => f (F.Const (z3 Z3.AST)) s -> F.Const (z3 Z3.AST) s++sortToZ3 :: forall (s :: Sort) z3. Z3.MonadZ3 z3 => Sing s -> z3 Z3.Sort+sortToZ3 SBooleanSort = Z3.mkBoolSort+sortToZ3 SIntegralSort = Z3.mkIntSort+sortToZ3 (SArraySort i e) = do+ z3i <- sortToZ3 i+ z3e <- sortToZ3 e+ Z3.mkArraySort z3i z3e++instance IToZ3 VarF where+ itoZ3 (Var n s) = F.Const $ do+ z3n <- Z3.mkStringSymbol n+ z3s <- sortToZ3 s+ Z3.mkVar z3n z3s++instance IToZ3 ConjunctionF where+ itoZ3 (And as) = F.Const $ Z3.mkAnd =<< mapM F.getConst as++instance IToZ3 DisjunctionF where+ itoZ3 (Or os) = F.Const $ Z3.mkOr =<< mapM F.getConst os++instance IToZ3 NegationF where+ itoZ3 (Not n) = F.Const $ Z3.mkNot =<< F.getConst n++instance IToZ3 (UniversalF v) where+ itoZ3 (Forall vs a) = F.Const $ do+ z3vs <- mapM (Z3.toApp <=< toZ3) vs+ Z3.mkForallConst [] z3vs =<< F.getConst a++instance IToZ3 (ExistentialF v) where+ itoZ3 (Exists vs a) = F.Const $ do+ z3vs <- mapM (Z3.toApp <=< toZ3) vs+ Z3.mkExistsConst [] z3vs =<< F.getConst a++instance IToZ3 EqualityF where+ itoZ3 (Equals _ a b) = F.Const . join $ liftM2 Z3.mkEq (F.getConst a) (F.getConst b)++instance IToZ3 ArithmeticF where+ itoZ3 (Const c) = F.Const $ Z3.mkInt c =<< Z3.mkIntSort+ itoZ3 (Add as) = F.Const $ Z3.mkAdd =<< mapM F.getConst as+ itoZ3 (Mul ms) = F.Const $ Z3.mkMul =<< mapM F.getConst ms+ itoZ3 (Divides c a) = F.Const $ do+ z3c <- Z3.mkInt c =<< Z3.mkIntSort+ z30 <- Z3.mkInt 0 =<< Z3.mkIntSort+ z3a <- F.getConst a+ Z3.mkEq z30 =<< Z3.mkMod z3a z3c+ itoZ3 (LessThan a b) = F.Const . join $ liftM2 Z3.mkLt (F.getConst a) (F.getConst b)++instance IToZ3 IfThenElseF where+ itoZ3 (IfThenElse _ i t e) = F.Const . join $ liftM3 Z3.mkIte (F.getConst i) (F.getConst t) (F.getConst e)++instance IToZ3 ArrayF where+ itoZ3 (Select _ _ a i) = F.Const . join $ liftM2 Z3.mkSelect (F.getConst a) (F.getConst i)+ itoZ3 (Store _ _ a i v) = F.Const . join $ liftM3 Z3.mkStore (F.getConst a) (F.getConst i) (F.getConst v)++instance ( IToZ3 f, IToZ3 g ) => IToZ3 (f :+: g) where+ itoZ3 (InL a) = itoZ3 a+ itoZ3 (InR b) = itoZ3 b++toZ3 :: forall f (s :: Sort) z3. ( IToZ3 f, Z3.MonadZ3 z3 ) => IFix f s -> z3 Z3.AST+toZ3 = F.getConst . icata itoZ3++class IFromZ3Into (f :: (Sort -> *) -> Sort -> *) (g :: (Sort -> *) -> Sort -> *) where+ ifromZ3App :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> String -> Z3.App -> Decoder g z3 (DynamicallySorted g)+ ifromZ3Quantifier :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> Bool -> [Z3.AST] -> Z3.AST -> Decoder g z3 (DynamicallySorted g)+ ifromZ3Numeral :: Z3.MonadZ3 z3 => Proxy f -> Int -> Decoder g z3 (DynamicallySorted g)++ ifromZ3App _ _ _ _ = empty+ ifromZ3Quantifier _ _ _ _ _ = empty+ ifromZ3Numeral _ _ = empty++class IFromZ3Into f f => IFromZ3 f++sortFromZ3 :: Z3.MonadZ3 z3 => Z3.Sort -> z3 DynamicSort+sortFromZ3 s = do+ k <- Z3.getSortKind s+ case k of+ Z3.Z3_BOOL_SORT -> return (DynamicSort SBooleanSort)+ Z3.Z3_INT_SORT -> return (DynamicSort SIntegralSort)+ Z3.Z3_ARRAY_SORT -> do+ DynamicSort i <- sortFromZ3 =<< Z3.getArraySortDomain s+ DynamicSort e <- sortFromZ3 =<< Z3.getArraySortRange s+ return (DynamicSort $ SArraySort i e)+ _ -> error "unrecognized sort"++instance IFromZ3 VarF+instance VarF :<: g => IFromZ3Into VarF g where+ ifromZ3App _ _ name app = do+ guard . null =<< Z3.getAppArgs app+ DynamicSort s <- sortFromZ3 =<< Z3.getSort =<< Z3.appToAst app+ return $ DynamicallySorted s (inject (Var name s))++instance IFromZ3 ConjunctionF+instance ConjunctionF :<: g => IFromZ3Into ConjunctionF g where+ ifromZ3App _ _ "true" app = do+ guard . null =<< Z3.getAppArgs app+ return . DynamicallySorted SBooleanSort $ true+ ifromZ3App _ r "and" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just as -> return . DynamicallySorted SBooleanSort $ and as+ _ -> empty+ ifromZ3App _ _ _ _ = empty++instance IFromZ3 DisjunctionF+instance DisjunctionF :<: g => IFromZ3Into DisjunctionF g where+ ifromZ3App _ _ "false" app = do+ guard . null =<< Z3.getAppArgs app+ return . DynamicallySorted SBooleanSort $ false+ ifromZ3App _ r "or" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just os -> return . DynamicallySorted SBooleanSort $ or os+ _ -> empty+ ifromZ3App _ _ _ _ = empty++instance IFromZ3 NegationF+instance NegationF :<: g => IFromZ3Into NegationF g where+ ifromZ3App _ r "not" app = do+ args <- mapM r =<< Z3.getAppArgs app+ guard (length args == 1)+ case toStaticallySorted (head args) of+ Just n -> return . DynamicallySorted SBooleanSort $ not n+ _ -> empty+ ifromZ3App _ _ _ _ = empty++varFromZ3 :: Z3.MonadZ3 z3 => Z3.AST -> Decoder VarF z3 (DynamicallySorted VarF)+varFromZ3 = ifromZ3 (Proxy :: Proxy (VarF :: (Sort -> *) -> Sort -> *)) varFromZ3++local :: Z3.MonadZ3 z3 => Decoder VarF z3 a -> Decoder g z3 a+local = Decoder . lift . flip evalStateT M.empty . unwrap++instance SingI v => IFromZ3 (UniversalF v)+instance ( UniversalF v :<: g, SingI v ) => IFromZ3Into (UniversalF v) g where+ ifromZ3Quantifier _ r True as f = do+ vs <- mapM (local . varFromZ3) as+ let (vvs, rest) = partition (isVSorted . fst) $ zip vs as++ if null vvs then empty else do+ let (vs', bound) = unzip vvs++ vs'' <- mapM (Z3.toApp . snd) rest+ a' <- if null vs'' then return f else Z3.mkForallConst [] vs'' f+ b <- r =<< Z3.substituteVars a' bound++ case toStaticallySorted b of+ Just b'' -> return . DynamicallySorted SBooleanSort $ forall (fromJust . mapM toStaticallySorted $ vs' :: [IFix VarF v]) b''+ _ -> empty+ where++ isVSorted :: DynamicallySorted VarF -> Bool+ isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )++ ifromZ3Quantifier _ _ _ _ _ = empty++instance SingI v => IFromZ3 (ExistentialF v)+instance ( ExistentialF v :<: g, SingI v ) => IFromZ3Into (ExistentialF v) g where+ ifromZ3Quantifier _ r False as f = do+ vs <- mapM (local . varFromZ3) as+ let (vvs, rest) = partition (isVSorted . fst) $ zip vs as++ if null vvs then empty else do+ let (vs', bound) = unzip vvs++ vs'' <- mapM (Z3.toApp . snd) rest+ a' <- if null vs'' then return f else Z3.mkExistsConst [] vs'' f+ b <- r =<< Z3.substituteVars a' bound++ case toStaticallySorted b of+ Just b'' -> return . DynamicallySorted SBooleanSort $ exists (fromJust . mapM toStaticallySorted $ vs' :: [IFix VarF v]) b''+ _ -> empty+ where++ isVSorted :: DynamicallySorted VarF -> Bool+ isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )++ ifromZ3Quantifier _ _ _ _ _ = empty++instance IFromZ3 EqualityF+instance EqualityF :<: g => IFromZ3Into EqualityF g where+ ifromZ3App _ r name app = case name of+ "=" -> ifromZ3'' =<< mapM r =<< Z3.getAppArgs app+ "iff" -> ifromZ3'' =<< mapM r =<< Z3.getAppArgs app+ _ -> empty++ where++ ifromZ3'' :: Z3.MonadZ3 z3 => [DynamicallySorted g] -> Decoder g z3 (DynamicallySorted g)+ ifromZ3'' [DynamicallySorted s1 a, DynamicallySorted s2 b] = case s1 %~ s2 of+ Proved Refl -> return . DynamicallySorted SBooleanSort $ inject (Equals s1 a b)+ Disproved _ -> empty+ ifromZ3'' _ = empty++instance IFromZ3 ArithmeticF+instance ArithmeticF :<: g => IFromZ3Into ArithmeticF g where+ ifromZ3Numeral _ c = return . DynamicallySorted SIntegralSort $ cnst c+ ifromZ3App _ r "+" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just as -> return . DynamicallySorted SIntegralSort $ add as+ _ -> empty+ ifromZ3App _ r "*" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just ms -> return . DynamicallySorted SIntegralSort $ mul ms+ _ -> empty+ ifromZ3App _ r "<" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just [k, l] -> return . DynamicallySorted SBooleanSort $ k .<. l+ _ -> empty+ ifromZ3App _ r ">" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just [k, l] -> return . DynamicallySorted SBooleanSort $ l .<. k+ _ -> empty+ ifromZ3App _ r "<=" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just [k, l] -> return . DynamicallySorted SBooleanSort $ k .<. l .+. cnst 1+ _ -> empty+ ifromZ3App _ r ">=" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case mapM toStaticallySorted args of+ Just [k, l] -> return . DynamicallySorted SBooleanSort $ l .<. k .+. cnst 1+ _ -> empty+ ifromZ3App _ r "=" app = do+ args <- Z3.getAppArgs app+ case args of+ [m, n] -> modulo m n <|> modulo n m+ _ -> empty++ where++ modulo k l = do+ ka <- Z3.getAstKind k+ kb <- Z3.getAstKind l+ case (ka, kb) of+ (Z3.Z3_NUMERAL_AST, Z3.Z3_APP_AST) -> do+ z <- Z3.getInt k+ app' <- Z3.toApp l+ name <- Z3.getSymbolString =<< Z3.getDeclName =<< Z3.getAppDecl app'+ case (z, name) of+ (0, "mod") -> do+ args <- Z3.getAppArgs app'+ case args of+ [n, c] -> do+ kc <- Z3.getAstKind c+ case kc of+ Z3.Z3_NUMERAL_AST -> do+ c' <- fromIntegral <$> Z3.getInt c+ n' <- r n+ case toStaticallySorted n' of+ Just n'' -> return . DynamicallySorted SBooleanSort $ c' .\. n''+ _ -> empty+ _ -> empty+ _ -> empty+ _ -> empty+ _ -> empty+ ifromZ3App _ _ _ _ = empty++instance IFromZ3 IfThenElseF+instance IfThenElseF :<: g => IFromZ3Into IfThenElseF g where+ ifromZ3App _ r "if" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case args of+ [DynamicallySorted SBooleanSort i, DynamicallySorted ts t, DynamicallySorted es e] -> case ts %~ es of+ Proved Refl -> return . DynamicallySorted ts $ inject (IfThenElse ts i t e)+ Disproved _ -> empty+ _ -> empty+ ifromZ3App _ _ _ _ = empty++instance IFromZ3 ArrayF+instance ArrayF :<: g => IFromZ3Into ArrayF g where+ ifromZ3App _ r "select" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case args of+ [DynamicallySorted (SArraySort is1 es) a, DynamicallySorted is2 i] -> case is1 %~ is2 of+ Proved Refl -> return . DynamicallySorted es $ inject (Select is1 es a i)+ Disproved _ -> empty+ _ -> empty+ ifromZ3App _ r "store" app = do+ args <- mapM r =<< Z3.getAppArgs app+ case args of+ [DynamicallySorted as@(SArraySort _ _) a, DynamicallySorted is i, DynamicallySorted es v] -> case as %~ SArraySort is es of+ Proved Refl -> return . DynamicallySorted as $ inject (Store is es a i v)+ Disproved _ -> empty+ _ -> empty+ ifromZ3App _ _ _ _ = empty++instance ( IFromZ3Into f (f :+: g), IFromZ3Into g (f :+: g) ) => IFromZ3 (f :+: g)+instance ( IFromZ3Into f h, IFromZ3Into g h ) => IFromZ3Into (f :+: g) h where+ ifromZ3App _ r name app = ifromZ3App (Proxy :: Proxy f) r name app <|> ifromZ3App (Proxy :: Proxy g) r name app+ ifromZ3Quantifier _ r q vs b = ifromZ3Quantifier (Proxy :: Proxy f) r q vs b <|> ifromZ3Quantifier (Proxy :: Proxy g) r q vs b+ ifromZ3Numeral _ c = ifromZ3Numeral (Proxy :: Proxy f) c <|> ifromZ3Numeral (Proxy :: Proxy g) c++ifromZ3 :: forall (f :: (Sort -> *) -> Sort -> *)+ (g :: (Sort -> *) -> Sort -> *)+ z3.+ ( IFromZ3Into f g, Z3.MonadZ3 z3 )+ => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> Z3.AST -> Decoder g z3 (DynamicallySorted g)+ifromZ3 p r a = do+ c <- Decoder $ get+ if a `M.member` c then do+ return (c M.! a)+ else do+ k <- Z3.getAstKind a+ e <- case k of+ Z3.Z3_NUMERAL_AST -> ifromZ3Numeral p . fromIntegral =<< Z3.getInt a+ Z3.Z3_APP_AST -> do+ app <- Z3.toApp a+ name <- Z3.getSymbolString =<< Z3.getDeclName =<< Z3.getAppDecl app+ ifromZ3App p r name app+ Z3.Z3_QUANTIFIER_AST -> do+ t <- Z3.isQuantifierForall a+ vs <- Z3.getQuantifierBoundVars a+ b <- Z3.getQuantifierBody a+ ifromZ3Quantifier p r t vs b+ _ -> empty+ Decoder $ modify (M.insert a e)+ return e++fromZ3 :: forall (f :: (Sort -> *) -> Sort -> *) (s :: Sort) z3. ( IFromZ3 f, Z3.MonadZ3 z3, SingI s ) => Z3.AST -> z3 (IFix f s)+fromZ3 a = let r = ifromZ3 (Proxy :: Proxy f) r in head' <=< fmap (mapMaybe toStaticallySorted) . runListT . flip evalStateT M.empty . unwrap . r $ a where+ head' (h : _) = return h+ head' _ = Z3.astToString a >>= \s -> error ("couldn't re-encode Z3 AST: " ++ s)