-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Model
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Instance declarations for our symbolic world
-----------------------------------------------------------------------------

{-# LANGUAGE BangPatterns         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DefaultSignatures    #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE Rank2Types           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Core.Model (
    Mergeable(..), Equality(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), Metric(..), minimize, maximize, assertWithPenalty, SIntegral, SFiniteBits(..)
  , ite, iteLazy, sFromIntegral, sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight, (.^)
  , oneIf, genVar, genVar_, forall, forall_, exists, exists_
  , pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed
  , sBool, sBool_, sBools, sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s, sWord32, sWord32_, sWord32s
  , sWord64, sWord64_, sWord64s, sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s, sInt64, sInt64_
  , sInt64s, sInteger, sInteger_, sIntegers, sReal, sReal_, sReals, sFloat, sFloat_, sFloats, sDouble, sDouble_, sDoubles
  , sFPHalf, sFPHalf_, sFPHalfs, sFPBFloat, sFPBFloat_, sFPBFloats, sFPSingle, sFPSingle_, sFPSingles, sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads
  , sFloatingPoint, sFloatingPoint_, sFloatingPoints
  , sChar, sChar_, sChars, sString, sString_, sStrings, sList, sList_, sLists
  , sRational, sRational_, sRationals
  , SymTuple, sTuple, sTuple_, sTuples
  , sEither, sEither_, sEithers, sMaybe, sMaybe_, sMaybes
  , sSet, sSet_, sSets
  , solve
  , slet
  , sRealToSInteger, label, observe, observeIf, sObserve
  , sAssert
  , liftQRem, liftDMod, symbolicMergeWithKind
  , genLiteral, genFromCV, genMkSymVar
  , sbvQuickCheck
  )
  where

import Control.Applicative    (ZipList(ZipList))
import Control.Monad          (when, unless, mplus)
import Control.Monad.Trans    (liftIO)
import Control.Monad.IO.Class (MonadIO)

import GHC.Generics (U1(..), M1(..), (:*:)(..), K1(..))
import qualified GHC.Generics as G

import GHC.Stack

import Data.Array  (Array, Ix, listArray, elems, bounds, rangeSize)
import Data.Bits   (Bits(..))
import Data.Char   (toLower, isDigit)
import Data.Int    (Int8, Int16, Int32, Int64)
import Data.Kind   (Type)
import Data.List   (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7, intercalate, isPrefixOf)
import Data.Maybe  (fromMaybe, mapMaybe)
import Data.String (IsString(..))
import Data.Word   (Word8, Word16, Word32, Word64)

import qualified Data.Set as Set

import Data.Proxy
import Data.Dynamic (fromDynamic, toDyn)

import Test.QuickCheck                         (Testable(..), Arbitrary(..))
import qualified Test.QuickCheck.Test    as QC (isSuccess)
import qualified Test.QuickCheck         as QC (quickCheckResult, counterexample)
import qualified Test.QuickCheck.Monadic as QC (monadicIO, run, assert, pre, monitor)

import qualified Data.Foldable as F (toList)

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

import Data.SBV.Provers.Prover (defaultSMTCfg, SafeResult(..), prove)
import Data.SBV.SMT.SMT        (ThmResult, showModel)

import Data.SBV.Utils.Lib      (isKString)

-- Symbolic-Word class instances

-- | Generate a finite symbolic bitvector, named
genVar :: MonadSymbolic m => VarContext -> Kind -> String -> m (SBV a)
genVar :: VarContext -> Kind -> String -> m (SBV a)
genVar VarContext
q Kind
k = VarContext -> Kind -> Maybe String -> m (SBV a)
forall a (m :: * -> *).
MonadSymbolic m =>
VarContext -> Kind -> Maybe String -> m (SBV a)
mkSymSBV VarContext
q Kind
k (Maybe String -> m (SBV a))
-> (String -> Maybe String) -> String -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
forall a. a -> Maybe a
Just

-- | Generate a finite symbolic bitvector, unnamed
genVar_ :: MonadSymbolic m => VarContext -> Kind -> m (SBV a)
genVar_ :: VarContext -> Kind -> m (SBV a)
genVar_ VarContext
q Kind
k = VarContext -> Kind -> Maybe String -> m (SBV a)
forall a (m :: * -> *).
MonadSymbolic m =>
VarContext -> Kind -> Maybe String -> m (SBV a)
mkSymSBV VarContext
q Kind
k Maybe String
forall a. Maybe a
Nothing

-- | Generate a finite constant bitvector
genLiteral :: Integral a => Kind -> a -> SBV b
genLiteral :: Kind -> a -> SBV b
genLiteral Kind
k = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SVal -> SBV b) -> (a -> SVal) -> a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (a -> Either CV (Cached SV)) -> a -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (a -> CV) -> a -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> a -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k

-- | Convert a constant to an integral value
genFromCV :: Integral a => CV -> a
genFromCV :: CV -> a
genFromCV (CV Kind
_ (CInteger Integer
x)) = Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
x
genFromCV CV
c                   = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"genFromCV: Unsupported non-integral value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

-- | Generalization of 'Data.SBV.genMkSymVar'
genMkSymVar :: MonadSymbolic m => Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar :: Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
k VarContext
mbq Maybe String
Nothing  = VarContext -> Kind -> m (SBV a)
forall (m :: * -> *) a.
MonadSymbolic m =>
VarContext -> Kind -> m (SBV a)
genVar_ VarContext
mbq Kind
k
genMkSymVar Kind
k VarContext
mbq (Just String
s) = VarContext -> Kind -> String -> m (SBV a)
forall (m :: * -> *) a.
MonadSymbolic m =>
VarContext -> Kind -> String -> m (SBV a)
genVar  VarContext
mbq Kind
k String
s

instance SymVal Bool where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Bool)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Bool)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KBool
  literal :: Bool -> SBV Bool
literal  = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SBV Bool) -> (Bool -> SVal) -> Bool -> SBV Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SVal
svBool
  fromCV :: CV -> Bool
fromCV   = CV -> Bool
cvToBool

instance SymVal Word8 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Word8)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Word8)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
False Int
8)
  literal :: Word8 -> SBV Word8
literal  = Kind -> Word8 -> SBV Word8
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
False Int
8)
  fromCV :: CV -> Word8
fromCV   = CV -> Word8
forall a. Integral a => CV -> a
genFromCV

instance SymVal Int8 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Int8)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Int8)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
True Int
8)
  literal :: Int8 -> SBV Int8
literal  = Kind -> Int8 -> SBV Int8
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
True Int
8)
  fromCV :: CV -> Int8
fromCV   = CV -> Int8
forall a. Integral a => CV -> a
genFromCV

instance SymVal Word16 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Word16)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Word16)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
False Int
16)
  literal :: Word16 -> SBV Word16
literal  = Kind -> Word16 -> SBV Word16
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
False Int
16)
  fromCV :: CV -> Word16
fromCV   = CV -> Word16
forall a. Integral a => CV -> a
genFromCV

instance SymVal Int16 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Int16)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Int16)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
True Int
16)
  literal :: Int16 -> SBV Int16
literal  = Kind -> Int16 -> SBV Int16
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
True Int
16)
  fromCV :: CV -> Int16
fromCV   = CV -> Int16
forall a. Integral a => CV -> a
genFromCV

instance SymVal Word32 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Word32)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Word32)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
False Int
32)
  literal :: Word32 -> SBV Word32
literal  = Kind -> Word32 -> SBV Word32
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
False Int
32)
  fromCV :: CV -> Word32
fromCV   = CV -> Word32
forall a. Integral a => CV -> a
genFromCV

instance SymVal Int32 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Int32)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Int32)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
True Int
32)
  literal :: Int32 -> SBV Int32
literal  = Kind -> Int32 -> SBV Int32
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
True Int
32)
  fromCV :: CV -> Int32
fromCV   = CV -> Int32
forall a. Integral a => CV -> a
genFromCV

instance SymVal Word64 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Word64)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Word64)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
False Int
64)
  literal :: Word64 -> SBV Word64
literal  = Kind -> Word64 -> SBV Word64
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
False Int
64)
  fromCV :: CV -> Word64
fromCV   = CV -> Word64
forall a. Integral a => CV -> a
genFromCV

instance SymVal Int64 where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Int64)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Int64)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Bool -> Int -> Kind
KBounded Bool
True Int
64)
  literal :: Int64 -> SBV Int64
literal  = Kind -> Int64 -> SBV Int64
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (Bool -> Int -> Kind
KBounded Bool
True Int
64)
  fromCV :: CV -> Int64
fromCV   = CV -> Int64
forall a. Integral a => CV -> a
genFromCV

instance SymVal Integer where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Integer)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Integer)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KUnbounded
  literal :: Integer -> SBV Integer
literal  = SVal -> SBV Integer
forall a. SVal -> SBV a
SBV (SVal -> SBV Integer)
-> (Integer -> SVal) -> Integer -> SBV Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KUnbounded (Either CV (Cached SV) -> SVal)
-> (Integer -> Either CV (Cached SV)) -> Integer -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (Integer -> CV) -> Integer -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
KUnbounded
  fromCV :: CV -> Integer
fromCV   = CV -> Integer
forall a. Integral a => CV -> a
genFromCV

instance SymVal Rational where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Rational)
mkSymVal                    = Kind -> VarContext -> Maybe String -> m (SBV Rational)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KRational
  literal :: Rational -> SBV Rational
literal                     = SVal -> SBV Rational
forall a. SVal -> SBV a
SBV (SVal -> SBV Rational)
-> (Rational -> SVal) -> Rational -> SBV Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KRational  (Either CV (Cached SV) -> SVal)
-> (Rational -> Either CV (Cached SV)) -> Rational -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (Rational -> CV) -> Rational -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
KRational (CVal -> CV) -> (Rational -> CVal) -> Rational -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> CVal
CRational
  fromCV :: CV -> Rational
fromCV (CV Kind
_ (CRational Rational
r)) = Rational
r
  fromCV CV
c                    = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ String
"SymVal.Rational: Unexpected non-rational value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

instance SymVal AlgReal where
  mkSymVal :: VarContext -> Maybe String -> m (SBV AlgReal)
mkSymVal                   = Kind -> VarContext -> Maybe String -> m (SBV AlgReal)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KReal
  literal :: AlgReal -> SBV AlgReal
literal                    = SVal -> SBV AlgReal
forall a. SVal -> SBV a
SBV (SVal -> SBV AlgReal)
-> (AlgReal -> SVal) -> AlgReal -> SBV AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KReal (Either CV (Cached SV) -> SVal)
-> (AlgReal -> Either CV (Cached SV)) -> AlgReal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (AlgReal -> CV) -> AlgReal -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
KReal (CVal -> CV) -> (AlgReal -> CVal) -> AlgReal -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgReal -> CVal
CAlgReal
  fromCV :: CV -> AlgReal
fromCV (CV Kind
_ (CAlgReal AlgReal
a)) = AlgReal
a
  fromCV CV
c                   = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ String
"SymVal.AlgReal: Unexpected non-real value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

  -- AlgReal needs its own definition of isConcretely
  -- to make sure we avoid using unimplementable Haskell functions
  isConcretely :: SBV AlgReal -> (AlgReal -> Bool) -> Bool
isConcretely (SBV (SVal Kind
KReal (Left (CV Kind
KReal (CAlgReal AlgReal
v))))) AlgReal -> Bool
p
     | AlgReal -> Bool
isExactRational AlgReal
v = AlgReal -> Bool
p AlgReal
v
  isConcretely SBV AlgReal
_ AlgReal -> Bool
_       = Bool
False

instance SymVal Float where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Float)
mkSymVal                 = Kind -> VarContext -> Maybe String -> m (SBV Float)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KFloat
  literal :: Float -> SBV Float
literal                  = SVal -> SBV Float
forall a. SVal -> SBV a
SBV (SVal -> SBV Float) -> (Float -> SVal) -> Float -> SBV Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KFloat (Either CV (Cached SV) -> SVal)
-> (Float -> Either CV (Cached SV)) -> Float -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (Float -> CV) -> Float -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
KFloat (CVal -> CV) -> (Float -> CVal) -> Float -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> CVal
CFloat
  fromCV :: CV -> Float
fromCV (CV Kind
_ (CFloat Float
a)) = Float
a
  fromCV CV
c                 = String -> Float
forall a. HasCallStack => String -> a
error (String -> Float) -> String -> Float
forall a b. (a -> b) -> a -> b
$ String
"SymVal.Float: Unexpected non-float value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

  -- For Float, we conservatively return 'False' for isConcretely. The reason is that
  -- this function is used for optimizations when only one of the argument is concrete,
  -- and in the presence of NaN's it would be incorrect to do any optimization
  isConcretely :: SBV Float -> (Float -> Bool) -> Bool
isConcretely SBV Float
_ Float -> Bool
_ = Bool
False

instance SymVal Double where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Double)
mkSymVal                  = Kind -> VarContext -> Maybe String -> m (SBV Double)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KDouble
  literal :: Double -> SBV Double
literal                   = SVal -> SBV Double
forall a. SVal -> SBV a
SBV (SVal -> SBV Double) -> (Double -> SVal) -> Double -> SBV Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KDouble (Either CV (Cached SV) -> SVal)
-> (Double -> Either CV (Cached SV)) -> Double -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (Double -> CV) -> Double -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
KDouble (CVal -> CV) -> (Double -> CVal) -> Double -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> CVal
CDouble
  fromCV :: CV -> Double
fromCV (CV Kind
_ (CDouble Double
a)) = Double
a
  fromCV CV
