diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,9 @@ # Revision history for expressions-z3 +## 0.1.5 + +* Z3 API + ## 0.1.4 * Bump dependencies diff --git a/expressions-z3.cabal b/expressions-z3.cabal --- a/expressions-z3.cabal +++ b/expressions-z3.cabal @@ -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 diff --git a/src/Data/Expression/Z3.hs b/src/Data/Expression/Z3.hs --- a/src/Data/Expression/Z3.hs +++ b/src/Data/Expression/Z3.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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)