------------------------------------------------------------------------
-- |
-- 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
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 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
$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 :: (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 (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 :: SatResult mdl core -> Bool
isSat Sat{} = Bool
True
isSat SatResult mdl core
_ = Bool
False

isUnsat :: SatResult mdl core -> Bool
isUnsat :: SatResult mdl core -> Bool
isUnsat Unsat{} = Bool
True
isUnsat SatResult mdl core
_ = Bool
False

isUnknown :: SatResult mdl core -> Bool
isUnknown :: SatResult mdl core -> Bool
isUnknown SatResult mdl core
Unknown = Bool
True
isUnknown SatResult mdl core
_ = Bool
False

forgetModelAndCore :: SatResult a b -> SatResult () ()
forgetModelAndCore :: 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