c                  = String -> Double
forall a. HasCallStack => String -> a
error (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ String
"SymVal.Double: Unexpected non-double value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

  -- For Double, we conservatively return 'False' for isConcretely. The reason is that
  -- this function is used for optimizations when only one of the argument is concrete,
  -- and in the presence of NaN's it would be incorrect to do any optimization
  isConcretely :: SBV Double -> (Double -> Bool) -> Bool
isConcretely SBV Double
_ Double -> Bool
_ = Bool
False

instance SymVal Char where
  mkSymVal :: VarContext -> Maybe String -> m (SBV Char)
mkSymVal                = Kind -> VarContext -> Maybe String -> m (SBV Char)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KChar
  literal :: Char -> SBV Char
literal Char
c               = SVal -> SBV Char
forall a. SVal -> SBV a
SBV (SVal -> SBV Char) -> (CVal -> SVal) -> CVal -> SBV Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KChar (Either CV (Cached SV) -> SVal)
-> (CVal -> Either CV (Cached SV)) -> CVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (CVal -> CV) -> CVal -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
KChar (CVal -> SBV Char) -> CVal -> SBV Char
forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar Char
c
  fromCV :: CV -> Char
fromCV (CV Kind
_ (CChar Char
a)) = Char
a
  fromCV CV
c                = String -> Char
forall a. HasCallStack => String -> a
error (String -> Char) -> String -> Char
forall a b. (a -> b) -> a -> b
$ String
"SymVal.String: Unexpected non-char value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

instance SymVal a => SymVal [a] where
  mkSymVal :: VarContext -> Maybe String -> m (SBV [a])
mkSymVal
    | [a] -> Bool
forall a. Typeable a => a -> Bool
isKString @[a] [a]
forall a. HasCallStack => a
undefined = Kind -> VarContext -> Maybe String -> m (SBV [a])
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar Kind
KString
    | Bool
True                     = Kind -> VarContext -> Maybe String -> m (SBV [a])
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Kind -> Kind
KList (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))

  literal :: [a] -> SBV [a]
literal [a]
as
    | [a] -> Bool
forall a. Typeable a => a -> Bool
isKString @[a] [a]
forall a. HasCallStack => a
undefined = case Dynamic -> Maybe String
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic ([a] -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn [a]
as) of
                                   Just String
s  -> SVal -> SBV [a]
forall a. SVal -> SBV a
SBV (SVal -> SBV [a]) -> (String -> SVal) -> String -> SBV [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KString (Either CV (Cached SV) -> SVal)
-> (String -> Either CV (Cached SV)) -> String -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (String -> CV) -> String -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
KString (CVal -> CV) -> (String -> CVal) -> String -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> CVal
CString (String -> SBV [a]) -> String -> SBV [a]
forall a b. (a -> b) -> a -> b
$ String
s
                                   Maybe String
Nothing -> String -> SBV [a]
forall a. HasCallStack => String -> a
error String
"SString: Cannot construct literal string!"
    | Bool
True                     = let k :: Kind
k = Kind -> Kind
KList (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a))
                                 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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CList ([CVal] -> CVal) -> [CVal] -> CVal
forall a b. (a -> b) -> a -> b
$ (a -> CVal) -> [a] -> [CVal]
forall a b. (a -> b) -> [a] -> [b]
map a -> CVal
forall a. SymVal a => a -> CVal
toCV [a]
as

  fromCV :: CV -> [a]
fromCV (CV Kind
_ (CString String
a)) = [a] -> Maybe [a] -> [a]
forall a. a -> Maybe a -> a
fromMaybe (String -> [a]
forall a. HasCallStack => String -> a
error String
"SString: Cannot extract a literal string!")
                                        (Dynamic -> Maybe [a]
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic (String -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn String
a))
  fromCV (CV Kind
_ (CList [CVal]
a))   = CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> (CVal -> CV) -> CVal -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)) (CVal -> a) -> [CVal] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CVal]
a
  fromCV CV
c                  = String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ String
"SymVal.fromCV: Unexpected non-list value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

instance ValidFloat eb sb => HasKind (FloatingPoint eb sb) where
  kindOf :: FloatingPoint eb sb -> Kind
kindOf FloatingPoint eb sb
_ = Int -> Int -> Kind
KFP (Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb))

instance ValidFloat eb sb => SymVal (FloatingPoint eb sb) where
  mkSymVal :: VarContext -> Maybe String -> m (SBV (FloatingPoint eb sb))
mkSymVal                   = Kind -> VarContext -> Maybe String -> m (SBV (FloatingPoint eb sb))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Int -> Int -> Kind
KFP (Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb)))
  literal :: FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
literal (FloatingPoint FP
r)  = let k :: Kind
k = Int -> Int -> Kind
KFP (Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy eb
forall k (t :: k). Proxy t
Proxy @eb)) (Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy sb
forall k (t :: k). Proxy t
Proxy @sb))
                               in SVal -> SBV (FloatingPoint eb sb)
forall a. SVal -> SBV a
SBV (SVal -> SBV (FloatingPoint eb sb))
-> SVal -> SBV (FloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (FP -> CVal
CFP FP
r)
  fromCV :: CV -> FloatingPoint eb sb
fromCV  (CV Kind
_ (CFP FP
r))     = FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint FP
r
  fromCV  CV
c                  = String -> FloatingPoint eb sb
forall a. HasCallStack => String -> a
error (String -> FloatingPoint eb sb) -> String -> FloatingPoint eb sb
forall a b. (a -> b) -> a -> b
$ String
"SymVal.FPR: Unexpected non-arbitrary-precision value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
c

toCV :: SymVal a => a -> CVal
toCV :: a -> CVal
toCV a
a = case a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
a of
           SBV (SVal Kind
_ (Left CV
cv)) -> CV -> CVal
cvVal CV
cv
           SBV a
_                      -> String -> CVal
forall a. HasCallStack => String -> a
error String
"SymVal.toCV: Impossible happened, couldn't produce a concrete value"

mkCVTup :: Int -> Kind -> [CVal] -> SBV a
mkCVTup :: Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
i k :: Kind
k@(KTuple [Kind]
ks) [CVal]
cs
  | Int
lks Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lcs Bool -> Bool -> Bool
&& Int
lks Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i
  = 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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CTuple [CVal]
cs
  | Bool
True
  = String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"SymVal.mkCVTup: Impossible happened. Malformed tuple received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Kind) -> String
forall a. Show a => a -> String
show (Int
i, Kind
k)
   where lks :: Int
lks = [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks
         lcs :: Int
lcs = [CVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
cs
mkCVTup Int
i Kind
k [CVal]
_
  = String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"SymVal.mkCVTup: Impossible happened. Non-tuple received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Kind) -> String
forall a. Show a => a -> String
show (Int
i, Kind
k)

fromCVTup :: Int -> CV -> [CV]
fromCVTup :: Int -> CV -> [CV]
fromCVTup Int
i inp :: CV
inp@(CV (KTuple [Kind]
ks) (CTuple [CVal]
cs))
   | Int
lks Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lcs Bool -> Bool -> Bool
&& Int
lks Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i
   = (Kind -> CVal -> CV) -> [Kind] -> [CVal] -> [CV]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Kind -> CVal -> CV
CV [Kind]
ks [CVal]
cs
   | Bool
True
   = String -> [CV]
forall a. HasCallStack => String -> a
error (String -> [CV]) -> String -> [CV]
forall a b. (a -> b) -> a -> b
$ String
"SymVal.fromCTup: Impossible happened. Malformed tuple received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, CV) -> String
forall a. Show a => a -> String
show (Int
i, CV
inp)
   where lks :: Int
lks = [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks
         lcs :: Int
lcs = [CVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
cs
fromCVTup Int
i CV
inp = String -> [CV]
forall a. HasCallStack => String -> a
error (String -> [CV]) -> String -> [CV]
forall a b. (a -> b) -> a -> b
$ String
"SymVal.fromCVTup: Impossible happened. Non-tuple received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, CV) -> String
forall a. Show a => a -> String
show (Int
i, CV
inp)

instance (SymVal a, SymVal b) => SymVal (Either a b) where
  mkSymVal :: VarContext -> Maybe String -> m (SBV (Either a b))
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV (Either a b))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (Either a b) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (Either a b)
forall k (t :: k). Proxy t
Proxy @(Either a b)))

  literal :: Either a b -> SBV (Either a b)
literal Either a b
s
    | Left  a
a <- Either a b
s = Either CVal CVal -> SBV (Either a b)
mk (Either CVal CVal -> SBV (Either a b))
-> Either CVal CVal -> SBV (Either a b)
forall a b. (a -> b) -> a -> b
$ CVal -> Either CVal CVal
forall a b. a -> Either a b
Left  (a -> CVal
forall a. SymVal a => a -> CVal
toCV a
a)
    | Right b
b <- Either a b
s = Either CVal CVal -> SBV (Either a b)
mk (Either CVal CVal -> SBV (Either a b))
-> Either CVal CVal -> SBV (Either a b)
forall a b. (a -> b) -> a -> b
$ CVal -> Either CVal CVal
forall a b. b -> Either a b
Right (b -> CVal
forall a. SymVal a => a -> CVal
toCV b
b)
    where k :: Kind
k  = Proxy (Either a b) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (Either a b)
forall k (t :: k). Proxy t
Proxy @(Either a b))

          mk :: Either CVal CVal -> SBV (Either a b)
mk = SVal -> SBV (Either a b)
forall a. SVal -> SBV a
SBV (SVal -> SBV (Either a b))
-> (Either CVal CVal -> SVal)
-> Either CVal CVal
-> SBV (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (Either CVal CVal -> Either CV (Cached SV))
-> Either CVal CVal
-> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (Either CVal CVal -> CV)
-> Either CVal CVal
-> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV)
-> (Either CVal CVal -> CVal) -> Either CVal CVal -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either CVal CVal -> CVal
CEither

  fromCV :: CV -> Either a b
fromCV (CV (KEither Kind
k1 Kind
_ ) (CEither (Left CVal
c)))  = a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> CV -> a
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k1 CVal
c
  fromCV (CV (KEither Kind
_  Kind
k2) (CEither (Right CVal
c))) = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ CV -> b
forall a. SymVal a => CV -> a
fromCV (CV -> b) -> CV -> b
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k2 CVal
c
  fromCV CV
bad                                   = String -> Either a b
forall a. HasCallStack => String -> a
error (String -> Either a b) -> String -> Either a b
forall a b. (a -> b) -> a -> b
$ String
"SymVal.fromCV (Either): Malformed either received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
bad

instance SymVal a => SymVal (Maybe a) where
  mkSymVal :: VarContext -> Maybe String -> m (SBV (Maybe a))
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV (Maybe a))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (Maybe a) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (Maybe a)
forall k (t :: k). Proxy t
Proxy @(Maybe a)))

  literal :: Maybe a -> SBV (Maybe a)
literal Maybe a
s
    | Maybe a
Nothing <- Maybe a
s = Maybe CVal -> SBV (Maybe a)
mk Maybe CVal
forall a. Maybe a
Nothing
    | Just  a
a <- Maybe a
s = Maybe CVal -> SBV (Maybe a)
mk (Maybe CVal -> SBV (Maybe a)) -> Maybe CVal -> SBV (Maybe a)
forall a b. (a -> b) -> a -> b
$ CVal -> Maybe CVal
forall a. a -> Maybe a
Just (a -> CVal
forall a. SymVal a => a -> CVal
toCV a
a)
    where k :: Kind
k = Proxy (Maybe a) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (Maybe a)
forall k (t :: k). Proxy t
Proxy @(Maybe a))

          mk :: Maybe CVal -> SBV (Maybe a)
mk = SVal -> SBV (Maybe a)
forall a. SVal -> SBV a
SBV (SVal -> SBV (Maybe a))
-> (Maybe CVal -> SVal) -> Maybe CVal -> SBV (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (Maybe CVal -> Either CV (Cached SV)) -> Maybe CVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (Maybe CVal -> CV) -> Maybe CVal -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (Maybe CVal -> CVal) -> Maybe CVal -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe CVal -> CVal
CMaybe

  fromCV :: CV -> Maybe a
fromCV (CV (KMaybe Kind
_) (CMaybe Maybe CVal
Nothing))  = Maybe a
forall a. Maybe a
Nothing
  fromCV (CV (KMaybe Kind
k) (CMaybe (Just CVal
x))) = 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 -> a) -> CV -> a
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k CVal
x
  fromCV CV
bad                               = String -> Maybe a
forall a. HasCallStack => String -> a
error (String -> Maybe a) -> String -> Maybe a
forall a b. (a -> b) -> a -> b
$ String
"SymVal.fromCV (Maybe): Malformed sum received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
bad

instance (Ord a, SymVal a) => SymVal (RCSet a) where
  mkSymVal :: VarContext -> Maybe String -> m (SBV (RCSet a))
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV (RCSet a))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (RCSet a) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (RCSet a)
forall k (t :: k). Proxy t
Proxy @(RCSet a)))

  literal :: RCSet a -> SBV (RCSet a)
literal RCSet a
eur = SVal -> SBV (RCSet a)
forall a. SVal -> SBV a
SBV (SVal -> SBV (RCSet a)) -> SVal -> SBV (RCSet a)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Set CVal -> RCSet CVal
dir (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
forall a b. (a -> b) -> a -> b
$ (a -> CVal) -> Set a -> Set CVal
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> CVal
forall a. SymVal a => a -> CVal
toCV Set a
s
    where (Set CVal -> RCSet CVal
dir, Set a
s) = case RCSet a
eur of
                      RegularSet Set a
x    -> (Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet,    Set a
x)
                      ComplementSet Set a
x -> (Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet, Set a
x)
          k :: Kind
k        = Proxy (RCSet a) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (RCSet a)
forall k (t :: k). Proxy t
Proxy @(RCSet a))

  fromCV :: CV -> RCSet a
