1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Core.Symbolic 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Symbolic values 10----------------------------------------------------------------------------- 11 12{-# LANGUAGE BangPatterns #-} 13{-# LANGUAGE CPP #-} 14{-# LANGUAGE DefaultSignatures #-} 15{-# LANGUAGE DeriveDataTypeable #-} 16{-# LANGUAGE DeriveFunctor #-} 17{-# LANGUAGE DeriveGeneric #-} 18{-# LANGUAGE FlexibleInstances #-} 19{-# LANGUAGE FunctionalDependencies #-} 20{-# LANGUAGE GADTs #-} 21{-# LANGUAGE GeneralizedNewtypeDeriving #-} 22{-# LANGUAGE NamedFieldPuns #-} 23{-# LANGUAGE OverloadedStrings #-} 24{-# LANGUAGE PatternGuards #-} 25{-# LANGUAGE Rank2Types #-} 26{-# LANGUAGE ScopedTypeVariables #-} 27{-# LANGUAGE TupleSections #-} 28{-# LANGUAGE TypeOperators #-} 29{-# LANGUAGE UndecidableInstances #-} -- for undetermined s in MonadState 30{-# LANGUAGE ViewPatterns #-} 31 32{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} 33 34module Data.SBV.Core.Symbolic 35 ( NodeId(..) 36 , SV(..), swKind, trueSV, falseSV 37 , Op(..), PBOp(..), OvOp(..), FPOp(..), NROp(..), StrOp(..), SeqOp(..), SetOp(..) 38 , RegExp(..), regExpToSMTString 39 , Quantifier(..), needsExistentials, VarContext(..) 40 , RoundingMode(..) 41 , SBVType(..), svUninterpreted, newUninterpreted 42 , SVal(..) 43 , svMkSymVar, sWordN, sWordN_, sIntN, sIntN_ 44 , ArrayContext(..), ArrayInfo 45 , svToSV, svToSymSV, forceSVArg 46 , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage 47 , Cached, cache, uncache, modifyState, modifyIncState 48 , ArrayIndex(..), FArrayIndex(..), uncacheAI, uncacheFAI 49 , NamedSymVar(..), Name, UserInputs, Inputs(..), getSV, swNodeId, namedNodeId, getUniversals 50 , prefixExistentials, prefixUniversals, onUserInputs, onInternInputs, onAllInputs 51 , addInternInput, addUserInput, getInputs, inputsFromListWith, userInputsToList 52 , getUserName', internInputsToList, inputsToList, quantifier, namedSymVar, getUserName 53 , lookupInput , getSValPathCondition, extendSValPathCondition 54 , getTableIndex 55 , SBVPgm(..), MonadSymbolic(..), SymbolicT, Symbolic, runSymbolic, State(..), withNewIncState, IncState(..), incrementInternalCounter 56 , inSMTMode, SBVRunMode(..), IStage(..), Result(..) 57 , registerKind, registerLabel, recordObservable 58 , addAssertion, addNewSMTOption, imposeConstraint, internalConstraint, internalVariable 59 , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension 60 , SolverCapabilities(..) 61 , extractSymbolicSimulationState, CnstMap 62 , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal 63 , MonadQuery(..), QueryT(..), Query, Queriable(..), Fresh(..), QueryState(..), QueryContext(..) 64 , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine 65 , validationRequested, outputSVal 66 ) where 67 68import Control.Arrow ((***)) 69import Control.DeepSeq (NFData(..)) 70import Control.Monad (when) 71import Control.Monad.Except (MonadError, ExceptT) 72import Control.Monad.Reader (MonadReader(..), ReaderT, runReaderT, 73 mapReaderT) 74import Control.Monad.State.Lazy (MonadState) 75import Control.Monad.Trans (MonadIO(liftIO), MonadTrans(lift)) 76import Control.Monad.Trans.Maybe (MaybeT) 77import Control.Monad.Writer.Strict (MonadWriter) 78import Data.Char (isAlpha, isAlphaNum, toLower) 79import Data.IORef (IORef, newIORef, readIORef) 80import Data.List (intercalate, sortBy) 81import Data.Maybe (isJust, fromJust, fromMaybe) 82import Data.String (IsString(fromString)) 83 84import Data.Time (getCurrentTime, UTCTime) 85 86import GHC.Stack 87import GHC.Generics (Generic) 88 89import qualified Control.Monad.State.Lazy as LS 90import qualified Control.Monad.State.Strict as SS 91import qualified Control.Monad.Writer.Lazy as LW 92import qualified Control.Monad.Writer.Strict as SW 93import qualified Data.IORef as R (modifyIORef') 94import qualified Data.Generics as G (Data(..)) 95import qualified Data.IntMap.Strict as IMap (IntMap, empty, toAscList, lookup, insertWith) 96import qualified Data.Map.Strict as Map (Map, empty, toList, lookup, insert, size) 97import qualified Data.Set as Set (Set, empty, toList, insert, member) 98import qualified Data.Foldable as F (toList) 99import qualified Data.Sequence as S (Seq, empty, (|>), (<|), filter, takeWhileL, fromList, lookup, elemIndexL) 100import qualified Data.Text as T 101 102import System.Mem.StableName 103 104import Data.SBV.Core.Kind 105import Data.SBV.Core.Concrete 106import Data.SBV.SMT.SMTLibNames 107import Data.SBV.Utils.TDiff (Timing) 108import Data.SBV.Utils.Lib (stringToQFS) 109 110import Data.SBV.Control.Types 111 112#if MIN_VERSION_base(4,11,0) 113import Control.Monad.Fail as Fail 114#endif 115 116-- | A symbolic node id 117newtype NodeId = NodeId { getId :: Int } 118 deriving (Eq, Ord, G.Data) 119 120-- | A symbolic word, tracking it's signedness and size. 121data SV = SV !Kind !NodeId 122 deriving G.Data 123 124-- | For equality, we merely use the node-id 125instance Eq SV where 126 SV _ n1 == SV _ n2 = n1 == n2 127 128-- | Again, simply use the node-id for ordering 129instance Ord SV where 130 SV _ n1 `compare` SV _ n2 = n1 `compare` n2 131 132instance HasKind SV where 133 kindOf (SV k _) = k 134 135instance Show SV where 136 show (SV _ (NodeId n)) = case n of 137 -2 -> "false" 138 -1 -> "true" 139 _ -> 's' : show n 140 141-- | Kind of a symbolic word. 142swKind :: SV -> Kind 143swKind (SV k _) = k 144 145-- | retrieve the node id of a symbolic word 146swNodeId :: SV -> NodeId 147swNodeId (SV _ nid) = nid 148 149-- | Forcing an argument; this is a necessary evil to make sure all the arguments 150-- to an uninterpreted function are evaluated before called; the semantics of uinterpreted 151-- functions is necessarily strict; deviating from Haskell's 152forceSVArg :: SV -> IO () 153forceSVArg (SV k n) = k `seq` n `seq` return () 154 155-- | Constant False as an 'SV'. Note that this value always occupies slot -2. 156falseSV :: SV 157falseSV = SV KBool $ NodeId (-2) 158 159-- | Constant True as an 'SV'. Note that this value always occupies slot -1. 160trueSV :: SV 161trueSV = SV KBool $ NodeId (-1) 162 163-- | Symbolic operations 164data Op = Plus 165 | Times 166 | Minus 167 | UNeg 168 | Abs 169 | Quot 170 | Rem 171 | Equal 172 | NotEqual 173 | LessThan 174 | GreaterThan 175 | LessEq 176 | GreaterEq 177 | Ite 178 | And 179 | Or 180 | XOr 181 | Not 182 | Shl 183 | Shr 184 | Rol Int 185 | Ror Int 186 | Extract Int Int -- Extract i j: extract bits i to j. Least significant bit is 0 (big-endian) 187 | Join -- Concat two words to form a bigger one, in the order given 188 | LkUp (Int, Kind, Kind, Int) !SV !SV -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value 189 | ArrEq ArrayIndex ArrayIndex -- Array equality 190 | ArrRead ArrayIndex 191 | KindCast Kind Kind 192 | Uninterpreted String 193 | Label String -- Essentially no-op; useful for code generation to emit comments. 194 | IEEEFP FPOp -- Floating-point ops, categorized separately 195 | NonLinear NROp -- Non-linear ops (mostly trigonometric), categorized separately 196 | OverflowOp OvOp -- Overflow-ops, categorized separately 197 | PseudoBoolean PBOp -- Pseudo-boolean ops, categorized separately 198 | StrOp StrOp -- String ops, categorized separately 199 | SeqOp SeqOp -- Sequence ops, categorized separately 200 | SetOp SetOp -- Set operations, categorized separately 201 | TupleConstructor Int -- Construct an n-tuple 202 | TupleAccess Int Int -- Access element i of an n-tuple; second argument is n 203 | EitherConstructor Kind Kind Bool -- Construct a sum; False: left, True: right 204 | EitherIs Kind Kind Bool -- Either branch tester; False: left, True: right 205 | EitherAccess Bool -- Either branch access; False: left, True: right 206 | MaybeConstructor Kind Bool -- Construct a maybe value; False: Nothing, True: Just 207 | MaybeIs Kind Bool -- Maybe tester; False: nothing, True: just 208 | MaybeAccess -- Maybe branch access; grab the contents of the just 209 deriving (Eq, Ord, G.Data) 210 211-- | Floating point operations 212data FPOp = FP_Cast Kind Kind SV -- From-Kind, To-Kind, RoundingMode. This is "value" conversion 213 | FP_Reinterpret Kind Kind -- From-Kind, To-Kind. This is bit-reinterpretation using IEEE-754 interchange format 214 | FP_Abs 215 | FP_Neg 216 | FP_Add 217 | FP_Sub 218 | FP_Mul 219 | FP_Div 220 | FP_FMA 221 | FP_Sqrt 222 | FP_Rem 223 | FP_RoundToIntegral 224 | FP_Min 225 | FP_Max 226 | FP_ObjEqual 227 | FP_IsNormal 228 | FP_IsSubnormal 229 | FP_IsZero 230 | FP_IsInfinite 231 | FP_IsNaN 232 | FP_IsNegative 233 | FP_IsPositive 234 deriving (Eq, Ord, G.Data) 235 236-- Note that the show instance maps to the SMTLib names. We need to make sure 237-- this mapping stays correct through SMTLib changes. The only exception 238-- is FP_Cast; where we handle different source/origins explicitly later on. 239instance Show FPOp where 240 show (FP_Cast f t r) = "(FP_Cast: " ++ show f ++ " -> " ++ show t ++ ", using RM [" ++ show r ++ "])" 241 show (FP_Reinterpret f t) = case t of 242 KFloat -> "(_ to_fp 8 24)" 243 KDouble -> "(_ to_fp 11 53)" 244 KFP eb sb -> "(_ to_fp " ++ show eb ++ " " ++ show sb ++ ")" 245 _ -> error $ "SBV.FP_Reinterpret: Unexpected conversion: " ++ show f ++ " to " ++ show t 246 show FP_Abs = "fp.abs" 247 show FP_Neg = "fp.neg" 248 show FP_Add = "fp.add" 249 show FP_Sub = "fp.sub" 250 show FP_Mul = "fp.mul" 251 show FP_Div = "fp.div" 252 show FP_FMA = "fp.fma" 253 show FP_Sqrt = "fp.sqrt" 254 show FP_Rem = "fp.rem" 255 show FP_RoundToIntegral = "fp.roundToIntegral" 256 show FP_Min = "fp.min" 257 show FP_Max = "fp.max" 258 show FP_ObjEqual = "=" 259 show FP_IsNormal = "fp.isNormal" 260 show FP_IsSubnormal = "fp.isSubnormal" 261 show FP_IsZero = "fp.isZero" 262 show FP_IsInfinite = "fp.isInfinite" 263 show FP_IsNaN = "fp.isNaN" 264 show FP_IsNegative = "fp.isNegative" 265 show FP_IsPositive = "fp.isPositive" 266 267-- | Non-linear operations 268data NROp = NR_Sin 269 | NR_Cos 270 | NR_Tan 271 | NR_ASin 272 | NR_ACos 273 | NR_ATan 274 | NR_Sqrt 275 | NR_Sinh 276 | NR_Cosh 277 | NR_Tanh 278 | NR_Exp 279 | NR_Log 280 | NR_Pow 281 deriving (Eq, Ord, G.Data) 282 283-- | The show instance carefully arranges for these to be printed as it can be understood by dreal 284instance Show NROp where 285 show NR_Sin = "sin" 286 show NR_Cos = "cos" 287 show NR_Tan = "tan" 288 show NR_ASin = "asin" 289 show NR_ACos = "acos" 290 show NR_ATan = "atan" 291 show NR_Sinh = "sinh" 292 show NR_Cosh = "cosh" 293 show NR_Tanh = "tanh" 294 show NR_Sqrt = "sqrt" 295 show NR_Exp = "exp" 296 show NR_Log = "log" 297 show NR_Pow = "pow" 298 299-- | Pseudo-boolean operations 300data PBOp = PB_AtMost Int -- ^ At most k 301 | PB_AtLeast Int -- ^ At least k 302 | PB_Exactly Int -- ^ Exactly k 303 | PB_Le [Int] Int -- ^ At most k, with coefficients given. Generalizes PB_AtMost 304 | PB_Ge [Int] Int -- ^ At least k, with coefficients given. Generalizes PB_AtLeast 305 | PB_Eq [Int] Int -- ^ Exactly k, with coefficients given. Generalized PB_Exactly 306 deriving (Eq, Ord, Show, G.Data) 307 308-- | Overflow operations 309data OvOp = Overflow_SMul_OVFL -- ^ Signed multiplication overflow 310 | Overflow_SMul_UDFL -- ^ Signed multiplication underflow 311 | Overflow_UMul_OVFL -- ^ Unsigned multiplication overflow 312 deriving (Eq, Ord, G.Data) 313 314-- | Show instance. It's important that these follow the internal z3 names 315instance Show OvOp where 316 show Overflow_SMul_OVFL = "bvsmul_noovfl" 317 show Overflow_SMul_UDFL = "bvsmul_noudfl" 318 show Overflow_UMul_OVFL = "bvumul_noovfl" 319 320-- | String operations. Note that we do not define @StrAt@ as it translates to 'StrSubstr' trivially. 321data StrOp = StrConcat -- ^ Concatenation of one or more strings 322 | StrLen -- ^ String length 323 | StrUnit -- ^ Unit string 324 | StrNth -- ^ Nth element 325 | StrSubstr -- ^ Retrieves substring of @s@ at @offset@ 326 | StrIndexOf -- ^ Retrieves first position of @sub@ in @s@, @-1@ if there are no occurrences 327 | StrContains -- ^ Does @s@ contain the substring @sub@? 328 | StrPrefixOf -- ^ Is @pre@ a prefix of @s@? 329 | StrSuffixOf -- ^ Is @suf@ a suffix of @s@? 330 | StrReplace -- ^ Replace the first occurrence of @src@ by @dst@ in @s@ 331 | StrStrToNat -- ^ Retrieve integer encoded by string @s@ (ground rewriting only) 332 | StrNatToStr -- ^ Retrieve string encoded by integer @i@ (ground rewriting only) 333 | StrToCode -- ^ Equivalent to Haskell's ord 334 | StrFromCode -- ^ Equivalent to Haskell's chr 335 | StrInRe RegExp -- ^ Check if string is in the regular expression 336 deriving (Eq, Ord, G.Data) 337 338-- | Regular expressions. Note that regular expressions themselves are 339-- concrete, but the 'Data.SBV.RegExp.match' function from the 'Data.SBV.RegExp.RegExpMatchable' class 340-- can check membership against a symbolic string/character. Also, we 341-- are preferring a datatype approach here, as opposed to coming up with 342-- some string-representation; there are way too many alternatives 343-- already so inventing one isn't a priority. Please get in touch if you 344-- would like a parser for this type as it might be easier to use. 345data RegExp = Literal String -- ^ Precisely match the given string 346 | All -- ^ Accept every string 347 | None -- ^ Accept no strings 348 | Range Char Char -- ^ Accept range of characters 349 | Conc [RegExp] -- ^ Concatenation 350 | KStar RegExp -- ^ Kleene Star: Zero or more 351 | KPlus RegExp -- ^ Kleene Plus: One or more 352 | Opt RegExp -- ^ Zero or one 353 | Loop Int Int RegExp -- ^ From @n@ repetitions to @m@ repetitions 354 | Union [RegExp] -- ^ Union of regular expressions 355 | Inter RegExp RegExp -- ^ Intersection of regular expressions 356 deriving (Eq, Ord, G.Data) 357 358-- | With overloaded strings, we can have direct literal regular expressions. 359instance IsString RegExp where 360 fromString = Literal 361 362-- | Regular expressions as a 'Num' instance. Note that 363-- only `+` (union) and `*` (concatenation) make sense. 364instance Num RegExp where 365 -- flatten the concats to make them simpler 366 Conc xs * y = Conc (xs ++ [y]) 367 x * Conc ys = Conc (x : ys) 368 x * y = Conc [x, y] 369 370 -- flatten the unions to make them simpler 371 Union xs + y = Union (xs ++ [y]) 372 x + Union ys = Union (x : ys) 373 x + y = Union [x, y] 374 375 abs = error "Num.RegExp: no abs method" 376 signum = error "Num.RegExp: no signum method" 377 378 fromInteger x 379 | x == 0 = None 380 | x == 1 = Literal "" -- Unit for concatenation is the empty string 381 | True = error $ "Num.RegExp: Only 0 and 1 makes sense as a reg-exp, no meaning for: " ++ show x 382 383 negate = error "Num.RegExp: no negate method" 384 385-- | Convert a reg-exp to a Haskell-like string 386instance Show RegExp where 387 show = regExpToString show 388 389-- | Convert a reg-exp to a SMT-lib acceptable representation 390regExpToSMTString :: RegExp -> String 391regExpToSMTString = regExpToString (\s -> '"' : stringToQFS s ++ "\"") 392 393-- | Convert a RegExp to a string, parameterized by how strings are converted 394regExpToString :: (String -> String) -> RegExp -> String 395regExpToString fs (Literal s) = "(str.to.re " ++ fs s ++ ")" 396regExpToString _ All = "re.allchar" 397regExpToString _ None = "re.nostr" 398regExpToString fs (Range ch1 ch2) = "(re.range " ++ fs [ch1] ++ " " ++ fs [ch2] ++ ")" 399regExpToString _ (Conc []) = show (1 :: Integer) 400regExpToString fs (Conc [x]) = regExpToString fs x 401regExpToString fs (Conc xs) = "(re.++ " ++ unwords (map (regExpToString fs) xs) ++ ")" 402regExpToString fs (KStar r) = "(re.* " ++ regExpToString fs r ++ ")" 403regExpToString fs (KPlus r) = "(re.+ " ++ regExpToString fs r ++ ")" 404regExpToString fs (Opt r) = "(re.opt " ++ regExpToString fs r ++ ")" 405regExpToString fs (Loop lo hi r) 406 | lo >= 0, hi >= lo = "((_ re.loop " ++ show lo ++ " " ++ show hi ++ ") " ++ regExpToString fs r ++ ")" 407 | True = error $ "Invalid regular-expression Loop with arguments: " ++ show (lo, hi) 408regExpToString fs (Inter r1 r2) = "(re.inter " ++ regExpToString fs r1 ++ " " ++ regExpToString fs r2 ++ ")" 409regExpToString _ (Union []) = "re.nostr" 410regExpToString fs (Union [x]) = regExpToString fs x 411regExpToString fs (Union xs) = "(re.union " ++ unwords (map (regExpToString fs) xs) ++ ")" 412 413-- | Show instance for @StrOp@. Note that the mapping here is 414-- important to match the SMTLib equivalents, see here: <http://rise4fun.com/z3/tutorialcontent/sequences> 415instance Show StrOp where 416 show StrConcat = "str.++" 417 show StrLen = "str.len" 418 show StrUnit = "str.unit" -- NB. This is actually a no-op, since in SMTLib characters are the same as strings. 419 show StrNth = "str.at" 420 show StrSubstr = "str.substr" 421 show StrIndexOf = "str.indexof" 422 show StrContains = "str.contains" 423 show StrPrefixOf = "str.prefixof" 424 show StrSuffixOf = "str.suffixof" 425 show StrReplace = "str.replace" 426 show StrStrToNat = "str.to.int" -- NB. SMTLib uses "int" here though only nats are supported 427 show StrNatToStr = "int.to.str" -- NB. SMTLib uses "int" here though only nats are supported 428 show StrToCode = "str.to_code" 429 show StrFromCode = "str.from_code" 430 -- Note the breakage here with respect to argument order. We fix this explicitly later. 431 show (StrInRe s) = "str.in.re " ++ regExpToSMTString s 432 433-- | Sequence operations. 434data SeqOp = SeqConcat -- ^ See StrConcat 435 | SeqLen -- ^ See StrLen 436 | SeqUnit -- ^ See StrUnit 437 | SeqNth -- ^ See StrNth 438 | SeqSubseq -- ^ See StrSubseq 439 | SeqIndexOf -- ^ See StrIndexOf 440 | SeqContains -- ^ See StrContains 441 | SeqPrefixOf -- ^ See StrPrefixOf 442 | SeqSuffixOf -- ^ See StrSuffixOf 443 | SeqReplace -- ^ See StrReplace 444 deriving (Eq, Ord, G.Data) 445 446-- | Show instance for SeqOp. Again, mapping is important. 447instance Show SeqOp where 448 show SeqConcat = "seq.++" 449 show SeqLen = "seq.len" 450 show SeqUnit = "seq.unit" 451 show SeqNth = "seq.nth" 452 show SeqSubseq = "seq.extract" 453 show SeqIndexOf = "seq.indexof" 454 show SeqContains = "seq.contains" 455 show SeqPrefixOf = "seq.prefixof" 456 show SeqSuffixOf = "seq.suffixof" 457 show SeqReplace = "seq.replace" 458 459-- | Set operations. 460data SetOp = SetEqual 461 | SetMember 462 | SetInsert 463 | SetDelete 464 | SetIntersect 465 | SetUnion 466 | SetSubset 467 | SetDifference 468 | SetComplement 469 | SetHasSize 470 deriving (Eq, Ord, G.Data) 471 472-- The show instance for 'SetOp' is merely for debugging, we map them separately so 473-- the mapped strings are less important here. 474instance Show SetOp where 475 show SetEqual = "==" 476 show SetMember = "Set.member" 477 show SetInsert = "Set.insert" 478 show SetDelete = "Set.delete" 479 show SetIntersect = "Set.intersect" 480 show SetUnion = "Set.union" 481 show SetSubset = "Set.subset" 482 show SetDifference = "Set.difference" 483 show SetComplement = "Set.complement" 484 show SetHasSize = "Set.setHasSize" 485 486-- Show instance for 'Op'. Note that this is largely for debugging purposes, not used 487-- for being read by any tool. 488instance Show Op where 489 show Shl = "<<" 490 show Shr = ">>" 491 492 show (Rol i) = "<<<" ++ show i 493 show (Ror i) = ">>>" ++ show i 494 495 show (Extract i j) = "choose [" ++ show i ++ ":" ++ show j ++ "]" 496 497 show (LkUp (ti, at, rt, l) i e) 498 = "lookup(" ++ tinfo ++ ", " ++ show i ++ ", " ++ show e ++ ")" 499 where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")" 500 501 show (ArrEq i j) = "array_" ++ show i ++ " == array_" ++ show j 502 show (ArrRead i) = "select array_" ++ show i 503 504 show (KindCast fr to) = "cast_" ++ show fr ++ "_" ++ show to 505 show (Uninterpreted i) = "[uninterpreted] " ++ i 506 507 show (Label s) = "[label] " ++ s 508 509 show (IEEEFP w) = show w 510 511 show (NonLinear w) = show w 512 513 show (PseudoBoolean p) = show p 514 515 show (OverflowOp o) = show o 516 517 show (StrOp s) = show s 518 show (SeqOp s) = show s 519 show (SetOp s) = show s 520 521 show (TupleConstructor 0) = "mkSBVTuple0" 522 show (TupleConstructor n) = "mkSBVTuple" ++ show n 523 show (TupleAccess i n) = "proj_" ++ show i ++ "_SBVTuple" ++ show n 524 525 -- Remember, while we try to maintain SMTLib compabitibility here, these output 526 -- is merely for debugging purposes. For how we actually render these in SMTLib, 527 -- look at the file SBV/SMT/SMTLib2.hs for these constructors. 528 show (EitherConstructor k1 k2 False) = "(_ left_SBVEither " ++ show (KEither k1 k2) ++ ")" 529 show (EitherConstructor k1 k2 True ) = "(_ right_SBVEither " ++ show (KEither k1 k2) ++ ")" 530 show (EitherIs k1 k2 False) = "(_ is (left_SBVEither (" ++ show k1 ++ ") " ++ show (KEither k1 k2) ++ "))" 531 show (EitherIs k1 k2 True ) = "(_ is (right_SBVEither (" ++ show k2 ++ ") " ++ show (KEither k1 k2) ++ "))" 532 show (EitherAccess False) = "get_left_SBVEither" 533 show (EitherAccess True ) = "get_right_SBVEither" 534 show (MaybeConstructor k False) = "(_ nothing_SBVMaybe " ++ show (KMaybe k) ++ ")" 535 show (MaybeConstructor k True) = "(_ just_SBVMaybe " ++ show (KMaybe k) ++ ")" 536 show (MaybeIs k False) = "(_ is (nothing_SBVMaybe () " ++ show (KMaybe k) ++ "))" 537 show (MaybeIs k True ) = "(_ is (just_SBVMaybe (" ++ show k ++ ") " ++ show (KMaybe k) ++ "))" 538 show MaybeAccess = "get_just_SBVMaybe" 539 540 show op 541 | Just s <- op `lookup` syms = s 542 | True = error "impossible happened; can't find op!" 543 where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-"), (UNeg, "-"), (Abs, "abs") 544 , (Quot, "quot") 545 , (Rem, "rem") 546 , (Equal, "=="), (NotEqual, "/=") 547 , (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") 548 , (Ite, "if_then_else") 549 , (And, "&"), (Or, "|"), (XOr, "^"), (Not, "~") 550 , (Join, "#") 551 ] 552 553-- | Quantifiers: forall or exists. Note that we allow 554-- arbitrary nestings. 555data Quantifier = ALL | EX deriving Eq 556 557-- | Show instance for 'Quantifier' 558instance Show Quantifier where 559 show ALL = "Forall" 560 show EX = "Exists" 561 562-- | Which context is this variable being created? 563data VarContext = NonQueryVar (Maybe Quantifier) -- in this case, it can be quantified 564 | QueryVar -- in this case, it is always existential 565 566-- | Are there any existential quantifiers? 567needsExistentials :: [Quantifier] -> Bool 568needsExistentials = (EX `elem`) 569 570-- | A simple type for SBV computations, used mainly for uninterpreted constants. 571-- We keep track of the signedness/size of the arguments. A non-function will 572-- have just one entry in the list. 573newtype SBVType = SBVType [Kind] 574 deriving (Eq, Ord) 575 576instance Show SBVType where 577 show (SBVType []) = error "SBV: internal error, empty SBVType" 578 show (SBVType xs) = intercalate " -> " $ map show xs 579 580-- | A symbolic expression 581data SBVExpr = SBVApp !Op ![SV] 582 deriving (Eq, Ord, G.Data) 583 584-- | To improve hash-consing, take advantage of commutative operators by 585-- reordering their arguments. 586reorder :: SBVExpr -> SBVExpr 587reorder s = case s of 588 SBVApp op [a, b] | isCommutative op && a > b -> SBVApp op [b, a] 589 _ -> s 590 where isCommutative :: Op -> Bool 591 isCommutative o = o `elem` [Plus, Times, Equal, NotEqual, And, Or, XOr] 592 593-- Show instance for 'SBVExpr'. Again, only for debugging purposes. 594instance Show SBVExpr where 595 show (SBVApp Ite [t, a, b]) = unwords ["if", show t, "then", show a, "else", show b] 596 show (SBVApp Shl [a, i]) = unwords [show a, "<<", show i] 597 show (SBVApp Shr [a, i]) = unwords [show a, ">>", show i] 598 show (SBVApp (Rol i) [a]) = unwords [show a, "<<<", show i] 599 show (SBVApp (Ror i) [a]) = unwords [show a, ">>>", show i] 600 show (SBVApp (PseudoBoolean pb) args) = unwords (show pb : map show args) 601 show (SBVApp (OverflowOp op) args) = unwords (show op : map show args) 602 show (SBVApp op [a, b]) = unwords [show a, show op, show b] 603 show (SBVApp op args) = unwords (show op : map show args) 604 605-- | A program is a sequence of assignments 606newtype SBVPgm = SBVPgm {pgmAssignments :: S.Seq (SV, SBVExpr)} 607 608-- | Helper synonym for text, in case we switch to something else later. 609type Name = T.Text 610 611-- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names 612data NamedSymVar = NamedSymVar !SV !Name 613 deriving (Show,Generic) 614 615-- | For comparison purposes, we simply use the SV and ignore the name 616instance Eq NamedSymVar where 617 (==) (NamedSymVar l _) (NamedSymVar r _) = l == r 618 619instance Ord NamedSymVar where 620 compare (NamedSymVar l _) (NamedSymVar r _) = compare l r 621 622-- | Convert to a named symvar, from string 623toNamedSV' :: SV -> String -> NamedSymVar 624toNamedSV' s = NamedSymVar s . T.pack 625 626-- | Convert to a named symvar, from text 627toNamedSV :: SV -> Name -> NamedSymVar 628toNamedSV = NamedSymVar 629 630-- | Get the node id from a named sym var 631namedNodeId :: NamedSymVar -> NodeId 632namedNodeId = swNodeId . getSV 633 634-- | Get the SV from a named sym var 635getSV :: NamedSymVar -> SV 636getSV (NamedSymVar s _) = s 637 638-- | Get the user-name typed value from named sym var 639getUserName :: NamedSymVar -> Name 640getUserName (NamedSymVar _ nm) = nm 641 642-- | Get the string typed value from named sym var 643getUserName' :: NamedSymVar -> String 644getUserName' = T.unpack . getUserName 645 646-- | Style of optimization. Note that in the pareto case the user is allowed 647-- to specify a max number of fronts to query the solver for, since there might 648-- potentially be an infinite number of them and there is no way to know exactly 649-- how many ahead of time. If 'Nothing' is given, SBV will possibly loop forever 650-- if the number is really infinite. 651data OptimizeStyle = Lexicographic -- ^ Objectives are optimized in the order given, earlier objectives have higher priority. 652 | Independent -- ^ Each objective is optimized independently. 653 | Pareto (Maybe Int) -- ^ Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. 654 deriving (Eq, Show) 655 656-- | Penalty for a soft-assertion. The default penalty is @1@, with all soft-assertions belonging 657-- to the same objective goal. A positive weight and an optional group can be provided by using 658-- the 'Penalty' constructor. 659data Penalty = DefaultPenalty -- ^ Default: Penalty of @1@ and no group attached 660 | Penalty Rational (Maybe String) -- ^ Penalty with a weight and an optional group 661 deriving Show 662 663-- | Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty 664-- for not satisfying it. 665data Objective a = Minimize String a -- ^ Minimize this metric 666 | Maximize String a -- ^ Maximize this metric 667 | AssertWithPenalty String a Penalty -- ^ A soft assertion, with an associated penalty 668 deriving (Show, Functor) 669 670-- | The name of the objective 671objectiveName :: Objective a -> String 672objectiveName (Minimize s _) = s 673objectiveName (Maximize s _) = s 674objectiveName (AssertWithPenalty s _ _) = s 675 676-- | The state we keep track of as we interact with the solver 677data QueryState = QueryState { queryAsk :: Maybe Int -> String -> IO String 678 , querySend :: Maybe Int -> String -> IO () 679 , queryRetrieveResponse :: Maybe Int -> IO String 680 , queryConfig :: SMTConfig 681 , queryTerminate :: IO () 682 , queryTimeOutValue :: Maybe Int 683 , queryAssertionStackDepth :: Int 684 } 685 686-- | Computations which support query operations. 687class Monad m => MonadQuery m where 688 queryState :: m State 689 690 default queryState :: (MonadTrans t, MonadQuery m', m ~ t m') => m State 691 queryState = lift queryState 692 693instance MonadQuery m => MonadQuery (ExceptT e m) 694instance MonadQuery m => MonadQuery (MaybeT m) 695instance MonadQuery m => MonadQuery (ReaderT r m) 696instance MonadQuery m => MonadQuery (SS.StateT s m) 697instance MonadQuery m => MonadQuery (LS.StateT s m) 698instance (MonadQuery m, Monoid w) => MonadQuery (SW.WriterT w m) 699instance (MonadQuery m, Monoid w) => MonadQuery (LW.WriterT w m) 700 701-- | A query is a user-guided mechanism to directly communicate and extract 702-- results from the solver. A generalization of 'Data.SBV.Query'. 703newtype QueryT m a = QueryT { runQueryT :: ReaderT State m a } 704 deriving (Applicative, Functor, Monad, MonadIO, MonadTrans, 705 MonadError e, MonadState s, MonadWriter w) 706 707instance Monad m => MonadQuery (QueryT m) where 708 queryState = QueryT ask 709 710mapQueryT :: (ReaderT State m a -> ReaderT State n b) -> QueryT m a -> QueryT n b 711mapQueryT f = QueryT . f . runQueryT 712{-# INLINE mapQueryT #-} 713 714-- | Create a fresh variable of some type in the underlying query monad transformer. 715-- For further control on how these variables are projected and embedded, see the 716-- 'Queriable' class. 717class Fresh m a where 718 fresh :: QueryT m a 719 720-- | An queriable value. This is a generalization of the 'Fresh' class, in case one needs 721-- to be more specific about how projections/embeddings are done. 722class Queriable m a b | a -> b where 723 -- | ^ Create a new symbolic value of type @a@ 724 create :: QueryT m a 725 -- | ^ Extract the current value in a SAT context 726 project :: a -> QueryT m b 727 -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other 728 -- via the 'QueryT' monad transformer. 729 embed :: b -> QueryT m a 730 731-- Have to define this one by hand, because we use ReaderT in the implementation 732instance MonadReader r m => MonadReader r (QueryT m) where 733 ask = lift ask 734 local f = mapQueryT $ mapReaderT $ local f 735 736-- | A query is a user-guided mechanism to directly communicate and extract 737-- results from the solver. 738type Query = QueryT IO 739 740instance MonadSymbolic Query where 741 symbolicEnv = queryState 742 743instance NFData OptimizeStyle where 744 rnf x = x `seq` () 745 746instance NFData Penalty where 747 rnf DefaultPenalty = () 748 rnf (Penalty p mbs) = rnf p `seq` rnf mbs 749 750instance NFData a => NFData (Objective a) where 751 rnf (Minimize s a) = rnf s `seq` rnf a 752 rnf (Maximize s a) = rnf s `seq` rnf a 753 rnf (AssertWithPenalty s a p) = rnf s `seq` rnf a `seq` rnf p 754 755-- | Result of running a symbolic computation 756data Result = Result { reskinds :: Set.Set Kind -- ^ kinds used in the program 757 , resTraces :: [(String, CV)] -- ^ quick-check counter-example information (if any) 758 , resObservables :: [(String, CV -> Bool, SV)] -- ^ observable expressions (part of the model) 759 , resUISegs :: [(String, [String])] -- ^ uninterpeted code segments 760 , resInputs :: ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- ^ inputs (possibly existential) + tracker vars 761 , resConsts :: (CnstMap, [(SV, CV)]) -- ^ constants 762 , resTables :: [((Int, Kind, Kind), [SV])] -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts 763 , resArrays :: [(Int, ArrayInfo)] -- ^ arrays (user specified) 764 , resUIConsts :: [(String, SBVType)] -- ^ uninterpreted constants 765 , resAxioms :: [(String, [String])] -- ^ axioms 766 , resAsgns :: SBVPgm -- ^ assignments 767 , resConstraints :: S.Seq (Bool, [(String, String)], SV) -- ^ additional constraints (boolean) 768 , resAssertions :: [(String, Maybe CallStack, SV)] -- ^ assertions 769 , resOutputs :: [SV] -- ^ outputs 770 } 771 772-- Show instance for 'Result'. Only for debugging purposes. 773instance Show Result where 774 -- If there's nothing interesting going on, just print the constant. Note that the 775 -- definiton of interesting here is rather subjective; but essentially if we reduced 776 -- the result to a single constant already, without any reference to anything. 777 show Result{resConsts=(_, cs), resOutputs=[r]} 778 | Just c <- r `lookup` cs 779 = show c 780 show (Result kinds _ _ cgs is (_, cs) ts as uis axs xs cstrs asserts os) = intercalate "\n" $ 781 (if null usorts then [] else "SORTS" : map (" " ++) usorts) 782 ++ ["INPUTS"] 783 ++ map shn (fst is) 784 ++ (if null (snd is) then [] else "TRACKER VARS" : map (shn . (EX,)) (snd is)) 785 ++ ["CONSTANTS"] 786 ++ concatMap shc cs 787 ++ ["TABLES"] 788 ++ map sht ts 789 ++ ["ARRAYS"] 790 ++ map sha as 791 ++ ["UNINTERPRETED CONSTANTS"] 792 ++ map shui uis 793 ++ ["USER GIVEN CODE SEGMENTS"] 794 ++ concatMap shcg cgs 795 ++ ["AXIOMS"] 796 ++ map shax axs 797 ++ ["DEFINE"] 798 ++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList (pgmAssignments xs)) 799 ++ ["CONSTRAINTS"] 800 ++ map ((" " ++) . shCstr) (F.toList cstrs) 801 ++ ["ASSERTIONS"] 802 ++ map ((" "++) . shAssert) asserts 803 ++ ["OUTPUTS"] 804 ++ sh2 os 805 where sh2 :: Show a => [a] -> [String] 806 sh2 = map ((" "++) . show) 807 808 usorts = [sh s t | KUserSort s t <- Set.toList kinds] 809 where sh s Nothing = s 810 sh s (Just es) = s ++ " (" ++ intercalate ", " es ++ ")" 811 812 shs sv = show sv ++ " :: " ++ show (swKind sv) 813 814 sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es 815 816 shc (sv, cv) 817 | sv == falseSV || sv == trueSV 818 = [] 819 | True 820 = [" " ++ show sv ++ " = " ++ show cv] 821 822 shcg (s, ss) = ("Variable: " ++ s) : map (" " ++) ss 823 824 shn (q, NamedSymVar sv nm) = " " <> ni <> " :: " ++ show (swKind sv) ++ ex ++ alias 825 where ni = show sv 826 ex | q == ALL = "" 827 | True = ", existential" 828 829 alias | ni == T.unpack nm = "" 830 | True = ", aliasing " ++ show nm 831 832 sha (i, (nm, (ai, bi), ctx)) = " " ++ ni ++ " :: " ++ show ai ++ " -> " ++ show bi ++ alias 833 ++ "\n Context: " ++ show ctx 834 where ni = "array_" ++ show i 835 alias | ni == nm = "" 836 | True = ", aliasing " ++ show nm 837 838 shui (nm, t) = " [uninterpreted] " ++ nm ++ " :: " ++ show t 839 840 shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss 841 842 shCstr (isSoft, [], c) = soft isSoft ++ show c 843 shCstr (isSoft, [(":named", nm)], c) = soft isSoft ++ nm ++ ": " ++ show c 844 shCstr (isSoft, attrs, c) = soft isSoft ++ show c ++ " (attributes: " ++ show attrs ++ ")" 845 846 soft True = "[SOFT] " 847 soft False = "" 848 849 shAssert (nm, stk, p) = " -- assertion: " ++ nm ++ " " ++ maybe "[No location]" 850#if MIN_VERSION_base(4,9,0) 851 prettyCallStack 852#else 853 showCallStack 854#endif 855 stk ++ ": " ++ show p 856 857-- | The context of a symbolic array as created 858data ArrayContext = ArrayFree (Maybe SV) -- ^ A new array, the contents are initialized with the given value, if any 859 | ArrayMutate ArrayIndex SV SV -- ^ An array created by mutating another array at a given cell 860 | ArrayMerge SV ArrayIndex ArrayIndex -- ^ An array created by symbolically merging two other arrays 861 862instance Show ArrayContext where 863 show (ArrayFree Nothing) = " initialized with random elements" 864 show (ArrayFree (Just sv)) = " initialized with " ++ show sv 865 show (ArrayMutate i a b) = " cloned from array_" ++ show i ++ " with " ++ show a ++ " :: " ++ show (swKind a) ++ " |-> " ++ show b ++ " :: " ++ show (swKind b) 866 show (ArrayMerge s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s 867 868-- | Expression map, used for hash-consing 869type ExprMap = Map.Map SBVExpr SV 870 871-- | Constants are stored in a map, for hash-consing. 872type CnstMap = Map.Map CV SV 873 874-- | Kinds used in the program; used for determining the final SMT-Lib logic to pick 875type KindSet = Set.Set Kind 876 877-- | Tables generated during a symbolic run 878type TableMap = Map.Map (Kind, Kind, [SV]) Int 879 880-- | Representation for symbolic arrays 881type ArrayInfo = (String, (Kind, Kind), ArrayContext) 882 883-- | SMT Arrays generated during a symbolic run 884type ArrayMap = IMap.IntMap ArrayInfo 885 886-- | Functional Arrays generated during a symbolic run 887type FArrayMap = IMap.IntMap (SVal -> SVal, IORef (IMap.IntMap SV)) 888 889-- | Uninterpreted-constants generated during a symbolic run 890type UIMap = Map.Map String SBVType 891 892-- | Code-segments for Uninterpreted-constants, as given by the user 893type CgMap = Map.Map String [String] 894 895-- | Cached values, implementing sharing 896type Cache a = IMap.IntMap [(StableName (State -> IO a), a)] 897 898-- | Stage of an interactive run 899data IStage = ISetup -- Before we initiate contact. 900 | ISafe -- In the context of a safe/safeWith call 901 | IRun -- After the contact is started 902 903-- | Are we cecking safety 904isSafetyCheckingIStage :: IStage -> Bool 905isSafetyCheckingIStage s = case s of 906 ISetup -> False 907 ISafe -> True 908 IRun -> False 909 910-- | Are we in setup? 911isSetupIStage :: IStage -> Bool 912isSetupIStage s = case s of 913 ISetup -> True 914 ISafe -> False 915 IRun -> True 916 917-- | Are we in a run? 918isRunIStage :: IStage -> Bool 919isRunIStage s = case s of 920 ISetup -> False 921 ISafe -> False 922 IRun -> True 923 924-- | Different means of running a symbolic piece of code 925data SBVRunMode = SMTMode QueryContext IStage Bool SMTConfig -- ^ In regular mode, with a stage. Bool is True if this is SAT. 926 | CodeGen -- ^ Code generation mode. 927 | Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)])) -- ^ Concrete simulation mode, with given environment if any. If Nothing: Random. 928 929-- Show instance for SBVRunMode; debugging purposes only 930instance Show SBVRunMode where 931 show (SMTMode qc ISetup True _) = "Satisfiability setup (" ++ show qc ++ ")" 932 show (SMTMode qc ISafe True _) = "Safety setup (" ++ show qc ++ ")" 933 show (SMTMode qc IRun True _) = "Satisfiability (" ++ show qc ++ ")" 934 show (SMTMode qc ISetup False _) = "Proof setup (" ++ show qc ++ ")" 935 show (SMTMode qc ISafe False _) = error $ "ISafe-False is not an expected/supported combination for SBVRunMode! (" ++ show qc ++ ")" 936 show (SMTMode qc IRun False _) = "Proof (" ++ show qc ++ ")" 937 show CodeGen = "Code generation" 938 show (Concrete Nothing) = "Concrete evaluation with random values" 939 show (Concrete (Just (True, _))) = "Concrete evaluation during model validation for sat" 940 show (Concrete (Just (False, _))) = "Concrete evaluation during model validation for prove" 941 942-- | Is this a CodeGen run? (i.e., generating code) 943isCodeGenMode :: State -> IO Bool 944isCodeGenMode State{runMode} = do rm <- readIORef runMode 945 return $ case rm of 946 Concrete{} -> False 947 SMTMode{} -> False 948 CodeGen -> True 949 950-- | The state in query mode, i.e., additional context 951data IncState = IncState { rNewInps :: IORef [NamedSymVar] -- always existential! 952 , rNewKinds :: IORef KindSet 953 , rNewConsts :: IORef CnstMap 954 , rNewArrs :: IORef ArrayMap 955 , rNewTbls :: IORef TableMap 956 , rNewUIs :: IORef UIMap 957 , rNewAsgns :: IORef SBVPgm 958 , rNewConstraints :: IORef (S.Seq (Bool, [(String, String)], SV)) 959 } 960 961-- | Get a new IncState 962newIncState :: IO IncState 963newIncState = do 964 is <- newIORef [] 965 ks <- newIORef Set.empty 966 nc <- newIORef Map.empty 967 am <- newIORef IMap.empty 968 tm <- newIORef Map.empty 969 ui <- newIORef Map.empty 970 pgm <- newIORef (SBVPgm S.empty) 971 cstrs <- newIORef S.empty 972 return IncState { rNewInps = is 973 , rNewKinds = ks 974 , rNewConsts = nc 975 , rNewArrs = am 976 , rNewTbls = tm 977 , rNewUIs = ui 978 , rNewAsgns = pgm 979 , rNewConstraints = cstrs 980 } 981 982-- | Get a new IncState 983withNewIncState :: State -> (State -> IO a) -> IO (IncState, a) 984withNewIncState st cont = do 985 is <- newIncState 986 R.modifyIORef' (rIncState st) (const is) 987 r <- cont st 988 finalIncState <- readIORef (rIncState st) 989 return (finalIncState, r) 990 991 992-- | User defined, with proper quantifiers 993type UserInputs = S.Seq (Quantifier, NamedSymVar) 994 995-- | Internally declared, always existential 996type InternInps = S.Seq NamedSymVar 997 998-- | Entire set of names, for faster lookup 999type AllInps = Set.Set Name 1000 1001-- | Inputs as a record of maps and sets. See above type-synonyms for their roles. 1002data Inputs = Inputs { userInputs :: !UserInputs 1003 , internInputs :: !InternInps 1004 , allInputs :: !AllInps 1005 } deriving (Eq,Show) 1006 1007-- | Semigroup instance; combining according to indexes. 1008instance Semigroup Inputs where 1009 (Inputs lui lii lai) <> (Inputs rui rii rai) = Inputs (lui <> rui) (lii <> rii) (lai <> rai) 1010 1011-- | Monoid instance, we start with no maps. 1012instance Monoid Inputs where 1013 mempty = Inputs { userInputs = mempty 1014 , internInputs = mempty 1015 , allInputs = mempty 1016 } 1017 1018-- | Get the quantifier 1019quantifier :: (Quantifier, NamedSymVar) -> Quantifier 1020quantifier = fst 1021 1022-- | Get the named symbolic variable 1023namedSymVar :: (Quantifier, NamedSymVar) -> NamedSymVar 1024namedSymVar = snd 1025 1026-- | Modify the user-inputs field 1027onUserInputs :: (UserInputs -> UserInputs) -> Inputs -> Inputs 1028onUserInputs f inp@Inputs{userInputs} = inp{userInputs = f userInputs} 1029 1030-- | Modify the internal-inputs field 1031onInternInputs :: (InternInps -> InternInps) -> Inputs -> Inputs 1032onInternInputs f inp@Inputs{internInputs} = inp{internInputs = f internInputs} 1033 1034-- | Modify the all-inputs field 1035onAllInputs :: (AllInps -> AllInps) -> Inputs -> Inputs 1036onAllInputs f inp@Inputs{allInputs} = inp{allInputs = f allInputs} 1037 1038-- | Add a new internal input 1039addInternInput :: SV -> Name -> Inputs -> Inputs 1040addInternInput sv nm = goAll . goIntern 1041 where !new = toNamedSV sv nm 1042 goIntern = onInternInputs (S.|> new) 1043 goAll = onAllInputs (Set.insert nm) 1044 1045-- | Add a new user input 1046addUserInput :: Quantifier -> SV -> Name -> Inputs -> Inputs 1047addUserInput q sv nm = goAll . goUser 1048 where new = toNamedSV sv nm 1049 goUser = onUserInputs (S.|> (q, new)) -- add to the end of the sequence 1050 goAll = onAllInputs (Set.insert nm) 1051 1052-- | Return user and internal inputs 1053getInputs :: Inputs -> (UserInputs, InternInps) 1054getInputs Inputs{userInputs, internInputs} = (userInputs, internInputs) 1055 1056-- | Find a user-input from its SV 1057lookupInput :: Eq a => (a -> SV) -> SV -> S.Seq a -> Maybe a 1058lookupInput f sv ns = res 1059 where 1060 i = getId (swNodeId sv) 1061 svs = fmap f ns 1062 res = case S.lookup i ns of -- Nothing on negative Int or Int > length seq 1063 Nothing -> secondLookup 1064 x@(Just e) -> if sv == f e then x else secondLookup 1065 -- we try the fast lookup first, if the node ids don't match then 1066 -- we use the more expensive O (n) to find the index and the elem 1067 secondLookup = S.elemIndexL sv svs >>= flip S.lookup ns 1068 1069-- | Extract universals 1070getUniversals :: UserInputs -> S.Seq NamedSymVar 1071getUniversals = fmap namedSymVar . S.filter ((== ALL) . quantifier) 1072 1073-- | Get a prefix of the user inputs by a predicate. Note that we could not rely 1074-- on fusion here but this is cheap and easy until there is an observable slow down from not fusing. 1075userInpsPrefixBy :: ((Quantifier, NamedSymVar) -> Bool) -> UserInputs -> UserInputs 1076userInpsPrefixBy = S.takeWhileL 1077 1078-- | Find prefix existentials, i.e., those that are at skolem positions and have valid model values. 1079prefixExistentials :: UserInputs -> UserInputs 1080prefixExistentials = userInpsPrefixBy ((/= ALL) . quantifier) 1081 1082-- | Find prefix universals. Corresponds to the above in a proof context. 1083prefixUniversals :: UserInputs -> UserInputs 1084prefixUniversals = userInpsPrefixBy ((== ALL) . quantifier) 1085 1086-- | Conversion from named-symvars to user-inputs 1087inputsFromListWith :: (NamedSymVar -> Quantifier) -> [NamedSymVar] -> UserInputs 1088inputsFromListWith f = S.fromList . fmap go 1089 where go n = (f n, n) 1090 1091-- | Helper functions around inputs. 1092-- TODO: remove these functions once lists have been pushed to edges of code base. 1093userInputsToList :: UserInputs -> [(Quantifier, NamedSymVar)] 1094userInputsToList = F.toList 1095 1096-- | Conversion from internal-inputs to list of named sym vars 1097internInputsToList :: InternInps -> [NamedSymVar] 1098internInputsToList = F.toList 1099 1100-- | Convert to regular lists 1101inputsToList :: Inputs -> ([(Quantifier, NamedSymVar)], [NamedSymVar]) 1102inputsToList = (userInputsToList *** internInputsToList) . getInputs 1103 1104-- | The state of the symbolic interpreter 1105data State = State { pathCond :: SVal -- ^ kind KBool 1106 , startTime :: UTCTime 1107 , runMode :: IORef SBVRunMode 1108 , rIncState :: IORef IncState 1109 , rCInfo :: IORef [(String, CV)] 1110 , rObservables :: IORef (S.Seq (Name, CV -> Bool, SV)) 1111 , rctr :: IORef Int 1112 , rUsedKinds :: IORef KindSet 1113 , rUsedLbls :: IORef (Set.Set String) 1114 , rinps :: IORef Inputs 1115 , rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV)) 1116 , routs :: IORef [SV] 1117 , rtblMap :: IORef TableMap 1118 , spgm :: IORef SBVPgm 1119 , rconstMap :: IORef CnstMap 1120 , rexprMap :: IORef ExprMap 1121 , rArrayMap :: IORef ArrayMap 1122 , rFArrayMap :: IORef FArrayMap 1123 , rUIMap :: IORef UIMap 1124 , rCgMap :: IORef CgMap 1125 , raxioms :: IORef [(String, [String])] 1126 , rSMTOptions :: IORef [SMTOption] 1127 , rOptGoals :: IORef [Objective (SV, SV)] 1128 , rAsserts :: IORef [(String, Maybe CallStack, SV)] 1129 , rSVCache :: IORef (Cache SV) 1130 , rAICache :: IORef (Cache ArrayIndex) 1131 , rFAICache :: IORef (Cache FArrayIndex) 1132 , rQueryState :: IORef (Maybe QueryState) 1133 } 1134 1135-- NFData is a bit of a lie, but it's sufficient, most of the content is iorefs that we don't want to touch 1136instance NFData State where 1137 rnf State{} = () 1138 1139-- | Get the current path condition 1140getSValPathCondition :: State -> SVal 1141getSValPathCondition = pathCond 1142 1143-- | Extend the path condition with the given test value. 1144extendSValPathCondition :: State -> (SVal -> SVal) -> State 1145extendSValPathCondition st f = st{pathCond = f (pathCond st)} 1146 1147-- | Are we running in proof mode? 1148inSMTMode :: State -> IO Bool 1149inSMTMode State{runMode} = do rm <- readIORef runMode 1150 return $ case rm of 1151 CodeGen -> False 1152 Concrete{} -> False 1153 SMTMode{} -> True 1154 1155-- | The "Symbolic" value. Either a constant (@Left@) or a symbolic 1156-- value (@Right Cached@). Note that caching is essential for making 1157-- sure sharing is preserved. 1158data SVal = SVal !Kind !(Either CV (Cached SV)) 1159 1160instance HasKind SVal where 1161 kindOf (SVal k _) = k 1162 1163-- Show instance for 'SVal'. Not particularly "desirable", but will do if needed 1164-- NB. We do not show the type info on constant KBool values, since there's no 1165-- implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement 1166-- of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!) 1167instance Show SVal where 1168 show (SVal KBool (Left c)) = showCV False c 1169 show (SVal k (Left c)) = showCV False c ++ " :: " ++ show k 1170 show (SVal k (Right _)) = "<symbolic> :: " ++ show k 1171 1172-- | This instance is only defined so that we can define an instance for 1173-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. 1174-- We really don't want an 'Eq' instance for 'Data.SBV.Core.SBV' or 'SVal'. As it really makes no sense. 1175-- But since we do want the 'Data.Bits.Bits' instance, we're forced to define equality. See 1176-- <http://github.com/LeventErkok/sbv/issues/301>. We simply error out. 1177instance Eq SVal where 1178 a == b = noEquals "==" ".==" (show a, show b) 1179 a /= b = noEquals "/=" "./=" (show a, show b) 1180 1181-- Bail out nicely. 1182noEquals :: String -> String -> (String, String) -> a 1183noEquals o n (l, r) = error $ unlines [ "" 1184 , "*** Data.SBV: Comparing symbolic values using Haskell's Eq class!" 1185 , "***" 1186 , "*** Received: " ++ l ++ " " ++ o ++ " " ++ r 1187 , "*** Instead use: " ++ l ++ " " ++ n ++ " " ++ r 1188 , "***" 1189 , "*** The Eq instance for symbolic values are necessiated only because" 1190 , "*** of the Bits class requirement. You must use symbolic equality" 1191 , "*** operators instead. (And complain to Haskell folks that they" 1192 , "*** remove the 'Eq' superclass from 'Bits'!.)" 1193 ] 1194 1195-- | Things we do not support in interactive mode, at least for now! 1196noInteractive :: [String] -> a 1197noInteractive ss = error $ unlines $ "" 1198 : "*** Data.SBV: Unsupported interactive/query mode feature." 1199 : map ("*** " ++) ss 1200 ++ ["*** Data.SBV: Please report this as a feature request!"] 1201 1202-- | Things we do not support in interactive mode, nor we ever intend to 1203noInteractiveEver :: [String] -> a 1204noInteractiveEver ss = error $ unlines $ "" 1205 : "*** Data.SBV: Unsupported interactive/query mode feature." 1206 : map ("*** " ++) ss 1207 1208-- | Modification of the state, but carefully handling the interactive tasks. 1209-- Note that the state is always updated regardless of the mode, but we get 1210-- to also perform extra operation in interactive mode. (Typically error out, but also simply 1211-- ignore if it has no impact.) 1212modifyState :: State -> (State -> IORef a) -> (a -> a) -> IO () -> IO () 1213modifyState st@State{runMode} field update interactiveUpdate = do 1214 R.modifyIORef' (field st) update 1215 rm <- readIORef runMode 1216 case rm of 1217 SMTMode _ IRun _ _ -> interactiveUpdate 1218 _ -> return () 1219 1220-- | Modify the incremental state 1221modifyIncState :: State -> (IncState -> IORef a) -> (a -> a) -> IO () 1222modifyIncState State{rIncState} field update = do 1223 incState <- readIORef rIncState 1224 R.modifyIORef' (field incState) update 1225 1226-- | Add an observable 1227-- notice that we cons like a list, we should build at the end of the seq, but cons to preserve semantics for now 1228recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO () 1229recordObservable st (T.pack -> nm) chk sv = modifyState st rObservables ((nm, chk, sv) S.<|) (return ()) 1230 1231-- | Increment the variable counter 1232incrementInternalCounter :: State -> IO Int 1233incrementInternalCounter st = do ctr <- readIORef (rctr st) 1234 modifyState st rctr (+1) (return ()) 1235 return ctr 1236 1237-- | Uninterpreted constants and functions. An uninterpreted constant is 1238-- a value that is indexed by its name. The only property the prover assumes 1239-- about these values are that they are equivalent to themselves; i.e., (for 1240-- functions) they return the same results when applied to same arguments. 1241-- We support uninterpreted-functions as a general means of black-box'ing 1242-- operations that are /irrelevant/ for the purposes of the proof; i.e., when 1243-- the proofs can be performed without any knowledge about the function itself. 1244svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal 1245svUninterpreted k nm code args = SVal k $ Right $ cache result 1246 where result st = do let ty = SBVType (map kindOf args ++ [k]) 1247 newUninterpreted st nm ty code 1248 sws <- mapM (svToSV st) args 1249 mapM_ forceSVArg sws 1250 newExpr st k $ SBVApp (Uninterpreted nm) sws 1251 1252-- | Create a new uninterpreted symbol, possibly with user given code 1253newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () 1254newUninterpreted st nm t mbCode 1255 | null nm || not enclosed && (not (isAlpha (head nm)) || not (all validChar (tail nm))) 1256 = error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier." 1257 | True = do uiMap <- readIORef (rUIMap st) 1258 case nm `Map.lookup` uiMap of 1259 Just t' -> checkType t' (return ()) 1260 Nothing -> do modifyState st rUIMap (Map.insert nm t) 1261 $ modifyIncState st rNewUIs (\newUIs -> case nm `Map.lookup` newUIs of 1262 Just t' -> checkType t' newUIs 1263 Nothing -> Map.insert nm t newUIs) 1264 1265 -- No need to record the code in interactive mode: CodeGen doesn't use interactive 1266 when (isJust mbCode) $ modifyState st rCgMap (Map.insert nm (fromJust mbCode)) (return ()) 1267 where checkType :: SBVType -> r -> r 1268 checkType t' cont 1269 | t /= t' = error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n" 1270 ++ " Current type : " ++ show t ++ "\n" 1271 ++ " Previously used at: " ++ show t' 1272 | True = cont 1273 1274 validChar x = isAlphaNum x || x `elem` ("_" :: String) 1275 enclosed = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` ("|\\" :: String)) (tail (init nm))) 1276 1277-- | Add a new sAssert based constraint 1278addAssertion :: State -> Maybe CallStack -> String -> SV -> IO () 1279addAssertion st cs msg cond = modifyState st rAsserts ((msg, cs, cond):) 1280 $ noInteractive [ "Named assertions (sAssert):" 1281 , " Tag: " ++ msg 1282 , " Loc: " ++ maybe "Unknown" show cs 1283 ] 1284 1285-- | Create an internal variable, which acts as an input but isn't visible to the user. 1286-- Such variables are existentially quantified in a SAT context, and universally quantified 1287-- in a proof context. 1288internalVariable :: State -> Kind -> IO SV 1289internalVariable st k = do (NamedSymVar sv nm) <- newSV st k 1290 rm <- readIORef (runMode st) 1291 let q = case rm of 1292 SMTMode _ _ True _ -> EX 1293 SMTMode _ _ False _ -> ALL 1294 CodeGen -> ALL 1295 Concrete{} -> ALL 1296 n = "__internal_sbv_" <> nm 1297 v = NamedSymVar sv n 1298 modifyState st rinps (addUserInput q sv n) 1299 $ modifyIncState st rNewInps (\newInps -> case q of 1300 EX -> v : newInps 1301 -- I don't think the following can actually happen 1302 -- but just be safe: 1303 ALL -> noInteractive [ "Internal universally quantified variable creation:" 1304 , " Named: " <> T.unpack nm 1305 ]) 1306 return sv 1307{-# INLINE internalVariable #-} 1308 1309-- | Create a new SV 1310newSV :: State -> Kind -> IO NamedSymVar 1311newSV st k = do ctr <- incrementInternalCounter st 1312 let sv = SV k (NodeId ctr) 1313 registerKind st k 1314 return $ NamedSymVar sv $ 's' `T.cons` T.pack (show ctr) 1315{-# INLINE newSV #-} 1316 1317-- | Register a new kind with the system, used for uninterpreted sorts. 1318-- NB: Is it safe to have new kinds in query mode? It could be that 1319-- the new kind might introduce a constraint that effects the logic. For 1320-- instance, if we're seeing 'Double' for the first time and using a BV 1321-- logic, then things would fall apart. But this should be rare, and hopefully 1322-- the success-response checking mechanism will catch the rare cases where this 1323-- is an issue. In either case, the user can always arrange for the right 1324-- logic by calling 'Data.SBV.setLogic' appropriately, so it seems safe to just 1325-- allow for this. 1326registerKind :: State -> Kind -> IO () 1327registerKind st k 1328 | KUserSort sortName _ <- k, map toLower sortName `elem` smtLibReservedNames 1329 = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name." 1330 | True 1331 = do -- Adding a kind to the incState is tricky; we only need to add it 1332 -- * If it's an uninterpreted sort that's not already in the general state 1333 -- * OR If it's a tuple-sort whose cardinality isn't already in the general state 1334 -- * OR If it's a list that's not already in the general state (so we can send the flatten commands) 1335 1336 existingKinds <- readIORef (rUsedKinds st) 1337 1338 modifyState st rUsedKinds (Set.insert k) $ do 1339 1340 -- Why do we discriminate here? Because the incremental context is sensitive to the 1341 -- order: In particular, if an uninterpreted kind is already in there, we don't 1342 -- want to re-add because double-declaration would be wrong. See 'cvtInc' for details. 1343 let needsAdding = case k of 1344 KUserSort{} -> k `notElem` existingKinds 1345 KList{} -> k `notElem` existingKinds 1346 KTuple nks -> length nks `notElem` [length oks | KTuple oks <- Set.toList existingKinds] 1347 KMaybe{} -> k `notElem` existingKinds 1348 KEither{} -> k `notElem` existingKinds 1349 _ -> False 1350 1351 when needsAdding $ modifyIncState st rNewKinds (Set.insert k) 1352 1353 -- Don't forget to register subkinds! 1354 case k of 1355 KBool {} -> return () 1356 KBounded {} -> return () 1357 KUnbounded{} -> return () 1358 KReal {} -> return () 1359 KUserSort {} -> return () 1360 KFloat {} -> return () 1361 KDouble {} -> return () 1362 KFP {} -> return () 1363 KChar {} -> return () 1364 KString {} -> return () 1365 KList ek -> registerKind st ek 1366 KSet ek -> registerKind st ek 1367 KTuple eks -> mapM_ (registerKind st) eks 1368 KMaybe ke -> registerKind st ke 1369 KEither k1 k2 -> mapM_ (registerKind st) [k1, k2] 1370 1371-- | Register a new label with the system, making sure they are unique and have no '|'s in them 1372registerLabel :: String -> State -> String -> IO () 1373registerLabel whence st nm 1374 | map toLower nm `elem` smtLibReservedNames 1375 = err "is a reserved string; please use a different name." 1376 | '|' `elem` nm 1377 = err "contains the character `|', which is not allowed!" 1378 | '\\' `elem` nm 1379 = err "contains the character `\\', which is not allowed!" 1380 | True 1381 = do old <- readIORef $ rUsedLbls st 1382 if nm `Set.member` old 1383 then err "is used multiple times. Please do not use duplicate names!" 1384 else modifyState st rUsedLbls (Set.insert nm) (return ()) 1385 1386 where err w = error $ "SBV (" ++ whence ++ "): " ++ show nm ++ " " ++ w 1387 1388-- | Create a new constant; hash-cons as necessary 1389newConst :: State -> CV -> IO SV 1390newConst st c = do 1391 constMap <- readIORef (rconstMap st) 1392 case c `Map.lookup` constMap of 1393 -- NB. Unlike in 'newExpr', we don't have to make sure the returned sv 1394 -- has the kind we asked for, because the constMap stores the full CV 1395 -- which already has a kind field in it. 1396 Just sv -> return sv 1397 Nothing -> do (NamedSymVar sv _) <- newSV st (kindOf c) 1398 let ins = Map.insert c sv 1399 modifyState st rconstMap ins $ modifyIncState st rNewConsts ins 1400 return sv 1401{-# INLINE newConst #-} 1402 1403-- | Create a new table; hash-cons as necessary 1404getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int 1405getTableIndex st at rt elts = do 1406 let key = (at, rt, elts) 1407 tblMap <- readIORef (rtblMap st) 1408 case key `Map.lookup` tblMap of 1409 Just i -> return i 1410 _ -> do let i = Map.size tblMap 1411 upd = Map.insert key i 1412 modifyState st rtblMap upd $ modifyIncState st rNewTbls upd 1413 return i 1414 1415-- | Create a new expression; hash-cons as necessary 1416newExpr :: State -> Kind -> SBVExpr -> IO SV 1417newExpr st k app = do 1418 let e = reorder app 1419 exprMap <- readIORef (rexprMap st) 1420 case e `Map.lookup` exprMap of 1421 -- NB. Check to make sure that the kind of the hash-consed value 1422 -- is the same kind as we're requesting. This might look unnecessary, 1423 -- at first, but `svSign` and `svUnsign` rely on this as we can 1424 -- get the same expression but at a different type. See 1425 -- <http://github.com/GaloisInc/cryptol/issues/566> as an example. 1426 Just sv | kindOf sv == k -> return sv 1427 _ -> do (NamedSymVar sv _) <- newSV st k 1428 let append (SBVPgm xs) = SBVPgm (xs S.|> (sv, e)) 1429 modifyState st spgm append $ modifyIncState st rNewAsgns append 1430 modifyState st rexprMap (Map.insert e sv) (return ()) 1431 return sv 1432{-# INLINE newExpr #-} 1433 1434-- | Convert a symbolic value to an internal SV 1435svToSV :: State -> SVal -> IO SV 1436svToSV st (SVal _ (Left c)) = newConst st c 1437svToSV st (SVal _ (Right f)) = uncache f st 1438 1439-- | Generalization of 'Data.SBV.svToSymSV' 1440svToSymSV :: MonadSymbolic m => SVal -> m SV 1441svToSymSV sbv = do st <- symbolicEnv 1442 liftIO $ svToSV st sbv 1443 1444------------------------------------------------------------------------- 1445-- * Symbolic Computations 1446------------------------------------------------------------------------- 1447-- | A Symbolic computation. Represented by a reader monad carrying the 1448-- state of the computation, layered on top of IO for creating unique 1449-- references to hold onto intermediate results. 1450 1451-- | Computations which support symbolic operations 1452class MonadIO m => MonadSymbolic m where 1453 symbolicEnv :: m State 1454 1455 default symbolicEnv :: (MonadTrans t, MonadSymbolic m', m ~ t m') => m State 1456 symbolicEnv = lift symbolicEnv 1457 1458instance MonadSymbolic m => MonadSymbolic (ExceptT e m) 1459instance MonadSymbolic m => MonadSymbolic (MaybeT m) 1460instance MonadSymbolic m => MonadSymbolic (ReaderT r m) 1461instance MonadSymbolic m => MonadSymbolic (SS.StateT s m) 1462instance MonadSymbolic m => MonadSymbolic (LS.StateT s m) 1463instance (MonadSymbolic m, Monoid w) => MonadSymbolic (SW.WriterT w m) 1464instance (MonadSymbolic m, Monoid w) => MonadSymbolic (LW.WriterT w m) 1465 1466-- | A generalization of 'Data.SBV.Symbolic'. 1467newtype SymbolicT m a = SymbolicT { runSymbolicT :: ReaderT State m a } 1468 deriving ( Applicative, Functor, Monad, MonadIO, MonadTrans 1469 , MonadError e, MonadState s, MonadWriter w 1470#if MIN_VERSION_base(4,11,0) 1471 , Fail.MonadFail 1472#endif 1473 ) 1474 1475-- | `MonadSymbolic` instance for `SymbolicT m` 1476instance MonadIO m => MonadSymbolic (SymbolicT m) where 1477 symbolicEnv = SymbolicT ask 1478 1479-- | Map a computation over the symbolic transformer. 1480mapSymbolicT :: (ReaderT State m a -> ReaderT State n b) -> SymbolicT m a -> SymbolicT n b 1481mapSymbolicT f = SymbolicT . f . runSymbolicT 1482{-# INLINE mapSymbolicT #-} 1483 1484-- Have to define this one by hand, because we use ReaderT in the implementation 1485instance MonadReader r m => MonadReader r (SymbolicT m) where 1486 ask = lift ask 1487 local f = mapSymbolicT $ mapReaderT $ local f 1488 1489-- | `Symbolic` is specialization of `SymbolicT` to the `IO` monad. Unless you are using 1490-- transformers explicitly, this is the type you should prefer. 1491type Symbolic = SymbolicT IO 1492 1493-- | Create a symbolic value, based on the quantifier we have. If an 1494-- explicit quantifier is given, we just use that. If not, then we 1495-- pick the quantifier appropriately based on the run-mode. 1496-- @randomCV@ is used for generating random values for this variable 1497-- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes. 1498svMkSymVar :: VarContext -> Kind -> Maybe String -> State -> IO SVal 1499svMkSymVar = svMkSymVarGen False 1500 1501-- | Create an existentially quantified tracker variable 1502svMkTrackerVar :: Kind -> String -> State -> IO SVal 1503svMkTrackerVar k nm = svMkSymVarGen True (NonQueryVar (Just EX)) k (Just nm) 1504 1505-- | Generalization of 'Data.SBV.sWordN' 1506sWordN :: MonadSymbolic m => Int -> String -> m SVal 1507sWordN w nm = symbolicEnv >>= liftIO . svMkSymVar (NonQueryVar Nothing) (KBounded False w) (Just nm) 1508 1509-- | Generalization of 'Data.SBV.sWordN_' 1510sWordN_ :: MonadSymbolic m => Int -> m SVal 1511sWordN_ w = symbolicEnv >>= liftIO . svMkSymVar (NonQueryVar Nothing) (KBounded False w) Nothing 1512 1513-- | Generalization of 'Data.SBV.sIntN' 1514sIntN :: MonadSymbolic m => Int -> String -> m SVal 1515sIntN w nm = symbolicEnv >>= liftIO . svMkSymVar (NonQueryVar Nothing) (KBounded True w) (Just nm) 1516 1517-- | Generalization of 'Data.SBV.sIntN_' 1518sIntN_ :: MonadSymbolic m => Int -> m SVal 1519sIntN_ w = symbolicEnv >>= liftIO . svMkSymVar (NonQueryVar Nothing) (KBounded True w) Nothing 1520 1521-- | Create a symbolic value, based on the quantifier we have. If an 1522-- explicit quantifier is given, we just use that. If not, then we 1523-- pick the quantifier appropriately based on the run-mode. 1524-- @randomCV@ is used for generating random values for this variable 1525-- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes. 1526svMkSymVarGen :: Bool -> VarContext -> Kind -> Maybe String -> State -> IO SVal 1527svMkSymVarGen isTracker varContext k mbNm st = do 1528 rm <- readIORef (runMode st) 1529 1530 let varInfo = case mbNm of 1531 Nothing -> ", of type " ++ show k 1532 Just nm -> ", while defining " ++ nm ++ " :: " ++ show k 1533 1534 disallow what = error $ "Data.SBV: Unsupported: " ++ what ++ varInfo ++ " in mode: " ++ show rm 1535 1536 noUI cont 1537 | isUserSort k = disallow "User defined sorts" 1538 | True = cont 1539 1540 (isQueryVar, mbQ) = case varContext of 1541 NonQueryVar mq -> (False, mq) 1542 QueryVar -> (True, Just EX) 1543 1544 mkS q = do (NamedSymVar sv internalName) <- newSV st k 1545 let nm = fromMaybe (T.unpack internalName) mbNm 1546 introduceUserName st (isQueryVar, isTracker) nm k q sv 1547 1548 mkC cv = do registerKind st k 1549 modifyState st rCInfo ((fromMaybe "_" mbNm, cv):) (return ()) 1550 return $ SVal k (Left cv) 1551 1552 case (mbQ, rm) of 1553 (Just q, SMTMode{} ) -> mkS q 1554 (Nothing, SMTMode _ _ isSAT _) -> mkS (if isSAT then EX else ALL) 1555 1556 (Just EX, CodeGen{}) -> disallow "Existentially quantified variables" 1557 (_ , CodeGen) -> noUI $ mkS ALL -- code generation, pick universal 1558 1559 (Just EX, Concrete Nothing) -> disallow "Existentially quantified variables" 1560 (_ , Concrete Nothing) -> noUI (randomCV k >>= mkC) 1561 1562 -- Model validation: 1563 (_ , Concrete (Just (_isSat, env))) -> do 1564 let bad why conc = error $ unlines [ "" 1565 , "*** Data.SBV: " ++ why 1566 , "***" 1567 , "*** To turn validation off, use `cfg{validateModel = False}`" 1568 , "***" 1569 , "*** " ++ conc 1570 ] 1571 1572 cant = "Validation engine is not capable of handling this case. Failed to validate." 1573 report = "Please report this as a bug in SBV!" 1574 1575 case () of 1576 () | isUserSort k -> bad ("Cannot validate models in the presence of user defined kinds, saw: " ++ show k) cant 1577 1578 _ -> do (NamedSymVar sv internalName) <- newSV st k 1579 1580 let nm = fromMaybe (T.unpack internalName) mbNm 1581 nsv = toNamedSV' sv nm 1582 1583 cv = case [(q, v) | ((q, nsv'), v) <- env, nsv == nsv'] of 1584 [] -> if isTracker 1585 then -- The sole purpose of a tracker variable is to send the optimization 1586 -- directive to the solver, so we can name "expressions" that are minimized 1587 -- or maximized. There will be no constraints on these when we are doing 1588 -- the validation; in fact they will not even be used anywhere during a 1589 -- validation run. So, simply push a zero value that inhabits all metrics. 1590 mkConstCV k (0::Integer) 1591 else bad ("Cannot locate variable: " ++ show (nsv, k)) report 1592 [(ALL, _)] -> -- We can stop here, as we can't really validate in the presence of a universal quantifier: 1593 -- we'd have to validate for each possible value. But that's more or less useless. Instead, 1594 -- just issue a warning and use 0 for this value. 1595 mkConstCV k (0::Integer) 1596 [(EX, Nothing)] -> bad ("Cannot locate model value of variable: " ++ show (getUserName' nsv)) report 1597 [(EX, Just c)] -> c 1598 r -> bad ( "Found multiple matching values for variable: " ++ show nsv 1599 ++ "\n*** " ++ show r) report 1600 1601 mkC cv 1602 1603-- | Introduce a new user name. We simply append a suffix if we have seen this variable before. 1604introduceUserName :: State -> (Bool, Bool) -> String -> Kind -> Quantifier -> SV -> IO SVal 1605introduceUserName st@State{runMode} (isQueryVar, isTracker) nmOrig k q sv = do 1606 old <- allInputs <$> readIORef (rinps st) 1607 1608 let nm = mkUnique (T.pack nmOrig) old 1609 1610 -- If this is not a query variable and we're in a query, reject it. 1611 -- See https://github.com/LeventErkok/sbv/issues/554 for the rationale. 1612 -- In theory, it should be possible to support this, but fixing it is 1613 -- rather costly as we'd have to track the regular updates and sync the 1614 -- incremental state appropriately. Instead, we issue an error message 1615 -- and ask the user to obey the query mode rules. 1616 rm <- readIORef runMode 1617 case rm of 1618 SMTMode _ IRun _ _ | not isQueryVar -> noInteractiveEver [ "Adding a new input variable in query mode: " ++ show nm 1619 , "" 1620 , "Hint: Use freshVar/freshVar_ for introducing new inputs in query mode." 1621 ] 1622 _ -> pure () 1623 1624 if isTracker && q == ALL 1625 then error $ "SBV: Impossible happened! A universally quantified tracker variable is being introduced: " ++ show nm 1626 else do let newInp olds = case q of 1627 EX -> toNamedSV sv nm : olds 1628 ALL -> noInteractive [ "Adding a new universally quantified variable: " 1629 , " Name : " ++ show nm 1630 , " Kind : " ++ show k 1631 , " Quantifier: Universal" 1632 , " Node : " ++ show sv 1633 , "Only existential variables are supported in query mode." 1634 ] 1635 if isTracker 1636 then modifyState st rinps (addInternInput sv nm) 1637 $ noInteractive ["Adding a new tracker variable in interactive mode: " ++ show nm] 1638 else modifyState st rinps (addUserInput q sv nm) 1639 $ modifyIncState st rNewInps newInp 1640 return $ SVal k $ Right $ cache (const (return sv)) 1641 1642 where -- The following can be rather slow if we keep reusing the same prefix, but I doubt it'll be a problem in practice 1643 -- Also, the following will fail if we span the range of integers without finding a match, but your computer would 1644 -- die way ahead of that happening if that's the case! 1645 mkUnique :: T.Text -> Set.Set Name -> T.Text 1646 mkUnique prefix names = head $ dropWhile (`Set.member` names) (prefix : [prefix <> "_" <> T.pack (show i) | i <- [(0::Int)..]]) 1647 1648-- | Generalization of 'Data.SBV.runSymbolic' 1649runSymbolic :: MonadIO m => SBVRunMode -> SymbolicT m a -> m (a, Result) 1650runSymbolic currentRunMode (SymbolicT c) = do 1651 st <- liftIO $ do 1652 currTime <- getCurrentTime 1653 rm <- newIORef currentRunMode 1654 ctr <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements 1655 cInfo <- newIORef [] 1656 observes <- newIORef mempty 1657 pgm <- newIORef (SBVPgm S.empty) 1658 emap <- newIORef Map.empty 1659 cmap <- newIORef Map.empty 1660 inps <- newIORef mempty 1661 outs <- newIORef [] 1662 tables <- newIORef Map.empty 1663 arrays <- newIORef IMap.empty 1664 fArrays <- newIORef IMap.empty 1665 uis <- newIORef Map.empty 1666 cgs <- newIORef Map.empty 1667 axioms <- newIORef [] 1668 swCache <- newIORef IMap.empty 1669 aiCache <- newIORef IMap.empty 1670 faiCache <- newIORef IMap.empty 1671 usedKinds <- newIORef Set.empty 1672 usedLbls <- newIORef Set.empty 1673 cstrs <- newIORef S.empty 1674 smtOpts <- newIORef [] 1675 optGoals <- newIORef [] 1676 asserts <- newIORef [] 1677 istate <- newIORef =<< newIncState 1678 qstate <- newIORef Nothing 1679 pure $ State { runMode = rm 1680 , startTime = currTime 1681 , pathCond = SVal KBool (Left trueCV) 1682 , rIncState = istate 1683 , rCInfo = cInfo 1684 , rObservables = observes 1685 , rctr = ctr 1686 , rUsedKinds = usedKinds 1687 , rUsedLbls = usedLbls 1688 , rinps = inps 1689 , routs = outs 1690 , rtblMap = tables 1691 , spgm = pgm 1692 , rconstMap = cmap 1693 , rArrayMap = arrays 1694 , rFArrayMap = fArrays 1695 , rexprMap = emap 1696 , rUIMap = uis 1697 , rCgMap = cgs 1698 , raxioms = axioms 1699 , rSVCache = swCache 1700 , rAICache = aiCache 1701 , rFAICache = faiCache 1702 , rConstraints = cstrs 1703 , rSMTOptions = smtOpts 1704 , rOptGoals = optGoals 1705 , rAsserts = asserts 1706 , rQueryState = qstate 1707 } 1708 _ <- liftIO $ newConst st falseCV -- s(-2) == falseSV 1709 _ <- liftIO $ newConst st trueCV -- s(-1) == trueSV 1710 r <- runReaderT c st 1711 res <- liftIO $ extractSymbolicSimulationState st 1712 1713 -- Clean-up after ourselves 1714 qs <- liftIO $ readIORef $ rQueryState st 1715 case qs of 1716 Nothing -> return () 1717 Just QueryState{queryTerminate} -> liftIO queryTerminate 1718 1719 return (r, res) 1720 1721-- | Grab the program from a running symbolic simulation state. 1722extractSymbolicSimulationState :: State -> IO Result 1723extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblMap=tables, rArrayMap=arrays, rUIMap=uis, raxioms=axioms 1724 , rAsserts=asserts, rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints=cstrs 1725 , rObservables=observes 1726 } = do 1727 SBVPgm rpgm <- readIORef pgm 1728 inpsO <- inputsToList <$> readIORef inps 1729 outsO <- reverse <$> readIORef outs 1730 1731 let swap (a, b) = (b, a) 1732 cmp (a, _) (b, _) = a `compare` b 1733 arrange (i, (at, rt, es)) = ((i, at, rt), es) 1734 1735 constMap <- readIORef (rconstMap st) 1736 let cnsts = sortBy cmp . map swap . Map.toList $ constMap 1737 1738 tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef tables 1739 arrs <- IMap.toAscList <$> readIORef arrays 1740 unint <- Map.toList <$> readIORef uis 1741 axs <- reverse <$> readIORef axioms 1742 knds <- readIORef usedKinds 1743 cgMap <- Map.toList <$> readIORef cgs 1744 1745 traceVals <- reverse <$> readIORef cInfo 1746 observables <- reverse . fmap (\(n,f,sv) -> (T.unpack n, f, sv)) . F.toList 1747 <$> readIORef observes 1748 extraCstrs <- readIORef cstrs 1749 assertions <- reverse <$> readIORef asserts 1750 1751 return $ Result knds traceVals observables cgMap inpsO (constMap, cnsts) tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO 1752 1753-- | Generalization of 'Data.SBV.addNewSMTOption' 1754addNewSMTOption :: MonadSymbolic m => SMTOption -> m () 1755addNewSMTOption o = do st <- symbolicEnv 1756 liftIO $ modifyState st rSMTOptions (o:) (return ()) 1757 1758-- | Generalization of 'Data.SBV.imposeConstraint' 1759imposeConstraint :: MonadSymbolic m => Bool -> [(String, String)] -> SVal -> m () 1760imposeConstraint isSoft attrs c = do st <- symbolicEnv 1761 rm <- liftIO $ readIORef (runMode st) 1762 1763 case rm of 1764 CodeGen -> error "SBV: constraints are not allowed in code-generation" 1765 _ -> liftIO $ do mapM_ (registerLabel "Constraint" st) [nm | (":named", nm) <- attrs] 1766 internalConstraint st isSoft attrs c 1767 1768-- | Require a boolean condition to be true in the state. Only used for internal purposes. 1769internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO () 1770internalConstraint st isSoft attrs b = do v <- svToSV st b 1771 1772 rm <- liftIO $ readIORef (runMode st) 1773 1774 -- Are we running validation? If so, we always want to 1775 -- add the constraint for debug purposes. Otherwie 1776 -- we only add it if it's interesting; i.e., not directly 1777 -- true or has some attributes. 1778 let isValidating = case rm of 1779 SMTMode _ _ _ cfg -> validationRequested cfg 1780 CodeGen -> False 1781 Concrete Nothing -> False 1782 Concrete (Just _) -> True -- The case when we *are* running the validation 1783 1784 let c = (isSoft, attrs, v) 1785 interesting = v /= trueSV || not (null attrs) 1786 1787 when (isValidating || interesting) $ 1788 modifyState st rConstraints (S.|> c) 1789 $ modifyIncState st rNewConstraints (S.|> c) 1790 1791-- | Generalization of 'Data.SBV.addSValOptGoal' 1792addSValOptGoal :: MonadSymbolic m => Objective SVal -> m () 1793addSValOptGoal obj = do st <- symbolicEnv 1794 1795 -- create the tracking variable here for the metric 1796 let mkGoal nm orig = liftIO $ do origSV <- svToSV st orig 1797 track <- svMkTrackerVar (kindOf orig) nm st 1798 trackSV <- svToSV st track 1799 return (origSV, trackSV) 1800 1801 let walk (Minimize nm v) = Minimize nm <$> mkGoal nm v 1802 walk (Maximize nm v) = Maximize nm <$> mkGoal nm v 1803 walk (AssertWithPenalty nm v mbP) = flip (AssertWithPenalty nm) mbP <$> mkGoal nm v 1804 1805 !obj' <- walk obj 1806 liftIO $ modifyState st rOptGoals (obj' :) 1807 $ noInteractive [ "Adding an optimization objective:" 1808 , " Objective: " ++ show obj 1809 ] 1810 1811-- | Generalization of 'Data.SBV.outputSVal' 1812outputSVal :: MonadSymbolic m => SVal -> m () 1813outputSVal (SVal _ (Left c)) = do 1814 st <- symbolicEnv 1815 sv <- liftIO $ newConst st c 1816 liftIO $ modifyState st routs (sv:) (return ()) 1817outputSVal (SVal _ (Right f)) = do 1818 st <- symbolicEnv 1819 sv <- liftIO $ uncache f st 1820 liftIO $ modifyState st routs (sv:) (return ()) 1821 1822--------------------------------------------------------------------------------- 1823-- * Cached values 1824--------------------------------------------------------------------------------- 1825 1826-- | We implement a peculiar caching mechanism, applicable to the use case in 1827-- implementation of SBV's. Whenever we do a state based computation, we do 1828-- not want to keep on evaluating it in the then-current state. That will 1829-- produce essentially a semantically equivalent value. Thus, we want to run 1830-- it only once, and reuse that result, capturing the sharing at the Haskell 1831-- level. This is similar to the "type-safe observable sharing" work, but also 1832-- takes into the account of how symbolic simulation executes. 1833-- 1834-- See Andy Gill's type-safe observable sharing trick for the inspiration behind 1835-- this technique: <http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf> 1836-- 1837-- Note that this is *not* a general memo utility! 1838newtype Cached a = Cached (State -> IO a) 1839 1840-- | Cache a state-based computation 1841cache :: (State -> IO a) -> Cached a 1842cache = Cached 1843 1844-- | Uncache a previously cached computation 1845uncache :: Cached SV -> State -> IO SV 1846uncache = uncacheGen rSVCache 1847 1848-- | An SMT array index is simply an int value 1849newtype ArrayIndex = ArrayIndex { unArrayIndex :: Int } deriving (Eq, Ord, G.Data) 1850 1851-- | We simply show indexes as the underlying integer 1852instance Show ArrayIndex where 1853 show (ArrayIndex i) = show i 1854 1855-- | A functional array index is simply an int value 1856newtype FArrayIndex = FArrayIndex { unFArrayIndex :: Int } deriving (Eq, Ord) 1857 1858-- | We simply show indexes as the underlying integer 1859instance Show FArrayIndex where 1860 show (FArrayIndex i) = show i 1861 1862-- | Uncache, retrieving SMT array indexes 1863uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex 1864uncacheAI = uncacheGen rAICache 1865 1866-- | Uncache, retrieving Functional array indexes 1867uncacheFAI :: Cached FArrayIndex -> State -> IO FArrayIndex 1868uncacheFAI = uncacheGen rFAICache 1869 1870-- | Generic uncaching. Note that this is entirely safe, since we do it in the IO monad. 1871uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a 1872uncacheGen getCache (Cached f) st = do 1873 let rCache = getCache st 1874 stored <- readIORef rCache 1875 sn <- f `seq` makeStableName f 1876 let h = hashStableName sn 1877 case (h `IMap.lookup` stored) >>= (sn `lookup`) of 1878 Just r -> return r 1879 Nothing -> do r <- f st 1880 r `seq` R.modifyIORef' rCache (IMap.insertWith (++) h [(sn, r)]) 1881 return r 1882 1883-- | Representation of SMTLib Program versions. As of June 2015, we're dropping support 1884-- for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case 1885-- SMTLib3 comes along and we want to support 2 and 3 simultaneously. 1886data SMTLibVersion = SMTLib2 1887 deriving (Bounded, Enum, Eq, Show) 1888 1889-- | The extension associated with the version 1890smtLibVersionExtension :: SMTLibVersion -> String 1891smtLibVersionExtension SMTLib2 = "smt2" 1892 1893-- | Representation of an SMT-Lib program. In between pre and post goes the refuted models 1894data SMTLibPgm = SMTLibPgm SMTLibVersion [String] 1895 1896instance NFData SMTLibVersion where rnf a = a `seq` () 1897instance NFData SMTLibPgm where rnf (SMTLibPgm v p) = rnf v `seq` rnf p 1898 1899instance Show SMTLibPgm where 1900 show (SMTLibPgm _ pre) = intercalate "\n" pre 1901 1902-- Other Technicalities.. 1903instance NFData CV where 1904 rnf (CV x y) = x `seq` y `seq` () 1905 1906instance NFData GeneralizedCV where 1907 rnf (ExtendedCV e) = e `seq` () 1908 rnf (RegularCV c) = c `seq` () 1909 1910#if MIN_VERSION_base(4,9,0) 1911#else 1912-- Can't really force this, but not a big deal 1913instance NFData CallStack where 1914 rnf _ = () 1915#endif 1916 1917instance NFData NamedSymVar where 1918 rnf (NamedSymVar s n) = rnf s `seq` rnf n 1919 1920instance NFData Result where 1921 rnf (Result kindInfo qcInfo obs cgs inps consts tbls arrs uis axs pgm cstr asserts outs) 1922 = rnf kindInfo `seq` rnf qcInfo `seq` rnf obs `seq` rnf cgs 1923 `seq` rnf inps `seq` rnf consts `seq` rnf tbls 1924 `seq` rnf arrs `seq` rnf uis `seq` rnf axs 1925 `seq` rnf pgm `seq` rnf cstr `seq` rnf asserts 1926 `seq` rnf outs 1927instance NFData Kind where rnf a = seq a () 1928instance NFData ArrayContext where rnf a = seq a () 1929instance NFData SV where rnf a = seq a () 1930instance NFData SBVExpr where rnf a = seq a () 1931instance NFData Quantifier where rnf a = seq a () 1932instance NFData SBVType where rnf a = seq a () 1933instance NFData SBVPgm where rnf a = seq a () 1934instance NFData (Cached a) where rnf (Cached f) = f `seq` () 1935instance NFData SVal where rnf (SVal x y) = rnf x `seq` rnf y 1936 1937instance NFData SMTResult where 1938 rnf (Unsatisfiable _ m ) = rnf m 1939 rnf (Satisfiable _ m ) = rnf m 1940 rnf (DeltaSat _ p m ) = rnf m `seq` rnf p 1941 rnf (SatExtField _ m ) = rnf m 1942 rnf (Unknown _ m ) = rnf m 1943 rnf (ProofError _ m mr) = rnf m `seq` rnf mr 1944 1945instance NFData SMTModel where 1946 rnf (SMTModel objs bndgs assocs uifuns) = rnf objs `seq` rnf bndgs `seq` rnf assocs `seq` rnf uifuns 1947 1948instance NFData SMTScript where 1949 rnf (SMTScript b m) = rnf b `seq` rnf m 1950 1951-- | Translation tricks needed for specific capabilities afforded by each solver 1952data SolverCapabilities = SolverCapabilities { 1953 supportsQuantifiers :: Bool -- ^ Supports SMT-Lib2 style quantifiers? 1954 , supportsDefineFun :: Bool -- ^ Supports define-fun construct? 1955 , supportsDistinct :: Bool -- ^ Supports calls to distinct? 1956 , supportsBitVectors :: Bool -- ^ Supports bit-vectors? 1957 , supportsUninterpretedSorts :: Bool -- ^ Supports SMT-Lib2 style uninterpreted-sorts 1958 , supportsUnboundedInts :: Bool -- ^ Supports unbounded integers? 1959 , supportsInt2bv :: Bool -- ^ Supports int2bv? 1960 , supportsReals :: Bool -- ^ Supports reals? 1961 , supportsApproxReals :: Bool -- ^ Supports printing of approximations of reals? 1962 , supportsDeltaSat :: Maybe String -- ^ Supports delta-satisfiability? (With given precision query) 1963 , supportsIEEE754 :: Bool -- ^ Supports floating point numbers? 1964 , supportsSets :: Bool -- ^ Supports set operations? 1965 , supportsOptimization :: Bool -- ^ Supports optimization routines? 1966 , supportsPseudoBooleans :: Bool -- ^ Supports pseudo-boolean operations? 1967 , supportsCustomQueries :: Bool -- ^ Supports interactive queries per SMT-Lib? 1968 , supportsGlobalDecls :: Bool -- ^ Supports global declarations? (Needed for push-pop.) 1969 , supportsDataTypes :: Bool -- ^ Supports datatypes? 1970 , supportsDirectAccessors :: Bool -- ^ Supports data-type accessors without full ascription? 1971 , supportsFlattenedModels :: Maybe [String] -- ^ Supports flattened model output? (With given config lines.) 1972 } 1973 1974-- | Solver configuration. See also 'Data.SBV.z3', 'Data.SBV.yices', 'Data.SBV.cvc4', 'Data.SBV.boolector', 'Data.SBV.mathSAT', etc. 1975-- which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be 1976-- created by varying those values. (Such as @z3{verbose=True}@.) 1977-- 1978-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does 1979-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to 1980-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite 1981-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after 1982-- the decimal point. The default value is 16, but it can be set to any positive integer. 1983-- 1984-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value 1985-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it 1986-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation 1987-- of the real value is not finite, i.e., if it is not rational. 1988-- 1989-- The 'printBase' field can be used to print numbers in base 2, 10, or 16. 1990-- 1991-- The 'crackNum' field can be used to display numbers in detail, all its bits and how they are laid out in memory. Works with all bounded number types 1992-- (i.e., SWord and SInt), but also with floats. It is particularly useful with floating-point numbers, as it shows you how they are laid out in 1993-- memory following the IEEE754 rules. 1994data SMTConfig = SMTConfig { 1995 verbose :: Bool -- ^ Debug mode 1996 , timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.) 1997 , printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.) 1998 , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) 1999 , crackNum :: Bool -- ^ For each numeric value, show it in detail in the model with its bits spliced out. Good for floats. 2000 , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. 2001 , allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all. 2002 , allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found. 2003 , satTrackUFs :: Bool -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions? 2004 , isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) 2005 , validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver. 2006 , optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints. 2007 , transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly) 2008 , smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool 2009 , dsatPrecision :: Maybe Double -- ^ Delta-sat precision 2010 , solver :: SMTSolver -- ^ The actual SMT solver. 2011 , extraArgs :: [String] -- ^ Extra command line arguments to pass to the solver. 2012 , allowQuantifiedQueries :: Bool -- ^ Should we permit use of quantifiers in the query mode? (Default: False. See <http://github.com/LeventErkok/sbv/issues/459> for why.) 2013 , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions 2014 , solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver 2015 , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess. 2016 , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied. 2017 } 2018 2019-- | We show the name of the solver for the config. Arguably this is misleading, but better than nothing. 2020instance Show SMTConfig where 2021 show = show . name . solver 2022 2023-- | Returns true if we have to perform validation 2024validationRequested :: SMTConfig -> Bool 2025validationRequested SMTConfig{validateModel, optimizeValidateConstraints} = validateModel || optimizeValidateConstraints 2026 2027-- We're just seq'ing top-level here, it shouldn't really matter. (i.e., no need to go deeper.) 2028instance NFData SMTConfig where 2029 rnf SMTConfig{} = () 2030 2031-- | A model, as returned by a solver 2032data SMTModel = SMTModel { 2033 modelObjectives :: [(String, GeneralizedCV)] -- ^ Mapping of symbolic values to objective values. 2034 , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)] -- ^ Mapping of input variables as reported by the solver. Only collected if model validation is requested. 2035 , modelAssocs :: [(String, CV)] -- ^ Mapping of symbolic values to constants. 2036 , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))] -- ^ Mapping of uninterpreted functions to association lists in the model. 2037 -- Note that an uninterpreted constant (function of arity 0) will be stored 2038 -- in the 'modelAssocs' field. 2039 } 2040 deriving Show 2041 2042-- | The result of an SMT solver call. Each constructor is tagged with 2043-- the 'SMTConfig' that created it so that further tools can inspect it 2044-- and build layers of results, if needed. For ordinary uses of the library, 2045-- this type should not be needed, instead use the accessor functions on 2046-- it. (Custom Show instances and model extractors.) 2047data SMTResult = Unsatisfiable SMTConfig (Maybe [String]) -- ^ Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter. 2048 | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model 2049 | DeltaSat SMTConfig (Maybe String) SMTModel -- ^ Delta satisfiable with queried string if available and model 2050 | SatExtField SMTConfig SMTModel -- ^ Prover returned a model, but in an extension field containing Infinite/epsilon 2051 | Unknown SMTConfig SMTReasonUnknown -- ^ Prover returned unknown, with the given reason 2052 | ProofError SMTConfig [String] (Maybe SMTResult) -- ^ Prover errored out, with possibly a bogus result 2053 2054-- | A script, to be passed to the solver. 2055data SMTScript = SMTScript { 2056 scriptBody :: String -- ^ Initial feed 2057 , scriptModel :: [String] -- ^ Continuation script, to extract results 2058 } 2059 2060-- | An SMT engine 2061type SMTEngine = forall res. 2062 SMTConfig -- ^ current configuration 2063 -> State -- ^ the state in which to run the engine 2064 -> String -- ^ program 2065 -> (State -> IO res) -- ^ continuation 2066 -> IO res 2067 2068-- | Solvers that SBV is aware of 2069data Solver = ABC 2070 | Boolector 2071 | CVC4 2072 | DReal 2073 | MathSAT 2074 | Yices 2075 | Z3 2076 deriving (Show, Enum, Bounded) 2077 2078-- | An SMT solver 2079data SMTSolver = SMTSolver { 2080 name :: Solver -- ^ The solver in use 2081 , executable :: String -- ^ The path to its executable 2082 , preprocess :: String -> String -- ^ Each line sent to the solver will be passed through this function (typically id) 2083 , options :: SMTConfig -> [String] -- ^ Options to provide to the solver 2084 , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output 2085 , capabilities :: SolverCapabilities -- ^ Various capabilities of the solver 2086 } 2087 2088-- | Query execution context 2089data QueryContext = QueryInternal -- ^ Triggered from inside SBV 2090 | QueryExternal -- ^ Triggered from user code 2091 2092-- | Show instance for 'QueryContext', for debugging purposes 2093instance Show QueryContext where 2094 show QueryInternal = "Internal Query" 2095 show QueryExternal = "User Query" 2096 2097{-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-} 2098{-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-} 2099{-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-} 2100{-# ANN type NROp ("HLint: ignore Use camelCase" :: String) #-} 2101