{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Control.Types (
CheckSatResult(..)
, Logic(..)
, SMTOption(..), isStartModeOption, setSMTOption
, SMTInfoFlag(..)
, SMTErrorBehavior(..)
, SMTReasonUnknown(..)
, SMTInfoResponse(..)
) where
import Generics.Deriving.Base (Generic)
import Generics.Deriving.Show (GShow, gshow)
import Control.DeepSeq (NFData(..))
data CheckSatResult = Sat
| Unsat
| Unk
deriving (CheckSatResult -> CheckSatResult -> Bool
(CheckSatResult -> CheckSatResult -> Bool)
-> (CheckSatResult -> CheckSatResult -> Bool) -> Eq CheckSatResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CheckSatResult -> CheckSatResult -> Bool
$c/= :: CheckSatResult -> CheckSatResult -> Bool
== :: CheckSatResult -> CheckSatResult -> Bool
$c== :: CheckSatResult -> CheckSatResult -> Bool
Eq, Int -> CheckSatResult -> ShowS
[CheckSatResult] -> ShowS
CheckSatResult -> String
(Int -> CheckSatResult -> ShowS)
-> (CheckSatResult -> String)
-> ([CheckSatResult] -> ShowS)
-> Show CheckSatResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CheckSatResult] -> ShowS
$cshowList :: [CheckSatResult] -> ShowS
show :: CheckSatResult -> String
$cshow :: CheckSatResult -> String
showsPrec :: Int -> CheckSatResult -> ShowS
$cshowsPrec :: Int -> CheckSatResult -> ShowS
Show)
data SMTInfoFlag = AllStatistics
| AssertionStackLevels
| Authors
| ErrorBehavior
| Name
| ReasonUnknown
| Version
| InfoKeyword String
data SMTErrorBehavior = ErrorImmediateExit
| ErrorContinuedExecution
deriving Int -> SMTErrorBehavior -> ShowS
[SMTErrorBehavior] -> ShowS
SMTErrorBehavior -> String
(Int -> SMTErrorBehavior -> ShowS)
-> (SMTErrorBehavior -> String)
-> ([SMTErrorBehavior] -> ShowS)
-> Show SMTErrorBehavior
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTErrorBehavior] -> ShowS
$cshowList :: [SMTErrorBehavior] -> ShowS
show :: SMTErrorBehavior -> String
$cshow :: SMTErrorBehavior -> String
showsPrec :: Int -> SMTErrorBehavior -> ShowS
$cshowsPrec :: Int -> SMTErrorBehavior -> ShowS
Show
data SMTReasonUnknown = UnknownMemOut
| UnknownIncomplete
| UnknownTimeOut
| UnknownOther String
deriving ((forall x. SMTReasonUnknown -> Rep SMTReasonUnknown x)
-> (forall x. Rep SMTReasonUnknown x -> SMTReasonUnknown)
-> Generic SMTReasonUnknown
forall x. Rep SMTReasonUnknown x -> SMTReasonUnknown
forall x. SMTReasonUnknown -> Rep SMTReasonUnknown x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SMTReasonUnknown x -> SMTReasonUnknown
$cfrom :: forall x. SMTReasonUnknown -> Rep SMTReasonUnknown x
Generic, SMTReasonUnknown -> ()
(SMTReasonUnknown -> ()) -> NFData SMTReasonUnknown
forall a. (a -> ()) -> NFData a
rnf :: SMTReasonUnknown -> ()
$crnf :: SMTReasonUnknown -> ()
NFData)
instance Show SMTReasonUnknown where
show :: SMTReasonUnknown -> String
show UnknownMemOut = "memout"
show UnknownIncomplete = "incomplete"
show UnknownTimeOut = "timeout"
show (UnknownOther s :: String
s) = String
s
data SMTInfoResponse = Resp_Unsupported
| Resp_AllStatistics [(String, String)]
| Resp_AssertionStackLevels Integer
| Resp_Authors [String]
| Resp_Error SMTErrorBehavior
| Resp_Name String
| Resp_ReasonUnknown SMTReasonUnknown
| Resp_Version String
| Resp_InfoKeyword String [String]
deriving Int -> SMTInfoResponse -> ShowS
[SMTInfoResponse] -> ShowS
SMTInfoResponse -> String
(Int -> SMTInfoResponse -> ShowS)
-> (SMTInfoResponse -> String)
-> ([SMTInfoResponse] -> ShowS)
-> Show SMTInfoResponse
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTInfoResponse] -> ShowS
$cshowList :: [SMTInfoResponse] -> ShowS
show :: SMTInfoResponse -> String
$cshow :: SMTInfoResponse -> String
showsPrec :: Int -> SMTInfoResponse -> ShowS
$cshowsPrec :: Int -> SMTInfoResponse -> ShowS
Show
instance Show SMTInfoFlag where
show :: SMTInfoFlag -> String
show AllStatistics = ":all-statistics"
show AssertionStackLevels = ":assertion-stack-levels"
show Authors = ":authors"
show ErrorBehavior = ":error-behavior"
show Name = ":name"
show ReasonUnknown = ":reason-unknown"
show Version = ":version"
show (InfoKeyword s :: String
s) = String
s
data SMTOption = DiagnosticOutputChannel FilePath
| ProduceAssertions Bool
| ProduceAssignments Bool
| ProduceProofs Bool
| ProduceInterpolants Bool
| ProduceUnsatAssumptions Bool
| ProduceUnsatCores Bool
| RandomSeed Integer
| ReproducibleResourceLimit Integer
| SMTVerbosity Integer
| OptionKeyword String [String]
| SetLogic Logic
| SetInfo String [String]
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
showList :: [SMTOption] -> ShowS
$cshowList :: [SMTOption] -> ShowS
show :: SMTOption -> String
$cshow :: SMTOption -> String
showsPrec :: Int -> SMTOption -> ShowS
$cshowsPrec :: Int -> SMTOption -> ShowS
Show, (forall x. SMTOption -> Rep SMTOption x)
-> (forall x. Rep SMTOption x -> SMTOption) -> Generic SMTOption
forall x. Rep SMTOption x -> SMTOption
forall x. SMTOption -> Rep SMTOption x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SMTOption x -> SMTOption
$cfrom :: forall x. SMTOption -> Rep SMTOption x
Generic, SMTOption -> ()
(SMTOption -> ()) -> NFData SMTOption
forall a. (a -> ()) -> NFData a
rnf :: SMTOption -> ()
$crnf :: SMTOption -> ()
NFData)
isStartModeOption :: SMTOption -> Bool
isStartModeOption :: SMTOption -> Bool
isStartModeOption DiagnosticOutputChannel{} = Bool
False
isStartModeOption ProduceAssertions{} = Bool
True
isStartModeOption ProduceAssignments{} = Bool
True
isStartModeOption ProduceProofs{} = Bool
True
isStartModeOption ProduceInterpolants{} = Bool
True
isStartModeOption ProduceUnsatAssumptions{} = Bool
True
isStartModeOption ProduceUnsatCores{} = Bool
True
isStartModeOption RandomSeed{} = Bool
True
isStartModeOption ReproducibleResourceLimit{} = Bool
False
isStartModeOption SMTVerbosity{} = Bool
False
isStartModeOption OptionKeyword{} = Bool
True
isStartModeOption SetLogic{} = Bool
True
isStartModeOption SetInfo{} = Bool
False
smtBool :: Bool -> String
smtBool :: Bool -> String
smtBool True = "true"
smtBool False = "false"
setSMTOption :: SMTOption -> String
setSMTOption :: SMTOption -> String
setSMTOption = SMTOption -> String
cvt
where cvt :: SMTOption -> String
cvt (DiagnosticOutputChannel f :: String
f) = [String] -> String
opt [":diagnostic-output-channel", ShowS
forall a. Show a => a -> String
show String
f]
cvt (ProduceAssertions b :: Bool
b) = [String] -> String
opt [":produce-assertions", Bool -> String
smtBool Bool
b]
cvt (ProduceAssignments b :: Bool
b) = [String] -> String
opt [":produce-assignments", Bool -> String
smtBool Bool
b]
cvt (ProduceProofs b :: Bool
b) = [String] -> String
opt [":produce-proofs", Bool -> String
smtBool Bool
b]
cvt (ProduceInterpolants b :: Bool
b) = [String] -> String
opt [":produce-interpolants", Bool -> String
smtBool Bool
b]
cvt (ProduceUnsatAssumptions b :: Bool
b) = [String] -> String
opt [":produce-unsat-assumptions", Bool -> String
smtBool Bool
b]
cvt (ProduceUnsatCores b :: Bool
b) = [String] -> String
opt [":produce-unsat-cores", Bool -> String
smtBool Bool
b]
cvt (RandomSeed i :: Integer
i) = [String] -> String
opt [":random-seed", Integer -> String
forall a. Show a => a -> String
show Integer
i]
cvt (ReproducibleResourceLimit i :: Integer
i) = [String] -> String
opt [":reproducible-resource-limit", Integer -> String
forall a. Show a => a -> String
show Integer
i]
cvt (SMTVerbosity i :: Integer
i) = [String] -> String
opt [":verbosity", Integer -> String
forall a. Show a => a -> String
show Integer
i]
cvt (OptionKeyword k :: String
k as :: [String]
as) = [String] -> String
opt (String
k String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
as)
cvt (SetLogic l :: Logic
l) = Logic -> String
logic Logic
l
cvt (SetInfo k :: String
k as :: [String]
as) = [String] -> String
info (String
k String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
as)
opt :: [String] -> String
opt xs :: [String]
xs = "(set-option " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
info :: [String] -> String
info xs :: [String]
xs = "(set-info " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
logic :: Logic -> String
logic Logic_NONE = "; NB. not setting the logic per user request of Logic_NONE"
logic l :: Logic
l = "(set-logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Logic -> String
forall a. Show a => a -> String
show Logic
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
data Logic
= AUFLIA
| AUFLIRA
| AUFNIRA
| LRA
| QF_ABV
| QF_AUFBV
| QF_AUFLIA
| QF_AX
| QF_BV
| QF_IDL
| QF_LIA
| QF_LRA
| QF_NIA
| QF_NRA
| QF_RDL
| QF_UF
| QF_UFBV
| QF_UFIDL
| QF_UFLIA
| QF_UFLRA
| QF_UFNRA
| QF_UFNIRA
| UFLRA
| UFNIA
| QF_FPBV
| QF_FP
| QF_FD
| QF_S
| Logic_ALL
| Logic_NONE
| CustomLogic String
deriving ((forall x. Logic -> Rep Logic x)
-> (forall x. Rep Logic x -> Logic) -> Generic Logic
forall x. Rep Logic x -> Logic
forall x. Logic -> Rep Logic x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Logic x -> Logic
$cfrom :: forall x. Logic -> Rep Logic x
Generic, Logic -> ()
(Logic -> ()) -> NFData Logic
forall a. (a -> ()) -> NFData a
rnf :: Logic -> ()
$crnf :: Logic -> ()
NFData)
instance GShow Logic
instance Show Logic where
show :: Logic -> String
show Logic_ALL = "ALL"
show (CustomLogic l :: String
l) = String
l
show l :: Logic
l = Logic -> String
forall a. GShow a => a -> String
gshow Logic
l
{-# ANN type SMTInfoResponse ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type Logic ("HLint: ignore Use camelCase" :: String) #-}