module Language.Hasmtlib.Type.Option where

import Language.Hasmtlib.Internal.Render
import Data.Data (Data)
import Data.ByteString.Builder

-- | Options for SMT-Solvers.
data SMTOption =
    PrintSuccess  Bool              -- ^ Print \"success\" after each operation
  | ProduceModels Bool              -- ^ Produce a satisfying assignment after each successful checkSat
  | Incremental   Bool              -- ^ Incremental solving
  deriving (Int -> SMTOption -> ShowS
[SMTOption] -> ShowS
SMTOption -> String
(Int -> SMTOption -> ShowS)
-> (SMTOption -> String)
-> ([SMTOption] -> ShowS)
-> Show SMTOption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SMTOption -> ShowS
showsPrec :: Int -> SMTOption -> ShowS
$cshow :: SMTOption -> String
show :: SMTOption -> String
$cshowList :: [SMTOption] -> ShowS
showList :: [SMTOption] -> ShowS
Show, SMTOption -> SMTOption -> Bool
(SMTOption -> SMTOption -> Bool)
-> (SMTOption -> SMTOption -> Bool) -> Eq SMTOption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SMTOption -> SMTOption -> Bool
== :: SMTOption -> SMTOption -> Bool
$c/= :: SMTOption -> SMTOption -> Bool
/= :: SMTOption -> SMTOption -> Bool
Eq, Eq SMTOption
Eq SMTOption =>
(SMTOption -> SMTOption -> Ordering)
-> (SMTOption -> SMTOption -> Bool)
-> (SMTOption -> SMTOption -> Bool)
-> (SMTOption -> SMTOption -> Bool)
-> (SMTOption -> SMTOption -> Bool)
-> (SMTOption -> SMTOption -> SMTOption)
-> (SMTOption -> SMTOption -> SMTOption)
-> Ord SMTOption
SMTOption -> SMTOption -> Bool
SMTOption -> SMTOption -> Ordering
SMTOption -> SMTOption -> SMTOption
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SMTOption -> SMTOption -> Ordering
compare :: SMTOption -> SMTOption -> Ordering
$c< :: SMTOption -> SMTOption -> Bool
< :: SMTOption -> SMTOption -> Bool
$c<= :: SMTOption -> SMTOption -> Bool
<= :: SMTOption -> SMTOption -> Bool
$c> :: SMTOption -> SMTOption -> Bool
> :: SMTOption -> SMTOption -> Bool
$c>= :: SMTOption -> SMTOption -> Bool
>= :: SMTOption -> SMTOption -> Bool
$cmax :: SMTOption -> SMTOption -> SMTOption
max :: SMTOption -> SMTOption -> SMTOption
$cmin :: SMTOption -> SMTOption -> SMTOption
min :: SMTOption -> SMTOption -> SMTOption
Ord, Typeable SMTOption
Typeable SMTOption =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SMTOption -> c SMTOption)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SMTOption)
-> (SMTOption -> Constr)
-> (SMTOption -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SMTOption))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTOption))
-> ((forall b. Data b => b -> b) -> SMTOption -> SMTOption)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SMTOption -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SMTOption -> r)
-> (forall u. (forall d. Data d => d -> u) -> SMTOption -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SMTOption -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SMTOption -> m SMTOption)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTOption -> m SMTOption)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTOption -> m SMTOption)
-> Data SMTOption
SMTOption -> Constr
SMTOption -> DataType
(forall b. Data b => b -> b) -> SMTOption -> SMTOption
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SMTOption -> u
forall u. (forall d. Data d => d -> u) -> SMTOption -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTOption -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTOption -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTOption
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTOption -> c SMTOption
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTOption)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTOption)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTOption -> c SMTOption
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTOption -> c SMTOption
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTOption
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTOption
$ctoConstr :: SMTOption -> Constr
toConstr :: SMTOption -> Constr
$cdataTypeOf :: SMTOption -> DataType
dataTypeOf :: SMTOption -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTOption)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTOption)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTOption)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTOption)
$cgmapT :: (forall b. Data b => b -> b) -> SMTOption -> SMTOption
gmapT :: (forall b. Data b => b -> b) -> SMTOption -> SMTOption
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTOption -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTOption -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTOption -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTOption -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTOption -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SMTOption -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTOption -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTOption -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTOption -> m SMTOption
Data)

instance Render SMTOption where
  render :: SMTOption -> Builder
render (PrintSuccess  Bool
b) = Builder -> Builder -> Bool -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"set-option" (Builder
":print-success"  :: Builder) Bool
b
  render (ProduceModels Bool
b) = Builder -> Builder -> Bool -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"set-option" (Builder
":produce-models" :: Builder) Bool
b
  render (Incremental   Bool
b) = Builder -> Builder -> Bool -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"set-option" (Builder
":incremental"    :: Builder) Bool
b