fromCV (CV (KSet Kind
a) (CSet (RegularSet    Set CVal
s))) = Set a -> RCSet a
forall a. Set a -> RCSet a
RegularSet    (Set a -> RCSet a) -> Set a -> RCSet a
forall a b. (a -> b) -> a -> b
$ (CVal -> a) -> Set CVal -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> (CVal -> CV) -> CVal -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
a) Set CVal
s
  fromCV (CV (KSet Kind
a) (CSet (ComplementSet Set CVal
s))) = Set a -> RCSet a
forall a. Set a -> RCSet a
ComplementSet (Set a -> RCSet a) -> Set a -> RCSet a
forall a b. (a -> b) -> a -> b
$ (CVal -> a) -> Set CVal -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> (CVal -> CV) -> CVal -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
a) Set CVal
s
  fromCV CV
bad                                    = String -> RCSet a
forall a. HasCallStack => String -> a
error (String -> RCSet a) -> String -> RCSet a
forall a b. (a -> b) -> a -> b
$ String
"SymVal.fromCV (Set): Malformed set received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
bad

-- | SymVal for 0-tuple (i.e., unit)
instance SymVal () where
  mkSymVal :: VarContext -> Maybe String -> m (SBV ())
mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV ())
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar ([Kind] -> Kind
KTuple [])
  literal :: () -> SBV ()
literal () = Int -> Kind -> [CVal] -> SBV ()
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
0   (Proxy () -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy ()
forall k (t :: k). Proxy t
Proxy @())) []
  fromCV :: CV -> ()
fromCV CV
cv  = Int -> CV -> [CV]
fromCVTup Int
0 CV
cv [CV] -> () -> ()
`seq` ()

-- | SymVal for 2-tuples
instance (SymVal a, SymVal b) => SymVal (a, b) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b))
mkSymVal         = Kind -> VarContext -> Maybe String -> m (SBV (a, b))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b)
forall k (t :: k). Proxy t
Proxy @(a, b)))
   literal :: (a, b) -> SBV (a, b)
literal (a
v1, b
v2) = Int -> Kind -> [CVal] -> SBV (a, b)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
2   (Proxy (a, b) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b)
forall k (t :: k). Proxy t
Proxy @(a, b))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2]
   fromCV :: CV -> (a, b)
fromCV  CV
cv       = let ~[CV
v1, CV
v2] = Int -> CV -> [CV]
fromCVTup Int
2 CV
cv
                      in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2)

-- | SymVal for 3-tuples
instance (SymVal a, SymVal b, SymVal c) => SymVal (a, b, c) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b, c))
mkSymVal             = Kind -> VarContext -> Maybe String -> m (SBV (a, b, c))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b, c) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c)
forall k (t :: k). Proxy t
Proxy @(a, b, c)))
   literal :: (a, b, c) -> SBV (a, b, c)
literal (a
v1, b
v2, c
v3) = Int -> Kind -> [CVal] -> SBV (a, b, c)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
3   (Proxy (a, b, c) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c)
forall k (t :: k). Proxy t
Proxy @(a, b, c))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2, c -> CVal
forall a. SymVal a => a -> CVal
toCV c
v3]
   fromCV :: CV -> (a, b, c)
fromCV  CV
cv           = let ~[CV
v1, CV
v2, CV
v3] = Int -> CV -> [CV]
fromCVTup Int
3 CV
cv
                          in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2, CV -> c
forall a. SymVal a => CV -> a
fromCV CV
v3)

-- | SymVal for 4-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d) => SymVal (a, b, c, d) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b, c, d))
mkSymVal                 = Kind -> VarContext -> Maybe String -> m (SBV (a, b, c, d))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b, c, d) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d)))
   literal :: (a, b, c, d) -> SBV (a, b, c, d)
literal (a
v1, b
v2, c
v3, d
v4) = Int -> Kind -> [CVal] -> SBV (a, b, c, d)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
4   (Proxy (a, b, c, d) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2, c -> CVal
forall a. SymVal a => a -> CVal
toCV c
v3, d -> CVal
forall a. SymVal a => a -> CVal
toCV d
v4]
   fromCV :: CV -> (a, b, c, d)
fromCV  CV
cv               = let ~[CV
v1, CV
v2, CV
v3, CV
v4] = Int -> CV -> [CV]
fromCVTup Int
4 CV
cv
                              in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2, CV -> c
forall a. SymVal a => CV -> a
fromCV CV
v3, CV -> d
forall a. SymVal a => CV -> a
fromCV CV
v4)

-- | SymVal for 5-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e) => SymVal (a, b, c, d, e) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b, c, d, e))
mkSymVal                     = Kind -> VarContext -> Maybe String -> m (SBV (a, b, c, d, e))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b, c, d, e) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e)))
   literal :: (a, b, c, d, e) -> SBV (a, b, c, d, e)
literal (a
v1, b
v2, c
v3, d
v4, e
v5) = Int -> Kind -> [CVal] -> SBV (a, b, c, d, e)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
5   (Proxy (a, b, c, d, e) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2, c -> CVal
forall a. SymVal a => a -> CVal
toCV c
v3, d -> CVal
forall a. SymVal a => a -> CVal
toCV d
v4, e -> CVal
forall a. SymVal a => a -> CVal
toCV e
v5]
   fromCV :: CV -> (a, b, c, d, e)
fromCV  CV
cv                   = let ~[CV
v1, CV
v2, CV
v3, CV
v4, CV
v5] = Int -> CV -> [CV]
fromCVTup Int
5 CV
cv
                                  in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2, CV -> c
forall a. SymVal a => CV -> a
fromCV CV
v3, CV -> d
forall a. SymVal a => CV -> a
fromCV CV
v4, CV -> e
forall a. SymVal a => CV -> a
fromCV CV
v5)

-- | SymVal for 6-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f) => SymVal (a, b, c, d, e, f) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b, c, d, e, f))
mkSymVal                         = Kind -> VarContext -> Maybe String -> m (SBV (a, b, c, d, e, f))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b, c, d, e, f) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e, f)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e, f)))
   literal :: (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f)
literal (a
v1, b
v2, c
v3, d
v4, e
v5, f
v6) = Int -> Kind -> [CVal] -> SBV (a, b, c, d, e, f)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
6   (Proxy (a, b, c, d, e, f) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e, f)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e, f))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2, c -> CVal
forall a. SymVal a => a -> CVal
toCV c
v3, d -> CVal
forall a. SymVal a => a -> CVal
toCV d
v4, e -> CVal
forall a. SymVal a => a -> CVal
toCV e
v5, f -> CVal
forall a. SymVal a => a -> CVal
toCV f
v6]
   fromCV :: CV -> (a, b, c, d, e, f)
fromCV  CV
cv                       = let ~[CV
v1, CV
v2, CV
v3, CV
v4, CV
v5, CV
v6] = Int -> CV -> [CV]
fromCVTup Int
6 CV
cv
                                      in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2, CV -> c
forall a. SymVal a => CV -> a
fromCV CV
v3, CV -> d
forall a. SymVal a => CV -> a
fromCV CV
v4, CV -> e
forall a. SymVal a => CV -> a
fromCV CV
v5, CV -> f
forall a. SymVal a => CV -> a
fromCV CV
v6)

-- | SymVal for 7-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g) => SymVal (a, b, c, d, e, f, g) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b, c, d, e, f, g))
mkSymVal                             = Kind -> VarContext -> Maybe String -> m (SBV (a, b, c, d, e, f, g))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b, c, d, e, f, g) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e, f, g)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e, f, g)))
   literal :: (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g)
literal (a
v1, b
v2, c
v3, d
v4, e
v5, f
v6, g
v7) = Int -> Kind -> [CVal] -> SBV (a, b, c, d, e, f, g)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
7   (Proxy (a, b, c, d, e, f, g) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e, f, g)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e, f, g))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2, c -> CVal
forall a. SymVal a => a -> CVal
toCV c
v3, d -> CVal
forall a. SymVal a => a -> CVal
toCV d
v4, e -> CVal
forall a. SymVal a => a -> CVal
toCV e
v5, f -> CVal
forall a. SymVal a => a -> CVal
toCV f
v6, g -> CVal
forall a. SymVal a => a -> CVal
toCV g
v7]
   fromCV :: CV -> (a, b, c, d, e, f, g)
fromCV  CV
cv                           = let ~[CV
v1, CV
v2, CV
v3, CV
v4, CV
v5, CV
v6, CV
v7] = Int -> CV -> [CV]
fromCVTup Int
7 CV
cv
                                          in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2, CV -> c
forall a. SymVal a => CV -> a
fromCV CV
v3, CV -> d
forall a. SymVal a => CV -> a
fromCV CV
v4, CV -> e
forall a. SymVal a => CV -> a
fromCV CV
v5, CV -> f
forall a. SymVal a => CV -> a
fromCV CV
v6, CV -> g
forall a. SymVal a => CV -> a
fromCV CV
v7)

-- | SymVal for 8-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h) => SymVal (a, b, c, d, e, f, g, h) where
   mkSymVal :: VarContext -> Maybe String -> m (SBV (a, b, c, d, e, f, g, h))
mkSymVal                                 = Kind
-> VarContext -> Maybe String -> m (SBV (a, b, c, d, e, f, g, h))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (Proxy (a, b, c, d, e, f, g, h) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e, f, g, h)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e, f, g, h)))
   literal :: (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h)
literal (a
v1, b
v2, c
v3, d
v4, e
v5, f
v6, g
v7, h
v8) = Int -> Kind -> [CVal] -> SBV (a, b, c, d, e, f, g, h)
forall a. Int -> Kind -> [CVal] -> SBV a
mkCVTup Int
8   (Proxy (a, b, c, d, e, f, g, h) -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy (a, b, c, d, e, f, g, h)
forall k (t :: k). Proxy t
Proxy @(a, b, c, d, e, f, g, h))) [a -> CVal
forall a. SymVal a => a -> CVal
toCV a
v1, b -> CVal
forall a. SymVal a => a -> CVal
toCV b
v2, c -> CVal
forall a. SymVal a => a -> CVal
toCV c
v3, d -> CVal
forall a. SymVal a => a -> CVal
toCV d
v4, e -> CVal
forall a. SymVal a => a -> CVal
toCV e
v5, f -> CVal
forall a. SymVal a => a -> CVal
toCV f
v6, g -> CVal
forall a. SymVal a => a -> CVal
toCV g
v7, h -> CVal
forall a. SymVal a => a -> CVal
toCV h
v8]
   fromCV :: CV -> (a, b, c, d, e, f, g, h)
fromCV  CV
cv                               = let ~[CV
v1, CV
v2, CV
v3, CV
v4, CV
v5, CV
v6, CV
v7, CV
v8] = Int -> CV -> [CV]
fromCVTup Int
8 CV
cv
                                              in (CV -> a
forall a. SymVal a => CV -> a
fromCV CV
v1, CV -> b
forall a. SymVal a => CV -> a
fromCV CV
v2, CV -> c
forall a. SymVal a => CV -> a
fromCV CV
v3, CV -> d
forall a. SymVal a => CV -> a
fromCV CV
v4, CV -> e
forall a. SymVal a => CV -> a
fromCV CV
v5, CV -> f
forall a. SymVal a => CV -> a
fromCV CV
v6, CV -> g
forall a. SymVal a => CV -> a
fromCV CV
v7, CV -> h
forall a. SymVal a => CV -> a
fromCV CV
v8)

instance IsString SString where
  fromString :: String -> SString
fromString = String -> SString
forall a. SymVal a => a -> SBV a
literal

------------------------------------------------------------------------------------
-- * Smart constructors for creating symbolic values. These are not strictly
-- necessary, as they are mere aliases for 'symbolic' and 'symbolics', but
-- they nonetheless make programming easier.
------------------------------------------------------------------------------------

