-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Data
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Internal data-structures for the sbv library
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards         #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Core.Data
 ( SBool, SWord8, SWord16, SWord32, SWord64
 , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble
 , SFloatingPoint, SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad
 , SRational
 , SChar, SString, SList
 , SEither, SMaybe
 , STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8
 , RCSet(..), SSet
 , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode
 , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero
 , sRNE, sRNA, sRTP, sRTN, sRTZ
 , SymVal(..)
 , CV(..), CVal(..), AlgReal(..), AlgRealPoly(..), ExtCV(..), GeneralizedCV(..), isRegularCV, cvSameType, cvToBool
 , mkConstCV ,liftCV2, mapCV, mapCV2
 , SV(..), trueSV, falseSV, trueCV, falseCV, normCV
 , SVal(..)
 , sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), sAnd, sOr, sAny, sAll, fromBool
 , SBV(..), NodeId(..), mkSymSBV
 , ArrayContext(..), ArrayInfo, SymArray(..), SArray(..)
 , sbvToSV, sbvToSymSV, forceSVArg
 , SBVExpr(..), newExpr
 , cache, Cached, uncache, uncacheAI, HasKind(..)
 , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExOp(..), SeqOp(..), RegExp(..), NamedSymVar(..), getTableIndex
 , SBVPgm(..), Symbolic, runSymbolic, State, getPathCondition, extendPathCondition
 , inSMTMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
 , SolverContext(..), internalVariable, internalConstraint, isCodeGenMode
 , SBVType(..), newUninterpreted
 , Quantifier(..), needsExistentials
 , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension, smtLibReservedNames
 , SolverCapabilities(..)
 , extractSymbolicSimulationState
 , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..)
 , OptimizeStyle(..), Penalty(..), Objective(..)
 , QueryState(..), QueryT(..), SMTProblem(..)
 ) where

import GHC.TypeLits

import GHC.Generics (Generic)
import GHC.Exts     (IsList(..))

import Control.DeepSeq        (NFData(..))
import Control.Monad.Trans    (liftIO)
import Data.Int               (Int8, Int16, Int32, Int64)
import Data.Word              (Word8, Word16, Word32, Word64)
import Data.List              (elemIndex)
import Data.Maybe             (fromMaybe)

import Data.Proxy
import Data.Typeable          (Typeable)

import qualified Data.Generics as G    (Data(..))

import qualified Data.IORef         as R    (readIORef)
import qualified Data.IntMap.Strict as IMap (size, insert)

import System.Random

import Data.SBV.Core.AlgReals
import Data.SBV.Core.SizedFloats
import Data.SBV.Core.Kind
import Data.SBV.Core.Concrete
import Data.SBV.Core.Symbolic
import Data.SBV.Core.Operations

import Data.SBV.Control.Types

import Data.SBV.SMT.SMTLibNames

import Data.SBV.Utils.Lib

-- | Get the current path condition
getPathCondition :: State -> SBool
getPathCondition :: State -> SBool
getPathCondition State
st = SVal -> SBool
forall a. SVal -> SBV a
SBV (State -> SVal
getSValPathCondition State
st)

-- | Extend the path condition with the given test value.
extendPathCondition :: State -> (SBool -> SBool) -> State
extendPathCondition :: State -> (SBool -> SBool) -> State
extendPathCondition State
st SBool -> SBool
f = State -> (SVal -> SVal) -> State
extendSValPathCondition State
st (SBool -> SVal
forall a. SBV a -> SVal
unSBV (SBool -> SVal) -> (SVal -> SBool) -> SVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> SBool
f (SBool -> SBool) -> (SVal -> SBool) -> SVal -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> SBool
forall a. SVal -> SBV a
SBV)

-- | The "Symbolic" value. The parameter @a@ is phantom, but is
-- extremely important in keeping the user interface strongly typed.
newtype SBV a = SBV { SBV a -> SVal
unSBV :: SVal }
              deriving ((forall x. SBV a -> Rep (SBV a) x)
-> (forall x. Rep (SBV a) x -> SBV a) -> Generic (SBV a)
forall x. Rep (SBV a) x -> SBV a
forall x. SBV a -> Rep (SBV a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SBV a) x -> SBV a
forall a x. SBV a -> Rep (SBV a) x
$cto :: forall a x. Rep (SBV a) x -> SBV a
$cfrom :: forall a x. SBV a -> Rep (SBV a) x
Generic, SBV a -> ()
(SBV a -> ()) -> NFData (SBV a)
forall a. SBV a -> ()
forall a. (a -> ()) -> NFData a
rnf :: SBV a -> ()
$crnf :: forall a. SBV a -> ()
NFData)

-- | A symbolic boolean/bit
type SBool   = SBV Bool

-- | 8-bit unsigned symbolic value
type SWord8  = SBV Word8

-- | 16-bit unsigned symbolic value
type SWord16 = SBV Word16

-- | 32-bit unsigned symbolic value
type SWord32 = SBV Word32

-- | 64-bit unsigned symbolic value
type SWord64 = SBV Word64

-- | 8-bit signed symbolic value, 2's complement representation
type SInt8   = SBV Int8

-- | 16-bit signed symbolic value, 2's complement representation
type SInt16  = SBV Int16

