1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Core.Data 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Internal data-structures for the sbv library 10----------------------------------------------------------------------------- 11 12{-# LANGUAGE CPP #-} 13{-# LANGUAGE DataKinds #-} 14{-# LANGUAGE DefaultSignatures #-} 15{-# LANGUAGE DeriveAnyClass #-} 16{-# LANGUAGE DeriveGeneric #-} 17{-# LANGUAGE FlexibleContexts #-} 18{-# LANGUAGE FlexibleInstances #-} 19{-# LANGUAGE InstanceSigs #-} 20{-# LANGUAGE MultiParamTypeClasses #-} 21{-# LANGUAGE PatternGuards #-} 22{-# LANGUAGE ScopedTypeVariables #-} 23{-# LANGUAGE TypeApplications #-} 24{-# LANGUAGE TypeFamilies #-} 25 26{-# OPTIONS_GHC -Wall -Werror #-} 27 28module Data.SBV.Core.Data 29 ( SBool, SWord8, SWord16, SWord32, SWord64 30 , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble 31 , SFloatingPoint, SFPHalf, SFPSingle, SFPDouble, SFPQuad 32 , SChar, SString, SList 33 , SEither, SMaybe 34 , STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8 35 , RCSet(..), SSet 36 , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode 37 , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero 38 , sRNE, sRNA, sRTP, sRTN, sRTZ 39 , SymVal(..) 40 , CV(..), CVal(..), AlgReal(..), AlgRealPoly(..), ExtCV(..), GeneralizedCV(..), isRegularCV, cvSameType, cvToBool 41 , mkConstCV ,liftCV2, mapCV, mapCV2 42 , SV(..), trueSV, falseSV, trueCV, falseCV, normCV 43 , SVal(..) 44 , sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), sAnd, sOr, sAny, sAll, fromBool 45 , SBV(..), NodeId(..), mkSymSBV 46 , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), SArray(..) 47 , sbvToSV, sbvToSymSV, forceSVArg 48 , SBVExpr(..), newExpr 49 , cache, Cached, uncache, uncacheAI, HasKind(..) 50 , Op(..), PBOp(..), FPOp(..), StrOp(..), SeqOp(..), RegExp(..), NamedSymVar(..), getTableIndex 51 , SBVPgm(..), Symbolic, runSymbolic, State, getPathCondition, extendPathCondition 52 , inSMTMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) 53 , SolverContext(..), internalVariable, internalConstraint, isCodeGenMode 54 , SBVType(..), newUninterpreted 55 , Quantifier(..), needsExistentials 56 , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension, smtLibReservedNames 57 , SolverCapabilities(..) 58 , extractSymbolicSimulationState 59 , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..) 60 , OptimizeStyle(..), Penalty(..), Objective(..) 61 , QueryState(..), QueryT(..), SMTProblem(..) 62 ) where 63 64import GHC.TypeLits 65 66import GHC.Generics (Generic) 67import GHC.Exts (IsList(..)) 68 69import Control.DeepSeq (NFData(..)) 70import Control.Monad.Trans (liftIO) 71import Data.Int (Int8, Int16, Int32, Int64) 72import Data.Word (Word8, Word16, Word32, Word64) 73import Data.List (elemIndex) 74import Data.Maybe (fromMaybe) 75 76import Data.Proxy 77import Data.Typeable (Typeable) 78 79import qualified Data.Generics as G (Data(..)) 80 81import qualified Data.IORef as R (readIORef, newIORef) 82import qualified Data.IntMap.Strict as IMap (size, insert, empty) 83 84import System.Random 85 86import Data.SBV.Core.AlgReals 87import Data.SBV.Core.SizedFloats 88import Data.SBV.Core.Kind 89import Data.SBV.Core.Concrete 90import Data.SBV.Core.Symbolic 91import Data.SBV.Core.Operations 92 93import Data.SBV.Control.Types 94 95import Data.SBV.SMT.SMTLibNames 96 97import Data.SBV.Utils.Lib 98 99-- | Get the current path condition 100getPathCondition :: State -> SBool 101getPathCondition st = SBV (getSValPathCondition st) 102 103-- | Extend the path condition with the given test value. 104extendPathCondition :: State -> (SBool -> SBool) -> State 105extendPathCondition st f = extendSValPathCondition st (unSBV . f . SBV) 106 107-- | The "Symbolic" value. The parameter @a@ is phantom, but is 108-- extremely important in keeping the user interface strongly typed. 109newtype SBV a = SBV { unSBV :: SVal } 110 deriving (Generic, NFData) 111 112-- | A symbolic boolean/bit 113type SBool = SBV Bool 114 115-- | 8-bit unsigned symbolic value 116type SWord8 = SBV Word8 117 118-- | 16-bit unsigned symbolic value 119type SWord16 = SBV Word16 120 121-- | 32-bit unsigned symbolic value 122type SWord32 = SBV Word32 123 124-- | 64-bit unsigned symbolic value 125type SWord64 = SBV Word64 126 127-- | 8-bit signed symbolic value, 2's complement representation 128type SInt8 = SBV Int8 129 130-- | 16-bit signed symbolic value, 2's complement representation 131type SInt16 = SBV Int16 132 133-- | 32-bit signed symbolic value, 2's complement representation 134type SInt32 = SBV Int32 135 136-- | 64-bit signed symbolic value, 2's complement representation 137type SInt64 = SBV Int64 138 139-- | Infinite precision signed symbolic value 140type SInteger = SBV Integer 141 142-- | Infinite precision symbolic algebraic real value 143type SReal = SBV AlgReal 144 145-- | IEEE-754 single-precision floating point numbers 146type SFloat = SBV Float 147 148-- | IEEE-754 double-precision floating point numbers 149type SDouble = SBV Double 150 151-- | A symbolic arbitrary precision floating point value 152type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb) 153 154-- | A symbolic half-precision float 155type SFPHalf = SBV FPHalf 156 157-- | A symbolic single-precision float 158type SFPSingle = SBV FPSingle 159 160-- | A symbolic double-precision float 161type SFPDouble = SBV FPDouble 162 163-- | A symbolic quad-precision float 164type SFPQuad = SBV FPQuad 165 166-- | A symbolic character. Note that this is the full unicode character set. 167-- see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml> 168-- for details. 169type SChar = SBV Char 170 171-- | A symbolic string. Note that a symbolic string is /not/ a list of symbolic characters, 172-- that is, it is not the case that @SString = [SChar]@, unlike what one might expect following 173-- Haskell strings. An 'SString' is a symbolic value of its own, of possibly arbitrary but finite length, 174-- and internally processed as one unit as opposed to a fixed-length list of characters. 175type SString = SBV String 176 177-- | A symbolic list of items. Note that a symbolic list is /not/ a list of symbolic items, 178-- that is, it is not the case that @SList a = [a]@, unlike what one might expect following 179-- haskell lists\/sequences. An 'SList' is a symbolic value of its own, of possibly arbitrary but finite 180-- length, and internally processed as one unit as opposed to a fixed-length list of items. 181-- Note that lists can be nested, i.e., we do allow lists of lists of ... items. 182type SList a = SBV [a] 183 184-- | Symbolic 'Either' 185type SEither a b = SBV (Either a b) 186 187-- | Symbolic 'Maybe' 188type SMaybe a = SBV (Maybe a) 189 190-- | Symbolic 'Data.Set'. Note that we use 'RCSet', which supports 191-- both regular sets and complements, i.e., those obtained from the 192-- universal set (of the right type) by removing elements. 193type SSet a = SBV (RCSet a) 194 195-- | Symbolic 2-tuple. NB. 'STuple' and 'STuple2' are equivalent. 196type STuple a b = SBV (a, b) 197 198-- | Symbolic 2-tuple. NB. 'STuple' and 'STuple2' are equivalent. 199type STuple2 a b = SBV (a, b) 200 201-- | Symbolic 3-tuple. 202type STuple3 a b c = SBV (a, b, c) 203 204-- | Symbolic 4-tuple. 205type STuple4 a b c d = SBV (a, b, c, d) 206 207-- | Symbolic 5-tuple. 208type STuple5 a b c d e = SBV (a, b, c, d, e) 209 210-- | Symbolic 6-tuple. 211type STuple6 a b c d e f = SBV (a, b, c, d, e, f) 212 213-- | Symbolic 7-tuple. 214type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g) 215 216-- | Symbolic 8-tuple. 217type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h) 218 219-- | IsList instance allows list literals to be written compactly. 220instance SymVal [a] => IsList (SList a) where 221 type Item (SList a) = a 222 fromList = literal 223 toList x = fromMaybe (error "IsList.toList used in a symbolic context!") (unliteral x) 224 225-- | Not-A-Number for 'Double' and 'Float'. Surprisingly, Haskell 226-- Prelude doesn't have this value defined, so we provide it here. 227nan :: Floating a => a 228nan = 0/0 229 230-- | Infinity for 'Double' and 'Float'. Surprisingly, Haskell 231-- Prelude doesn't have this value defined, so we provide it here. 232infinity :: Floating a => a 233infinity = 1/0 234 235-- | Symbolic variant of Not-A-Number. This value will inhabit 236-- 'SFloat', 'SDouble' and 'SFloatingPoint'. types. 237sNaN :: (Floating a, SymVal a) => SBV a 238sNaN = literal nan 239 240-- | Symbolic variant of infinity. This value will inhabit both 241-- 'SFloat', 'SDouble' and 'SFloatingPoint'. types. 242sInfinity :: (Floating a, SymVal a) => SBV a 243sInfinity = literal infinity 244 245-- | Internal representation of a symbolic simulation result 246newtype SMTProblem = SMTProblem {smtLibPgm :: SMTConfig -> SMTLibPgm} -- ^ SMTLib representation, given the config 247 248-- | Symbolic 'True' 249sTrue :: SBool 250sTrue = SBV (svBool True) 251 252-- | Symbolic 'False' 253sFalse :: SBool 254sFalse = SBV (svBool False) 255 256-- | Symbolic boolean negation 257sNot :: SBool -> SBool 258sNot (SBV b) = SBV (svNot b) 259 260-- | Symbolic conjunction 261infixr 3 .&& 262(.&&) :: SBool -> SBool -> SBool 263SBV x .&& SBV y = SBV (x `svAnd` y) 264 265-- | Symbolic disjunction 266infixr 2 .|| 267(.||) :: SBool -> SBool -> SBool 268SBV x .|| SBV y = SBV (x `svOr` y) 269 270-- | Symbolic logical xor 271infixl 6 .<+> 272(.<+>) :: SBool -> SBool -> SBool 273SBV x .<+> SBV y = SBV (x `svXOr` y) 274 275-- | Symbolic nand 276infixr 3 .~& 277(.~&) :: SBool -> SBool -> SBool 278x .~& y = sNot (x .&& y) 279 280-- | Symbolic nor 281infixr 2 .~| 282(.~|) :: SBool -> SBool -> SBool 283x .~| y = sNot (x .|| y) 284 285-- | Symbolic implication 286infixr 1 .=> 287(.=>) :: SBool -> SBool -> SBool 288x .=> y = sNot x .|| y 289-- NB. Do *not* try to optimize @x .=> x = True@ here! If constants go through, it'll get simplified. 290-- The case "x .=> x" can hit is extremely rare, and the getAllSatResult function relies on this 291-- trick to generate constraints in the unlucky case of ui-function models. 292 293-- | Symbolic boolean equivalence 294infixr 1 .<=> 295(.<=>) :: SBool -> SBool -> SBool 296x .<=> y = (x .&& y) .|| (sNot x .&& sNot y) 297 298-- | Conversion from 'Bool' to 'SBool' 299fromBool :: Bool -> SBool 300fromBool True = sTrue 301fromBool False = sFalse 302 303-- | Generalization of 'and' 304sAnd :: [SBool] -> SBool 305sAnd = foldr (.&&) sTrue 306 307-- | Generalization of 'or' 308sOr :: [SBool] -> SBool 309sOr = foldr (.||) sFalse 310 311-- | Generalization of 'any' 312sAny :: (a -> SBool) -> [a] -> SBool 313sAny f = sOr . map f 314 315-- | Generalization of 'all' 316sAll :: (a -> SBool) -> [a] -> SBool 317sAll f = sAnd . map f 318 319-- | 'RoundingMode' can be used symbolically 320instance SymVal RoundingMode 321 322-- | The symbolic variant of 'RoundingMode' 323type SRoundingMode = SBV RoundingMode 324 325-- | Symbolic variant of 'RoundNearestTiesToEven' 326sRoundNearestTiesToEven :: SRoundingMode 327sRoundNearestTiesToEven = literal RoundNearestTiesToEven 328 329-- | Symbolic variant of 'RoundNearestTiesToAway' 330sRoundNearestTiesToAway :: SRoundingMode 331sRoundNearestTiesToAway = literal RoundNearestTiesToAway 332 333-- | Symbolic variant of 'RoundTowardPositive' 334sRoundTowardPositive :: SRoundingMode 335sRoundTowardPositive = literal RoundTowardPositive 336 337-- | Symbolic variant of 'RoundTowardNegative' 338sRoundTowardNegative :: SRoundingMode 339sRoundTowardNegative = literal RoundTowardNegative 340 341-- | Symbolic variant of 'RoundTowardZero' 342sRoundTowardZero :: SRoundingMode 343sRoundTowardZero = literal RoundTowardZero 344 345-- | Alias for 'sRoundNearestTiesToEven' 346sRNE :: SRoundingMode 347sRNE = sRoundNearestTiesToEven 348 349-- | Alias for 'sRoundNearestTiesToAway' 350sRNA :: SRoundingMode 351sRNA = sRoundNearestTiesToAway 352 353-- | Alias for 'sRoundTowardPositive' 354sRTP :: SRoundingMode 355sRTP = sRoundTowardPositive 356 357-- | Alias for 'sRoundTowardNegative' 358sRTN :: SRoundingMode 359sRTN = sRoundTowardNegative 360 361-- | Alias for 'sRoundTowardZero' 362sRTZ :: SRoundingMode 363sRTZ = sRoundTowardZero 364 365-- | A 'Show' instance is not particularly "desirable," when the value is symbolic, 366-- but we do need this instance as otherwise we cannot simply evaluate Haskell functions 367-- that return symbolic values and have their constant values printed easily! 368instance Show (SBV a) where 369 show (SBV sv) = show sv 370 371-- | This instance is only defined so that we can define an instance for 372-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use 373-- 'Data.SBV.EqSymbolic' instead. 374instance Eq (SBV a) where 375 SBV a == SBV b = a == b 376 SBV a /= SBV b = a /= b 377 378instance HasKind a => HasKind (SBV a) where 379 kindOf _ = kindOf (Proxy @a) 380 381-- | Convert a symbolic value to a symbolic-word 382sbvToSV :: State -> SBV a -> IO SV 383sbvToSV st (SBV s) = svToSV st s 384 385------------------------------------------------------------------------- 386-- * Symbolic Computations 387------------------------------------------------------------------------- 388 389-- | Generalization of 'Data.SBV.mkSymSBV' 390mkSymSBV :: forall a m. MonadSymbolic m => VarContext -> Kind -> Maybe String -> m (SBV a) 391mkSymSBV vc k mbNm = SBV <$> (symbolicEnv >>= liftIO . svMkSymVar vc k mbNm) 392 393-- | Generalization of 'Data.SBV.sbvToSymSW' 394sbvToSymSV :: MonadSymbolic m => SBV a -> m SV 395sbvToSymSV sbv = do 396 st <- symbolicEnv 397 liftIO $ sbvToSV st sbv 398 399-- | Actions we can do in a context: Either at problem description 400-- time or while we are dynamically querying. 'Symbolic' and 'Query' are 401-- two instances of this class. Note that we use this mechanism 402-- internally and do not export it from SBV. 403class SolverContext m where 404 -- | Add a constraint, any satisfying instance must satisfy this condition. 405 constrain :: SBool -> m () 406 -- | Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot. 407 softConstrain :: SBool -> m () 408 -- | Add a named constraint. The name is used in unsat-core extraction. 409 namedConstraint :: String -> SBool -> m () 410 -- | Add a constraint, with arbitrary attributes. 411 constrainWithAttribute :: [(String, String)] -> SBool -> m () 412 -- | Set info. Example: @setInfo ":status" ["unsat"]@. 413 setInfo :: String -> [String] -> m () 414 -- | Set an option. 415 setOption :: SMTOption -> m () 416 -- | Set the logic. 417 setLogic :: Logic -> m () 418 -- | Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere 419 -- string, use for commenting purposes. The second argument is intended to hold the multiple-lines 420 -- of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom 421 -- itself, to see whether it's actually well-formed or is sensible by any means. 422 -- A separate formalization of SMT-Lib would be very useful here. 423 addAxiom :: String -> [String] -> m () 424 -- | Set a solver time-out value, in milli-seconds. This function 425 -- essentially translates to the SMTLib call @(set-info :timeout val)@, 426 -- and your backend solver may or may not support it! The amount given 427 -- is in milliseconds. Also see the function 'Data.SBV.Control.timeOut' for finer level 428 -- control of time-outs, directly from SBV. 429 setTimeOut :: Integer -> m () 430 -- | Get the state associated with this context 431 contextState :: m State 432 433 {-# MINIMAL constrain, softConstrain, namedConstraint, constrainWithAttribute, setOption, addAxiom, contextState #-} 434 435 -- time-out, logic, and info are simply options in our implementation, so default implementation suffices 436 setTimeOut t = setOption $ OptionKeyword ":timeout" [show t] 437 setLogic = setOption . SetLogic 438 setInfo k = setOption . SetInfo k 439 440-- | A class representing what can be returned from a symbolic computation. 441class Outputtable a where 442 -- | Generalization of 'Data.SBV.output' 443 output :: MonadSymbolic m => a -> m a 444 445instance Outputtable (SBV a) where 446 output i = do 447 outputSVal (unSBV i) 448 return i 449 450instance Outputtable a => Outputtable [a] where 451 output = mapM output 452 453instance Outputtable () where 454 output = return 455 456instance (Outputtable a, Outputtable b) => Outputtable (a, b) where 457 output = mlift2 (,) output output 458 459instance (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) where 460 output = mlift3 (,,) output output output 461 462instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) where 463 output = mlift4 (,,,) output output output output 464 465instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) where 466 output = mlift5 (,,,,) output output output output output 467 468instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) where 469 output = mlift6 (,,,,,) output output output output output output 470 471instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) where 472 output = mlift7 (,,,,,,) output output output output output output output 473 474instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) where 475 output = mlift8 (,,,,,,,) output output output output output output output output 476 477------------------------------------------------------------------------------- 478-- * Symbolic Values 479------------------------------------------------------------------------------- 480-- | A 'SymVal' is a potential symbolic value that can be created instances of to be fed to a symbolic program. 481class (HasKind a, Typeable a) => SymVal a where 482 -- | Generalization of 'Data.SBV.mkSymVal' 483 mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV a) 484 -- | Turn a literal constant to symbolic 485 literal :: a -> SBV a 486 -- | Extract a literal, from a CV representation 487 fromCV :: CV -> a 488 -- | Does it concretely satisfy the given predicate? 489 isConcretely :: SBV a -> (a -> Bool) -> Bool 490 491 -- minimal complete definition: Nothing. 492 -- Giving no instances is okay when defining an uninterpreted/enumerated sort, but otherwise you really 493 -- want to define: literal, fromCV, mkSymVal 494 495 default mkSymVal :: (MonadSymbolic m, Read a, G.Data a) => VarContext -> Maybe String -> m (SBV a) 496 mkSymVal vc mbNm = SBV <$> (symbolicEnv >>= liftIO . svMkSymVar vc k mbNm) 497 where -- NB.A call of the form 498 -- constructUKind (Proxy @a) 499 -- would be wrong here, as it would uninterpret the Proxy datatype! 500 -- So, we have to use the dreaded undefined value in this case. 501 k = constructUKind (undefined :: a) 502 503 default literal :: Show a => a -> SBV a 504 literal x = let k@(KUserSort _ conts) = kindOf x 505 sx = show x 506 mbIdx = case conts of 507 Just xs -> sx `elemIndex` xs 508 Nothing -> Nothing 509 in SBV $ SVal k (Left (CV k (CUserSort (mbIdx, sx)))) 510 511 default fromCV :: Read a => CV -> a 512 fromCV (CV _ (CUserSort (_, s))) = read s 513 fromCV cv = error $ "Cannot convert CV " ++ show cv ++ " to kind " ++ show (kindOf (Proxy @a)) 514 515 isConcretely s p 516 | Just i <- unliteral s = p i 517 | True = False 518 519 -- | Generalization of 'Data.SBV.forall' 520 forall :: MonadSymbolic m => String -> m (SBV a) 521 forall = mkSymVal (NonQueryVar (Just ALL)) . Just 522 523 -- | Generalization of 'Data.SBV.forall_' 524 forall_ :: MonadSymbolic m => m (SBV a) 525 forall_ = mkSymVal (NonQueryVar (Just ALL)) Nothing 526 527 -- | Generalization of 'Data.SBV.mkForallVars' 528 mkForallVars :: MonadSymbolic m => Int -> m [SBV a] 529 mkForallVars n = mapM (const forall_) [1 .. n] 530 531 -- | Generalization of 'Data.SBV.exists' 532 exists :: MonadSymbolic m => String -> m (SBV a) 533 exists = mkSymVal (NonQueryVar (Just EX)) . Just 534 535 -- | Generalization of 'Data.SBV.exists_' 536 exists_ :: MonadSymbolic m => m (SBV a) 537 exists_ = mkSymVal (NonQueryVar (Just EX)) Nothing 538 539 -- | Generalization of 'Data.SBV.mkExistVars' 540 mkExistVars :: MonadSymbolic m => Int -> m [SBV a] 541 mkExistVars n = mapM (const exists_) [1 .. n] 542 543 -- | Generalization of 'Data.SBV.free' 544 free :: MonadSymbolic m => String -> m (SBV a) 545 free = mkSymVal (NonQueryVar Nothing) . Just 546 547 -- | Generalization of 'Data.SBV.free_' 548 free_ :: MonadSymbolic m => m (SBV a) 549 free_ = mkSymVal (NonQueryVar Nothing) Nothing 550 551 -- | Generalization of 'Data.SBV.mkFreeVars' 552 mkFreeVars :: MonadSymbolic m => Int -> m [SBV a] 553 mkFreeVars n = mapM (const free_) [1 .. n] 554 555 -- | Generalization of 'Data.SBV.symbolic' 556 symbolic :: MonadSymbolic m => String -> m (SBV a) 557 symbolic = free 558 559 -- | Generalization of 'Data.SBV.symbolics' 560 symbolics :: MonadSymbolic m => [String] -> m [SBV a] 561 symbolics = mapM symbolic 562 563 -- | Extract a literal, if the value is concrete 564 unliteral :: SBV a -> Maybe a 565 unliteral (SBV (SVal _ (Left c))) = Just $ fromCV c 566 unliteral _ = Nothing 567 568 -- | Is the symbolic word concrete? 569 isConcrete :: SBV a -> Bool 570 isConcrete (SBV (SVal _ (Left _))) = True 571 isConcrete _ = False 572 573 -- | Is the symbolic word really symbolic? 574 isSymbolic :: SBV a -> Bool 575 isSymbolic = not . isConcrete 576 577instance (Random a, SymVal a) => Random (SBV a) where 578 randomR (l, h) g = case (unliteral l, unliteral h) of 579 (Just lb, Just hb) -> let (v, g') = randomR (lb, hb) g in (literal (v :: a), g') 580 _ -> error "SBV.Random: Cannot generate random values with symbolic bounds" 581 random g = let (v, g') = random g in (literal (v :: a) , g') 582 583--------------------------------------------------------------------------------- 584-- * Symbolic Arrays 585--------------------------------------------------------------------------------- 586 587-- | Flat arrays of symbolic values 588-- An @array a b@ is an array indexed by the type @'SBV' a@, with elements of type @'SBV' b@. 589-- 590-- If a default value is supplied, then all the array elements will be initialized to this value. 591-- Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce 592-- an uninterpreted constant. 593-- 594-- While it's certainly possible for user to create instances of 'SymArray', the 595-- 'SArray' and 'SFunArray' instances already provided should cover most use cases 596-- in practice. Note that there are a few differences between these two models in 597-- terms of use models: 598-- 599-- * 'SArray' produces SMTLib arrays, and requires a solver that understands the 600-- array theory. 'SFunArray' is internally handled, and thus can be used with 601-- any solver. (Note that all solvers except 'Data.SBV.abc' support arrays, so this isn't 602-- a big decision factor.) 603-- 604-- * For both arrays, if a default value is supplied, then reading from uninitialized 605-- cell will return that value. If the default is not given, then reading from 606-- uninitialized cells is still OK for both arrays, and will produce an uninterpreted 607-- constant in both cases. 608-- 609-- * Only 'SArray' supports checking equality of arrays. (That is, checking if an entire 610-- array is equivalent to another.) 'SFunArray's cannot be checked for equality. In general, 611-- checking wholesale equality of arrays is a difficult decision problem and should be 612-- avoided if possible. 613-- 614-- * Only 'SFunArray' supports compilation to C. Programs using 'SArray' will not be 615-- accepted by the C-code generator. 616-- 617-- * You cannot use quickcheck on programs that contain these arrays. (Neither 'SArray' 618-- nor 'SFunArray'.) 619-- 620-- * With 'SArray', SBV transfers all array-processing to the SMT-solver. So, it can generate 621-- programs more quickly, but they might end up being too hard for the solver to handle. With 622-- 'SFunArray', SBV only generates code for individual elements and the array itself never 623-- shows up in the resulting SMTLib program. This puts more onus on the SBV side and might 624-- have some performance impacts, but it might generate problems that are easier for the SMT 625-- solvers to handle. 626-- 627-- As a rule of thumb, try 'SArray' first. These should generate compact code. However, if 628-- the backend solver has hard time solving the generated problems, switch to 629-- 'SFunArray'. If you still have issues, please report so we can see what the problem might be! 630-- 631-- NB. 'sListArray' insists on a concrete initializer, because not having one would break 632-- referential transparency. See https://github.com/LeventErkok/sbv/issues/553 for details. 633class SymArray array where 634 -- | Generalization of 'Data.SBV.newArray_' 635 newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b) 636 -- | Generalization of 'Data.SBV.newArray' 637 newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b) 638 -- | Create a literal array 639 sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b 640 -- | Read the array element at @a@ 641 readArray :: array a b -> SBV a -> SBV b 642 -- | Update the element at @a@ to be @b@ 643 writeArray :: SymVal b => array a b -> SBV a -> SBV b -> array a b 644 -- | Merge two given arrays on the symbolic condition 645 -- Intuitively: @mergeArrays cond a b = if cond then a else b@. 646 -- Merging pushes the if-then-else choice down on to elements 647 mergeArrays :: SymVal b => SBV Bool -> array a b -> array a b -> array a b 648 -- | Internal function, not exported to the user 649 newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b) 650 651 {-# MINIMAL readArray, writeArray, mergeArrays, ((newArray_, newArray) | newArrayInState), sListArray #-} 652 newArray_ mbVal = symbolicEnv >>= liftIO . newArrayInState Nothing mbVal 653 newArray nm mbVal = symbolicEnv >>= liftIO . newArrayInState (Just nm) mbVal 654 655 -- Despite our MINIMAL pragma and default implementations for newArray_ and 656 -- newArray, we must provide a dummy implementation for newArrayInState: 657 newArrayInState = error "undefined: newArrayInState" 658 659-- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml> 660-- 661-- * Maps directly to SMT-lib arrays 662-- 663-- * Reading from an unintialized value is OK. If the default value is given in 'newArray', it will 664-- be the result. Otherwise, the read yields an uninterpreted constant. 665-- 666-- * Can check for equality of these arrays 667-- 668-- * Cannot be used in code-generation (i.e., compilation to C) 669-- 670-- * Cannot quick-check theorems using @SArray@ values 671-- 672-- * Typically slower as it heavily relies on SMT-solving for the array theory 673newtype SArray a b = SArray { unSArray :: SArr } 674 675instance (HasKind a, HasKind b) => Show (SArray a b) where 676 show SArray{} = "SArray<" ++ showType (Proxy @a) ++ ":" ++ showType (Proxy @b) ++ ">" 677 678instance SymArray SArray where 679 readArray (SArray arr) (SBV a) = SBV (readSArr arr a) 680 writeArray (SArray arr) (SBV a) (SBV b) = SArray (writeSArr arr a b) 681 mergeArrays (SBV t) (SArray a) (SArray b) = SArray (mergeSArr t a b) 682 683 sListArray :: forall a b. (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> SArray a b 684 sListArray initializer = foldl (uncurry . writeArray) arr 685 where arr = SArray $ SArr ks $ cache r 686 where ks = (kindOf (Proxy @a), kindOf (Proxy @b)) 687 r st = do amap <- R.readIORef (rArrayMap st) 688 689 let k = ArrayIndex $ IMap.size amap 690 iVal = literal initializer 691 692 iSV <- sbvToSV st iVal 693 694 let upd = IMap.insert (unArrayIndex k) ("array_" ++ show k, ks, ArrayFree (Just iSV)) 695 696 k `seq` modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd 697 return k 698 699 newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) 700 newArrayInState mbNm mbVal st = do mapM_ (registerKind st) [aknd, bknd] 701 SArray <$> newSArr st (aknd, bknd) (mkNm mbNm) (unSBV <$> mbVal) 702 where mkNm Nothing t = "array_" ++ show t 703 mkNm (Just nm) _ = nm 704 aknd = kindOf (Proxy @a) 705 bknd = kindOf (Proxy @b) 706 707-- | Arrays implemented internally, without translating to SMT-Lib functions: 708-- 709-- * Internally handled by the library and not mapped to SMT-Lib, hence can 710-- be used with solvers that don't support arrays. (Such as abc.) 711-- 712-- * Reading from an unintialized value is OK. If the default value is given in 'newArray', it will 713-- be the result. Otherwise, the read yields an uninterpreted constant. 714-- 715-- * Cannot check for equality of arrays. 716-- 717-- * Can be used in code-generation (i.e., compilation to C). 718-- 719-- * Can not quick-check theorems using @SFunArray@ values 720-- 721-- * Typically faster as it gets compiled away during translation. 722newtype SFunArray a b = SFunArray { unSFunArray :: SFunArr } 723 724instance (HasKind a, HasKind b) => Show (SFunArray a b) where 725 show SFunArray{} = "SFunArray<" ++ showType (Proxy @a) ++ ":" ++ showType (Proxy @b) ++ ">" 726 727instance SymArray SFunArray where 728 readArray (SFunArray arr) (SBV a) = SBV (readSFunArr arr a) 729 writeArray (SFunArray arr) (SBV a) (SBV b) = SFunArray (writeSFunArr arr a b) 730 mergeArrays (SBV t) (SFunArray a) (SFunArray b) = SFunArray (mergeSFunArr t a b) 731 732 sListArray :: forall a b. (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> SFunArray a b 733 sListArray initializer = foldl (uncurry . writeArray) arr 734 where arr = SFunArray $ SFunArr ks $ cache r 735 where ks = (kindOf (Proxy @a), kindOf (Proxy @b)) 736 737 r st = do amap <- R.readIORef (rFArrayMap st) 738 739 memoTable <- R.newIORef IMap.empty 740 741 let k = FArrayIndex $ IMap.size amap 742 iVal = literal initializer 743 mkUninitialized = const (unSBV iVal) 744 upd = IMap.insert (unFArrayIndex k) (mkUninitialized, memoTable) 745 746 k `seq` modifyState st rFArrayMap upd (return ()) 747 return k 748 749 newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) 750 newArrayInState mbNm mbVal st = do mapM_ (registerKind st) [aknd, bknd] 751 SFunArray <$> newSFunArr st (aknd, bknd) (mkNm mbNm) (unSBV <$> mbVal) 752 where mkNm Nothing t = "funArray_" ++ show t 753 mkNm (Just nm) _ = nm 754 aknd = kindOf (Proxy @a) 755 bknd = kindOf (Proxy @b) 756