    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.SatResult
    -- Description : Simple datastructure for capturing the result of a SAT/SMT query
    -- Copyright   : (c) Galois, Inc 2015-2020
    -- License     : BSD3
    -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
    -- Stability   : provisional
    ------------------------------------------------------------------------
    {-# 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
    [SatResult mdl core] -> ShowS
    SatResult mdl core -> String
    (Int -> SatResult mdl core -> ShowS)
    -> (SatResult mdl core -> String)
    -> ([SatResult mdl core] -> ShowS)
    -> Show (SatResult mdl core)
    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
    $cshowsPrec :: forall mdl core.
    (Show mdl, Show core) =>
    Int -> SatResult mdl core -> ShowS
    showsPrec :: Int -> SatResult mdl core -> ShowS
    $cshow :: forall mdl core.
    (Show mdl, Show core) =>
    SatResult mdl core -> String
    show :: SatResult mdl core -> String
    $cshowList :: forall mdl core.
    (Show mdl, Show core) =>
    [SatResult mdl core] -> ShowS
    showList :: [SatResult mdl core] -> ShowS
    Show, (forall x. SatResult mdl core -> Rep (SatResult mdl core) x)
    -> (forall x. Rep (SatResult mdl core) x -> SatResult mdl core)
    -> Generic (SatResult mdl core)
    forall x. Rep (SatResult mdl core) x -> SatResult mdl core
    forall x. SatResult mdl core -> Rep (SatResult mdl core) x
    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
    $cfrom :: forall mdl core x. SatResult mdl core -> Rep (SatResult mdl core) x
    from :: forall x. SatResult mdl core -> Rep (SatResult mdl core) x
    $cto :: forall mdl core x. Rep (SatResult mdl core) x -> SatResult mdl core
    to :: forall x. Rep (SatResult mdl core) x -> SatResult mdl core
    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   -> q -> SatResult q r
    forall mdl core. mdl -> SatResult mdl core
    Sat (q -> SatResult q r) -> t q -> t (SatResult q r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> t q
    f a
    m
      Unsat b
    c -> r -> SatResult q r
    forall mdl core. core -> SatResult mdl core
    Unsat (r -> SatResult q r) -> t r -> t (SatResult q r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> b -> t r
    g b
    c
      SatResult a b
    Unknown -> SatResult q r -> t (SatResult q r)
    forall a. a -> t a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure SatResult q r
    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{} = () -> SatResult () ()
    forall mdl core. mdl -> SatResult mdl core
    Sat ()
    forgetModelAndCore Unsat{} = () -> SatResult () ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
    forgetModelAndCore SatResult a b
    Unknown = SatResult () ()
    forall mdl core. SatResult mdl core
    Unknown