-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Control.Types
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Types related to interactive queries
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric  #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Control.Types (
       CheckSatResult(..)
     , Logic(..)
     , SMTOption(..), isStartModeOption, isOnlyOnceOption
     , SMTInfoFlag(..)
     , SMTErrorBehavior(..)
     , SMTReasonUnknown(..)
     , SMTInfoResponse(..)
     ) where

import Control.DeepSeq (NFData(..))
import GHC.Generics (Generic)

-- | Result of a 'Data.SBV.Control.checkSat' or 'Data.SBV.Control.checkSatAssuming' call.
data CheckSatResult = Sat                   -- ^ Satisfiable: A model is available, which can be queried with 'Data.SBV.Control.getValue'.
                    | DSat (Maybe String)   -- ^ Delta-satisfiable: A delta-sat model is available. String is the precision info, if available.
                    | Unsat                 -- ^ Unsatisfiable: No model is available. Unsat cores might be obtained via 'Data.SBV.Control.getUnsatCore'.
                    | Unk                   -- ^ Unknown: Use 'Data.SBV.Control.getUnknownReason' to obtain an explanation why this might be the case.
                    deriving (CheckSatResult -> CheckSatResult -> Bool
(CheckSatResult -> CheckSatResult -> Bool)
-> (CheckSatResult -> CheckSatResult -> Bool) -> Eq CheckSatResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CheckSatResult -> CheckSatResult -> Bool
== :: CheckSatResult -> CheckSatResult -> Bool
$c/= :: CheckSatResult -> CheckSatResult -> Bool
/= :: 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
$cshowsPrec :: Int -> CheckSatResult -> ShowS
showsPrec :: Int -> CheckSatResult -> ShowS
$cshow :: CheckSatResult -> String
show :: CheckSatResult -> String
$cshowList :: [CheckSatResult] -> ShowS
showList :: [CheckSatResult] -> ShowS
Show, CheckSatResult -> ()
(CheckSatResult -> ()) -> NFData CheckSatResult
forall a. (a -> ()) -> NFData a
$crnf :: CheckSatResult -> ()
rnf :: CheckSatResult -> ()
NFData, (forall x. CheckSatResult -> Rep CheckSatResult x)
-> (forall x. Rep CheckSatResult x -> CheckSatResult)
-> Generic CheckSatResult
forall x. Rep CheckSatResult x -> CheckSatResult
forall x. CheckSatResult -> Rep CheckSatResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CheckSatResult -> Rep CheckSatResult x
from :: forall x. CheckSatResult -> Rep CheckSatResult x
$cto :: forall x. Rep CheckSatResult x -> CheckSatResult
to :: forall x. Rep CheckSatResult x -> CheckSatResult
Generic)

-- | Collectable information from the solver.
data SMTInfoFlag = AllStatistics
                 | AssertionStackLevels
                 | Authors
                 | ErrorBehavior
                 | Name
                 | ReasonUnknown
                 | Version
                 | InfoKeyword String

-- | Behavior of the solver for errors.
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
$cshowsPrec :: Int -> SMTErrorBehavior -> ShowS
showsPrec :: Int -> SMTErrorBehavior -> ShowS
$cshow :: SMTErrorBehavior -> String
show :: SMTErrorBehavior -> String
$cshowList :: [SMTErrorBehavior] -> ShowS
showList :: [SMTErrorBehavior] -> ShowS
Show

-- | Reason for reporting unknown.
data SMTReasonUnknown = UnknownMemOut
                      | UnknownIncomplete
                      | UnknownTimeOut
                      | UnknownOther      String

-- | Trivial rnf instance
instance NFData SMTReasonUnknown where rnf :: SMTReasonUnknown -> ()
rnf SMTReasonUnknown
a = SMTReasonUnknown -> () -> ()
forall a b. a -> b -> b
seq SMTReasonUnknown
a ()

-- | Show instance for unknown
instance Show SMTReasonUnknown where
  show :: SMTReasonUnknown -> String
show SMTReasonUnknown
UnknownMemOut     = String
"memout"
  show SMTReasonUnknown
UnknownIncomplete = String
"incomplete"
  show SMTReasonUnknown
UnknownTimeOut    = String
"timeout"
  show (UnknownOther String
s)  = String
s

