{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE LambdaCase #-}
module What4.SatResult
( SatResult(..)
, isSat
, isUnsat
, isUnknown
, forgetModelAndCore
, traverseSatResult
) where
import GHC.Generics (Generic)
data SatResult mdl core
= Sat mdl
| Unsat core
| Unknown
deriving (Int -> SatResult mdl core -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall mdl core.
(Show mdl, Show core) =>
Int -> SatResult mdl core -> ShowS
forall mdl core.
(Show mdl, Show core) =>
[SatResult mdl core] -> ShowS
forall mdl core.
(Show mdl, Show core) =>
SatResult mdl core -> String
showList :: [SatResult mdl core] -> ShowS
$cshowList :: forall mdl core.
(Show mdl, Show core) =>
[SatResult mdl core] -> ShowS
show :: SatResult mdl core -> String
$cshow :: forall mdl core.
(Show mdl, Show core) =>
SatResult mdl core -> String
showsPrec :: Int -> SatResult mdl core -> ShowS
$cshowsPrec :: forall mdl core.
(Show mdl, Show core) =>
Int -> SatResult mdl core -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall mdl core x. Rep (SatResult mdl core) x -> SatResult mdl core
forall mdl core x. SatResult mdl core -> Rep (SatResult mdl core) x
$cto :: forall mdl core x. Rep (SatResult mdl core) x -> SatResult mdl core
$cfrom :: forall mdl core x. SatResult mdl core -> Rep (SatResult mdl core) x
Generic)
traverseSatResult :: Applicative t =>
(a -> t q) ->
(b -> t r) ->
SatResult a b -> t (SatResult q r)
traverseSatResult :: forall (t :: Type -> Type) a q b r.
Applicative t =>
(a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)
traverseSatResult a -> t q
f b -> t r
g = \case
Sat a
m -> forall mdl core. mdl -> SatResult mdl core
Sat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> t q
f a
m
Unsat b
c -> forall mdl core. core -> SatResult mdl core
Unsat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> t r
g b
c
SatResult a b
Unknown -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall mdl core. SatResult mdl core
Unknown
isSat :: SatResult mdl core -> Bool
isSat :: forall mdl core. SatResult mdl core -> Bool
isSat Sat{} = Bool
True
isSat SatResult mdl core
_ = Bool
False
isUnsat :: SatResult mdl core -> Bool
isUnsat :: forall mdl core. SatResult mdl core -> Bool
isUnsat Unsat{} = Bool
True
isUnsat SatResult mdl core
_ = Bool
False
isUnknown :: SatResult mdl core -> Bool
isUnknown :: forall mdl core. SatResult mdl core -> Bool
isUnknown SatResult mdl core
Unknown = Bool
True
isUnknown SatResult mdl core
_ = Bool
False
forgetModelAndCore :: SatResult a b -> SatResult () ()
forgetModelAndCore :: forall a b. SatResult a b -> SatResult () ()
forgetModelAndCore Sat{} = forall mdl core. mdl -> SatResult mdl core
Sat ()
forgetModelAndCore Unsat{} = forall mdl core. core -> SatResult mdl core
Unsat ()
forgetModelAndCore SatResult a b
Unknown = forall mdl core. SatResult mdl core
Unknown