-- | 32-bit signed symbolic value, 2's complement representation
type SInt32  = SBV Int32

-- | 64-bit signed symbolic value, 2's complement representation
type SInt64  = SBV Int64

-- | Infinite precision signed symbolic value
type SInteger = SBV Integer

-- | Infinite precision symbolic algebraic real value
type SReal = SBV AlgReal

-- | IEEE-754 single-precision floating point numbers
type SFloat = SBV Float

-- | IEEE-754 double-precision floating point numbers
type SDouble = SBV Double

-- | A symbolic arbitrary precision floating point value
type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb)

-- | A symbolic half-precision float
type SFPHalf = SBV FPHalf

-- | A symbolic brain-float precision float
type SFPBFloat = SBV FPBFloat

-- | A symbolic single-precision float
type SFPSingle = SBV FPSingle

-- | A symbolic double-precision float
type SFPDouble = SBV FPDouble

-- | A symbolic quad-precision float
type SFPQuad = SBV FPQuad

-- | A symbolic character. Note that this is the full unicode character set.
-- see: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>
-- for details.
type SChar = SBV Char

-- | A symbolic string. Note that a symbolic string is /not/ a list of symbolic characters,
-- that is, it is not the case that @SString = [SChar]@, unlike what one might expect following
-- Haskell strings. An 'SString' is a symbolic value of its own, of possibly arbitrary but finite length,
-- and internally processed as one unit as opposed to a fixed-length list of characters.
type SString = SBV String

-- | A symbolic rational value.
type SRational = SBV Rational

-- | A symbolic list of items. Note that a symbolic list is /not/ a list of symbolic items,
-- that is, it is not the case that @SList a = [a]@, unlike what one might expect following
-- haskell lists\/sequences. An 'SList' is a symbolic value of its own, of possibly arbitrary but finite
-- length, and internally processed as one unit as opposed to a fixed-length list of items.
-- Note that lists can be nested, i.e., we do allow lists of lists of ... items.
type SList a = SBV [a]

-- | Symbolic 'Either'
type SEither a b = SBV (Either a b)

-- | Symbolic 'Maybe'
type SMaybe a = SBV (Maybe a)

-- | Symbolic 'Data.Set'. Note that we use 'RCSet', which supports
-- both regular sets and complements, i.e., those obtained from the
-- universal set (of the right type) by removing elements.
type SSet a = SBV (RCSet a)

-- | Symbolic 2-tuple. NB. 'STuple' and 'STuple2' are equivalent.
type STuple a b = SBV (a, b)

-- | Symbolic 2-tuple. NB. 'STuple' and 'STuple2' are equivalent.
type STuple2 a b = SBV (a, b)

-- | Symbolic 3-tuple.
type STuple3 a b c = SBV (a, b, c)

-- | Symbolic 4-tuple.
type STuple4 a b c d = SBV (a, b, c, d)

-- | Symbolic 5-tuple.
type STuple5 a b c d e = SBV (a, b, c, d, e)

-- | Symbolic 6-tuple.
type STuple6 a b c d e f = SBV (a, b, c, d, e, f)

-- | Symbolic 7-tuple.
type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)

-- | Symbolic 8-tuple.
type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)

-- | IsList instance allows list literals to be written compactly.
instance SymVal [a] => IsList (SList a) where
  type Item (SList a) = a
  fromList :: [Item (SList a)] -> SList a
fromList = [Item (SList a)] -> SList a
forall a. SymVal a => a -> SBV a
literal
  toList :: SList a -> [Item (SList a)]
toList SList a
x = [a] -> Maybe [a] -> [a]
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> [a]
forall a. HasCallStack => [Char] -> a
error [Char]
"IsList.toList used in a symbolic context!") (SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
x)

-- | Not-A-Number for 'Double' and 'Float'. Surprisingly, Haskell
-- Prelude doesn't have this value defined, so we provide it here.
nan :: Floating a => a
nan :: a
nan = a
0a -> a -> a
forall a. Fractional a => a -> a -> a
/a
0

-- | Infinity for 'Double' and 'Float'. Surprisingly, Haskell
-- Prelude doesn't have this value defined, so we provide it here.
infinity :: Floating a => a
infinity :: a
infinity = a
1a -> a -> a
forall a. Fractional a => a -> a -> a
/a
0

-- | Symbolic variant of Not-A-Number. This value will inhabit
-- 'SFloat', 'SDouble' and 'SFloatingPoint'. types.
sNaN :: (Floating a, SymVal a) => SBV a
sNaN :: SBV a
sNaN = a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
forall a. Floating a => a
nan

-- | Symbolic variant of infinity. This value will inhabit both
-- 'SFloat', 'SDouble' and 'SFloatingPoint'. types.
sInfinity :: (Floating a, SymVal a) => SBV a
sInfinity :: SBV a
sInfinity = a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
forall a. Floating a => a
infinity

-- | Internal representation of a symbolic simulation result
newtype SMTProblem = SMTProblem {SMTProblem -> SMTConfig -> SMTLibPgm
smtLibPgm :: SMTConfig -> SMTLibPgm} -- ^ SMTLib representation, given the config