-- | Generalization of 'Data.SBV.sBool'
sBool :: MonadSymbolic m => String -> m SBool
sBool :: String -> m (SBV Bool)
sBool = String -> m (SBV Bool)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sBool_'
sBool_ :: MonadSymbolic m => m SBool
sBool_ :: m (SBV Bool)
sBool_ = m (SBV Bool)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sBools'
sBools :: MonadSymbolic m => [String] -> m [SBool]
sBools :: [String] -> m [SBV Bool]
sBools = [String] -> m [SBV Bool]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sWord8'
sWord8 :: MonadSymbolic m => String -> m SWord8
sWord8 :: String -> m (SBV Word8)
sWord8 = String -> m (SBV Word8)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sWord8_'
sWord8_ :: MonadSymbolic m => m SWord8
sWord8_ :: m (SBV Word8)
sWord8_ = m (SBV Word8)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sWord8s'
sWord8s :: MonadSymbolic m => [String] -> m [SWord8]
sWord8s :: [String] -> m [SBV Word8]
sWord8s = [String] -> m [SBV Word8]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sWord16'
sWord16 :: MonadSymbolic m => String -> m SWord16
sWord16 :: String -> m (SBV Word16)
sWord16 = String -> m (SBV Word16)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sWord16_'
sWord16_ :: MonadSymbolic m => m SWord16
sWord16_ :: m (SBV Word16)
sWord16_ = m (SBV Word16)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sWord16s'
sWord16s :: MonadSymbolic m => [String] -> m [SWord16]
sWord16s :: [String] -> m [SBV Word16]
sWord16s = [String] -> m [SBV Word16]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sWord32'
sWord32 :: MonadSymbolic m => String -> m SWord32
sWord32 :: String -> m (SBV Word32)
sWord32 = String -> m (SBV Word32)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sWord32_'
sWord32_ :: MonadSymbolic m => m SWord32
sWord32_ :: m (SBV Word32)
sWord32_ = m (SBV Word32)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sWord32s'
sWord32s :: MonadSymbolic m => [String] -> m [SWord32]
sWord32s :: [String] -> m [SBV Word32]
sWord32s = [String] -> m [SBV Word32]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sWord64'
sWord64 :: MonadSymbolic m => String -> m SWord64
sWord64 :: String -> m (SBV Word64)
sWord64 = String -> m (SBV Word64)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sWord64_'
sWord64_ :: MonadSymbolic m => m SWord64
sWord64_ :: m (SBV Word64)
sWord64_ = m (SBV Word64)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sWord64s'
sWord64s :: MonadSymbolic m => [String] -> m [SWord64]
sWord64s :: [String] -> m [SBV Word64]
sWord64s = [String] -> m [SBV Word64]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInt8'
sInt8 :: MonadSymbolic m => String -> m SInt8
sInt8 :: String -> m (SBV Int8)
sInt8 = String -> m (SBV Int8)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInt8_'
sInt8_ :: MonadSymbolic m => m SInt8
sInt8_ :: m (SBV Int8)
sInt8_ = m (SBV Int8)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sInt8s'
sInt8s :: MonadSymbolic m => [String] -> m [SInt8]
sInt8s :: [String] -> m [SBV Int8]
sInt8s = [String] -> m [SBV Int8]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInt16'
sInt16 :: MonadSymbolic m => String -> m SInt16
sInt16 :: String -> m (SBV Int16)
sInt16 = String -> m (SBV Int16)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInt16_'
sInt16_ :: MonadSymbolic m => m SInt16
sInt16_ :: m (SBV Int16)
sInt16_ = m (SBV Int16)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sInt16s'
sInt16s :: MonadSymbolic m => [String] -> m [SInt16]
sInt16s :: [String] -> m [SBV Int16]
sInt16s = [String] -> m [SBV Int16]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInt32'
sInt32 :: MonadSymbolic m => String -> m SInt32
sInt32 :: String -> m (SBV Int32)
sInt32 = String -> m (SBV Int32)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInt32_'
sInt32_ :: MonadSymbolic m => m SInt32
sInt32_ :: m (SBV Int32)
sInt32_ = m (SBV Int32)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sInt32s'
sInt32s :: MonadSymbolic m => [String] -> m [SInt32]
sInt32s :: [String] -> m [SBV Int32]
sInt32s = [String] -> m [SBV Int32]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInt64'
sInt64 :: MonadSymbolic m => String -> m SInt64
sInt64 :: String -> m (SBV Int64)
sInt64 = String -> m (SBV Int64)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInt64_'
sInt64_ :: MonadSymbolic m => m SInt64
sInt64_ :: m (SBV Int64)
sInt64_ = m (SBV Int64)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sInt64s'
sInt64s :: MonadSymbolic m => [String] -> m [SInt64]
sInt64s :: [String] -> m [SBV Int64]
sInt64s = [String] -> m [SBV Int64]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInteger'
sInteger:: MonadSymbolic m => String -> m SInteger
sInteger :: String -> m (SBV Integer)
sInteger = String -> m (SBV Integer)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInteger_'
sInteger_:: MonadSymbolic m => m SInteger
sInteger_ :: m (SBV Integer)
sInteger_ = m (SBV Integer)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sIntegers'
sIntegers :: MonadSymbolic m => [String] -> m [SInteger]
sIntegers :: [String] -> m [SBV Integer]
sIntegers = [String] -> m [SBV Integer]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sReal'
sReal:: MonadSymbolic m => String -> m SReal
sReal :: String -> m (SBV AlgReal)
sReal = String -> m (SBV AlgReal)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sReal_'
sReal_:: MonadSymbolic m => m SReal
sReal_ :: m (SBV AlgReal)
sReal_ = m (SBV AlgReal)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sReals'
sReals :: MonadSymbolic m => [String] -> m [SReal]
sReals :: [String] -> m [SBV AlgReal]
sReals = [String] -> m [SBV AlgReal]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFloat'
sFloat :: MonadSymbolic m => String -> m SFloat
sFloat :: String -> m (SBV Float)
sFloat = String -> m (SBV Float)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFloat_'
sFloat_ :: MonadSymbolic m => m SFloat
sFloat_ :: m (SBV Float)
sFloat_ = m (SBV Float)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFloats'
sFloats :: MonadSymbolic m => [String] -> m [SFloat]
sFloats :: [String] -> m [SBV Float]
sFloats = [String] -> m [SBV Float]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sDouble'
sDouble :: MonadSymbolic m => String -> m SDouble
sDouble :: String -> m (SBV Double)
sDouble = String -> m (SBV Double)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sDouble_'
sDouble_ :: MonadSymbolic m => m SDouble
sDouble_ :: m (SBV Double)
sDouble_ = m (SBV Double)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sDoubles'
sDoubles :: MonadSymbolic m => [String] -> m [SDouble]
sDoubles :: [String] -> m [SBV Double]
sDoubles = [String] -> m [SBV Double]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFPHalf'
sFPHalf :: String -> Symbolic SFPHalf
sFPHalf :: String -> Symbolic SFPHalf
sFPHalf = String -> Symbolic SFPHalf
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFPHalf_'
sFPHalf_ :: Symbolic SFPHalf
sFPHalf_ :: Symbolic SFPHalf
sFPHalf_ = Symbolic SFPHalf
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFPHalfs'
sFPHalfs :: [String] -> Symbolic [SFPHalf]
sFPHalfs :: [String] -> Symbolic [SFPHalf]
sFPHalfs = [String] -> Symbolic [SFPHalf]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFPBFloat'
sFPBFloat :: String -> Symbolic SFPBFloat
sFPBFloat :: String -> Symbolic SFPBFloat
sFPBFloat = String -> Symbolic SFPBFloat
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFPBFloat_'
sFPBFloat_ :: Symbolic SFPBFloat
sFPBFloat_ :: Symbolic SFPBFloat
sFPBFloat_ = Symbolic SFPBFloat
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFPBFloats'
sFPBFloats :: [String] -> Symbolic [SFPBFloat]
sFPBFloats :: [String] -> Symbolic [SFPBFloat]
sFPBFloats = [String] -> Symbolic [SFPBFloat]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFPSingle'
sFPSingle :: String -> Symbolic SFPSingle
sFPSingle :: String -> Symbolic SFPSingle
sFPSingle = String -> Symbolic SFPSingle
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFPSingle_'
sFPSingle_ :: Symbolic SFPSingle
sFPSingle_ :: Symbolic SFPSingle
sFPSingle_ = Symbolic SFPSingle
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFPSingles'
sFPSingles :: [String] -> Symbolic [SFPSingle]
sFPSingles :: [String] -> Symbolic [SFPSingle]
sFPSingles = [String] -> Symbolic [SFPSingle]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFPDouble'
sFPDouble :: String -> Symbolic SFPDouble
sFPDouble :: String -> Symbolic SFPDouble
sFPDouble = String -> Symbolic SFPDouble
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFPDouble_'
sFPDouble_ :: Symbolic SFPDouble
sFPDouble_ :: Symbolic SFPDouble
sFPDouble_ = Symbolic SFPDouble
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFPDoubles'
sFPDoubles :: [String] -> Symbolic [SFPDouble]
sFPDoubles :: [String] -> Symbolic [SFPDouble]
sFPDoubles = [String] -> Symbolic [SFPDouble]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFPQuad'
sFPQuad :: String -> Symbolic SFPQuad
sFPQuad :: String -> Symbolic SFPQuad
sFPQuad = String -> Symbolic SFPQuad
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFPQuad_'
sFPQuad_ :: Symbolic SFPQuad
sFPQuad_ :: Symbolic SFPQuad
sFPQuad_ = Symbolic SFPQuad
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFPQuads'
sFPQuads :: [String] -> Symbolic [SFPQuad]
sFPQuads :: [String] -> Symbolic [SFPQuad]
sFPQuads = [String] -> Symbolic [SFPQuad]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sFloatingPoint'
sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb)
sFloatingPoint :: String -> Symbolic (SFloatingPoint eb sb)
sFloatingPoint = String -> Symbolic (SFloatingPoint eb sb)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sFloatingPoint_'
sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb)
sFloatingPoint_ :: Symbolic (SFloatingPoint eb sb)
sFloatingPoint_ = Symbolic (SFloatingPoint eb sb)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sFloatingPoints'
sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb]
sFloatingPoints :: [String] -> Symbolic [SFloatingPoint eb sb]
sFloatingPoints = [String] -> Symbolic [SFloatingPoint eb sb]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

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

-- | Generalization of 'Data.SBV.sChar_'
sChar_ :: MonadSymbolic m => m SChar
sChar_ :: m (SBV Char)
sChar_ = m (SBV Char)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

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

