expressions-z3 0.1.4 → 0.1.5
raw patch · 4 files changed
+160/−48 lines, 4 files
Files
- ChangeLog.md +4/−0
- expressions-z3.cabal +1/−1
- src/Data/Expression/Z3.hs +77/−1
- test/Main.hs +78/−46
ChangeLog.md view
@@ -1,5 +1,9 @@ # Revision history for expressions-z3 +## 0.1.5++* Z3 API+ ## 0.1.4 * Bump dependencies
expressions-z3.cabal view
@@ -1,5 +1,5 @@ name: expressions-z3-version: 0.1.4+version: 0.1.5 synopsis: Encode and Decode expressions from Z3 ASTs description: A simple interface for converting expressions back and forth between pure
src/Data/Expression/Z3.hs view
@@ -10,8 +10,25 @@ , TypeOperators , UndecidableInstances #-} -module Data.Expression.Z3 ( IToZ3, toZ3, IFromZ3, fromZ3 ) where+module Data.Expression.Z3 ( IToZ3+ , toZ3+ , IFromZ3+ , fromZ3 + -- Z3 API wrappers+ , assert+ , model+ , unsatcore+ , interpolate+ , eliminate++ -- re-export Z3 API+ , Z3.local+ , Z3.push+ , Z3.pop+ , Z3.check+ , Z3.Result(..) ) where+ import Control.Applicative hiding (Const) import Control.Monad import Control.Monad.IO.Class@@ -366,3 +383,62 @@ fromZ3 a = let r = ifromZ3 (Proxy :: Proxy f) r in head' <=< fmap (mapMaybe toStaticallySorted) . toList . 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)+++--+-- Z3 API+--++assert :: forall (f :: (Sort -> *) -> Sort -> *) z3. ( IToZ3 f, Z3.MonadZ3 z3 ) => IFix f 'BooleanSort -> z3 ()+assert = Z3.assert <=< toZ3++model :: forall (f :: (Sort -> *) -> Sort -> *) (s :: Sort) z3.+ ( IToZ3 f, IFromZ3 f, IShow f, Z3.MonadZ3 z3, SingI s ) => IFix f s -> z3 (IFix f s)+model e = do+ e' <- toZ3 e+ r <- Z3.getModel+ case r of+ (Z3.Sat, Just m) -> do+ v <- Z3.modelEval m e' True+ case v of+ Just v' -> fromZ3 v'+ Nothing -> error $ "failed valuating " ++ show e+ (Z3.Unsat, _) -> error "failed extracting model from an unsatisfiable query"+ _ -> error "failed extracting model"++unsatcore :: forall (f :: (Sort -> *) -> Sort -> *) z3. ( IToZ3 f, Z3.MonadZ3 z3 ) => [IFix f 'BooleanSort] -> z3 [IFix f 'BooleanSort]+unsatcore fs = do+ as <- mapM toZ3 fs+ ps <- mapM (const $ Z3.mkFreshBoolVar "p") fs+ zipWithM_ (\a p -> Z3.assert =<< Z3.mkIff a p) as ps+ r <- Z3.checkAssumptions ps+ case r of+ Z3.Sat -> error "failed extracting unsat core from a satisfiable query"+ Z3.Unsat -> map (M.fromList (zip ps fs) M.!) <$> Z3.getUnsatCore+ _ -> error "failed extracting unsat core"++interpolate :: forall (f :: (Sort -> *) -> Sort -> *) z3.+ ( IToZ3 f, IFromZ3 f, Z3.MonadZ3 z3 ) => [IFix f 'BooleanSort] -> z3 [IFix f 'BooleanSort]+interpolate [] = return []+interpolate [_] = return []+interpolate (f : fs) = do+ f' <- toZ3 f+ fs' <- mapM toZ3 fs+ q <- foldM (\a g -> Z3.mkAnd . (: [g]) =<< Z3.mkInterpolant a) f' fs'+ r <- Z3.local $ Z3.computeInterpolant q =<< Z3.mkParams++ case r of+ Just (Left _ ) -> error "failed extracting interpolants from a satisfiable query"+ Just (Right is) -> mapM fromZ3 is+ _ -> error "failed extracting interpolants"++eliminate :: forall (f :: (Sort -> *) -> Sort -> *) z3.+ ( IToZ3 f, IFromZ3 f, Z3.MonadZ3 z3 ) => IFix f 'BooleanSort -> z3 (IFix f 'BooleanSort)+eliminate f = do+ g <- Z3.mkGoal True True False+ Z3.goalAssert g =<< toZ3 f+ qe <- Z3.mkTactic "qe"+ aig <- Z3.mkTactic "aig"+ t <- Z3.andThenTactic qe aig+ a <- Z3.applyTactic t g+ fromZ3 =<< Z3.mkAnd =<< Z3.getGoalFormulas =<< Z3.getApplyResultSubgoal a 0
test/Main.hs view
@@ -6,13 +6,13 @@ , RankNTypes , TypeOperators #-} -import Control.Applicative+import Control.Applicative hiding (Const) import Control.Monad import Control.Monad.Trans.Class import Control.Monad.Trans.Maybe import Data.Singletons import Prelude hiding (and, not)-import Z3.Monad hiding (Sort, eval)+import Z3.Monad hiding (Sort, eval, assert, local) import qualified Prelude as P @@ -20,27 +20,37 @@ import Data.Expression.Z3 data Test where- ShouldBe :: forall f. ( IToZ3 f, IShow f ) => IFix f 'BooleanSort -> Result -> Test- HasModel :: forall f (s :: Sort).- ( IToZ3 f- , IFromZ3 f- , IEq1 f- , IShow f- , EqualityF :<: f- , NegationF :<: f- , SingI s )- => IFix f 'BooleanSort -> (IFix f s, IFix f s) -> Test+ IsConstant :: forall f. ( IShow f, ArithmeticF :<: f ) => IFix f 'IntegralSort -> Int -> Test+ IsOneOf :: forall f (s :: Sort). ( IShow f, IEq1 f, IFunctor f ) => IFix f s -> [IFix f s] -> Test+ ShouldBe :: forall f. ( IToZ3 f, IShow f ) => IFix f 'BooleanSort -> Result -> Test+ HasModel :: forall f (s :: Sort).+ ( IToZ3 f+ , IFromZ3 f+ , IEq1 f+ , IShow f+ , EqualityF :<: f+ , NegationF :<: f+ , SingI s )+ => IFix f 'BooleanSort -> (IFix f s, IFix f s) -> Test test :: Test -> (String, IO Bool)+test (IsConstant a v) =+ ( "Test " ++ show a ++ " is an expected constant value"+ , return $ case match a of+ Just (Const c) -> c == v+ _ -> False )+test (IsOneOf a bs) =+ ( "Test " ++ show a ++ " is one of " ++ show bs+ , return $ any (a ==) bs ) test (ShouldBe a r) = ( "Test " ++ show a ++ " is " ++ show r , evalZ3 $ do- assert =<< toZ3 a+ assert a liftA (r ==) check ) test (HasModel a (ex, ev)) = ( "Test " ++ show a ++ " has model with " ++ show ex ++ " = " ++ show ev , evalZ3 $ do- assert =<< toZ3 a+ assert a go ) where go = do@@ -54,45 +64,67 @@ Nothing -> return False Just ew -> if ev == ew then return True else do- assert =<< toZ3 (ex ./=. ew)+ assert (ex ./=. ew) go main :: IO () main = do- putStrLn ""- guard . P.and =<< traverse eval props where+ -- model+ m <- evalZ3 . local $ do+ assert j+ model (x :: Lia 'IntegralSort) - props = [ p1, p2, p3, p4, p5, p6 ]- tests = map test props- column = maximum $ map (length . fst) tests+ -- unsat+ (u : _) <- evalZ3 $ unsatcore [ not i, h, true, k ] - eval t = do- let (n, a) = test t- putStr $ n ++ take (column - length n) (repeat ' ') ++ " "- r <- a- if r then putStrLn "passed" else putStrLn "failed"- return r+ -- interpolate+ [l] <- evalZ3 $ interpolate [ h, not i ] - p1 = f `ShouldBe` Sat- p2 = not f `ShouldBe` Unsat- p3 = g `ShouldBe` Sat- p4 = not g `ShouldBe` Unsat- p5 = h `HasModel` (x, c5)- p6 = i `HasModel` (x, c5)+ -- eliminate+ v <- evalZ3 $ eliminate g - f, g, h, i :: Lia 'BooleanSort- f = forall [x] (exists [y] (x .+. y .=. c0))- g = forall [x, y] (x .=. y .->. (x .+. c1) .=. (y .+. c1))- h = (x .+. m1 .=. y .+. c1) .&. (y .+. m1 .=. z .+. c1) .&. (z .=. c1)- i = x .>. c0+ let+ p1 = f `ShouldBe` Sat+ p2 = not f `ShouldBe` Unsat+ p3 = g `ShouldBe` Sat+ p4 = not g `ShouldBe` Unsat+ p5 = h `HasModel` (x, c5)+ p6 = i `HasModel` (x, c5)+ p7 = m `IsConstant` 8+ p8 = u `IsOneOf` [ h, not i, k ]+ p9 = not (h .->. l) `ShouldBe` Unsat+ p10 = (l .&. not i) `ShouldBe` Unsat+ p11 = not v `ShouldBe` Unsat - x, y, z :: forall f. VarF :<: f => IFix f 'IntegralSort- x = var "x"- y = var "y"- z = var "z"+ eval t = do+ let (n, a) = test t+ putStr $ n ++ take (column - length n) (repeat ' ') ++ " "+ r <- a+ if r then putStrLn "passed" else putStrLn "failed"+ return r - c0, c1, c5, m1 :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort- c0 = cnst 0- c1 = cnst 1- c5 = cnst 5- m1 = cnst (-1)+ props = [ p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11 ]+ tests = map test props+ column = maximum $ map (length . fst) tests++ putStrLn ""+ guard . P.and =<< traverse eval props where++ f, g, h, i, j :: Lia 'BooleanSort+ f = forall [x] (exists [y] (x .+. y .=. c0))+ g = forall [x, y] (x .=. y .->. (x .+. c1) .=. (y .+. c1))+ h = (x .+. m1 .=. y .+. c1) .&. (y .+. m1 .=. z .+. c1) .&. (z .=. c1)+ i = x .>. c0+ j = x .=. c5 .+. c1 .+. c1 .+. c1+ k = x .=. y .+. c1 .+. c1++ x, y, z :: forall f. VarF :<: f => IFix f 'IntegralSort+ x = var "x"+ y = var "y"+ z = var "z"++ c0, c1, c5, m1 :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort+ c0 = cnst 0+ c1 = cnst 1+ c5 = cnst 5+ m1 = cnst (-1)