-- | Symbolic 'True'
sTrue :: SBool
sTrue :: SBool
sTrue = SVal -> SBool
forall a. SVal -> SBV a
SBV (Bool -> SVal
svBool Bool
True)

-- | Symbolic 'False'
sFalse :: SBool
sFalse :: SBool
sFalse = SVal -> SBool
forall a. SVal -> SBV a
SBV (Bool -> SVal
svBool Bool
False)

-- | Symbolic boolean negation
sNot :: SBool -> SBool
sNot :: SBool -> SBool
sNot (SBV SVal
b) = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SVal
svNot SVal
b)

-- | Symbolic conjunction
infixr 3 .&&
(.&&) :: SBool -> SBool -> SBool
SBV SVal
x .&& :: SBool -> SBool -> SBool
.&& SBV SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svAnd` SVal
y)

-- | Symbolic disjunction
infixr 2 .||
(.||) :: SBool -> SBool -> SBool
SBV SVal
x .|| :: SBool -> SBool -> SBool
.|| SBV SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svOr` SVal
y)

-- | Symbolic logical xor
infixl 6 .<+>
(.<+>) :: SBool -> SBool -> SBool
SBV SVal
x .<+> :: SBool -> SBool -> SBool
.<+> SBV SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svXOr` SVal
y)

-- | Symbolic nand
infixr 3 .~&
(.~&) :: SBool -> SBool -> SBool
SBool
x .~& :: SBool -> SBool -> SBool
.~& SBool
y = SBool -> SBool
sNot (SBool
x SBool -> SBool -> SBool
.&& SBool
y)

-- | Symbolic nor
infixr 2 .~|
(.~|) :: SBool -> SBool -> SBool
SBool
x .~| :: SBool -> SBool -> SBool
.~| SBool
y = SBool -> SBool
sNot (SBool
x SBool -> SBool -> SBool
.|| SBool
y)

-- | Symbolic implication
infixr 1 .=>
(.=>) :: SBool -> SBool -> SBool
SBool
x .=> :: SBool -> SBool -> SBool
.=> SBool
y = SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.|| SBool
y
-- NB. Do *not* try to optimize @x .=> x = True@ here! If constants go through, it'll get simplified.
-- The case "x .=> x" can hit is extremely rare, and the getAllSatResult function relies on this
-- trick to generate constraints in the unlucky case of ui-function models.

-- | Symbolic boolean equivalence
infixr 1 .<=>
(.<=>) :: SBool -> SBool -> SBool
SBool
x .<=> :: SBool -> SBool -> SBool
.<=> SBool
y = (SBool
x SBool -> SBool -> SBool
.&& SBool
y) SBool -> SBool -> SBool
.|| (SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.&& SBool -> SBool
sNot SBool
y)

-- | Conversion from 'Bool' to 'SBool'
fromBool :: Bool -> SBool
fromBool :: Bool -> SBool
fromBool Bool
True  = SBool
sTrue
fromBool Bool
False = SBool
sFalse

-- | Generalization of 'and'
sAnd :: [SBool] -> SBool
sAnd :: [SBool] -> SBool
sAnd = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
(.&&) SBool
sTrue

-- | Generalization of 'or'
sOr :: [SBool] -> SBool
sOr :: [SBool] -> SBool
sOr  = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
(.||) SBool
sFalse

-- | Generalization of 'any'
sAny :: (a -> SBool) -> [a] -> SBool
sAny :: (a -> SBool) -> [a] -> SBool
sAny a -> SBool
f = [SBool] -> SBool
sOr  ([SBool] -> SBool) -> ([a] -> [SBool]) -> [a] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SBool) -> [a] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map a -> SBool
f

-- | Generalization of 'all'
sAll :: (a -> SBool) -> [a] -> SBool
sAll :: (a -> SBool) -> [a] -> SBool
sAll a -> SBool
f = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> ([a] -> [SBool]) -> [a] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SBool) -> [a] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map a -> SBool
f

-- | 'RoundingMode' can be used symbolically
instance SymVal RoundingMode

-- | The symbolic variant of 'RoundingMode'
type SRoundingMode = SBV RoundingMode

-- | Symbolic variant of 'RoundNearestTiesToEven'
sRoundNearestTiesToEven :: SRoundingMode
sRoundNearestTiesToEven :: SBV RoundingMode
sRoundNearestTiesToEven = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundNearestTiesToEven

-- | Symbolic variant of 'RoundNearestTiesToAway'
sRoundNearestTiesToAway :: SRoundingMode
sRoundNearestTiesToAway :: SBV RoundingMode
sRoundNearestTiesToAway = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundNearestTiesToAway

-- | Symbolic variant of 'RoundTowardPositive'
sRoundTowardPositive :: SRoundingMode
sRoundTowardPositive :: SBV RoundingMode
sRoundTowardPositive = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundTowardPositive

-- | Symbolic variant of 'RoundTowardNegative'
sRoundTowardNegative :: SRoundingMode
sRoundTowardNegative :: SBV RoundingMode
sRoundTowardNegative = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundTowardNegative

-- | Symbolic variant of 'RoundTowardZero'
sRoundTowardZero :: SRoundingMode
sRoundTowardZero :: SBV RoundingMode
sRoundTowardZero = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundTowardZero

-- | Alias for 'sRoundNearestTiesToEven'
sRNE :: SRoundingMode
sRNE :: SBV RoundingMode
sRNE = SBV RoundingMode
sRoundNearestTiesToEven

-- | Alias for 'sRoundNearestTiesToAway'
sRNA :: SRoundingMode
sRNA :: SBV RoundingMode
sRNA = SBV RoundingMode
sRoundNearestTiesToAway

-- | Alias for 'sRoundTowardPositive'
sRTP :: SRoundingMode
sRTP :: SBV RoundingMode
sRTP = SBV RoundingMode
sRoundTowardPositive

-- | Alias for 'sRoundTowardNegative'
sRTN :: SRoundingMode
sRTN :: SBV RoundingMode
sRTN = SBV RoundingMode
sRoundTowardNegative

-- | Alias for 'sRoundTowardZero'
sRTZ :: SRoundingMode
sRTZ :: SBV RoundingMode
sRTZ = SBV RoundingMode
sRoundTowardZero

-- | A 'Show' instance is not particularly "desirable," when the value is symbolic,
-- but we do need this instance as otherwise we cannot simply evaluate Haskell functions
-- that return symbolic values and have their constant values printed easily!
instance Show (SBV a) where
  show :: SBV a -> [Char]
show (SBV SVal
sv) = SVal -> [Char]
forall a. Show a => a -> [Char]
show SVal
sv

-- | This instance is only defined so that we can define an instance for
-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use
-- 'Data.SBV.EqSymbolic' instead.
instance Eq (SBV a) where
  SBV SVal
a == :: SBV a -> SBV a -> Bool
== SBV SVal
b = SVal
a SVal -> SVal -> Bool
forall a. Eq a => a -> a -> Bool
== SVal
b
  SBV SVal
a /= :: SBV a -> SBV a -> Bool
/= SBV SVal
b = SVal
a SVal -> SVal -> Bool
forall a. Eq a => a -> a -> Bool
/= SVal
b

instance HasKind a => HasKind (SBV a) where
  kindOf :: SBV a -> Kind
kindOf SBV a
_ = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)

-- | Convert a symbolic value to a symbolic-word
sbvToSV :: State -> SBV a -> IO SV
sbvToSV :: State -> SBV a -> IO SV
sbvToSV State
st (SBV SVal
s) = State -> SVal -> IO SV
svToSV State
st SVal
s

-------------------------------------------------------------------------
-- * Symbolic Computations
-------------------------------------------------------------------------

-- | Generalization of 'Data.SBV.mkSymSBV'
mkSymSBV :: forall a m. MonadSymbolic m => VarContext -> Kind -> Maybe String -> m (SBV a)
mkSymSBV :: VarContext -> Kind -> Maybe [Char] -> m (SBV a)
mkSymSBV VarContext
vc Kind
k Maybe [Char]
mbNm = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> m SVal -> m (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe [Char] -> State -> IO SVal
svMkSymVar VarContext
vc Kind
k Maybe [Char]
mbNm)

-- | Generalization of 'Data.SBV.sbvToSymSW'
sbvToSymSV :: MonadSymbolic m => SBV a -> m SV
sbvToSymSV :: SBV a -> m SV
sbvToSymSV SBV a
sbv = do
        State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
        IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sbv

-- | Actions we can do in a context: Either at problem description
-- time or while we are dynamically querying. 'Symbolic' and 'Query' are
-- two instances of this class. Note that we use this mechanism
-- internally and do not export it from SBV.
class SolverContext m where
   -- | Add a constraint, any satisfying instance must satisfy this condition.
   constrain :: SBool -> m ()
   -- | Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.
   softConstrain :: SBool -> m ()
   -- | Add a named constraint. The name is used in unsat-core extraction.
   namedConstraint :: String -> SBool -> m ()
   -- | Add a constraint, with arbitrary attributes.
   constrainWithAttribute :: [(String, String)] -> SBool -> m ()
   -- | Set info. Example: @setInfo ":status" ["unsat"]@.
   setInfo :: String -> [String] -> m ()
   -- | Set an option.
   setOption :: SMTOption -> m ()
   -- | Set the logic.
   setLogic :: Logic -> m ()
   -- | Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere
   -- string, use for commenting purposes. The second argument is intended to hold the multiple-lines
   -- of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom
   -- itself, to see whether it's actually well-formed or is sensible by any means.
   -- A separate formalization of SMT-Lib would be very useful here.
   addAxiom :: String -> [String] -> m ()
   -- | Add a user-defined SMTLib function. You should define the name given here as an uninterpreted
   -- value as well. SBV performs no checks on the SMTLib definition you give, so if it doesn't match
   -- the required type, or is malformed in any way, the call will fail at run-time.
   addSMTDefinition :: String -> [String] -> m ()
   -- | Set a solver time-out value, in milli-seconds. This function
   -- essentially translates to the SMTLib call @(set-info :timeout val)@,
   -- and your backend solver may or may not support it! The amount given
   -- is in milliseconds. Also see the function 'Data.SBV.Control.timeOut' for finer level
   -- control of time-outs, directly from SBV.
   setTimeOut :: Integer -> m ()
   -- | Get the state associated with this context
   contextState :: m State

   {-# MINIMAL constrain, softConstrain, namedConstraint, constrainWithAttribute, setOption, addAxiom, addSMTDefinition, contextState #-}

   -- time-out, logic, and info are  simply options in our implementation, so default implementation suffices
   setTimeOut Integer
t = SMTOption -> m ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> m ()) -> SMTOption -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> SMTOption
OptionKeyword [Char]
":timeout" [Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
t]
   setLogic     = SMTOption -> m ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> m ()) -> (Logic -> SMTOption) -> Logic -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Logic -> SMTOption
SetLogic
   setInfo    [Char]
k = SMTOption -> m ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> m ()) -> ([[Char]] -> SMTOption) -> [[Char]] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]] -> SMTOption
SetInfo [Char]
k

-- | A class representing what can be returned from a symbolic computation.
class Outputtable a where
  -- | Generalization of 'Data.SBV.output'
  output :: MonadSymbolic m => a -> m a

instance Outputtable (SBV a) where
  output :: SBV a -> m (SBV a)
output SBV a
i = do
          SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal (SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
i)
          SBV a -> m (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV a
i

instance Outputtable a => Outputtable [a] where
  output :: [a] -> m [a]
output = (a -> m a) -> [a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance Outputtable () where
  output :: () -> m ()
output = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return

instance (Outputtable a, Outputtable b) => Outputtable (a, b) where
  output :: (a, b) -> m (a, b)
output = (a -> b -> (a, b))
-> (a -> m a) -> (b -> m b) -> (a, b) -> m (a, b)
forall (m :: * -> *) a' b' r a b.
Monad m =>
(a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r
mlift2 (,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) where
  output :: (a, b, c) -> m (a, b, c)
output = (a -> b -> c -> (a, b, c))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (a, b, c)
-> m (a, b, c)
forall (m :: * -> *) a' b' c' r a b c.
Monad m =>
(a' -> b' -> c' -> r)
-> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r
mlift3 (,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) where
  output :: (a, b, c, d) -> m (a, b, c, d)
output = (a -> b -> c -> d -> (a, b, c, d))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (a, b, c, d)
-> m (a, b, c, d)
forall (m :: * -> *) a' b' c' d' r a b c d.
Monad m =>
(a' -> b' -> c' -> d' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (a, b, c, d)
-> m r
mlift4 (,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) where
  output :: (a, b, c, d, e) -> m (a, b, c, d, e)
output = (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (a, b, c, d, e)
-> m (a, b, c, d, e)
forall (m :: * -> *) a' b' c' d' e' r a b c d e.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (a, b, c, d, e)
-> m r
mlift5 (,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) where
  output :: (a, b, c, d, e, f) -> m (a, b, c, d, e, f)
output = (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (f -> m f)
-> (a, b, c, d, e, f)
-> m (a, b, c, d, e, f)
forall (m :: * -> *) a' b' c' d' e' f' r a b c d e f.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> f' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (a, b, c, d, e, f)
-> m r
mlift6 (,,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output f -> m f
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) where
  output :: (a, b, c, d, e, f, g) -> m (a, b, c, d, e, f, g)
output = (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (f -> m f)
-> (g -> m g)
-> (a, b, c, d, e, f, g)
-> m (a, b, c, d, e, f, g)
forall (m :: * -> *) a' b' c' d' e' f' g' r a b c d e f g.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> f' -> g' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (g -> m g')
-> (a, b, c, d, e, f, g)
-> m r
mlift7 (,,,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output f -> m f
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output g -> m g
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

instance (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
  output :: (a, b, c, d, e, f, g, h) -> m (a, b, c, d, e, f, g, h)
output = (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (f -> m f)
-> (g -> m g)
-> (h -> m h)
-> (a, b, c, d, e, f, g, h)
-> m (a, b, c, d, e, f, g, h)
forall (m :: * -> *) a' b' c' d' e' f' g' h' r a b c d e f g h.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (g -> m g')
-> (h -> m h')
-> (a, b, c, d, e, f, g, h)
-> m r
mlift8 (,,,,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output f -> m f
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output g -> m g
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output h -> m h
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

-------------------------------------------------------------------------------
-- * Symbolic Values
-------------------------------------------------------------------------------
-- | A 'SymVal' is a potential symbolic value that can be created instances of to be fed to a symbolic program.
class (HasKind a, Typeable a) => SymVal a where
  -- | Generalization of 'Data.SBV.mkSymVal'
  mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV a)
  -- | Turn a literal constant to symbolic
  literal :: a -> SBV a
  -- | Extract a literal, from a CV representation
  fromCV :: CV -> a
  -- | Does it concretely satisfy the given predicate?
  isConcretely :: SBV a -> (a -> Bool) -> Bool

  -- minimal complete definition: Nothing.
  -- Giving no instances is okay when defining an uninterpreted/enumerated sort, but otherwise you really
  -- want to define: literal, fromCV, mkSymVal

  default mkSymVal :: (MonadSymbolic m, Read a, G.Data a) => VarContext -> Maybe String -> m (SBV a)
  mkSymVal VarContext
vc Maybe [Char]
mbNm = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> m SVal -> m (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe [Char] -> State -> IO SVal
svMkSymVar VarContext
vc Kind
k Maybe [Char]
mbNm)
    where -- NB.A call of the form
          --      constructUKind (Proxy @a)
          -- would be wrong here, as it would uninterpret the Proxy datatype!
          -- So, we have to use the dreaded undefined value in this case.
          k :: Kind
k = a -> Kind
forall a. (Read a, Data a) => a -> Kind
constructUKind (a
forall a. HasCallStack => a
undefined :: a)

  default literal :: Show a => a -> SBV a
  literal a
x = let k :: Kind
k  = a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
x
                  sx :: [Char]
sx = a -> [Char]
forall a. Show a => a -> [Char]
show a
x
                  conts :: Maybe [[Char]]
conts = case Kind
k of
                           KUserSort [Char]
_ Maybe [[Char]]
cts -> Maybe [[Char]]
cts
                           Kind
_               -> Maybe [[Char]]
forall a. Maybe a
Nothing
                  mbIdx :: Maybe Int
mbIdx = case Maybe [[Char]]
conts of
                            Just [[Char]]
xs -> [Char]
sx [Char] -> [[Char]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [[Char]]
xs
                            Maybe [[Char]]
Nothing -> Maybe Int
forall a. Maybe a
Nothing
              in SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (Kind -> CVal -> CV
CV Kind
k ((Maybe Int, [Char]) -> CVal
CUserSort (Maybe Int
mbIdx, [Char]
sx))))

  default fromCV :: Read a => CV -> a
  fromCV (CV Kind
_ (CUserSort (Maybe Int
_, [Char]
s))) = [Char] -> a
forall a. Read a => [Char] -> a
read [Char]
s
  fromCV CV
cv                        = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot convert CV " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CV -> [Char]
forall a. Show a => a -> [Char]
show CV
cv [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" to kind " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> [Char]
forall a. Show a => a -> [Char]
show (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a))

  isConcretely SBV a
s a -> Bool
p
    | Just a
i <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s = a -> Bool
p a
i
    | Bool
True                  = Bool
False

  -- | Generalization of 'Data.SBV.sbvForall'
  sbvForall :: MonadSymbolic m => String -> m (SBV a)
  sbvForall = VarContext -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe [Char] -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL)) (Maybe [Char] -> m (SBV a))
-> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just

  -- | Generalization of 'Data.SBV.sbvForall_'
  sbvForall_ :: MonadSymbolic m => m (SBV a)
  sbvForall_ = VarContext -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe [Char] -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL)) Maybe [Char]
forall a. Maybe a
Nothing

  -- | Generalization of 'Data.SBV.mkForallVars'
  mkForallVars :: MonadSymbolic m => Int -> m [SBV a]
  mkForallVars Int
n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m (SBV a) -> Int -> m (SBV a)
forall a b. a -> b -> a
const m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_) [Int
1 .. Int
n]

  -- | Generalization of 'Data.SBV.sbvExists'
  sbvExists :: MonadSymbolic m => String -> m (SBV a)
  sbvExists = VarContext -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe [Char] -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX)) (Maybe [Char] -> m (SBV a))
-> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just

  -- | Generalization of 'Data.SBV.sbvExists_'
  sbvExists_ :: MonadSymbolic m => m (SBV a)
  sbvExists_ = VarContext -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe [Char] -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX)) Maybe [Char]
forall a. Maybe a
Nothing

  -- | Generalization of 'Data.SBV.mkExistVars'
  mkExistVars :: MonadSymbolic m => Int -> m [SBV a]
  mkExistVars Int
n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m (SBV a) -> Int -> m (SBV a)
forall a b. a -> b -> a
const m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_) [Int
1 .. Int
n]

  -- | Generalization of 'Data.SBV.free'
  free :: MonadSymbolic m => String -> m (SBV a)
  free = VarContext -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe [Char] -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar Maybe Quantifier
forall a. Maybe a
Nothing) (Maybe [Char] -> m (SBV a))
-> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just

  -- | Generalization of 'Data.SBV.free_'
  free_ :: MonadSymbolic m => m (SBV a)
  free_ = VarContext -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe [Char] -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar Maybe Quantifier
forall a. Maybe a
Nothing) Maybe [Char]
forall a. Maybe a
Nothing

  -- | Generalization of 'Data.SBV.mkFreeVars'
  mkFreeVars :: MonadSymbolic m => Int -> m [SBV a]
  mkFreeVars Int
n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m (SBV a) -> Int -> m (SBV a)
forall a b. a -> b -> a
const m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_) [Int
1 .. Int
n]

  -- | Generalization of 'Data.SBV.symbolic'
  symbolic :: MonadSymbolic m => String -> m (SBV a)
  symbolic = [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[Char] -> m (SBV a)
free

  -- | Generalization of 'Data.SBV.symbolics'
  symbolics :: MonadSymbolic m => [String] -> m [SBV a]
  symbolics = ([Char] -> m (SBV a)) -> [[Char]] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[Char] -> m (SBV a)
symbolic

  -- | Extract a literal, if the value is concrete
  unliteral :: SBV a -> Maybe a
  unliteral (SBV (SVal Kind
_ (Left CV
c))) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ CV -> a
forall a. SymVal a => CV -> a
fromCV CV
c
  unliteral SBV a
_                       = Maybe a
forall a. Maybe a
Nothing

  -- | Is the symbolic word concrete?
  isConcrete :: SBV a -> Bool
  isConcrete (SBV (SVal Kind
_ (Left CV
_))) = Bool
True
  isConcrete SBV a
_                       = Bool
False

  -- | Is the symbolic word really symbolic?
  isSymbolic :: SBV a -> Bool
  isSymbolic = Bool -> Bool
not (Bool -> Bool) -> (SBV a -> Bool) -> SBV a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete

instance (Random a, SymVal a) => Random (SBV a) where
  randomR :: (SBV a, SBV a) -> g -> (SBV a, g)
randomR (SBV a
l, SBV a
h) g
g = case (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
l, SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
h) of
                       (Just a
lb, Just a
hb) -> let (a
v, g
g') = (a, a) -> g -> (a, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (a
lb, a
hb) g
g in (a -> SBV a
forall a. SymVal a => a -> SBV a
literal (a
v :: a), g
g')
                       (Maybe a, Maybe a)
_                  -> [Char] -> (SBV a, g)
forall a. HasCallStack => [Char] -> a
error [Char]
"SBV.Random: Cannot generate random values with symbolic bounds"
  random :: g -> (SBV a, g)
random         g
g = let (a
v, g
g') = g -> (a, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g in (a -> SBV a
forall a. SymVal a => a -> SBV a
literal (a
v :: a) , g
g')

---------------------------------------------------------------------------------
-- * Symbolic Arrays
---------------------------------------------------------------------------------

-- | Arrays of symbolic values
-- An @array a b@ is an array indexed by the type @'SBV' a@, with elements of type @'SBV' b@.
--
-- If a default value is supplied, then all the array elements will be initialized to this value.
-- Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce
-- an uninterpreted constant.
--
-- The reason for this class is rather historic. In the past, SBV provided two different kinds of
-- arrays: an `SArray` abstraction that mapped directly to SMTLib arrays  (which is still available
-- today), and a functional notion of arrays that used internal caching, called @SFunArray@. The latter
-- has been removed as the code turned out to be rather tricky and hard to maintain; so we only
-- have one instance of this class. But end users can add their own instances, if needed.
--
-- NB. 'sListArray' insists on a concrete initializer, because not having one would break
-- referential transparency. See https://github.com/LeventErkok/sbv/issues/553 for details.
class SymArray array where
  -- | Generalization of 'Data.SBV.newArray_'
  newArray_      :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
  -- | Generalization of 'Data.SBV.newArray'
  newArray       :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
  -- | Create a literal array
  sListArray     :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b
  -- | Read the array element at @a@
  readArray      :: array a b -> SBV a -> SBV b
  -- | Update the element at @a@ to be @b@
  writeArray     :: SymVal b => array a b -> SBV a -> SBV b -> array a b
  -- | Merge two given arrays on the symbolic condition
  -- Intuitively: @mergeArrays cond a b = if cond then a else b@.
  -- Merging pushes the if-then-else choice down on to elements
  mergeArrays    :: SymVal b => SBV Bool -> array a b -> array a b -> array a b
  -- | Internal function, not exported to the user
  newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b)

  {-# MINIMAL readArray, writeArray, mergeArrays, ((newArray_, newArray) | newArrayInState), sListArray #-}
  newArray_   Maybe (SBV b)
mbVal = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m (array a b)) -> m (array a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (array a b) -> m (array a b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (array a b) -> m (array a b))
-> (State -> IO (array a b)) -> State -> m (array a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
newArrayInState Maybe [Char]
forall a. Maybe a
Nothing   Maybe (SBV b)
mbVal
  newArray [Char]
nm Maybe (SBV b)
mbVal = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m (array a b)) -> m (array a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (array a b) -> m (array a b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (array a b) -> m (array a b))
-> (State -> IO (array a b)) -> State -> m (array a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
newArrayInState ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
nm) Maybe (SBV b)
mbVal

  -- Despite our MINIMAL pragma and default implementations for newArray_ and
  -- newArray, we must provide a dummy implementation for newArrayInState:
  newArrayInState = [Char] -> Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
forall a. HasCallStack => [Char] -> a
error [Char]
"undefined: newArrayInState"

-- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml>
--
--   * Maps directly to SMT-lib arrays
--
--   * Reading from an uninitialized value is OK. If the default value is given in 'newArray', it will
--     be the result. Otherwise, the read yields an uninterpreted constant.
--
--   * Can check for equality of these arrays
--
--   * Cannot be used in code-generation (i.e., compilation to C)
--
--   * Cannot quick-check theorems using @SArray@ values
newtype SArray a b = SArray { SArray a b -> SArr
unSArray :: SArr }

instance (HasKind a, HasKind b) => Show (SArray a b) where
  show :: SArray a b -> [Char]
show SArray{} = [Char]
"SArray<" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy a -> [Char]
forall a. HasKind a => a -> [Char]
showType (Proxy a
forall k (t :: k). Proxy t
Proxy @a) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy b -> [Char]
forall a. HasKind a => a -> [Char]
showType (Proxy b
forall k (t :: k). Proxy t
Proxy @b) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
">"

instance SymArray SArray where
  readArray :: SArray a b -> SBV a -> SBV b
readArray   (SArray SArr
arr) (SBV SVal
a)               = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SArr -> SVal -> SVal
readSArr SArr
arr SVal
a)
  writeArray :: SArray a b -> SBV a -> SBV b -> SArray a b
writeArray  (SArray SArr
arr) (SBV SVal
a)    (SBV SVal
b)    = SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SArr -> SVal -> SVal -> SArr
writeSArr SArr
arr SVal
a SVal
b)
  mergeArrays :: SBool -> SArray a b -> SArray a b -> SArray a b
mergeArrays (SBV SVal
t)      (SArray SArr
a) (SArray SArr
b) = SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SVal -> SArr -> SArr -> SArr
mergeSArr SVal
t SArr
a SArr
b)

  sListArray :: forall a b. (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> SArray a b
  sListArray :: b -> [(SBV a, SBV b)] -> SArray a b
sListArray b
initializer = (SArray a b -> (SBV a, SBV b) -> SArray a b)
-> SArray a b -> [(SBV a, SBV b)] -> SArray a b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((SBV a -> SBV b -> SArray a b) -> (SBV a, SBV b) -> SArray a b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((SBV a -> SBV b -> SArray a b) -> (SBV a, SBV b) -> SArray a b)
-> (SArray a b -> SBV a -> SBV b -> SArray a b)
-> SArray a b
-> (SBV a, SBV b)
-> SArray a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SArray a b -> SBV a -> SBV b -> SArray a b
forall (array :: * -> * -> *) b a.
(SymArray array, SymVal b) =>
array a b -> SBV a -> SBV b -> array a b
writeArray) SArray a b
arr
    where arr :: SArray a b
arr = SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SArr -> SArray a b) -> SArr -> SArray a b
forall a b. (a -> b) -> a -> b
$ (Kind, Kind) -> Cached ArrayIndex -> SArr
SArr (Kind, Kind)
ks (Cached ArrayIndex -> SArr) -> Cached ArrayIndex -> SArr
forall a b. (a -> b) -> a -> b
$ (State -> IO ArrayIndex) -> Cached ArrayIndex
forall a. (State -> IO a) -> Cached a
cache State -> IO ArrayIndex
r
           where ks :: (Kind, Kind)
ks   = (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b))
                 r :: State -> IO ArrayIndex
r State
st = do ArrayMap
amap <- IORef ArrayMap -> IO ArrayMap
forall a. IORef a -> IO a
R.readIORef (State -> IORef ArrayMap
rArrayMap State
st)

                           let k :: ArrayIndex
k    = Int -> ArrayIndex
ArrayIndex (Int -> ArrayIndex) -> Int -> ArrayIndex
forall a b. (a -> b) -> a -> b
$ ArrayMap -> Int
forall a. IntMap a -> Int
IMap.size ArrayMap
amap
                               iVal :: SBV b
iVal = b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
initializer

                           SV
iSV <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
iVal

                           let upd :: ArrayMap -> ArrayMap
upd  = Int -> ([Char], (Kind, Kind), ArrayContext) -> ArrayMap -> ArrayMap
forall a. Int -> a -> IntMap a -> IntMap a
IMap.insert (ArrayIndex -> Int
unArrayIndex ArrayIndex
k) ([Char]
"array_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> [Char]
forall a. Show a => a -> [Char]
show ArrayIndex
k, (Kind, Kind)
ks, Maybe SV -> ArrayContext
ArrayFree (SV -> Maybe SV
forall a. a -> Maybe a
Just SV
iSV))

                           ArrayIndex
k ArrayIndex -> IO () -> IO ()
`seq` State
-> (State -> IORef ArrayMap)
-> (ArrayMap -> ArrayMap)
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef ArrayMap
rArrayMap ArrayMap -> ArrayMap
upd (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef ArrayMap) -> (ArrayMap -> ArrayMap) -> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef ArrayMap
rNewArrs ArrayMap -> ArrayMap
upd
                           ArrayIndex -> IO ArrayIndex
forall (m :: * -> *) a. Monad m => a -> m a
return ArrayIndex
k

  newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b)
  newArrayInState :: Maybe [Char] -> Maybe (SBV b) -> State -> IO (SArray a b)
newArrayInState Maybe [Char]
mbNm Maybe (SBV b)
mbVal State
st = do (Kind -> IO ()) -> [Kind] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (State -> Kind -> IO ()
registerKind State
st) [Kind
aknd, Kind
bknd]
                                     SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SArr -> SArray a b) -> IO SArr -> IO (SArray a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> (Kind, Kind) -> (Int -> [Char]) -> Maybe SVal -> IO SArr
newSArr State
st (Kind
aknd, Kind
bknd) (Maybe [Char] -> Int -> [Char]
forall a. Show a => Maybe [Char] -> a -> [Char]
mkNm Maybe [Char]
mbNm) (SBV b -> SVal
forall a. SBV a -> SVal
unSBV (SBV b -> SVal) -> Maybe (SBV b) -> Maybe SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SBV b)
mbVal)
     where mkNm :: Maybe [Char] -> a -> [Char]
mkNm Maybe [Char]
Nothing   a
t = [Char]
"array_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
           mkNm (Just [Char]
nm) a
_ = [Char]
nm
           aknd :: Kind
aknd = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
           bknd :: Kind
bknd = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)