-- | Generalization of 'Data.SBV.sString'
sString :: MonadSymbolic m => String -> m SString
sString :: String -> m SString
sString = String -> m SString
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sString_'
sString_ :: MonadSymbolic m => m SString
sString_ :: m SString
sString_ = m SString
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sStrings'
sStrings :: MonadSymbolic m => [String] -> m [SString]
sStrings :: [String] -> m [SString]
sStrings = [String] -> m [SString]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sList'
sList :: (SymVal a, MonadSymbolic m) => String -> m (SList a)
sList :: String -> m (SList a)
sList = String -> m (SList a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sList_'
sList_ :: (SymVal a, MonadSymbolic m) => m (SList a)
sList_ :: m (SList a)
sList_ = m (SList a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sLists'
sLists :: (SymVal a, MonadSymbolic m) => [String] -> m [SList a]
sLists :: [String] -> m [SList a]
sLists = [String] -> m [SList a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Identify tuple like things. Note that there are no methods, just instances to control type inference
class SymTuple a
instance SymTuple ()
instance SymTuple (a, b)
instance SymTuple (a, b, c)
instance SymTuple (a, b, c, d)
instance SymTuple (a, b, c, d, e)
instance SymTuple (a, b, c, d, e, f)
instance SymTuple (a, b, c, d, e, f, g)
instance SymTuple (a, b, c, d, e, f, g, h)

-- | Generalization of 'Data.SBV.sTuple'
sTuple :: (SymTuple tup, SymVal tup, MonadSymbolic m) => String -> m (SBV tup)
sTuple :: String -> m (SBV tup)
sTuple = String -> m (SBV tup)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sTuple_'
sTuple_ :: (SymTuple tup, SymVal tup, MonadSymbolic m) => m (SBV tup)
sTuple_ :: m (SBV tup)
sTuple_ = m (SBV tup)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sTuples'
sTuples :: (SymTuple tup, SymVal tup, MonadSymbolic m) => [String] -> m [SBV tup]
sTuples :: [String] -> m [SBV tup]
sTuples = [String] -> m [SBV tup]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sRational'
sRational :: MonadSymbolic m => String -> m SRational
sRational :: String -> m (SBV Rational)
sRational = String -> m (SBV Rational)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sRational_'
sRational_ :: MonadSymbolic m => m SRational
sRational_ :: m (SBV Rational)
sRational_ = m (SBV Rational)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sRationals'
sRationals :: MonadSymbolic m => [String] -> m [SRational]
sRationals :: [String] -> m [SBV Rational]
sRationals = [String] -> m [SBV Rational]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sEither'
sEither :: (SymVal a, SymVal b, MonadSymbolic m) => String -> m (SEither a b)
sEither :: String -> m (SEither a b)
sEither = String -> m (SEither a b)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sEither_'
sEither_ :: (SymVal a, SymVal b, MonadSymbolic m) => m (SEither a b)
sEither_ :: m (SEither a b)
sEither_ = m (SEither a b)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sEithers'
sEithers :: (SymVal a, SymVal b, MonadSymbolic m) => [String] -> m [SEither a b]
sEithers :: [String] -> m [SEither a b]
sEithers = [String] -> m [SEither a b]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sMaybe'
sMaybe :: (SymVal a, MonadSymbolic m) => String -> m (SMaybe a)
sMaybe :: String -> m (SMaybe a)
sMaybe = String -> m (SMaybe a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sMaybe_'
sMaybe_ :: (SymVal a, MonadSymbolic m) => m (SMaybe a)
sMaybe_ :: m (SMaybe a)
sMaybe_ = m (SMaybe a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sMaybes'
sMaybes :: (SymVal a, MonadSymbolic m) => [String] -> m [SMaybe a]
sMaybes :: [String] -> m [SMaybe a]
sMaybes = [String] -> m [SMaybe a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sSet'
sSet :: (Ord a, SymVal a, MonadSymbolic m) => String -> m (SSet a)
sSet :: String -> m (SSet a)
sSet = String -> m (SSet a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sMaybe_'
sSet_ :: (Ord a, SymVal a, MonadSymbolic m) => m (SSet a)
sSet_ :: m (SSet a)
sSet_ = m (SSet a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sMaybes'
sSets :: (Ord a, SymVal a, MonadSymbolic m) => [String] -> m [SSet a]
sSets :: [String] -> m [SSet a]
sSets = [String] -> m [SSet a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.solve'
solve :: MonadSymbolic m => [SBool] -> m SBool
solve :: [SBV Bool] -> m (SBV Bool)
solve = SBV Bool -> m (SBV Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV Bool -> m (SBV Bool))
-> ([SBV Bool] -> SBV Bool) -> [SBV Bool] -> m (SBV Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SBV Bool] -> SBV Bool
sAnd

-- | Convert an SReal to an SInteger. That is, it computes the
-- largest integer @n@ that satisfies @sIntegerToSReal n <= r@
-- essentially giving us the @floor@.
--
-- For instance, @1.3@ will be @1@, but @-1.3@ will be @-2@.
sRealToSInteger :: SReal -> SInteger
sRealToSInteger :: SBV AlgReal -> SBV Integer
sRealToSInteger SBV AlgReal
x
  | Just AlgReal
i <- SBV AlgReal -> Maybe AlgReal
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV AlgReal
x, AlgReal -> Bool
isExactRational AlgReal
i
  = Integer -> SBV Integer
forall a. SymVal a => a -> SBV a
literal (Integer -> SBV Integer) -> Integer -> SBV Integer
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor (AlgReal -> Rational
forall a. Real a => a -> Rational
toRational AlgReal
i)
  | Bool
True
  = SVal -> SBV Integer
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KUnbounded (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y)))
  where y :: State -> IO SV
y State
st = do SV
xsv <- State -> SBV AlgReal -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV AlgReal
x
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KUnbounded (Op -> [SV] -> SBVExpr
SBVApp (Kind -> Kind -> Op
KindCast Kind
KReal Kind
KUnbounded) [SV
xsv])

-- | label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code.
-- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. Compare this to 'observe'
-- which is good for printing counter-examples.
label :: SymVal a => String -> SBV a -> SBV a
label :: String -> SBV a -> SBV a
label String
m SBV a
x
   | Just a
_ <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
x = SBV a
x
   | Bool
True                  = 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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k    = SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
x
        r :: State -> IO SV
r State
st = do SV
xsv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
x
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (String -> Op
Label String
m) [SV
xsv])


-- | Check if an observable name is good.
checkObservableName :: String -> Maybe String
checkObservableName :: String -> Maybe String
checkObservableName String
lbl
  | String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lbl
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"SBV.observe: Bad empty name!"
  | (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
lbl String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
smtLibReservedNames
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"SBV.observe: The name chosen is reserved, please change it!: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
lbl
  | String
"s" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
lbl Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit (Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
1 String
lbl)
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"SBV.observe: Names of the form sXXX are internal to SBV, please use a different name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
lbl
  | Bool
True
  = Maybe String
forall a. Maybe a
Nothing

-- | Observe the value of an expression, if the given condition holds.  Such values are useful in model construction, as they are printed part of a satisfying model, or a
-- counter-example. The same works for quick-check as well. Useful when we want to see intermediate values, or expected/obtained
-- pairs in a particular run. Note that an observed expression is always symbolic, i.e., it won't be constant folded. Compare this to 'label'
-- which is used for putting a label in the generated SMTLib-C code.
observeIf :: SymVal a => (a -> Bool) -> String -> SBV a -> SBV a
observeIf :: (a -> Bool) -> String -> SBV a -> SBV a
observeIf a -> Bool
cond String
m SBV a
x
  | Just String
bad <- String -> Maybe String
checkObservableName String
m
  = String -> SBV a
forall a. HasCallStack => String -> a
error String
bad
  | Bool
True
  = 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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
x
        r :: State -> IO SV
r State
st = do SV
xsv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
x
                  State -> String -> (CV -> Bool) -> SV -> IO ()
recordObservable State
st String
m (a -> Bool
cond (a -> Bool) -> (CV -> a) -> CV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> a
forall a. SymVal a => CV -> a
fromCV) SV
xsv
                  SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
xsv

-- | Observe the value of an expression, unconditionally. See 'observeIf' for a generalized version.
observe :: SymVal a => String -> SBV a -> SBV a
observe :: String -> SBV a -> SBV a
observe = (a -> Bool) -> String -> SBV a -> SBV a
forall a. SymVal a => (a -> Bool) -> String -> SBV a -> SBV a
observeIf (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | A variant of observe that you can use at the top-level. This is useful with quick-check, for instance.
sObserve :: SymVal a => String -> SBV a -> Symbolic ()
sObserve :: String -> SBV a -> Symbolic ()
sObserve String
m SBV a
x
  | Just String
bad <- String -> Maybe String
checkObservableName String
m
  = String -> Symbolic ()
forall a. HasCallStack => String -> a
error String
bad
  | Bool
True
  = do State
st <- SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
       IO () -> Symbolic ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Symbolic ()) -> IO () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do SV
xsv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
x
                   State -> String -> (CV -> Bool) -> SV -> IO ()
recordObservable State
st String
m (Bool -> CV -> Bool
forall a b. a -> b -> a
const Bool
True) SV
xsv

-- | Symbolic Equality. Note that we can't use Haskell's 'Eq' class since Haskell insists on returning Bool
-- Comparing symbolic values will necessarily return a symbolic value.
infix 4 .==, ./=, .===, ./==
class EqSymbolic a where
  -- | Symbolic equality.
  (.==) :: a -> a -> SBool
  -- | Symbolic inequality.
  (./=) :: a -> a -> SBool
  -- | Strong equality. On floats ('SFloat'/'SDouble'), strong equality is object equality; that
  -- is @NaN == NaN@ holds, but @+0 == -0@ doesn't. On other types, (.===) is simply (.==).
  -- Note that (.==) is the /right/ notion of equality for floats per IEEE754 specs, since by
  -- definition @+0 == -0@ and @NaN@ equals no other value including itself. But occasionally
  -- we want to be stronger and state @NaN@ equals @NaN@ and @+0@ and @-0@ are different from
  -- each other. In a context where your type is concrete, simply use `Data.SBV.fpIsEqualObject`. But in
  -- a polymorphic context, use the strong equality instead.
  --
  -- NB. If you do not care about or work with floats, simply use (.==) and (./=).
  (.===) :: a -> a -> SBool
  -- | Negation of strong equality. Equaivalent to negation of (.===) on all types.
  (./==) :: a -> a -> SBool

  -- | Returns (symbolic) 'sTrue' if all the elements of the given list are different.
  distinct :: [a] -> SBool

  -- | Returns (symbolic) `sTrue` if all the elements of the given list are different. The second
  -- list contains exceptions, i.e., if an element belongs to that set, it will be considered
  -- distinct regardless of repetition.
  --
  -- >>> prove $ \a -> distinctExcept [a, a] [0::SInteger] .<=> a .== 0
  -- Q.E.D.
  -- >>> prove $ \a b -> distinctExcept [a, b] [0::SWord8] .<=> (a .== b .=> a .== 0)
  -- Q.E.D.
  -- >>> prove $ \a b c d -> distinctExcept [a, b, c, d] [] .== distinct [a, b, c, (d::SInteger)]
  -- Q.E.D.
  distinctExcept :: [a] -> [a] -> SBool

  -- | Returns (symbolic) 'sTrue' if all the elements of the given list are the same.
  allEqual :: [a] -> SBool

  -- | Symbolic membership test.
  sElem    :: a -> [a] -> SBool

  -- | Symbolic negated membership test.
  sNotElem :: a -> [a] -> SBool

  {-# MINIMAL (.==) #-}

  a
x ./=  a
y = SBV Bool -> SBV Bool
sNot (a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.==  a
y)
  a
x .=== a
y = a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
y
  a
x ./== a
y = SBV Bool -> SBV Bool
sNot (a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.=== a
y)

  allEqual []     = SBV Bool
sTrue
  allEqual (a
x:[a]
xs) = (a -> SBV Bool) -> [a] -> SBV Bool
forall a. (a -> SBV Bool) -> [a] -> SBV Bool
sAll (a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.==) [a]
xs

  -- Default implementation of distinct. Note that we override
  -- this method for the base types to generate better code.
  distinct []     = SBV Bool
sTrue
  distinct (a
x:[a]
xs) = (a -> SBV Bool) -> [a] -> SBV Bool
forall a. (a -> SBV Bool) -> [a] -> SBV Bool
sAll (a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
./=) [a]
xs SBV Bool -> SBV Bool -> SBV Bool
.&& [a] -> SBV Bool
forall a. EqSymbolic a => [a] -> SBV Bool
distinct [a]
xs

  -- Default implementation of distinctExcept. Note that we override
  -- this method for the base types to generate better code.
  distinctExcept [a]
es [a]
ignored = [a] -> SBV Bool
go [a]
es
    where isIgnored :: a -> SBV Bool
isIgnored = (a -> [a] -> SBV Bool
forall a. EqSymbolic a => a -> [a] -> SBV Bool
`sElem` [a]
ignored)

          go :: [a] -> SBV Bool
go []     = SBV Bool
sTrue
          go (a
x:[a]
xs) = let xOK :: SBV Bool
xOK  = a -> SBV Bool
isIgnored a
x SBV Bool -> SBV Bool -> SBV Bool
.|| (a -> SBV Bool) -> [a] -> SBV Bool
forall a. (a -> SBV Bool) -> [a] -> SBV Bool
sAll (\a
y -> a -> SBV Bool
isIgnored a
y SBV Bool -> SBV Bool -> SBV Bool
.|| a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
./= a
y) [a]
xs
                      in SBV Bool
xOK SBV Bool -> SBV Bool -> SBV Bool
.&& [a] -> SBV Bool
go [a]
xs

  a
x `sElem`    [a]
xs = (a -> SBV Bool) -> [a] -> SBV Bool
forall a. (a -> SBV Bool) -> [a] -> SBV Bool
sAny (a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
x) [a]
xs
  a
x `sNotElem` [a]
xs = SBV Bool -> SBV Bool
sNot (a
x a -> [a] -> SBV Bool
forall a. EqSymbolic a => a -> [a] -> SBV Bool
`sElem` [a]
xs)

-- | Symbolic Comparisons. Similar to 'Eq', we cannot implement Haskell's 'Ord' class
-- since there is no way to return an 'Ordering' value from a symbolic comparison.
-- Furthermore, 'OrdSymbolic' requires 'Mergeable' to implement if-then-else, for the
-- benefit of implementing symbolic versions of 'max' and 'min' functions.
infix 4 .<, .<=, .>, .>=
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
  -- | Symbolic less than.
  (.<)  :: a -> a -> SBool
  -- | Symbolic less than or equal to.
  (.<=) :: a -> a -> SBool
  -- | Symbolic greater than.
  (.>)  :: a -> a -> SBool
  -- | Symbolic greater than or equal to.
  (.>=) :: a -> a -> SBool
  -- | Symbolic minimum.
  smin  :: a -> a -> a
  -- | Symbolic maximum.
  smax  :: a -> a -> a
  -- | Is the value within the allowed /inclusive/ range?
  inRange    :: a -> (a, a) -> SBool

  {-# MINIMAL (.<) #-}

  a
a .<= a
b    = a
a a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< a
b SBV Bool -> SBV Bool -> SBV Bool
.|| a
a a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
b
  a
a .>  a
b    = a
b a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<  a
a
  a
a .>= a
b    = a
b a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<= a
a

  a
a `smin` a
b = SBV Bool -> a -> a -> a
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (a
a a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<= a
b) a
a a
b
  a
a `smax` a
b = SBV Bool -> a -> a -> a
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (a
a a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<= a
b) a
b a
a

  inRange a
x (a
y, a
z) = a
x a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= a
y SBV Bool -> SBV Bool -> SBV Bool
.&& a
x a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<= a
z


{- We can't have a generic instance of the form:

instance Eq a => EqSymbolic a where
  x .== y = if x == y then true else sFalse

even if we're willing to allow Flexible/undecidable instances..
This is because if we allow this it would imply EqSymbolic (SBV a);
since (SBV a) has to be Eq as it must be a Num. But this wouldn't be
the right choice obviously; as the Eq instance is bogus for SBV
for natural reasons..
-}

-- It is tempting to put in an @Eq a@ superclass here. But doing so
-- is complicated, as it requires all underlying types to have equality,
-- which is at best shaky for algebraic reals and sets. So, leave it out.
instance EqSymbolic (SBV a) where
  SBV SVal
x .== :: SBV a -> SBV a -> SBV Bool
.== SBV SVal
y = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svEqual SVal
x SVal
y)
  SBV SVal
x ./= :: SBV a -> SBV a -> SBV Bool
./= SBV SVal
y = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svNotEqual SVal
x SVal
y)

  SBV SVal
x .=== :: SBV a -> SBV a -> SBV Bool
.=== SBV SVal
y = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svStrongEqual SVal
x SVal
y)

  -- Custom version of distinct that generates better code for base types
  distinct :: [SBV a] -> SBV Bool
distinct []                                             = SBV Bool
sTrue
  distinct [SBV a
_]                                            = SBV Bool
sTrue
  distinct [SBV a]
xs | (SBV a -> Bool) -> [SBV a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SBV a -> Bool
forall a. SBV a -> Bool
isConc [SBV a]
xs                             = [SBV a] -> SBV Bool
forall a. EqSymbolic a => [a] -> SBV Bool
checkDiff [SBV a]
xs
              | [SBV SVal
a, SBV SVal
b] <- [SBV a]
xs, SVal
a SVal -> SVal -> Bool
`is` Bool -> SVal
svBool Bool
True  = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SBV Bool) -> SVal -> SBV Bool
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svNot SVal
b
              | [SBV SVal
a, SBV SVal
b] <- [SBV a]
xs, SVal
b SVal -> SVal -> Bool
`is` Bool -> SVal
svBool Bool
True  = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SBV Bool) -> SVal -> SBV Bool
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
svNot SVal
a
              | [SBV SVal
a, SBV SVal
b] <- [SBV a]
xs, SVal
a SVal -> SVal -> Bool
`is` Bool -> SVal
svBool Bool
False = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV SVal
b
              | [SBV SVal
a, SBV SVal
b] <- [SBV a]
xs, SVal
b SVal -> SVal -> Bool
`is` Bool -> SVal
svBool Bool
False = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV SVal
a
              | [SBV a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV a]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2 Bool -> Bool -> Bool
&& SBV a -> Bool
forall a. SBV a -> Bool
isBool ([SBV a] -> SBV a
forall a. [a] -> a
head [SBV a]
xs)         = SBV Bool
sFalse
              | Bool
True                                      = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r)))
    where r :: State -> IO SV
r State
st = do [SV]
xsv <- (SBV a -> IO SV) -> [SBV a] -> IO [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st) [SBV a]
xs
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp Op
NotEqual [SV]
xsv)

          -- We call this in case all are concrete, which will
          -- reduce to a constant and generate no code at all!
          -- Note that this is essentially the same as the default
          -- definition, which unfortunately we can no longer call!
          checkDiff :: [a] -> SBV Bool
checkDiff []     = SBV Bool
sTrue
          checkDiff (a
a:[a]
as) = (a -> SBV Bool) -> [a] -> SBV Bool
forall a. (a -> SBV Bool) -> [a] -> SBV Bool
sAll (a
a a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
./=) [a]
as SBV Bool -> SBV Bool -> SBV Bool
.&& [a] -> SBV Bool
checkDiff [a]
as

          -- Sigh, we can't use isConcrete since that requires SymVal
          -- constraint that we don't have here. (To support SBools.)
          isConc :: SBV a -> Bool
isConc (SBV (SVal Kind
_ (Left CV
_))) = Bool
True
          isConc SBV a
_                       = Bool
False

          -- Likewise here; need to go lower.
          SVal Kind
k1 (Left CV
c1) is :: SVal -> SVal -> Bool
`is` SVal Kind
k2 (Left CV
c2) = (Kind
k1, CV
c1) (Kind, CV) -> (Kind, CV) -> Bool
forall a. Eq a => a -> a -> Bool
== (Kind
k2, CV
c2)
          SVal
_                 `is` SVal
_                 = Bool
False

          isBool :: SBV a -> Bool
isBool (SBV (SVal Kind
KBool Either CV (Cached SV)
_)) = Bool
True
          isBool SBV a
_                    = Bool
False

  -- Custom version of distinctExcept that generates better code for base types
  -- We essentially keep track of an array and count cardinalities as we walk along.
  distinctExcept :: [SBV a] -> [SBV a] -> SBV Bool
distinctExcept []  [SBV a]
_       = SBV Bool
sTrue
  distinctExcept [SBV a
_] [SBV a]
_       = SBV Bool
sTrue
  distinctExcept [SBV a]
es  [SBV a]
ignored
     | (SBV a -> Bool) -> [SBV a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SBV a -> Bool
forall a. SBV a -> Bool
isConc ([SBV a]
es [SBV a] -> [SBV a] -> [SBV a]
forall a. [a] -> [a] -> [a]
++ [SBV a]
ignored)
    = [SBV a] -> SBV Bool
forall a. EqSymbolic a => [a] -> SBV Bool
distinct ((SBV a -> Bool) -> [SBV a] -> [SBV a]
forall a. (a -> Bool) -> [a] -> [a]
filter SBV a -> Bool
ignoreConc [SBV a]
es)
    | Bool
True
    = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r)))
    where ignoreConc :: SBV a -> Bool
