1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Control.Types 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Types related to interactive queries 10----------------------------------------------------------------------------- 11 12{-# OPTIONS_GHC -Wall -Werror #-} 13 14module Data.SBV.Control.Types ( 15 CheckSatResult(..) 16 , Logic(..) 17 , SMTOption(..), isStartModeOption, isOnlyOnceOption, setSMTOption 18 , SMTInfoFlag(..) 19 , SMTErrorBehavior(..) 20 , SMTReasonUnknown(..) 21 , SMTInfoResponse(..) 22 ) where 23 24import Control.DeepSeq (NFData(..)) 25 26-- | Result of a 'Data.SBV.Control.checkSat' or 'Data.SBV.Control.checkSatAssuming' call. 27data CheckSatResult = Sat -- ^ Satisfiable: A model is available, which can be queried with 'Data.SBV.Control.getValue'. 28 | DSat (Maybe String) -- ^ Delta-satisfiable: A delta-sat model is available. String is the precision info, if available. 29 | Unsat -- ^ Unsatisfiable: No model is available. Unsat cores might be obtained via 'Data.SBV.Control.getUnsatCore'. 30 | Unk -- ^ Unknown: Use 'Data.SBV.Control.getUnknownReason' to obtain an explanation why this might be the case. 31 deriving (Eq, Show) 32 33-- | Collectable information from the solver. 34data SMTInfoFlag = AllStatistics 35 | AssertionStackLevels 36 | Authors 37 | ErrorBehavior 38 | Name 39 | ReasonUnknown 40 | Version 41 | InfoKeyword String 42 43-- | Behavior of the solver for errors. 44data SMTErrorBehavior = ErrorImmediateExit 45 | ErrorContinuedExecution 46 deriving Show 47 48-- | Reason for reporting unknown. 49data SMTReasonUnknown = UnknownMemOut 50 | UnknownIncomplete 51 | UnknownTimeOut 52 | UnknownOther String 53 54-- | Trivial rnf instance 55instance NFData SMTReasonUnknown where rnf a = seq a () 56 57-- | Show instance for unknown 58instance Show SMTReasonUnknown where 59 show UnknownMemOut = "memout" 60 show UnknownIncomplete = "incomplete" 61 show UnknownTimeOut = "timeout" 62 show (UnknownOther s) = s 63 64-- | Collectable information from the solver. 65data SMTInfoResponse = Resp_Unsupported 66 | Resp_AllStatistics [(String, String)] 67 | Resp_AssertionStackLevels Integer 68 | Resp_Authors [String] 69 | Resp_Error SMTErrorBehavior 70 | Resp_Name String 71 | Resp_ReasonUnknown SMTReasonUnknown 72 | Resp_Version String 73 | Resp_InfoKeyword String [String] 74 deriving Show 75 76-- Show instance for SMTInfoFlag maintains smt-lib format per the SMTLib2 standard document. 77instance Show SMTInfoFlag where 78 show AllStatistics = ":all-statistics" 79 show AssertionStackLevels = ":assertion-stack-levels" 80 show Authors = ":authors" 81 show ErrorBehavior = ":error-behavior" 82 show Name = ":name" 83 show ReasonUnknown = ":reason-unknown" 84 show Version = ":version" 85 show (InfoKeyword s) = s 86 87-- | Option values that can be set in the solver, following the SMTLib specification <http://smtlib.cs.uiowa.edu/language.shtml>. 88-- 89-- Note that not all solvers may support all of these! 90-- 91-- Furthermore, SBV doesn't support the following options allowed by SMTLib. 92-- 93-- * @:interactive-mode@ (Deprecated in SMTLib, use 'ProduceAssertions' instead.) 94-- * @:print-success@ (SBV critically needs this to be True in query mode.) 95-- * @:produce-models@ (SBV always sets this option so it can extract models.) 96-- * @:regular-output-channel@ (SBV always requires regular output to come on stdout for query purposes.) 97-- * @:global-declarations@ (SBV always uses global declarations since definitions are accumulative.) 98-- 99-- Note that 'SetLogic' and 'SetInfo' are, strictly speaking, not SMTLib options. However, we treat it as such here 100-- uniformly, as it fits better with how options work. 101data SMTOption = DiagnosticOutputChannel FilePath 102 | ProduceAssertions Bool 103 | ProduceAssignments Bool 104 | ProduceProofs Bool 105 | ProduceInterpolants Bool 106 | ProduceUnsatAssumptions Bool 107 | ProduceUnsatCores Bool 108 | RandomSeed Integer 109 | ReproducibleResourceLimit Integer 110 | SMTVerbosity Integer 111 | OptionKeyword String [String] 112 | SetLogic Logic 113 | SetInfo String [String] 114 deriving Show 115 116-- | Can this command only be run at the very beginning? If 'True' then 117-- we will reject setting these options in the query mode. Note that this 118-- classification follows the SMTLib document. 119isStartModeOption :: SMTOption -> Bool 120isStartModeOption DiagnosticOutputChannel{} = False 121isStartModeOption ProduceAssertions{} = True 122isStartModeOption ProduceAssignments{} = True 123isStartModeOption ProduceProofs{} = True 124isStartModeOption ProduceInterpolants{} = True 125isStartModeOption ProduceUnsatAssumptions{} = True 126isStartModeOption ProduceUnsatCores{} = True 127isStartModeOption RandomSeed{} = True 128isStartModeOption ReproducibleResourceLimit{} = False 129isStartModeOption SMTVerbosity{} = False 130isStartModeOption OptionKeyword{} = True -- Conservative. 131isStartModeOption SetLogic{} = True 132isStartModeOption SetInfo{} = False 133 134-- | Can this option be set multiple times? I'm only making a guess here. 135-- If this returns True, then we'll only send the last instance we see. 136-- We might need to update as necessary. 137isOnlyOnceOption :: SMTOption -> Bool 138isOnlyOnceOption DiagnosticOutputChannel{} = True 139isOnlyOnceOption ProduceAssertions{} = True 140isOnlyOnceOption ProduceAssignments{} = True 141isOnlyOnceOption ProduceProofs{} = True 142isOnlyOnceOption ProduceInterpolants{} = True 143isOnlyOnceOption ProduceUnsatAssumptions{} = True 144isOnlyOnceOption ProduceUnsatCores{} = True 145isOnlyOnceOption RandomSeed{} = False 146isOnlyOnceOption ReproducibleResourceLimit{} = False 147isOnlyOnceOption SMTVerbosity{} = False 148isOnlyOnceOption OptionKeyword{} = False -- This is really hard to determine. Just being permissive 149isOnlyOnceOption SetLogic{} = True 150isOnlyOnceOption SetInfo{} = False 151 152-- SMTLib's True/False is spelled differently than Haskell's. 153smtBool :: Bool -> String 154smtBool True = "true" 155smtBool False = "false" 156 157-- | Translate an option setting to SMTLib. Note the SetLogic/SetInfo discrepancy. 158setSMTOption :: SMTOption -> String 159setSMTOption = cvt 160 where cvt (DiagnosticOutputChannel f) = opt [":diagnostic-output-channel", show f] 161 cvt (ProduceAssertions b) = opt [":produce-assertions", smtBool b] 162 cvt (ProduceAssignments b) = opt [":produce-assignments", smtBool b] 163 cvt (ProduceProofs b) = opt [":produce-proofs", smtBool b] 164 cvt (ProduceInterpolants b) = opt [":produce-interpolants", smtBool b] 165 cvt (ProduceUnsatAssumptions b) = opt [":produce-unsat-assumptions", smtBool b] 166 cvt (ProduceUnsatCores b) = opt [":produce-unsat-cores", smtBool b] 167 cvt (RandomSeed i) = opt [":random-seed", show i] 168 cvt (ReproducibleResourceLimit i) = opt [":reproducible-resource-limit", show i] 169 cvt (SMTVerbosity i) = opt [":verbosity", show i] 170 cvt (OptionKeyword k as) = opt (k : as) 171 cvt (SetLogic l) = logic l 172 cvt (SetInfo k as) = info (k : as) 173 174 opt xs = "(set-option " ++ unwords xs ++ ")" 175 info xs = "(set-info " ++ unwords xs ++ ")" 176 177 logic Logic_NONE = "; NB. not setting the logic per user request of Logic_NONE" 178 logic l = "(set-logic " ++ show l ++ ")" 179 180-- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the 181-- user can override this choice using a call to 'Data.SBV.setLogic' This is especially handy if one is experimenting with custom 182-- logics that might be supported on new solvers. See <http://smtlib.cs.uiowa.edu/logics.shtml> for the official list. 183data Logic 184 = 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. 185 | AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. 186 | AUFNIRA -- ^ Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. 187 | LRA -- ^ Linear formulas in linear real arithmetic. 188 | QF_ABV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays. 189 | QF_AUFBV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols. 190 | QF_AUFLIA -- ^ Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols. 191 | QF_AX -- ^ Quantifier-free formulas over the theory of arrays with extensionality. 192 | QF_BV -- ^ Quantifier-free formulas over the theory of fixed-size bitvectors. 193 | 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. 194 | QF_LIA -- ^ Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables. 195 | QF_LRA -- ^ Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. 196 | QF_NIA -- ^ Quantifier-free integer arithmetic. 197 | QF_NRA -- ^ Quantifier-free real arithmetic. 198 | 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. 199 | QF_UF -- ^ Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. 200 | QF_UFBV -- ^ Unquantified formulas over bitvectors with uninterpreted sort function and symbols. 201 | QF_UFIDL -- ^ Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. 202 | QF_UFLIA -- ^ Unquantified linear integer arithmetic with uninterpreted sort and function symbols. 203 | QF_UFLRA -- ^ Unquantified linear real arithmetic with uninterpreted sort and function symbols. 204 | QF_UFNRA -- ^ Unquantified non-linear real arithmetic with uninterpreted sort and function symbols. 205 | QF_UFNIRA -- ^ Unquantified non-linear real integer arithmetic with uninterpreted sort and function symbols. 206 | UFLRA -- ^ Linear real arithmetic with uninterpreted sort and function symbols. 207 | UFNIA -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols. 208 | QF_FPBV -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors. 209 | QF_FP -- ^ Quantifier-free formulas over the theory of floating point numbers. 210 | QF_FD -- ^ Quantifier-free finite domains. 211 | QF_S -- ^ Quantifier-free formulas over the theory of strings. 212 | Logic_ALL -- ^ The catch-all value. 213 | Logic_NONE -- ^ Use this value when you want SBV to simply not set the logic. 214 | CustomLogic String -- ^ In case you need a really custom string! 215 216-- The show instance is "almost" the derived one, but not quite! 217instance Show Logic where 218 show AUFLIA = "AUFLIA" 219 show AUFLIRA = "AUFLIRA" 220 show AUFNIRA = "AUFNIRA" 221 show LRA = "LRA" 222 show QF_ABV = "QF_ABV" 223 show QF_AUFBV = "QF_AUFBV" 224 show QF_AUFLIA = "QF_AUFLIA" 225 show QF_AX = "QF_AX" 226 show QF_BV = "QF_BV" 227 show QF_IDL = "QF_IDL" 228 show QF_LIA = "QF_LIA" 229 show QF_LRA = "QF_LRA" 230 show QF_NIA = "QF_NIA" 231 show QF_NRA = "QF_NRA" 232 show QF_RDL = "QF_RDL" 233 show QF_UF = "QF_UF" 234 show QF_UFBV = "QF_UFBV" 235 show QF_UFIDL = "QF_UFIDL" 236 show QF_UFLIA = "QF_UFLIA" 237 show QF_UFLRA = "QF_UFLRA" 238 show QF_UFNRA = "QF_UFNRA" 239 show QF_UFNIRA = "QF_UFNIRA" 240 show UFLRA = "UFLRA" 241 show UFNIA = "UFNIA" 242 show QF_FPBV = "QF_FPBV" 243 show QF_FP = "QF_FP" 244 show QF_FD = "QF_FD" 245 show QF_S = "QF_S" 246 show Logic_ALL = "ALL" 247 show Logic_NONE = "Logic_NONE" 248 show (CustomLogic l) = l 249 250{-# ANN type SMTInfoResponse ("HLint: ignore Use camelCase" :: String) #-} 251{-# ANN type Logic ("HLint: ignore Use camelCase" :: String) #-} 252