Commits

David Castro  committed adbae0d

Result datatype simplified in Z3.Base.

  • Participants
  • Parent commits 6530b4e

Comments (0)

Files changed (3)

     , Model
 
     -- ** Satisfiability result
-    , Result(..)
+    , Result
 
     -- * Configuration
     , mkConfig
 
 import Z3.Base.C
 
-import Control.Applicative ( Applicative(..), (<$>) )
+import Control.Applicative ( (<$>) )
 import Control.Exception ( bracket )
-import Data.Foldable ( Foldable )
 import Data.Int
 import Data.Ratio ( Ratio, numerator, denominator, (%) )
-import Data.Traversable ( Traversable )
 import Data.Typeable ( Typeable )
 import Data.Word
 import Foreign hiding ( toBool )
 
 -- | Result of a satisfiability check.
 --
-data Result a
-    = Sat a
+data Result
+    = Sat
     | Unsat
     | Undef
-    deriving (Eq, Ord, Read, Show, Foldable, Traversable)
-
-instance Functor Result where
-  fmap f (Sat x) = Sat $ f x
-  fmap _ Unsat   = Unsat
-  fmap _ Undef   = Undef
-
-instance Applicative Result where
-  pure = return
-  Sat f <*> x = f <$> x
-  Unsat <*> _ = Unsat
-  Undef <*> _ = Undef
-
-instance Monad Result where
-  return = Sat
-  Sat x >>= f = f x
-  Unsat >>= _ = Unsat
-  Undef >>= _ = Undef
+    deriving (Eq, Ord, Read, Show)
 
 -- | Convert 'Z3_lbool' from Z3.Base.C to 'Result'
 --
-toResult :: Z3_lbool -> Result ()
+toResult :: Z3_lbool -> Result
 toResult lb
-    | lb == z3_l_true  = Sat ()
+    | lb == z3_l_true  = Sat
     | lb == z3_l_false = Unsat
     | lb == z3_l_undef = Undef
     | otherwise        = error "Z3.Base.toResult: illegal `Z3_lbool' value"
 --
 -- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>
 --
-getModel :: Context -> IO (Result Model)
+getModel :: Context -> IO (Result, Maybe Model)
 getModel c =
   alloca $ \mptr ->
-    z3_check_and_get_model (unContext c) mptr >>= peekModel mptr . toResult
-  where peekModel :: Ptr (Ptr Z3_model)
-                  -> Result ()
-                  -> IO (Result Model)
-        peekModel _ Unsat                   = return Unsat
-        peekModel _ Undef                   = return Undef
-        peekModel p (Sat ()) | p == nullPtr = error "Z3.Base.getModel: Panic! nullPtr!"
-                             | otherwise    = Sat . Model <$> peek p
+    z3_check_and_get_model (unContext c) mptr >>= \lb ->
+      (toResult lb,) <$> peekModel mptr
+  where peekModel :: Ptr (Ptr Z3_model) -> IO (Maybe Model)
+        peekModel p | p == nullPtr = return Nothing
+                    | otherwise    = Just . Model <$> peek p
 
 -- | Delete a model object.
 --
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>
 --
-check :: Context -> IO (Result ())
+check :: Context -> IO Result
 check ctx = toResult <$> z3_check (unContext ctx)
 
 -- TODO Constraints: Z3_check_assumptions

File Z3/Lang/Monad.hs

     , showModel
 
     -- * Satisfiability result
-    , Base.Result(..)
+    , Base.Result
 
     ) where
 
 assertCnstr = liftZ3Op2 Base.assertCnstr
 
 -- | Check satisfiability.
-check :: Z3 (Base.Result ())
+check :: Z3 Base.Result
 check = liftZ3Op Base.check
 
 eval :: Base.Model -> Base.AST -> Z3 (Maybe Base.AST)
 getReal :: Base.AST -> Z3 Rational
 getReal = liftZ3Op2 Base.getReal
 
-getModel :: Z3 (Base.Result Base.Model)
+getModel :: Z3 (Base.Result, Maybe Base.Model)
 getModel = liftZ3Op Base.getModel
 
 delModel :: Base.Model -> Z3 ()
 delModel = liftZ3Op2 Base.delModel
 
-withModel :: (Base.Model -> Z3 a) -> Z3 (Base.Result a)
+withModel :: (Base.Model -> Z3 a) -> Z3 (Maybe a)
 withModel f = do
- m <- getModel
+ (_,m) <- getModel
  r <- traverse f m
  _ <- traverse delModel m
  return r
 
-showModel :: Z3 (Base.Result String)
+showModel :: Z3 (Maybe String)
 showModel = withModel (liftZ3Op2 Base.showModel)
 
 showContext :: Z3 String

File Z3/Lang/Prelude.hs

 
     -- * Z3 script
       Z3
-    , Base.Result(..)
+    , Base.Result
     , evalZ3
     , Args(..)
     , stdArgs
 
 -- | Check satisfiability and evaluate the given expression if a model exists.
 --
-checkModel :: forall a. IsTy a => Expr a -> Z3 (Result a)
+checkModel :: forall a. IsTy a => Expr a -> Z3 (Maybe a)
 checkModel e = do
   a <- compileWithTCC e
   withModel (fixResult a)