ignoreConc SBV a
x = case SBV a
x SBV a -> [SBV a] -> SBV Bool
forall a. EqSymbolic a => a -> [a] -> SBV Bool
`sElem` [SBV a]
ignored of
                           SBV (SVal Kind
KBool (Left CV
cv)) -> CV -> Bool
cvToBool CV
cv
                           SBV Bool
_                          -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"distinctExcept: Impossible happened, concrete sElem failed: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SBV a], [SBV a], SBV a) -> String
forall a. Show a => a -> String
show ([SBV a]
es, [SBV a]
ignored, SBV a
x)

          ek :: Kind
ek = case [SBV a] -> SBV a
forall a. [a] -> a
head [SBV a]
es of  -- Head is safe here as we're guaranteed to have a non-empty es by pattern matching above. (Actually, there'll be at least two elements)
                 SBV (SVal Kind
k Either CV (Cached SV)
_) -> Kind
k

          r :: State -> IO SV
r State
st = do let zero :: SBV Integer
zero = SBV Integer
0 :: SInteger

                    SArray a Integer
arr <- SArr -> SArray a Integer
forall a b. SArr -> SArray a b
SArray (SArr -> SArray a Integer) -> IO SArr -> IO (SArray a Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr
newSArr State
st (Kind
ek, Kind
KUnbounded) (\Int
i -> String
"array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) (SVal -> Maybe SVal
forall a. a -> Maybe a
Just (SBV Integer -> SVal
forall a. SBV a -> SVal
unSBV SBV Integer
zero))

                    let incr :: SBV a -> SArray a Integer -> SBV Integer
incr SBV a
x SArray a Integer
table = SBV Bool -> SBV Integer -> SBV Integer -> SBV Integer
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (SBV a
x SBV a -> [SBV a] -> SBV Bool
forall a. EqSymbolic a => a -> [a] -> SBV Bool
`sElem` [SBV a]
ignored) SBV Integer
zero (SBV Integer
1 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SArray a Integer -> SBV a -> SBV Integer
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray a Integer
table SBV a
x)

                        finalArray :: SArray a Integer
finalArray = (SArray a Integer -> SBV a -> SArray a Integer)
-> SArray a Integer -> [SBV a] -> SArray a Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SArray a Integer
table SBV a
x -> SArray a Integer -> SBV a -> SBV Integer -> SArray a Integer
forall (array :: * -> * -> *) b a.
(SymArray array, SymVal b) =>
array a b -> SBV a -> SBV b -> array a b
writeArray SArray a Integer
table SBV a
x (SBV a -> SArray a Integer -> SBV Integer
incr SBV a
x SArray a Integer
table)) SArray a Integer
arr [SBV a]
es

                    State -> SBV Bool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (SBV Bool -> IO SV) -> SBV Bool -> IO SV
forall a b. (a -> b) -> a -> b
$ (SBV a -> SBV Bool) -> [SBV a] -> SBV Bool
forall a. (a -> SBV Bool) -> [a] -> SBV Bool
sAll (\SBV a
e -> SArray a Integer -> SBV a -> SBV Integer
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray a Integer
finalArray SBV a
e SBV Integer -> SBV Integer -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<= SBV Integer
1) [SBV a]
es

          -- Sigh, we can't use isConcrete since that requires SymVal
          -- constraint that we don't have here. (To support SBools.)
          isConc :: SBV a -> Bool
isConc (SBV (SVal Kind
_ (Left CV
_))) = Bool
True
          isConc SBV a
_                       = Bool
False

-- | If comparison is over something SMTLib can handle, just translate it. Otherwise desugar.
instance (Ord a, SymVal a) => OrdSymbolic (SBV a) where
  a :: SBV a
a@(SBV SVal
x) .< :: SBV a -> SBV a -> SBV Bool
.<  b :: SBV a
b@(SBV SVal
y) | String -> SBV a -> SBV a -> Bool
forall a. (SymVal a, HasKind a) => String -> SBV a -> SBV a -> Bool
smtComparable String
"<"   SBV a
a SBV a
b = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svLessThan SVal
x SVal
y)
                          | Bool
True                    = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svStructuralLessThan SVal
x SVal
y)

  a :: SBV a
a@(SBV SVal
x) .<= :: SBV a -> SBV a -> SBV Bool
.<= b :: SBV a
b@(SBV SVal
y) | String -> SBV a -> SBV a -> Bool
forall a. (SymVal a, HasKind a) => String -> SBV a -> SBV a -> Bool
smtComparable String
".<=" SBV a
a SBV a
b = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svLessEq SVal
x SVal
y)
                          | Bool
True                    = SBV a
a SBV a -> SBV a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< SBV a
b SBV Bool -> SBV Bool -> SBV Bool
.|| SBV a
a SBV a -> SBV a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== SBV a
b

  a :: SBV a
a@(SBV SVal
x) .> :: SBV a -> SBV a -> SBV Bool
.>  b :: SBV a
b@(SBV SVal
y) | String -> SBV a -> SBV a -> Bool
forall a. (SymVal a, HasKind a) => String -> SBV a -> SBV a -> Bool
smtComparable String
">"   SBV a
a SBV a
b = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svGreaterThan SVal
x SVal
y)
                          | Bool
True                    = SBV a
b SBV a -> SBV a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< SBV a
a

  a :: SBV a
a@(SBV SVal
x) .>= :: SBV a -> SBV a -> SBV Bool
.>= b :: SBV a
b@(SBV SVal
y) | String -> SBV a -> SBV a -> Bool
forall a. (SymVal a, HasKind a) => String -> SBV a -> SBV a -> Bool
smtComparable String
">="  SBV a
a SBV a
b = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> SVal -> SVal
svGreaterEq SVal
x SVal
y)
                          | Bool
True                    = SBV a
b SBV a -> SBV a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<= SBV a
a

-- Is this a type that's comparable by underlying translation to SMTLib?
-- Note that we allow concrete versions to go through unless the type is a set, as there's really no reason not to.
smtComparable :: (SymVal a, HasKind a) => String -> SBV a -> SBV a -> Bool
smtComparable :: String -> SBV a -> SBV a -> Bool
smtComparable String
op SBV a
x SBV a
y
  | SBV a -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete SBV a
x Bool -> Bool -> Bool
&& SBV a -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete SBV a
y Bool -> Bool -> Bool
&& Bool -> Bool
not (Kind -> Bool
forall a. HasKind a => a -> Bool
isSet Kind
k)
  = Bool
True
  | Bool
True
  = case Kind
k of
      Kind
KBool         -> Bool
True
      KBounded   {} -> Bool
True
      KUnbounded {} -> Bool
True
      KReal      {} -> Bool
True
      KUserSort  {} -> Bool
True
      Kind
KFloat        -> Bool
True
      Kind
KDouble       -> Bool
True
      KRational  {} -> Bool
True
      KFP        {} -> Bool
True
      Kind
KChar         -> Bool
True
      Kind
KString       -> Bool
True
      KList      {} -> Bool
nope     -- Unfortunately, no way for us to desugar this
      KSet       {} -> Bool
nope     -- Ditto here..
      KTuple     {} -> Bool
False
      KMaybe     {} -> Bool
False
      KEither    {} -> Bool
False
 where k :: Kind
k    = SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
x
       nope :: Bool
nope = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.OrdSymbolic: SMTLib does not support " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

-- Bool
instance EqSymbolic Bool where
  Bool
x .== :: Bool -> Bool -> SBV Bool
.== Bool
y = Bool -> SBV Bool
fromBool (Bool -> SBV Bool) -> Bool -> SBV Bool
forall a b. (a -> b) -> a -> b
$ Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y

-- Lists
instance EqSymbolic a => EqSymbolic [a] where
  []     .== :: [a] -> [a] -> SBV Bool
.== []     = SBV Bool
sTrue
  (a
x:[a]
xs) .== (a
y:[a]
ys) = a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
y SBV Bool -> SBV Bool -> SBV Bool
.&& [a]
xs [a] -> [a] -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== [a]
ys
  [a]
_      .== [a]
_      = SBV Bool
sFalse

instance OrdSymbolic a => OrdSymbolic [a] where
  []     .< :: [a] -> [a] -> SBV Bool
.< []     = SBV Bool
sFalse
  []     .< [a]
_      = SBV Bool
sTrue
  [a]
_      .< []     = SBV Bool
sFalse
  (a
x:[a]
xs) .< (a
y:[a]
ys) = a
x a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< a
y SBV Bool -> SBV Bool -> SBV Bool
.|| (a
x a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
y SBV Bool -> SBV Bool -> SBV Bool
.&& [a]
xs [a] -> [a] -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< [a]
ys)

-- Maybe
instance EqSymbolic a => EqSymbolic (Maybe a) where
  Maybe a
Nothing .== :: Maybe a -> Maybe a -> SBV Bool
.== Maybe a
Nothing = SBV Bool
sTrue
  Just a
a  .== Just a
b  = a
a a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
b
  Maybe a
_       .== Maybe a
_       = SBV Bool
sFalse

instance OrdSymbolic a => OrdSymbolic (Maybe a) where
  Maybe a
Nothing .< :: Maybe a -> Maybe a -> SBV Bool
.<  Maybe a
Nothing = SBV Bool
sFalse
  Maybe a
Nothing .<  Maybe a
_       = SBV Bool
sTrue
  Just a
_  .<  Maybe a
Nothing = SBV Bool
sFalse
  Just a
a  .<  Just a
b  = a
a a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< a
b

-- Either
instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) where
  Left a
a  .== :: Either a b -> Either a b -> SBV Bool
.== Left a
b  = a
a a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
b
  Right b
a .== Right b
b = b
a b -> b -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== b
b
  Either a b
_       .== Either a b
_       = SBV Bool
sFalse

instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) where
  Left a
a  .< :: Either a b -> Either a b -> SBV Bool
.< Left a
b  = a
a a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< a
b
  Left a
_  .< Right b
_ = SBV Bool
sTrue
  Right b
_ .< Left a
_  = SBV Bool
sFalse
  Right b
a .< Right b
b = b
a b -> b -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< b
b

-- 2-Tuple
instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) where
  (a
a0, b
b0) .== :: (a, b) -> (a, b) -> SBV Bool
.== (a
a1, b
b1) = a
a0 a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
a1 SBV Bool -> SBV Bool -> SBV Bool
.&& b
b0 b -> b -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== b
b1

instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) where
  (a
a0, b
b0) .< :: (a, b) -> (a, b) -> SBV Bool
.< (a
a1, b
b1) = a
a0 a -> a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< a
a1 SBV Bool -> SBV Bool -> SBV Bool
.|| (a
a0 a -> a -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== a
a1 SBV Bool -> SBV Bool -> SBV Bool
.&& b
b0 b -> b -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< b
b1)