-- | Collectable information from the solver.
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
$cshowsPrec :: Int -> SMTInfoResponse -> ShowS
showsPrec :: Int -> SMTInfoResponse -> ShowS
$cshow :: SMTInfoResponse -> String
show :: SMTInfoResponse -> String
$cshowList :: [SMTInfoResponse] -> ShowS
showList :: [SMTInfoResponse] -> ShowS
Show

-- Show instance for SMTInfoFlag maintains smt-lib format per the SMTLib2 standard document.
instance Show SMTInfoFlag where
  show :: SMTInfoFlag -> String
show SMTInfoFlag
AllStatistics        = String
":all-statistics"
  show SMTInfoFlag
AssertionStackLevels = String
":assertion-stack-levels"
  show SMTInfoFlag
Authors              = String
":authors"
  show SMTInfoFlag
ErrorBehavior        = String
":error-behavior"
  show SMTInfoFlag
Name                 = String
":name"
  show SMTInfoFlag
ReasonUnknown        = String
":reason-unknown"
  show SMTInfoFlag
Version              = String
":version"
  show (InfoKeyword String
s)      = String
s

-- | Option values that can be set in the solver, following the SMTLib specification <https://smt-lib.org/language.shtml>.
--
-- Note that not all solvers may support all of these!
--
-- Furthermore, SBV doesn't support the following options allowed by SMTLib.
--
--    * @:interactive-mode@                (Deprecated in SMTLib, use 'ProduceAssertions' instead.)
--    * @:print-success@                   (SBV critically needs this to be True in query mode.)
--    * @:produce-models@                  (SBV always sets this option so it can extract models.)
--    * @:regular-output-channel@          (SBV always requires regular output to come on stdout for query purposes.)
--    * @:global-declarations@             (SBV always uses global declarations since definitions are accumulative.)
--
-- Note that 'SetLogic' and 'SetInfo' are, strictly speaking, not SMTLib options. However, we treat it as such here
-- uniformly, as it fits better with how options work.
data SMTOption = DiagnosticOutputChannel   FilePath
               | ProduceAssertions         Bool
               | ProduceAssignments        Bool
               | ProduceProofs             Bool
               | ProduceInterpolants       Bool
               | ProduceUnsatAssumptions   Bool
               | ProduceUnsatCores         Bool
               | ProduceAbducts            Bool
               | RandomSeed                Integer
               | ReproducibleResourceLimit Integer
               | SMTVerbosity              Integer
               | OptionKeyword             String  [String]
               | SetLogic                  Logic
               | SetInfo                   String  [String]
               | SetTimeOut                Integer
               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

-- | Can this command only be run at the very beginning? If 'True' then
-- we will reject setting these options in the query mode. Note that this
-- classification follows the SMTLib document.
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 ProduceAbducts{}            = Bool
True
isStartModeOption RandomSeed{}                = Bool
True
isStartModeOption ReproducibleResourceLimit{} = Bool
False
isStartModeOption SMTVerbosity{}              = Bool
False
isStartModeOption OptionKeyword{}             = Bool
True  -- Conservative.
isStartModeOption SetLogic{}                  = Bool
True
isStartModeOption SetInfo{}                   = Bool
False
isStartModeOption SetTimeOut{}                = Bool
True

-- | Can this option be set multiple times? I'm only making a guess here.
-- If this returns True, then we'll only send the last instance we see.
-- We might need to update as necessary.
isOnlyOnceOption :: SMTOption -> Bool
isOnlyOnceOption :: SMTOption -> Bool
isOnlyOnceOption DiagnosticOutputChannel{}   = Bool
True
isOnlyOnceOption ProduceAssertions{}         = Bool
True
isOnlyOnceOption ProduceAssignments{}        = Bool
True
isOnlyOnceOption ProduceProofs{}             = Bool
True
isOnlyOnceOption ProduceInterpolants{}       = Bool
True
isOnlyOnceOption ProduceUnsatAssumptions{}   = Bool
True
isOnlyOnceOption ProduceAbducts{}            = Bool
False
isOnlyOnceOption ProduceUnsatCores{}         = Bool
True
isOnlyOnceOption RandomSeed{}                = Bool
False
isOnlyOnceOption ReproducibleResourceLimit{} = Bool
False
isOnlyOnceOption SMTVerbosity{}              = Bool
False
isOnlyOnceOption OptionKeyword{}             = Bool
False -- This is really hard to determine. Just being permissive
isOnlyOnceOption SetLogic{}                  = Bool
True
isOnlyOnceOption SetInfo{}                   = Bool
False
isOnlyOnceOption SetTimeOut{}                = Bool
False

-- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
-- user can override this choice using a call to 'Data.SBV.setLogic' This is especially handy if one is experimenting with custom
-- logics that might be supported on new solvers. See <https://smt-lib.org/logics.shtml> for the official list.
data Logic
  = AUFLIA             -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.
  | AUFLIRA            -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.
  | AUFNIRA            -- ^ Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.
  | LRA                -- ^ Linear formulas in linear real arithmetic.
  | QF_ABV             -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays.
  | QF_AUFBV           -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.
  | QF_AUFLIA          -- ^ Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.
  | QF_AX              -- ^ Quantifier-free formulas over the theory of arrays with extensionality.
  | QF_BV              -- ^ Quantifier-free formulas over the theory of fixed-size bitvectors.
  | QF_IDL             -- ^ Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.
  | QF_LIA             -- ^ Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.
  | QF_LRA             -- ^ Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.
  | QF_NIA             -- ^ Quantifier-free integer arithmetic.
  | QF_NRA             -- ^ Quantifier-free real arithmetic.
  | QF_RDL             -- ^ Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.
  | QF_UF              -- ^ Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.
  | QF_UFBV            -- ^ Unquantified formulas over bitvectors with uninterpreted sort function and symbols.
  | QF_UFIDL           -- ^ Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.
  | QF_UFLIA           -- ^ Unquantified linear integer arithmetic with uninterpreted sort and function symbols.
  | QF_UFLRA           -- ^ Unquantified linear real arithmetic with uninterpreted sort and function symbols.
  | QF_UFNRA           -- ^ Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.
  | QF_UFNIRA          -- ^ Unquantified non-linear real integer arithmetic with uninterpreted sort and function symbols.
  | UFLRA              -- ^ Linear real arithmetic with uninterpreted sort and function symbols.
  | UFNIA              -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols.
  | QF_FPBV            -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors.
  | QF_FP              -- ^ Quantifier-free formulas over the theory of floating point numbers.
  | QF_FD              -- ^ Quantifier-free finite domains.
  | QF_S               -- ^ Quantifier-free formulas over the theory of strings.
  | Logic_ALL          -- ^ The catch-all value.
  | Logic_NONE         -- ^ Use this value when you want SBV to simply not set the logic.
  | CustomLogic String -- ^ In case you need a really custom string!

-- The show instance is "almost" the derived one, but not quite!
instance Show Logic where
  show :: Logic -> String
show Logic
AUFLIA          = String
"AUFLIA"
  show Logic
AUFLIRA         = String
"AUFLIRA"
  show Logic
AUFNIRA         = String
"AUFNIRA"
  show Logic
LRA             = String
"LRA"
  show Logic
QF_ABV          = String
"QF_ABV"
  show Logic
QF_AUFBV        = String
"QF_AUFBV"
  show Logic
QF_AUFLIA       = String
"QF_AUFLIA"
  show Logic
QF_AX           = String
"QF_AX"
  show Logic
QF_BV           = String
"QF_BV"
  show Logic
QF_IDL          = String
"QF_IDL"
  show Logic
QF_LIA          = String
"QF_LIA"
  show Logic
QF_LRA          = String
"QF_LRA"
  show Logic
QF_NIA          = String
"QF_NIA"
  show Logic
QF_NRA          = String
"QF_NRA"
  show Logic
QF_RDL          = String
"QF_RDL"
  show Logic
QF_UF           = String
"QF_UF"
  show Logic
QF_UFBV         = String
"QF_UFBV"
  show Logic
QF_UFIDL        = String
"QF_UFIDL"
  show Logic
QF_UFLIA        = String
"QF_UFLIA"
  show Logic
QF_UFLRA        = String
"QF_UFLRA"
  show Logic
QF_UFNRA        = String
"QF_UFNRA"
  show Logic
QF_UFNIRA       = String
"QF_UFNIRA"
  show Logic
UFLRA           = String
"UFLRA"
  show Logic
UFNIA           = String
"UFNIA"
  show Logic
QF_FPBV         = String
"QF_FPBV"
  show Logic
QF_FP           = String
"QF_FP"
  show Logic
QF_FD           = String
"QF_FD"
  show Logic
QF_S            = String
"QF_S"
  show Logic
Logic_ALL       = String
"ALL"
  show Logic
Logic_NONE      = String
"Logic_NONE"
  show (CustomLogic String
l) = String
l

{- HLint ignore type SMTInfoResponse "Use camelCase" -}
{- HLint ignore type Logic           "Use camelCase" -}