-----------------------------------------------------------------------------
-- |
-- 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, setSMTOption
     , SMTInfoFlag(..)
     , SMTErrorBehavior(..)
     , SMTReasonUnknown(..)
     , SMTInfoResponse(..)
     ) where

import Generics.Deriving.Base (Generic)
import Generics.Deriving.Show (GShow, gshow)

import Control.DeepSeq (NFData(..))

-- | 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'.
                    | 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
/= :: 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)

-- | 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
showList :: [SMTErrorBehavior] -> ShowS
$cshowList :: [SMTErrorBehavior] -> ShowS
show :: SMTErrorBehavior -> String
$cshow :: SMTErrorBehavior -> String
showsPrec :: Int -> SMTErrorBehavior -> ShowS
$cshowsPrec :: Int -> SMTErrorBehavior -> ShowS
Show

-- | Reason for reporting unknown.
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)

-- | Show instance for unknown
instance Show SMTReasonUnknown where
  show :: SMTReasonUnknown -> String
show UnknownMemOut     = "memout"
  show UnknownIncomplete = "incomplete"
  show UnknownTimeOut    = "timeout"
  show (UnknownOther s :: 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
showList :: [SMTInfoResponse] -> ShowS
$cshowList :: [SMTInfoResponse] -> ShowS
show :: SMTInfoResponse -> String
$cshow :: SMTInfoResponse -> String
showsPrec :: Int -> SMTInfoResponse -> ShowS
$cshowsPrec :: Int -> SMTInfoResponse -> ShowS
Show

-- Show instance for SMTInfoFlag maintains smt-lib format per the SMTLib2 standard document.
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

-- | Option values that can be set in the solver, following the SMTLib specification <http://smtlib.cs.uiowa.edu/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
               | 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)

-- | 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 RandomSeed{}                = Bool
True
isStartModeOption ReproducibleResourceLimit{} = Bool
False
isStartModeOption SMTVerbosity{}              = Bool
False
isStartModeOption OptionKeyword{}             = Bool
True  -- Conservative.
isStartModeOption SetLogic{}                  = Bool
True
isStartModeOption SetInfo{}                   = Bool
False

-- SMTLib's True/False is spelled differently than Haskell's.
smtBool :: Bool -> String
smtBool :: Bool -> String
smtBool True  = "true"
smtBool False = "false"

-- | Translate an option setting to SMTLib. Note the SetLogic/SetInfo discrepancy.
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]
++ ")"

-- | 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 <http://smtlib.cs.uiowa.edu/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!
  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)

-- The show instance is "almost" the derived one, but not quite!
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) #-}