-- 3-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) where
  (a
a0, b
b0, c
c0) .== :: (a, b, c) -> (a, b, c) -> SBV Bool
.== (a
a1, b
b1, c
c1) = (a
a0, b
b0) (a, b) -> (a, b) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1) SBV Bool -> SBV Bool -> SBV Bool
.&& c
c0 c -> c -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== c
c1

instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) where
  (a
a0, b
b0, c
c0) .< :: (a, b, c) -> (a, b, c) -> SBV Bool
.< (a
a1, b
b1, c
c1) = (a
a0, b
b0) (a, b) -> (a, b) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< (a
a1, b
b1) SBV Bool -> SBV Bool -> SBV Bool
.|| ((a
a0, b
b0) (a, b) -> (a, b) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1) SBV Bool -> SBV Bool -> SBV Bool
.&& c
c0 c -> c -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< c
c1)

-- 4-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) where
  (a
a0, b
b0, c
c0, d
d0) .== :: (a, b, c, d) -> (a, b, c, d) -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1) = (a
a0, b
b0, c
c0) (a, b, c) -> (a, b, c) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1) SBV Bool -> SBV Bool -> SBV Bool
.&& d
d0 d -> d -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== d
d1

instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) where
  (a
a0, b
b0, c
c0, d
d0) .< :: (a, b, c, d) -> (a, b, c, d) -> SBV Bool
.< (a
a1, b
b1, c
c1, d
d1) = (a
a0, b
b0, c
c0) (a, b, c) -> (a, b, c) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< (a
a1, b
b1, c
c1) SBV Bool -> SBV Bool -> SBV Bool
.|| ((a
a0, b
b0, c
c0) (a, b, c) -> (a, b, c) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1) SBV Bool -> SBV Bool -> SBV Bool
.&& d
d0 d -> d -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< d
d1)

-- 5-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) where
  (a
a0, b
b0, c
c0, d
d0, e
e0) .== :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1) = (a
a0, b
b0, c
c0, d
d0) (a, b, c, d) -> (a, b, c, d) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1) SBV Bool -> SBV Bool -> SBV Bool
.&& e
e0 e -> e -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== e
e1

instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) where
  (a
a0, b
b0, c
c0, d
d0, e
e0) .< :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBV Bool
.< (a
a1, b
b1, c
c1, d
d1, e
e1) = (a
a0, b
b0, c
c0, d
d0) (a, b, c, d) -> (a, b, c, d) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< (a
a1, b
b1, c
c1, d
d1) SBV Bool -> SBV Bool -> SBV Bool
.|| ((a
a0, b
b0, c
c0, d
d0) (a, b, c, d) -> (a, b, c, d) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1) SBV Bool -> SBV Bool -> SBV Bool
.&& e
e0 e -> e -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< e
e1)

-- 6-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) where
  (a
a0, b
b0, c
c0, d
d0, e
e0, f
f0) .== :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1) = (a
a0, b
b0, c
c0, d
d0, e
e0) (a, b, c, d, e) -> (a, b, c, d, e) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1) SBV Bool -> SBV Bool -> SBV Bool
.&& f
f0 f -> f -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== f
f1

instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) where
  (a
a0, b
b0, c
c0, d
d0, e
e0, f
f0) .< :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBV Bool
.< (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1) =    (a
a0, b
b0, c
c0, d
d0, e
e0) (a, b, c, d, e) -> (a, b, c, d, e) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<  (a
a1, b
b1, c
c1, d
d1, e
e1)
                                                       SBV Bool -> SBV Bool -> SBV Bool
.|| ((a
a0, b
b0, c
c0, d
d0, e
e0) (a, b, c, d, e) -> (a, b, c, d, e) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1) SBV Bool -> SBV Bool -> SBV Bool
.&& f
f0 f -> f -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< f
f1)

-- 7-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) where
  (a
a0, b
b0, c
c0, d
d0, e
e0, f
f0, g
g0) .== :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1, g
g1) = (a
a0, b
b0, c
c0, d
d0, e
e0, f
f0) (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1) SBV Bool -> SBV Bool -> SBV Bool
.&& g
g0 g -> g -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== g
g1

instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) where
  (a
a0, b
b0, c
c0, d
d0, e
e0, f
f0, g
g0) .< :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBV Bool
.< (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1, g
g1) =    (a
a0, b
b0, c
c0, d
d0, e
e0, f
f0) (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.<  (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1)
                                                               SBV Bool -> SBV Bool -> SBV Bool
.|| ((a
a0, b
b0, c
c0, d
d0, e
e0, f
f0) (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== (a
a1, b
b1, c
c1, d
d1, e
e1, f
f1) SBV Bool -> SBV Bool -> SBV Bool
.&& g
g0 g -> g -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.< g
g1)

-- | Symbolic Numbers. This is a simple class that simply incorporates all number like
-- base types together, simplifying writing polymorphic type-signatures that work for all
-- symbolic numbers, such as 'SWord8', 'SInt8' etc. For instance, we can write a generic
-- list-minimum function as follows:
--
-- @
--    mm :: SIntegral a => [SBV a] -> SBV a
--    mm = foldr1 (\a b -> ite (a .<= b) a b)
-- @
--
-- It is similar to the standard 'Integral' class, except ranging over symbolic instances.
class (SymVal a, Num a, Bits a, Integral a) => SIntegral a

-- 'SIntegral' Instances, skips Real/Float/Bool
instance SIntegral Word8
instance SIntegral Word16
instance SIntegral Word32
instance SIntegral Word64
instance SIntegral Int8
instance SIntegral Int16
instance SIntegral Int32
instance SIntegral Int64
instance SIntegral Integer

-- | Finite bit-length symbolic values. Essentially the same as 'SIntegral', but further leaves out 'Integer'. Loosely
-- based on Haskell's @FiniteBits@ class, but with more methods defined and structured differently to fit into the
-- symbolic world view. Minimal complete definition: 'sFiniteBitSize'.
class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where
    -- | Bit size.
    sFiniteBitSize      :: SBV a -> Int
    -- | Least significant bit of a word, always stored at index 0.
    lsb                 :: SBV a -> SBool
    -- | Most significant bit of a word, always stored at the last position.
    msb                 :: SBV a -> SBool
    -- | Big-endian blasting of a word into its bits.
    blastBE             :: SBV a -> [SBool]
    -- | Little-endian blasting of a word into its bits.
    blastLE             :: SBV a -> [SBool]
    -- | Reconstruct from given bits, given in little-endian.
    fromBitsBE          :: [SBool] -> SBV a
    -- | Reconstruct from given bits, given in little-endian.
    fromBitsLE          :: [SBool] -> SBV a
    -- | Replacement for 'testBit', returning 'SBool' instead of 'Bool'.
    sTestBit            :: SBV a -> Int -> SBool
    -- | Variant of 'sTestBit', where we want to extract multiple bit positions.
    sExtractBits        :: SBV a -> [Int] -> [SBool]
    -- | Variant of 'popCount', returning a symbolic value.
    sPopCount           :: SBV a -> SWord8
    -- | A combo of 'setBit' and 'clearBit', when the bit to be set is symbolic.
    setBitTo            :: SBV a -> Int -> SBool -> SBV a
    -- | Full adder, returns carry-out from the addition. Only for unsigned quantities.
    fullAdder           :: SBV a -> SBV a -> (SBool, SBV a)
    -- | Full multiplier, returns both high and low-order bits. Only for unsigned quantities.
    fullMultiplier      :: SBV a -> SBV a -> (SBV a, SBV a)
    -- | Count leading zeros in a word, big-endian interpretation.
    sCountLeadingZeros  :: SBV a -> SWord8
    -- | Count trailing zeros in a word, big-endian interpretation.
    sCountTrailingZeros :: SBV a -> SWord8

    {-# MINIMAL sFiniteBitSize #-}

    -- Default implementations
    lsb (SBV SVal
v) = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> Int -> SVal
svTestBit SVal
v Int
0)
    msb SBV a
x       = SBV a -> Int -> SBV Bool
forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV a
x (SBV a -> Int
forall a. SFiniteBits a => SBV a -> Int
sFiniteBitSize SBV a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

    blastBE   = [SBV Bool] -> [SBV Bool]
forall a. [a] -> [a]
reverse ([SBV Bool] -> [SBV Bool])
-> (SBV a -> [SBV Bool]) -> SBV a -> [SBV Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> [SBV Bool]
forall a. SFiniteBits a => SBV a -> [SBV Bool]
blastLE
    blastLE SBV a
x = (Int -> SBV Bool) -> [Int] -> [SBV Bool]
forall a b. (a -> b) -> [a] -> [b]
map (SBV a -> Int -> SBV Bool
forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV a
x) [Int
0 .. SBV a -> Int
forall a. HasKind a => a -> Int
intSizeOf SBV a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

    fromBitsBE = [SBV Bool] -> SBV a
forall a. SFiniteBits a => [SBV Bool] -> SBV a
fromBitsLE ([SBV Bool] -> SBV a)
-> ([SBV Bool] -> [SBV Bool]) -> [SBV Bool] -> SBV a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SBV Bool] -> [SBV Bool]
forall a. [a] -> [a]
reverse
    fromBitsLE [SBV Bool]
bs
       | [SBV Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV Bool]
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
w
       = String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"SBV.SFiniteBits.fromBitsLE/BE: Expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" bits, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SBV Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV Bool]
bs)
       | Bool
True
       = SBV a
result
       where w :: Int
w = SBV a -> Int
forall a. SFiniteBits a => SBV a -> Int
sFiniteBitSize SBV a
result
             result :: SBV a
result = SBV a -> Int -> [SBV Bool] -> SBV a
forall t. (Mergeable t, Bits t) => t -> Int -> [SBV Bool] -> t
go SBV a
0 Int
0 [SBV Bool]
bs

             go :: t -> Int -> [SBV Bool] -> t
go !t
acc Int
_  []     = t
acc
             go !t
acc !Int
i (SBV Bool
x:[SBV Bool]
xs) = t -> Int -> [SBV Bool] -> t
go (SBV Bool -> t -> t -> t
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
x (t -> Int -> t
forall a. Bits a => a -> Int -> a
setBit t
acc Int
i) t
acc) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [SBV Bool]
xs

    sTestBit (SBV SVal
x) Int
i = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (SVal -> Int -> SVal
svTestBit SVal
x Int
i)
    sExtractBits SBV a
x     = (Int -> SBV Bool) -> [Int] -> [SBV Bool]
forall a b. (a -> b) -> [a] -> [b]
map (SBV a -> Int -> SBV Bool
forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV a
x)

    -- NB. 'sPopCount' returns an 'SWord8', which can overflow when used on quantities that have
    -- more than 255 bits. For the regular interface, this suffices for all types we support.
    -- For the Dynamic interface, if we ever implement this, this will fail for bit-vectors
    -- larger than that many bits. The alternative would be to return SInteger here, but that
    -- seems a total overkill for most use cases. If such is required, users are encouraged
    -- to define their own variants, which is rather easy.
    sPopCount SBV a
x
      | SBV a -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete SBV a
x  = SBV Word8 -> SBV a -> SBV Word8
forall t t. (Num t, Num t, Bits t) => t -> t -> t
go SBV Word8
0 SBV a
x
      | Bool
True          = [SBV Word8] -> SBV Word8
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [SBV Bool -> SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
b SBV Word8
1 SBV Word8
0 | SBV Bool
b <- SBV a -> [SBV Bool]
forall a. SFiniteBits a => SBV a -> [SBV Bool]
blastLE SBV a
x]
      where -- concrete case
            go :: t -> t -> t
go !t
c t
0 = t
c
            go !t
c t
w = t -> t -> t
go (t
ct -> t -> t
forall a. Num a => a -> a -> a
+t
1) (t
w t -> t -> t
forall a. Bits a => a -> a -> a
.&. (t
wt -> t -> t
forall a. Num a => a -> a -> a
-t
1))

    setBitTo SBV a
x Int
i SBV Bool
b = SBV Bool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
b (SBV a -> Int -> SBV a
forall a. Bits a => a -> Int -> a
setBit SBV a
x Int
i) (SBV a -> Int -> SBV a
forall a. Bits a => a -> Int -> a
clearBit SBV a
x Int
i)

    fullAdder SBV a
a SBV a
b
      | SBV a -> Bool
forall a. Bits a => a -> Bool
isSigned SBV a
a = String -> (SBV Bool, SBV a)
forall a. HasCallStack => String -> a
error String
"fullAdder: only works on unsigned numbers"
      | Bool
True       = (SBV a
a SBV a -> SBV a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.> SBV a
s SBV Bool -> SBV Bool -> SBV Bool
.|| SBV a
b SBV a -> SBV a -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.> SBV a
s, SBV a
s)
      where s :: SBV a
s = SBV a
a SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SBV a
b

    -- N.B. The higher-order bits are determined using a simple shift-add multiplier,
    -- thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently
    -- with properties involving this function, at least with the current state of the art.
    fullMultiplier SBV a
a SBV a
b
      | SBV a -> Bool
forall a. Bits a => a -> Bool
isSigned SBV a
a = String -> (SBV a, SBV a)
forall a. HasCallStack => String -> a
error String
"fullMultiplier: only works on unsigned numbers"
      | Bool
True       = (Int -> SBV a -> SBV a -> SBV a
go (SBV a -> Int
forall a. SFiniteBits a => SBV a -> Int
sFiniteBitSize SBV a
a) SBV a
0 SBV a
a, SBV a
aSBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
*SBV a
b)
      where go :: Int -> SBV a -> SBV a -> SBV a
go Int
0 SBV a
p SBV a
_ = SBV a
p
            go Int
n SBV a
p SBV a
x = let (SBV Bool
c, SBV a
p')  = SBV Bool
-> (SBV Bool, SBV a) -> (SBV Bool, SBV a) -> (SBV Bool, SBV a)
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (SBV a -> SBV Bool
forall a. SFiniteBits a => SBV a -> SBV Bool
lsb SBV a
x) (SBV a -> SBV a -> (SBV Bool, SBV a)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV Bool, SBV a)
fullAdder SBV a
p SBV a
b) (SBV Bool
sFalse, SBV a
p)
                           (SBV Bool
o, SBV a
p'') = SBV Bool -> SBV a -> (SBV Bool, SBV a)
forall a. SFiniteBits a => SBV Bool -> SBV a -> (SBV Bool, SBV a)
shiftIn SBV Bool
c SBV a
p'
                           (SBV Bool
_, SBV a
x')  = SBV Bool -> SBV a -> (SBV Bool, SBV a)
forall a. SFiniteBits a => SBV Bool -> SBV a -> (SBV Bool, SBV a)
shiftIn SBV Bool
o SBV a
x
                       in Int -> SBV a -> SBV a -> SBV a
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SBV a
p'' SBV a
x'
            shiftIn :: SBV Bool -> SBV a -> (SBV Bool, SBV a)
shiftIn SBV Bool
k SBV a
v = (SBV a -> SBV Bool
forall a. SFiniteBits a => SBV a -> SBV Bool
lsb SBV a
v, SBV a
mask SBV a -> SBV a -> SBV a
forall a. Bits a => a -> a -> a
.|. (SBV a
v SBV a -> Int -> SBV a
forall a. Bits a => a -> Int -> a
`shiftR` Int
1))
               where mask :: SBV a
mask = SBV Bool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
k (Int -> SBV a
forall a. Bits a => Int -> a
bit (SBV a -> Int
forall a. SFiniteBits a => SBV a -> Int
sFiniteBitSize SBV a
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) SBV a
0

    -- See the note for 'sPopCount' for a comment on why we return 'SWord8'
    sCountLeadingZeros SBV a
x = Int -> SBV Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
m SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
- Int -> SBV Word8
go Int
m
      where m :: Int
m = SBV a -> Int
forall a. SFiniteBits a => SBV a -> Int
sFiniteBitSize SBV a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

            -- NB. When i is 0 below, which happens when x is 0 as we count all the way down,
            -- we return -1, which is equal to 2^n-1, giving us: n-1-(2^n-1) = n-2^n = n, as required, i.e., the bit-size.
            go :: Int -> SWord8
            go :: Int -> SBV Word8
go Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = SBV Word8
i8
                 | Bool
True  = SBV Bool -> SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (SBV a -> Int -> SBV Bool
forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV a
x Int
i) SBV Word8
i8 (Int -> SBV Word8
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
               where i8 :: SBV Word8
i8 = Word8 -> SBV Word8
forall a. SymVal a => a -> SBV a
literal (Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i :: Word8)

    -- See the note for 'sPopCount' for a comment on why we return 'SWord8'
    sCountTrailingZeros SBV a
x = Int -> SBV Word8
go Int
0
       where m :: Int
m = SBV a -> Int
forall a. SFiniteBits a => SBV a -> Int
sFiniteBitSize SBV a
x

             go :: Int -> SWord8
             go :: Int -> SBV Word8
go Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m = SBV Word8
i8
                  | Bool
True   = SBV Bool -> SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite (SBV a -> Int -> SBV Bool
forall a. SFiniteBits a => SBV a -> Int -> SBV Bool
sTestBit SBV a
x Int
i) SBV Word8
i8 (Int -> SBV Word8
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1))
                where i8 :: SBV Word8
i8 = Word8 -> SBV Word8
forall a. SymVal a => a -> SBV a
literal (Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i :: Word8)

-- 'SFiniteBits' Instances, skips Real/Float/Bool/Integer
instance SFiniteBits Word8  where sFiniteBitSize :: SBV Word8 -> Int
sFiniteBitSize SBV Word8
_ =  Int
8
instance SFiniteBits Word16 where sFiniteBitSize :: SBV Word16 -> Int
sFiniteBitSize SBV Word16
_ = Int
16
instance SFiniteBits Word32 where sFiniteBitSize :: SBV Word32 -> Int
sFiniteBitSize SBV Word32
_ = Int
32
instance SFiniteBits Word64 where sFiniteBitSize :: SBV Word64 -> Int
sFiniteBitSize SBV Word64
_ = Int
64
instance SFiniteBits Int8   where sFiniteBitSize :: SBV Int8 -> Int
sFiniteBitSize SBV Int8
_ =  Int
8
instance SFiniteBits Int16  where sFiniteBitSize :: SBV Int16 -> Int
sFiniteBitSize SBV Int16
_ = Int
16
instance SFiniteBits Int32  where sFiniteBitSize :: SBV Int32 -> Int
sFiniteBitSize SBV Int32
_ = Int
32
instance SFiniteBits Int64  where sFiniteBitSize :: SBV Int64 -> Int
sFiniteBitSize SBV Int64
_ = Int
64

-- | Returns 1 if the boolean is 'sTrue', otherwise 0.
oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf :: SBV Bool -> SBV a
oneIf SBV Bool
t = SBV Bool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBV Bool -> a -> a -> a
ite SBV Bool
t SBV a
1 SBV a
0

-- | Lift a pseudo-boolean op, performing checks
liftPB :: String -> PBOp -> [SBool] -> SBool
liftPB :: String -> PBOp -> [SBV Bool] -> SBV Bool
liftPB String
w PBOp
o [SBV Bool]
xs
  | Just String
e <- PBOp -> Maybe String
check PBOp
o
  = String -> SBV Bool
forall a. HasCallStack => String -> a
error (String -> SBV Bool) -> String -> SBV Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
  | Bool
True
  = SBV Bool
result
  where check :: PBOp -> Maybe String
check (PB_AtMost  Int
k) = Int -> Maybe String
forall a. (Ord a, Num a, Show a) => a -> Maybe String
pos Int
k
        check (PB_AtLeast Int
k) = Int -> Maybe String
forall a. (Ord a, Num a, Show a) => a -> Maybe String
pos Int
k
        check (PB_Exactly Int
k) = Int -> Maybe String
forall a. (Ord a, Num a, Show a) => a -> Maybe String
pos Int
k
        check (PB_Le [Int]
cs   Int
k) = Int -> Maybe String
forall a. (Ord a, Num a, Show a) => a -> Maybe String
pos Int
k Maybe String -> Maybe String -> Maybe String
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` [Int] -> Maybe String
match [Int]
cs
        check (PB_Ge [Int]
cs   Int
k) = Int -> Maybe String
forall a. (Ord a, Num a, Show a) => a -> Maybe String
pos Int
k Maybe String -> Maybe String -> Maybe String
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` [Int] -> Maybe String
match [Int]
cs
        check (PB_Eq [Int]
cs   Int
k) = Int -> Maybe String
forall a. (Ord a, Num a, Show a) => a -> Maybe String
pos Int
k Maybe String -> Maybe String -> Maybe String
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` [Int] -> Maybe String
match [Int]
cs

        pos :: a -> Maybe String
pos a
k
          | a
k a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"comparison value must be positive, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
k
          | Bool
True  = Maybe String
forall a. Maybe a
Nothing

        match :: [Int] -> Maybe String
match [Int]
cs
          | (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0) [Int]
cs = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"coefficients must be non-negative. Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show [Int]
cs
          | Int
lxs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
lcs   = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"coefficient length must match number of arguments. Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
lcs, Int
lxs)
          | Bool
True         = Maybe String
forall a. Maybe a
Nothing
          where lxs :: Int
lxs = [SBV Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV Bool]
xs
                lcs :: Int
lcs = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
cs

        result :: SBV Bool
result = SVal -> SBV Bool
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r)))
        r :: State -> IO SV
r State
st   = do [SV]
xsv <- (SBV Bool -> IO SV) -> [SBV Bool] -> IO [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (State -> SBV Bool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st) [SBV Bool]
xs
                    -- PseudoBoolean's implicitly require support for integers, so make sure to register that kind!
                    State -> Kind -> IO ()
registerKind State
st Kind
KUnbounded
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp (PBOp -> Op
PseudoBoolean PBOp
o) [SV]
xsv)

-- | 'sTrue' if at most @k@ of the input arguments are 'sTrue'
pbAtMost :: [SBool] -> Int -> SBool
pbAtMost :: [SBV Bool] -> Int -> SBV Bool
pbAtMost [SBV Bool]
xs Int
k
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0             = String -> SBV Bool
forall a. HasCallStack => String -> a
error (String -> SBV Bool) -> String -> SBV Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.pbAtMost: Non-negative value required, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
 | (SBV Bool -> Bool) -> [SBV Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SBV Bool -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete [SBV Bool]
xs = Bool -> SBV Bool
forall a. SymVal a => a -> SBV a
literal (Bool -> SBV Bool) -> Bool -> SBV Bool
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((SBV Bool -> Integer) -> [SBV Bool] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int -> SBV Bool -> Integer
pbToInteger String
"pbAtMost" Int
1) [SBV Bool]
xs) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k
 | Bool
True              = String -> PBOp -> [SBV Bool] -> SBV Bool
liftPB String
"pbAtMost" (Int -> PBOp
PB_AtMost Int
k) [SBV Bool]
xs

-- | 'sTrue' if at least @k@ of the input arguments are 'sTrue'
pbAtLeast :: [SBool] -> Int -> SBool
pbAtLeast :: [SBV Bool] -> Int -> SBV Bool
pbAtLeast [SBV Bool]
xs Int
k
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0             = String -> SBV Bool
forall a. HasCallStack => String -> a
error (String -> SBV Bool) -> String -> SBV Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.pbAtLeast: Non-negative value required, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
 | (SBV Bool -> Bool) -> [SBV Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SBV Bool -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete [SBV Bool]
xs = Bool -> SBV Bool
forall a. SymVal a => a -> SBV a
literal (Bool -> SBV Bool) -> Bool -> SBV Bool
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((SBV Bool -> Integer) -> [SBV Bool] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int -> SBV Bool -> Integer
pbToInteger String
"pbAtLeast" Int
1) [SBV Bool]
xs) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k
 | Bool
True              = String -> PBOp -> [SBV Bool] -> SBV Bool
liftPB String
"pbAtLeast" (Int -> PBOp
PB_AtLeast Int
k) [SBV Bool]
xs

-- | 'sTrue' if exactly @k@ of the input arguments are 'sTrue'
pbExactly :: [SBool] -> Int -> SBool
pbExactly :: [SBV Bool] -> Int -> SBV Bool
pbExactly [SBV Bool]
xs Int
k
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0             = String -> SBV Bool
forall a. HasCallStack => String -> a
error (String -> SBV Bool) -> String -> SBV Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.pbExactly: Non-negative value required, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
 | (SBV Bool -> Bool) -> [SBV Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SBV Bool -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete [SBV Bool]
xs = Bool -> SBV Bool
forall a. SymVal a => a -> SBV a
literal (Bool -> SBV Bool) -> Bool -> SBV Bool
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((SBV Bool -> Integer) -> [SBV Bool] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int -> SBV Bool -> Integer
pbToInteger String
"pbExactly" Int
1) [SBV Bool]
xs) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k
 | Bool
True              = String -> PBOp -> [SBV Bool] -> SBV Bool
liftPB String
"pbExactly" (Int -> PBOp
PB_Exactly Int
k) [SBV Bool]
xs

-- | 'sTrue' if the sum of coefficients for 'sTrue' elements is at most @k@. Generalizes 'pbAtMost'.
pbLe :: [(Int, SBool)] -> Int -> SBool
pbLe :: [(Int, SBV Bool)] -> Int -> SBV Bool
pbLe [(Int, SBV Bool)]
xs Int
k
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0                     = String -> SBV Bool
forall a. HasCallStack => String -> a
error (String -> SBV Bool) -> String -> SBV Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.pbLe: Non-negative value required, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
 | ((Int, SBV Bool) -> Bool) -> [(Int, SBV Bool)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SBV Bool -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete (SBV Bool -> Bool)
-> ((Int, SBV Bool) -> SBV Bool) -> (Int, SBV Bool) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, SBV Bool) -> SBV Bool
forall a b. (a, b) -> b
snd) [(Int, SBV Bool)]
xs = Bool -> SBV Bool
forall a. SymVal a => a -> SBV a
literal (Bool -> SBV Bool) -> Bool -> SBV Bool
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [String -> Int -> SBV Bool -> Integer
pbToInteger String
"pbLe" Int
c SBV Bool
b | (Int
c, SBV Bool
b) <- [(Int, SBV Bool)]
xs] Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k
 | Bool
True                      = String -> PBOp -> [SBV Bool] -> SBV Bool
liftPB String
"pbLe" ([Int] -> Int -> PBOp
PB_Le (((Int, SBV Bool) -> Int) -> [(Int, SBV Bool)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, SBV Bool) -> Int
forall a b. (a, b) -> a
fst [(Int, SBV Bool)]
xs) Int
k) (((Int, SBV Bool) -> SBV Bool) -> [(Int, SBV Bool)] -> [SBV Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Int, SBV Bool) -> SBV Bool
forall a b. (a, b) -> b
snd [(Int, SBV Bool)]
xs)

-- | 'sTrue' if the sum of coefficients for 'sTrue' elements is at least @k@. Generalizes 'pbAtLeast'.
pbGe :: [(Int, SBool)] -> Int -> SBool
pbGe :: [(Int, SBV Bool)] -> Int -> SBV Bool
pbGe [(Int, SBV Bool)]
xs Int
k
 | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0                     = String -> SBV Bool
forall a. HasCallStack => String -> a
error (String -> SBV Bool) -> String -> SBV Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.pbGe: Non-negative value required, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++