------------------------------------------------------------------------
-- |
-- 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 (Show, Generic)

traverseSatResult :: Applicative t =>
  (a -> t q) ->
  (b -> t r) ->
  SatResult a b -> t (SatResult q r)
traverseSatResult f g = \case
  Sat m   -> Sat <$> f m
  Unsat c -> Unsat <$> g c
  Unknown -> pure Unknown

isSat :: SatResult mdl core -> Bool
isSat Sat{} = True
isSat _ = False

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

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

forgetModelAndCore :: SatResult a b -> SatResult () ()
forgetModelAndCore Sat{} = Sat ()
forgetModelAndCore Unsat{} = Unsat ()
forgetModelAndCore Unknown = Unknown