z3-encoding 0.2.1.1 → 0.3.0.0
raw patch · 13 files changed
+595/−536 lines, 13 files
Files
- src/Z3/Assertion.hs +0/−63
- src/Z3/Base/Atom.hs +61/−0
- src/Z3/Base/Class.hs +195/−0
- src/Z3/Base/Logic.hs +95/−0
- src/Z3/Class.hs +0/−223
- src/Z3/Context.hs +26/−9
- src/Z3/Datatypes.hs +36/−0
- src/Z3/Encoding.hs +0/−52
- src/Z3/Logic.hs +0/−18
- src/Z3/Z3Pred.hs +136/−0
- test/Z3/Demo.hs +0/−123
- test/Z3/Test.hs +35/−39
- z3-encoding.cabal +11/−9
− src/Z3/Assertion.hs
@@ -1,63 +0,0 @@--- |--- Assertions provided by libraries *for convenience*--- It is not hard-coded into Z3.Logic.Pred-----module Z3.Assertion (Assertion(..)) where--import Z3.Class-import Z3.Encoding()-import Z3.Monad--import qualified Data.Map as M-import qualified Data.Set as S--data Assertion where- -- | k is mapped to v in (m :: M.Map k v)- -- XXX: m should be any "term", too strong now- InMap :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion- -- | v is in s- -- XXX: s should be any "term", too strong now- InSet :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion- -- | All below are binary relationships- -- XXX: Should make sure v1 ~ v2, too weak now- Equal :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- LessE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- Less :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- Greater :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion--instance Z3Encoded Assertion where- encode (InMap k v m) = do- kTm <- encode k- vTm <- encode v- mTm <- encode m- lhs <- mkSelect mTm kTm- mkEq lhs vTm- encode (InSet e s) = do- eTm <- encode e- sTm <- encode s- lhs <- mkSelect sTm eTm- -- XXX: magic number- one <- (mkIntSort >>= mkInt 1)- mkEq one lhs- encode (Equal t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkEq a1 a2- encode (LessE t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkLe a1 a2- encode (GreaterE t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkGe a1 a2- encode (Less t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkLt a1 a2- encode (Greater t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkGt a1 a2
+ src/Z3/Base/Atom.hs view
@@ -0,0 +1,61 @@+-- |+-- Atomic predicates+--++module Z3.Base.Atom (Atom(..)) where++import Z3.Base.Class+import Z3.Monad++import qualified Data.Map as M+import qualified Data.Set as S++data Atom where+ -- | k is mapped to v in (m :: M.Map k v)+ -- XXX: m should be any "term", too strong now+ InMap :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Atom+ -- | v is in s+ -- XXX: s should be any "term", too strong now+ InSet :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Atom+ -- | All below are binary relationships+ -- XXX: Should make sure v1 ~ v2, too weak now+ Equal :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom+ LessE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom+ GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom+ Less :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom+ Greater :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom++instance Z3Encoded Atom where+ encode (InMap k v m) = do+ kTm <- encode k+ vTm <- encode v+ mTm <- encode m+ lhs <- mkSelect mTm kTm+ mkEq lhs vTm+ encode (InSet e s) = do+ eTm <- encode e+ sTm <- encode s+ lhs <- mkSelect sTm eTm+ -- XXX: magic number+ one <- (mkIntSort >>= mkInt 1)+ mkEq one lhs+ encode (Equal t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkEq a1 a2+ encode (LessE t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkLe a1 a2+ encode (GreaterE t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkGe a1 a2+ encode (Less t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkLt a1 a2+ encode (Greater t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkGt a1 a2
+ src/Z3/Base/Class.hs view
@@ -0,0 +1,195 @@+-- |+-- Type classes and built-in implementation for primitive Haskell types+-- ++module Z3.Base.Class (+ -- ** Types whose values are encodable to Z3 internal AST+ Z3Encoded(..),+ -- ** Types representable as Z3 Sort+ -- XXX: Unsound now+ -- XXX: Too flexible, can be used to encode Type ADT+ Z3Sorted(..),+ -- ** Type proxy helper, used with Z3Sorted+ Z3Sort(..),+ -- ** Types with reserved value for Z3 encoding use+ -- XXX: Magic value for built-in types+ Z3Reserved(..),+ -- ** Monad which can be instantiated into a concrete context+ SMT(..),+ Datatypes,+ ValBindings,+ emptyValBindings,+ -- ** Heterogenous list, a hack to encode different "term" into a list+ -- Used to encode function argument list+ HeteroList(..),+ mapH+) where++import Z3.Monad++import Control.Monad.Except++import qualified Data.Map as M+import qualified Data.Set as S++data Z3Sort a = Z3Sort++class Z3Encoded a where+ encode :: SMT m e => a -> m e AST++type Datatypes ty = [(String, [(String, [(String, ty)])])]+type ValBindings = ([String], HeteroList)++emptyValBindings :: ValBindings+emptyValBindings = ([], Nil)+++-- | XXX: Unsound+class Z3Sorted a where+ -- | Map a value to Sort, the value should be a type-level thing+ sortOf :: SMT m e => a -> m e Sort+ sortOf _ = sortPhantom (Z3Sort :: Z3Sort a)++ -- | Map a Haskell type to Sort+ sortPhantom :: SMT m e => Z3Sort a -> m e Sort+ sortPhantom _ = smtError "sort error"++class Z3Encoded a => Z3Reserved a where+ def :: a++class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where+ -- | Globally unique id+ genFreshId :: m e Int++ -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad+ runSMT :: Z3Sorted ty => ValBindings -> Datatypes ty -> e -> m e a -> IO (Either String a)++ bindVals :: ([String], HeteroList) -> m e ()+ bindVals (x:xs, Cons v vs) = do+ ast <- encode v+ st <- sortOf v+ bindVal x ast st+ bindVals (xs, vs)+ bindVals _ = return ()++ modifyValBindCtx :: ValBindings -> m e ()++ -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort+ bindVal :: String -> AST -> Sort -> m e ()++ getValBindMaybe :: String -> m e (Maybe (AST, Sort))++ getValBind :: String -> m e (AST, Sort)+ getValBind x = getValBindMaybe x >>= \case+ Just p -> return p+ Nothing -> smtError $ "no such variable: " ++ x++ getDataTypeMaybe :: String -> m e (Maybe Sort)++ getDataType :: String -> m e Sort+ getDataType x = getDataTypeMaybe x >>= \case+ Just p -> return p+ Nothing -> smtError $ "no such type variable: " ++ x++ -- | Get extra+ getExtra :: m e e++ -- | Set extra+ modifyExtra :: (e -> e) -> m e ()++ -- | User don't have to import throwError+ smtError :: String -> m e a+ smtError = throwError++instance Z3Reserved Int where+ def = -1 -- XXX: Magic number++instance Z3Sorted Int where+ sortPhantom _ = mkIntSort++instance Z3Encoded Int where+ encode i = mkIntSort >>= mkInt i++instance Z3Reserved Double where+ def = -1.0 -- XXX: Magic number++instance Z3Sorted Double where+ sortPhantom _ = mkRealSort++instance Z3Encoded Double where+ encode = mkRealNum++instance Z3Reserved Bool where+ def = False -- XXX: Magic number++instance Z3Sorted Bool where+ sortPhantom _ = mkBoolSort++instance Z3Encoded Bool where+ encode = mkBool++-- The basic idea:+-- For each (k, v), assert in Z3 that if we select k from array we will get+-- the same value v+-- HACK: to set a default value for rest fields (or else we always get the last asserted value+-- as default, which is certainly not complying to finite map's definition), thus the+-- user should guarantee that he/she will never never think this value as a vaid one,+-- if not, he/she might get "a valid value mapped to a invalid key" semantics+instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where+ encode m = do+ fid <- genFreshId+ arrSort <- sortOf m+ arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort+ mapM_ (\(k, v) -> do+ kast <- encode k+ vast <- encode v+ sel <- mkSelect arr kast+ mkEq sel vast >>= assert) (M.toList m)+ arrValueDef <- mkArrayDefault arr+ vdef <- encode (def :: v)+ mkEq arrValueDef vdef >>= assert+ return arr++instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where+ sortPhantom _ = do+ sk <- sortPhantom (Z3Sort :: Z3Sort k)+ sv <- sortPhantom (Z3Sort :: Z3Sort v)+ mkArraySort sk sv++-- Basic idea:+-- Set v =def= Map v {0, 1}+-- Thank god, this is much more sound+instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where+ encode s = do+ setSort <- sortOf s+ fid <- genFreshId+ arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort+ mapM_ (\e -> do+ ast <- encode e+ sel <- mkSelect arr ast+ one <- (mkIntSort >>= mkInt 1)+ mkEq sel one >>= assert) (S.toList s)+ arrValueDef <- mkArrayDefault arr+ zero <- (mkIntSort >>= mkInt 0)+ mkEq zero arrValueDef >>= assert+ return arr++instance Z3Sorted v => Z3Sorted (S.Set v) where+ sortPhantom _ = do+ sortElem <- sortPhantom (Z3Sort :: Z3Sort v)+ intSort <- mkIntSort+ mkArraySort sortElem intSort+++data HeteroList where+ Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList+ Nil :: HeteroList++instance Eq HeteroList where+ Nil == Nil = True+ Cons _ h1 == Cons _ h2 = h1 == h2+ _ == _ = False++mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]+mapH _ Nil = []+mapH f (Cons a l) = f a : mapH f l
+ src/Z3/Base/Logic.hs view
@@ -0,0 +1,95 @@+-- | Predicates++module Z3.Base.Logic (Pred(..)) where++import Z3.Monad+import Z3.Base.Class+import Z3.Base.Atom++data Pred t ty a where+ PTrue :: Pred t ty a+ PFalse :: Pred t ty a+ PConj :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PDisj :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PXor :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PNeg :: Pred t ty a -> Pred t ty a+ PForAll :: String -> ty -> Pred t ty a -> Pred t ty a+ PExists :: String -> ty -> Pred t ty a -> Pred t ty a+ PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a+ PImpli :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PIff :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PAtom :: Atom -> Pred t ty a+ -- User-extension+ PExt :: a -> Pred t ty a++instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where+ encode PTrue = mkTrue+ encode PFalse = mkFalse+ encode (PConj p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkAnd [a1, a2]++ encode (PDisj p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkOr [a1, a2]++ encode (PXor p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkXor a1 a2++ encode (PNeg p) = encode p >>= mkNot++ encode (PForAll x ty p) = do+ sym <- mkStringSymbol x+ xsort <- sortOf ty+ -- "0" is de brujin idx for current binder+ -- it is passed to Z3 which returns an intenal (idx :: AST)+ -- This (idx :: AST) will be used to replace the variable+ -- in the abstraction body when encountered, thus it is stored+ -- in context by bindVal we provide+ -- XXX: we should save and restore qualifier context here+ idx <- mkBound 0 xsort+ local $ do+ bindVal x idx xsort+ body <- encode p+ -- The first [] is [Pattern], which is not really useful here+ mkForall [] [sym] [xsort] body++ encode (PExists x ty p) = do+ sym <- mkStringSymbol x+ xsort <- sortOf ty+ idx <- mkBound 0 xsort+ local $ do+ bindVal x idx xsort+ a <- encode p+ mkExists [] [sym] [xsort] a++ -- HACK+ encode (PExists2 x y ty p) = do+ sym1 <- mkStringSymbol x+ sym2 <- mkStringSymbol y+ xsort <- sortOf ty+ idx1 <- mkBound 0 xsort+ idx2 <- mkBound 1 xsort+ local $ do+ bindVal x idx1 xsort+ bindVal y idx2 xsort+ a <- encode p+ mkExists [] [sym1, sym2] [xsort, xsort] a++ encode (PImpli p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkImplies a1 a2++ encode (PIff p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkIff a1 a2++ encode (PAtom a) = encode a++ encode (PExt ext) = encode ext
− src/Z3/Class.hs
@@ -1,223 +0,0 @@--- |--- Type classes and built-in implementation for primitive Haskell types--- --module Z3.Class (- -- ** Types whose values are encodable to Z3 internal AST- Z3Encoded(..),- -- ** Types representable as Z3 Sort- -- XXX: Unsound now- -- XXX: Too flexible, can be used to encode Type ADT- Z3Sorted(..),- -- ** Type proxy helper, used with Z3Sorted- Z3Sort(..),- -- ** Types with reserved value for Z3 encoding use- -- XXX: Magic value for built-in types- Z3Reserved(..),- -- ** Monad which can be instantiated into a concrete context- SMT(..)-) where--import Z3.Monad-import Z3.Logic--import Control.Monad.Except--import qualified Data.Map as M-import qualified Data.Set as S--data Z3Sort a = Z3Sort--class Z3Encoded a where- encode :: SMT m e => a -> m e AST---- | XXX: Unsound-class Z3Sorted a where- -- | Map a value to Sort, the value should be a type-level thing- sort :: SMT m e => a -> m e Sort- sort _ = sortPhantom (Z3Sort :: Z3Sort a)-- -- | Map a Haskell type to Sort- sortPhantom :: SMT m e => Z3Sort a -> m e Sort- sortPhantom _ = smtError "sort error"--class Z3Encoded a => Z3Reserved a where- def :: a--class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where- -- | Globally unique id- genFreshId :: m e Int-- -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad- runSMT :: Z3Sorted ty => [(String, [(String, [(String, ty)])])] -> e -> m e a -> IO (Either String a)-- -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort- bindQualified :: String -> AST -> Sort -> m e ()-- -- | Get the above AST- -- FIXME: The context management need extra -- we need to make sure that old binding wouldn't be destoryed- -- XXX: We shouldn't expose a Map here. A fallible query interface is better- getQualifierCtx :: m e (M.Map String (AST, Sort))-- -- | Get the preprocessed datatype context, a map from ADT's type name to its Z3 Sort- -- XXX: We shouldn't expose a Map here. A fallible query interface is better- getDataTypeCtx :: m e (M.Map String Sort)-- -- | Get extra- getExtra :: m e e-- -- | Set extra- modifyExtra :: (e -> e) -> m e ()-- -- | User don't have to import throwError- smtError :: String -> m e a- smtError = throwError--instance Z3Reserved Int where- def = -1 -- XXX: Magic number--instance Z3Sorted Int where- sortPhantom _ = mkIntSort--instance Z3Encoded Int where- encode i = mkIntSort >>= mkInt i--instance Z3Reserved Double where- def = -1.0 -- XXX: Magic number--instance Z3Sorted Double where- sortPhantom _ = mkRealSort--instance Z3Encoded Double where- encode = mkRealNum--instance Z3Reserved Bool where- def = False -- XXX: Magic number--instance Z3Sorted Bool where- sortPhantom _ = mkBoolSort--instance Z3Encoded Bool where- encode = mkBool---- The basic idea:--- For each (k, v), assert in Z3 that if we select k from array we will get--- the same value v--- HACK: to set a default value for rest fields (or else we always get the last asserted value--- as default, which is certainly not complying to finite map's definition), thus the--- user should guarantee that he/she will never never think this value as a vaid one,--- if not, he/she might get "a valid value mapped to a invalid key" semantics-instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where- encode m = do- fid <- genFreshId- arrSort <- sort m- arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort- mapM_ (\(k, v) -> do- kast <- encode k- vast <- encode v- sel <- mkSelect arr kast- mkEq sel vast >>= assert) (M.toList m)- arrValueDef <- mkArrayDefault arr- vdef <- encode (def :: v)- mkEq arrValueDef vdef >>= assert- return arr--instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where- sortPhantom _ = do- sk <- sortPhantom (Z3Sort :: Z3Sort k)- sv <- sortPhantom (Z3Sort :: Z3Sort v)- mkArraySort sk sv---- Basic idea:--- Set v =def= Map v {0, 1}--- Thank god, this is much more sound-instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where- encode s = do- setSort <- sort s- fid <- genFreshId- arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort- mapM_ (\e -> do- ast <- encode e- sel <- mkSelect arr ast- one <- (mkIntSort >>= mkInt 1)- mkEq sel one >>= assert) (S.toList s)- arrValueDef <- mkArrayDefault arr- zero <- (mkIntSort >>= mkInt 0)- mkEq zero arrValueDef >>= assert- return arr--instance Z3Sorted v => Z3Sorted (S.Set v) where- sortPhantom _ = do- sortElem <- sortPhantom (Z3Sort :: Z3Sort v)- intSort <- mkIntSort- mkArraySort sortElem intSort--instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where- encode PTrue = mkTrue- encode PFalse = mkFalse- encode (PConj p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkAnd [a1, a2]-- encode (PDisj p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkOr [a1, a2]-- encode (PXor p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkXor a1 a2-- encode (PNeg p) = encode p >>= mkNot-- encode (PForAll x ty p) = do- sym <- mkStringSymbol x- xsort <- sort ty- -- "0" is de brujin idx for current binder- -- it is passed to Z3 which returns an intenal (idx :: AST)- -- This (idx :: AST) will be used to replace the variable- -- in the abstraction body when encountered, thus it is stored- -- in context by bindQualified we provide- -- XXX: we should save and restore qualifier context here- idx <- mkBound 0 xsort- local $ do- bindQualified x idx xsort- body <- encode p- -- The first [] is [Pattern], which is not really useful here- mkForall [] [sym] [xsort] body-- encode (PExists x ty p) = do- sym <- mkStringSymbol x- xsort <- sort ty- idx <- mkBound 0 xsort- local $ do- bindQualified x idx xsort- a <- encode p- mkExists [] [sym] [xsort] a-- -- HACK- encode (PExists2 x y ty p) = do- sym1 <- mkStringSymbol x- sym2 <- mkStringSymbol y- xsort <- sort ty- idx1 <- mkBound 0 xsort- idx2 <- mkBound 1 xsort- local $ do- bindQualified x idx1 xsort- bindQualified y idx2 xsort- a <- encode p- mkExists [] [sym1, sym2] [xsort, xsort] a-- encode (PImpli p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkImplies a1 a2-- encode (PIff p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkIff a1 a2-- encode (PAssert a) = encode a
src/Z3/Context.hs view
@@ -2,11 +2,11 @@ -- | A concrete context implement SMT provided *for convenience* -module Z3.Context (Z3SMT) where+module Z3.Context (Z3SMT, localSMT) where import Z3.Monad-import Z3.Class-import Z3.Encoding+import Z3.Base.Class+import Z3.Datatypes import Control.Monad.State import Control.Monad.Except@@ -14,7 +14,7 @@ data SMTContext e = SMTContext { -- | Bind local variables introduced by qualifiers to de brujin index in Z3- _qualifierContext :: M.Map String (AST, Sort),+ _valBindCtx :: M.Map String (AST, Sort), -- | From type name to Z3 sort _datatypeCtx :: M.Map String Sort, -- | Counter used to generate globally unique ID@@ -36,12 +36,13 @@ modify (\ctx -> ctx { _counter = i + 1 }) return i - runSMT datatypes e smt = evalZ3With Nothing opts m+ runSMT initialBindings datatypes e smt = evalZ3With Nothing opts m where smt' = do sorts <- mapM encodeDataType datatypes let datatypeCtx = M.fromList (zip (map fst datatypes) sorts) modify $ \ctx -> ctx { _datatypeCtx = datatypeCtx }+ bindVals initialBindings smt -- XXX: not sure what does this option mean@@ -49,13 +50,29 @@ m = evalStateT (runExceptT (unZ3SMT smt')) (SMTContext M.empty M.empty 0 e) - bindQualified x idx s = modify $ \ctx ->- ctx { _qualifierContext = M.insert x (idx, s) (_qualifierContext ctx) }+ bindVal x ast st = modify $ \ctx ->+ ctx { _valBindCtx = M.insert x (ast, st) (_valBindCtx ctx) } - getQualifierCtx = _qualifierContext <$> get+ modifyValBindCtx bindings = do+ modify $ \ctx -> ctx { _valBindCtx = M.empty }+ bindVals bindings - getDataTypeCtx = _datatypeCtx <$> get+ getValBindMaybe x = do+ ctx <- _valBindCtx <$> get+ return $ M.lookup x ctx + getDataTypeMaybe x = do+ ctx <- _datatypeCtx <$> get+ return $ M.lookup x ctx+ getExtra = _extra <$> get modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }+++localSMT :: Z3SMT e a -> Z3SMT e a+localSMT m = do+ s <- get+ ret <- local m+ put s+ return ret
+ src/Z3/Datatypes.hs view
@@ -0,0 +1,36 @@+-- |+-- Z3 encoding for datatypes+--++module Z3.Datatypes (+ -- ** encode constructor application+ encodeCons,+ -- ** encode datatype definition+ encodeDataType+) where++import Z3.Base.Class+import Z3.Monad hiding (mkMap, App)++encodeCons :: SMT m e => String -> HeteroList -> Sort -> m e AST+encodeCons fname args retSort = do+ paramSorts <- sequence $ mapH sortOf args+ sym <- mkStringSymbol fname+ decl <- mkFuncDecl sym paramSorts retSort+ argASTs <- sequence $ mapH encode args+ mkApp decl argASTs++encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort+encodeDataType (tyName, alts) = do+ constrs <- mapM (\(consName, fields) -> do+ consSym <- mkStringSymbol consName+ -- recognizer. e.g. is_None None = True, is_None (Some _) = False+ recogSym <- mkStringSymbol ("is_" ++ consName)+ flds <- flip mapM fields $ \(fldName, fldTy) -> do+ symFld <- mkStringSymbol fldName+ s <- sortOf fldTy+ return (symFld, Just s, -1) -- XXX: non-rec+ mkConstructor consSym recogSym flds+ ) alts+ sym <- mkStringSymbol tyName+ mkDatatype sym constrs
− src/Z3/Encoding.hs
@@ -1,52 +0,0 @@--- |--- Prviding some Z3 encoding for certain language constructs--- Require a Class.SMT context to work--module Z3.Encoding (- -- ** Heterogenous list, a hack to encode different "term" into a list- -- Used to encode function argument list- HeteroList(..),- -- ** encode function application- encodeApp,- -- ** encode datatype definition- encodeDataType-) where--import Z3.Class-import Z3.Monad hiding (mkMap, App)--data HeteroList where- Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList- Nil :: HeteroList--instance Eq HeteroList where- Nil == Nil = True- Cons _ h1 == Cons _ h2 = h1 == h2- _ == _ = False--mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]-mapH _ Nil = []-mapH f (Cons a l) = f a : mapH f l--encodeApp :: SMT m e => String -> HeteroList -> Sort -> m e AST-encodeApp fname args retSort = do- paramSorts <- sequence $ mapH sort args- sym <- mkStringSymbol fname- decl <- mkFuncDecl sym paramSorts retSort- argASTs <- sequence $ mapH encode args- mkApp decl argASTs--encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort-encodeDataType (tyName, alts) = do- constrs <- mapM (\(consName, fields) -> do- consSym <- mkStringSymbol consName- -- recognizer. e.g. is_None None = True, is_None (Some _) = False- recogSym <- mkStringSymbol ("is_" ++ consName)- flds <- flip mapM fields $ \(fldName, fldTy) -> do- symFld <- mkStringSymbol fldName- s <- sort fldTy- return (symFld, Just s, -1) -- XXX: non-rec- mkConstructor consSym recogSym flds- ) alts- sym <- mkStringSymbol tyName- mkDatatype sym constrs
− src/Z3/Logic.hs
@@ -1,18 +0,0 @@--- | Predicates--module Z3.Logic (Pred(..)) where--data Pred t ty a where- PTrue :: Pred t ty a- PFalse :: Pred t ty a- PConj :: Pred t ty a -> Pred t ty a -> Pred t ty a- PDisj :: Pred t ty a -> Pred t ty a -> Pred t ty a- PXor :: Pred t ty a -> Pred t ty a -> Pred t ty a- PNeg :: Pred t ty a -> Pred t ty a- PForAll :: String -> ty -> Pred t ty a -> Pred t ty a- PExists :: String -> ty -> Pred t ty a -> Pred t ty a- PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a- PImpli :: Pred t ty a -> Pred t ty a -> Pred t ty a- PIff :: Pred t ty a -> Pred t ty a -> Pred t ty a- PAssert :: a -> Pred t ty a- deriving (Show)
+ src/Z3/Z3Pred.hs view
@@ -0,0 +1,136 @@+{-+ Sealed AST for out-of-box use++ The design choice is to fix all possible *primitive*+ types as an AST, so a sound type checking is possible here.++ Question: How to handle TmApp (which is only instantiated as+ constructors) and potential user functions here? Do we have to+ provide an extra field or user can make up a Encoded Expr which+ layers on top of Term here (while preserving (expected) type soundness+ provided in this module)?++-}+{-# LANGUAGE StandaloneDeriving #-}++module Z3.Z3Pred where++import Z3.Base.Logic+import Z3.Base.Class+import Z3.Base.Atom+import Z3.Context+import Z3.Datatypes+import Z3.Monad++data Term = -- XXX: Verify that TmVar can serve at the same time as+ -- qualified var, bounded var, and zero-arity constructor+ TmVar String+ | TmInt Int+ | TmDouble Double+ | TmBool Bool+ | TmString String+ | TmLE Term Term+ | TmGE Term Term+ | TmSub Term Term+ | TmAdd Term Term+ | TmMul Term Term+ | TmDiv Term Term+ | TmMod Term Term+ | TmRem Term Term+ | TmMinus Term+ | TmIf Term Term Term+ | TmCons String HeteroList Type++deriving instance Eq Term++data Type = TyBool+ | TyInt+ | TyDouble+ | TyString+ | TyMap Type Type+ | TySet Type+ | TyADT String++deriving instance Eq Type++type Z3Pred tm = Pred tm Type ()++instance Z3Encoded Term where+ encode (TmVar x) = fst <$> getValBind x+ encode (TmInt n) = encode n+ encode (TmBool b) = encode b+ encode (TmLE t1 t2) = encode (LessE t1 t2)+ encode (TmGE t1 t2) = encode (GreaterE t1 t2)+ encode (TmAdd t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkAdd [a1, a2]+ encode (TmSub t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkSub [a1, a2]+ encode (TmMul t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkMul [a1, a2]+ encode (TmDiv t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkDiv a1 a2+ encode (TmMod t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkMod a1 a2+ encode (TmRem t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkRem a1 a2+ encode (TmMinus t) = do+ a <- encode t+ mkUnaryMinus a+ encode (TmIf p c a) = do+ a1 <- encode p+ a2 <- encode c+ a3 <- encode a+ mkIte a1 a2 a3+ encode (TmCons fname args retty) = do+ retSort <- sortOf retty+ encodeCons fname args retSort++-- XXX: Maybe if we have type checking this can be neater+instance Z3Sorted Term where+ sortOf (TmVar x) = snd <$> getValBind x+ sortOf (TmInt _) = mkIntSort+ sortOf (TmBool _) = mkBoolSort+ sortOf (TmLE _ _) = mkBoolSort+ sortOf (TmGE _ _) = mkBoolSort+ sortOf (TmAdd _ _) = mkIntSort+ sortOf (TmSub _ _) = mkIntSort+ sortOf (TmMul _ _) = mkIntSort+ sortOf (TmDiv _ _) = mkIntSort+ sortOf (TmMod _ _) = mkIntSort+ sortOf (TmRem _ _) = mkIntSort+ sortOf (TmMinus _) = mkIntSort+ sortOf (TmIf _ c _) = sortOf c+ sortOf (TmCons _ _ retty) = sortOf retty++instance Z3Sorted Type where+ sortOf TyBool = mkBoolSort+ sortOf TyInt = mkIntSort+ sortOf TyDouble = mkRealSort+ sortOf (TyMap ty1 ty2) = do+ s1 <- sortOf ty1+ s2 <- sortOf ty2+ mkArraySort s1 s2+ sortOf (TySet ty) = do+ s <- sortOf ty+ intSort <- mkIntSort+ mkArraySort s intSort+ sortOf (TyADT tyName) = getDataType tyName++instance Z3Encoded () where++checkPre :: Z3Sorted tm => Z3Pred tm -> Z3SMT e (Result, Maybe Model)+checkPre pre = local $ do+ ast <- encode pre+ local (assert ast >> getModel)
− test/Z3/Demo.hs
@@ -1,123 +0,0 @@--- Demo of how to instantiate the Pred--module Z3.Demo where--import Z3.Logic-import Z3.Class-import Z3.Encoding-import Z3.Assertion-import Z3.Monad--import qualified Data.Map as M--data Term = TmVar String- | TmNum Int- | TmBool Bool- | TmLE Term Term- | TmGE Term Term- | TmSub Term Term- | TmAdd Term Term- | TmMul Term Term- | TmDiv Term Term- | TmMod Term Term- | TmRem Term Term- | TmMinus Term- | TmIf Term Term Term- | TmApp String HeteroList Type--deriving instance Eq Term--data Type = TyBool- | TyInt- | TyDouble- | TyMap Type Type- | TySet Type- | TyADT String--deriving instance Eq Type--type Z3Pred = Pred Term Type Assertion--instance Z3Encoded Term where- encode (TmVar x) = do- ctx <- getQualifierCtx- case M.lookup x ctx of- Just (idx, _) -> return idx- Nothing -> smtError $ "Can't find variable " ++ x- encode (TmNum n) = mkIntSort >>= mkInt n- encode (TmBool b) = mkBool b- encode (TmLE t1 t2) = encode (LessE t1 t2)- encode (TmGE t1 t2) = encode (GreaterE t1 t2)- encode (TmAdd t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkAdd [a1, a2]- encode (TmSub t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkSub [a1, a2]- encode (TmMul t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkMul [a1, a2]- encode (TmDiv t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkDiv a1 a2- encode (TmMod t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkMod a1 a2- encode (TmRem t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkRem a1 a2- encode (TmMinus t) = do- a <- encode t- mkUnaryMinus a- encode (TmIf p c a) = do- a1 <- encode p- a2 <- encode c- a3 <- encode a- mkIte a1 a2 a3- encode (TmApp fname args retty) = do- retSort <- sort retty- encodeApp fname args retSort--instance Z3Sorted Term where- sort (TmVar x) = do- ctx <- getQualifierCtx- case M.lookup x ctx of- Just (_, s) -> return s- Nothing -> smtError $ "Can't find variable " ++ x- sort (TmNum _) = mkIntSort- sort (TmBool _) = mkBoolSort- sort (TmLE _ _) = mkBoolSort- sort (TmGE _ _) = mkBoolSort- sort (TmAdd _ _) = mkIntSort- sort (TmSub _ _) = mkIntSort- sort (TmMul _ _) = mkIntSort- sort (TmDiv _ _) = mkIntSort- sort (TmMod _ _) = mkIntSort- sort (TmRem _ _) = mkIntSort- sort (TmMinus _) = mkIntSort- sort (TmIf _ c _) = sort c- sort (TmApp _ _ retty) = sort retty--instance Z3Sorted Type where- sort TyBool = mkBoolSort- sort TyInt = mkIntSort- sort TyDouble = mkRealSort- sort (TyMap ty1 ty2) = do- s1 <- sort ty1- s2 <- sort ty2- mkArraySort s1 s2- sort (TySet ty) = do- s <- sort ty- intSort <- mkIntSort- mkArraySort s intSort- sort (TyADT tyName) = do- ctx <- getDataTypeCtx- case M.lookup tyName ctx of- Just s -> return s- Nothing -> smtError $ "Undefined type: " ++ tyName
test/Z3/Test.hs view
@@ -1,13 +1,15 @@ module Z3.Test (spec) where -import Z3.Class-import Z3.Logic-import Z3.Demo-import Z3.Encoding-import Z3.Context-import Z3.Assertion import Z3.Monad hiding (mkMap) +import Z3.Base.Class+import Z3.Base.Logic+import Z3.Base.Atom++import Z3.Z3Pred+import Z3.Datatypes+import Z3.Context+ import Control.Monad (forM_) import Control.Monad.IO.Class (liftIO) import qualified Data.Map as M@@ -15,7 +17,7 @@ import Test.Hspec -tests :: [(Z3Pred, Either String Result)]+tests :: [(Z3Pred Term, Either String Result)] tests = [ (PTrue, Right Sat), (PFalse, Right Unsat),@@ -24,45 +26,40 @@ (PDisj PTrue PFalse, Right Sat), (PDisj PFalse PFalse, Right Unsat), (PNeg PFalse, Right Sat),- (PAssert (Equal (1 :: Int) (1 :: Int)), Right Sat),- (PAssert (Equal True False), Right Unsat),+ (PAtom (Equal (1 :: Int) (1 :: Int)), Right Sat),+ (PAtom (Equal True False), Right Unsat), (PForAll "x" TyInt PTrue, Right Sat),- (PExists "x" TyInt (PAssert (Equal (TmVar "x") (1 :: Int))), Right Sat),- (PForAll "x" TyInt (PImpli (PAssert (Less (TmVar "x") (0 :: Int)))- (PAssert (Less (TmVar "x") (1 :: Int)))), Right Sat),- (PForAll "x" TyInt (PImpli (PAssert (Less (TmVar "x") (1 :: Int)))- (PAssert (Less (TmVar "x") (0 :: Int)))), Right Unsat),+ (PExists "x" TyInt (PAtom (Equal (TmVar "x") (1 :: Int))), Right Sat),+ (PForAll "x" TyInt (PImpli (PAtom (Less (TmVar "x") (0 :: Int)))+ (PAtom (Less (TmVar "x") (1 :: Int)))), Right Sat),+ (PForAll "x" TyInt (PImpli (PAtom (Less (TmVar "x") (1 :: Int)))+ (PAtom (Less (TmVar "x") (0 :: Int)))), Right Unsat), (PForAll "x" TyInt (PImpli PTrue PFalse), Right Unsat),- (PAssert (InMap (1 :: Int) (1 :: Int) (M.singleton (1 :: Int) 1)), Right Sat),- (PAssert (InSet (10 :: Int) (S.singleton (10 :: Int))), Right Sat),- (PAssert (Equal (TmApp "none" Nil (TyADT "optionInt"))- (TmApp "none" Nil (TyADT "optionInt"))), Right Sat),+ (PAtom (InMap (1 :: Int) (1 :: Int) (M.singleton (1 :: Int) 1)), Right Sat),+ (PAtom (InSet (10 :: Int) (S.singleton (10 :: Int))), Right Sat),+ (PAtom (Equal (TmCons "none" Nil (TyADT "optionInt"))+ (TmCons "none" Nil (TyADT "optionInt"))), Right Sat), (PForAll "x" (TyADT "optionInt") PTrue, Right Sat),- (PAssert (Equal (TmApp "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))- (TmApp "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))), Right Sat),- (PExists "x" TyInt $ PConj (PAssert $ GreaterE (TmSub (TmVar "x") (TmNum 1)) (3 :: Int))- (PAssert $ GreaterE (TmSub (TmSub (TmVar "x") (TmNum 2)) (TmNum 1)) (0 :: Int)), Right Sat),- (PExists "x" TyInt $ PConj (PAssert $ Less (TmVar "x") (TmNum 0))- (PNeg $ PAssert $ LessE (TmVar "x") (TmNum 0)), Right Unsat),- (PExists2 "x" "y" TyInt $ PConj (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")- (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat),- (PExists2 "x" "y" TyInt $ PConj (PConj (PAssert $ LessE (TmVar "x") $ TmNum 3)- (PAssert $ LessE (TmVar "y") $ TmNum 3))- (PAssert $ GreaterE (TmAdd (TmVar "x") (TmVar "y")) $ TmNum 9), Right Unsat),- (PExists2 "x" "y" TyInt $ PNeg $ PConj (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")- (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat)+ (PAtom (Equal (TmCons "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))+ (TmCons "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))), Right Sat),+ (PExists "x" TyInt $ PConj (PAtom $ GreaterE (TmSub (TmVar "x") (TmInt 1)) (3 :: Int))+ (PAtom $ GreaterE (TmSub (TmSub (TmVar "x") (TmInt 2)) (TmInt 1)) (0 :: Int)), Right Sat),+ (PExists "x" TyInt $ PConj (PAtom $ Less (TmVar "x") (TmInt 0))+ (PNeg $ PAtom $ LessE (TmVar "x") (TmInt 0)), Right Unsat),+ (PExists2 "x" "y" TyInt $ PConj (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")+ (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat),+ (PExists2 "x" "y" TyInt $ PConj (PConj (PAtom $ LessE (TmVar "x") $ TmInt 3)+ (PAtom $ LessE (TmVar "y") $ TmInt 3))+ (PAtom $ GreaterE (TmAdd (TmVar "x") (TmVar "y")) $ TmInt 9), Right Unsat),+ (PExists2 "x" "y" TyInt $ PNeg $ PConj (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")+ (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat) ] -checkPre :: Z3Pred -> Z3SMT () (Result, Maybe Model)-checkPre pre = local $ do- ast <- encode pre- local (assert ast >> getModel)--test :: (Z3Pred, Either String Result) -> IO ()+test :: (Z3Pred Term, Either String Result) -> IO () test (p, expected) = do let adts = [("optionInt", [("none", []), ("just", [("val", TyInt)])])]- ret <- runSMT adts () $ do+ ret <- runSMT emptyValBindings adts () $ do (r, _mm) <- checkPre p case r of Unsat -> do@@ -76,4 +73,3 @@ spec = forM_ tests $ (\pair@(p, expected) -> do it {-(show p ++ " → " ++ show expected )-}"no show" $ test pair)-
z3-encoding.cabal view
@@ -2,14 +2,14 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: z3-encoding-version: 0.2.1.1+version: 0.3.0.0 synopsis: High-level assertion encoding to Z3 solver description: A library targeting at providing high-level, extensible, easy to use Haskell interface to Z3 solver. license: MIT license-file: LICENSE-author: Zhen Zhang-maintainer: izgzhen@gmail.com+author: Zhen Zhang <izgzhen@gmail.com>+maintainer: Zhen Zhang <izgzhen@gmail.com> -- copyright: category: Language build-type: Simple@@ -20,11 +20,12 @@ location: https://github.com/izgzhen/z3-encoding library- exposed-modules: Z3.Class- Z3.Logic- Z3.Encoding- Z3.Assertion+ exposed-modules: Z3.Base.Class+ Z3.Base.Logic+ Z3.Base.Atom+ Z3.Datatypes Z3.Context+ Z3.Z3Pred -- other-modules: -- other-extensions: build-depends: base >=4.9 && <4.10,@@ -37,13 +38,14 @@ ScopedTypeVariables MultiParamTypeClasses RankNTypes+ LambdaCase GADTs default-language: Haskell2010 ghc-options: -Wall test-suite z3-encoding-test type: exitcode-stdio-1.0- other-modules: Z3.Test, Z3.Demo+ other-modules: Z3.Test hs-source-dirs: test main-is: Spec.hs build-depends: base >=4.9 && <4.10@@ -52,5 +54,5 @@ , hspec >= 1.3 , containers >=0.5 && <0.6 ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall- default-extensions: StandaloneDeriving+-- default-extensions: StandaloneDeriving default-language: Haskell2010