expressions-z3 0.3 → 0.4
raw patch · 3 files changed
+17/−13 lines, 3 filesdep ~expressions
Dependency ranges changed: expressions
Files
- ChangeLog.md +4/−0
- expressions-z3.cabal +2/−2
- src/Data/Expression/Z3.hs +11/−11
ChangeLog.md view
@@ -1,5 +1,9 @@ # Revision history for expressions-z3 +## 0.4++* Bump dependencies+ ## 0.3 * Bump dependencies
expressions-z3.cabal view
@@ -1,5 +1,5 @@ name: expressions-z3-version: 0.3+version: 0.4 synopsis: Encode and Decode expressions from Z3 ASTs description: A simple interface for converting expressions back and forth between pure@@ -64,7 +64,7 @@ exposed-modules: Data.Expression.Z3 build-depends: base >=4.9 && <4.13, containers >=0.5 && <0.7,- expressions >=0.1.7 && <0.4,+ expressions >=0.4 && <0.5, singletons >=2.2 && <2.6, transformers >=0.5.2 && <0.6, list-t >=1.0 && <1.1,
src/Data/Expression/Z3.hs view
@@ -47,7 +47,7 @@ import qualified Data.Map as M import qualified Z3.Monad as Z3 -type Cache g = M.Map Z3.AST (DynamicallySorted g)+type Cache g = M.Map Z3.AST (DynamicallySortedFix g) newtype Decoder g a b = Decoder { unwrap :: StateT (Cache g) (ListT a) b } deriving ( Functor, Applicative, Alternative, Monad, MonadIO ) @@ -120,9 +120,9 @@ 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 :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySortedFix g)) -> String -> Z3.App -> Decoder g z3 (DynamicallySortedFix g)+ ifromZ3Quantifier :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySortedFix g)) -> Bool -> [Z3.AST] -> Z3.AST -> Decoder g z3 (DynamicallySortedFix g)+ ifromZ3Numeral :: Z3.MonadZ3 z3 => Proxy f -> Int -> Decoder g z3 (DynamicallySortedFix g) ifromZ3App _ _ _ _ = empty ifromZ3Quantifier _ _ _ _ _ = empty@@ -183,7 +183,7 @@ _ -> empty ifromZ3App _ _ _ _ = empty -varFromZ3 :: Z3.MonadZ3 z3 => Z3.AST -> Decoder VarF z3 (DynamicallySorted VarF)+varFromZ3 :: Z3.MonadZ3 z3 => Z3.AST -> Decoder VarF z3 (DynamicallySorted Var) varFromZ3 = ifromZ3 (Proxy :: Proxy (VarF :: (Sort -> *) -> Sort -> *)) varFromZ3 local :: Z3.MonadZ3 z3 => Decoder VarF z3 a -> Decoder g z3 a@@ -207,8 +207,8 @@ _ -> empty where - isVSorted :: DynamicallySorted VarF -> Bool- isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )+ isVSorted :: DynamicallySorted Var -> Bool+ isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted Var -> Maybe (IFix VarF v) ) ifromZ3Quantifier _ _ _ _ _ = empty @@ -230,8 +230,8 @@ _ -> empty where - isVSorted :: DynamicallySorted VarF -> Bool- isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )+ isVSorted :: DynamicallySorted Var -> Bool+ isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted Var -> Maybe (IFix VarF v) ) ifromZ3Quantifier _ _ _ _ _ = empty @@ -244,7 +244,7 @@ where - ifromZ3'' :: Z3.MonadZ3 z3 => [DynamicallySorted g] -> Decoder g z3 (DynamicallySorted g)+ ifromZ3'' :: Z3.MonadZ3 z3 => [DynamicallySortedFix g] -> Decoder g z3 (DynamicallySortedFix g) ifromZ3'' [DynamicallySorted s1 a, DynamicallySorted s2 b] = case s1 %~ s2 of Proved Refl -> return . toDynamicallySorted . inject $ Equals s1 a b Disproved _ -> empty@@ -357,7 +357,7 @@ (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)+ => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySortedFix g)) -> Z3.AST -> Decoder g z3 (DynamicallySortedFix g) ifromZ3 p r a = do c <- Decoder $ get if a `M.member` c then do