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

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

{-# OPTIONS_GHC -Wall -Werror #-}

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

import GHC.TypeLits (KnownNat, Nat, Symbol, KnownSymbol, symbolVal, AppendSymbol, type (+), type (-), type (<=), natVal)

import GHC.Exts     (IsList(..))

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

import Data.Kind (Type)
import Data.Proxy
import Data.Typeable          (Typeable)

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

import System.Random

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

import Data.SBV.Control.Types

import Data.SBV.SMT.SMTLibNames

import Data.SBV.Utils.Lib

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | A symbolic unsigned bit-vector carrying its size info
type SWord (n :: Nat) = SBV (WordN n)

-- | A symbolic signed bit-vector carrying its size info
type SInt (n :: Nat) = SBV (IntN n)

-- | A symbolic character. Note that this is the full unicode character set.
-- see: <https://smt-lib.org/theories-UnicodeStrings.shtml>
-- for details.
type SChar = SBV Char

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

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

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

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

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

-- | Symbolic arrays. A symbolic array is more akin to a function in SMTLib (and thus in SBV),
-- as opposed to contagious-storage with a finite range as found in many programming languages.
-- Additionally, the domain uses object-equality in the SMTLib semantics. Object equality is
-- the same as regular equality for most types, except for IEEE-Floats, where @NaN@ doesn't compare
-- equal to itself and @+0@ and @-0@ are not distinguished. So, if your index type is a float,
-- then @NaN@ can be stored correctly, and @0@ and @-0@ will be distinguished. If you don't use
-- floats, then you can treat this the same as regular equality in Haskell.
type SArray a b = SBV (ArrayModel a b)

-- | Symbolic 'Data.Set'. Note that we use 'RCSet', which supports
-- both regular sets and complements, i.e., those obtained from the
-- universal set (of the right type) by removing elements. Similar to 'SArray'
-- the contents are stored with object equality, which makes a difference if the
-- underlying type contains IEEE Floats.
type SSet a = SBV (RCSet a)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Symbolic boolean equivalence
infixr 1 .<=>
(.<=>) :: SBool -> SBool -> SBool
SBV SVal
x .<=> :: SBool -> SBool -> SBool
.<=> SBV SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svEqual` SVal
y)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Values that we can turn into a constraint
class MonadSymbolic m => Constraint m a where
  mkConstraint :: State -> a -> m ()

-- | Base case: simple booleans
instance MonadSymbolic m => Constraint m SBool where
  mkConstraint :: State -> SBool -> m ()
mkConstraint State
_ SBool
out = m SBool -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m SBool -> m ()) -> m SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> m SBool
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
output SBool
out

-- | An existential symbolic variable, used in building quantified constraints. The name
-- attached via the symbol is used during skolemization to create a skolem-function name
-- when this variable is eliminated.
newtype Exists (nm :: Symbol) a = Exists (SBV a)

-- | An existential unique symbolic variable, used in building quantified constraints. The name
-- attached via the symbol is used during skolemization. It's split into two extra names, suffixed
-- @_eu1@ and @_eu2@, to name the universals in the equivalent formula:
-- \(\exists! x\,P(x)\Leftrightarrow \exists x\,P(x) \land \forall x_{eu1} \forall x_{eu2} (P(x_{eu1}) \land P(x_{eu2}) \Rightarrow x_{eu1} = x_{eu2}) \)
newtype ExistsUnique (nm :: Symbol) a = ExistsUnique (SBV a)

-- | A universal symbolic variable, used in building quantified constraints. The name attached via the symbol is used
-- during skolemization. It names the corresponding argument to the skolem-functions within the scope of this quantifier.
newtype Forall (nm :: Symbol) a = Forall (SBV a)

-- | Exactly @n@ existential symbolic variables, used in building quantified constraints. The name attached
-- will be prefixed in front of @_1@, @_2@, ..., @_n@ to form the names of the variables.
newtype ExistsN (n :: Nat) (nm :: Symbol) a = ExistsN [SBV a]

-- | Exactly @n@ universal symbolic variables, used in in building quantified constraints. The name attached
-- will be prefixed in front of @_1@, @_2@, ..., @_n@ to form the names of the variables.
newtype ForallN (n :: Nat) (nm :: Symbol) a = ForallN [SBV a]

-- | make a quantifier argument in the given state
mkQArg :: forall m a. (HasKind a, MonadIO m) => State -> Quantifier -> m (SBV a)
mkQArg :: forall (m :: * -> *) a.
(HasKind a, MonadIO m) =>
State -> Quantifier -> m (SBV a)
mkQArg State
st Quantifier
q = do let k :: Kind
k = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
                 sv <- IO SV -> m SV
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ Quantifier -> State -> Kind -> IO SV
quantVar Quantifier
q State
st Kind
k
                 pure $ SBV $ SVal k (Right (cache (const (return sv))))

-- | Functions of a single existential
instance (SymVal a, Constraint m r) => Constraint m (Exists nm a -> r) where
  mkConstraint :: State -> (Exists nm a -> r) -> m ()
mkConstraint State
st Exists nm a -> r
fn = State -> Quantifier -> m (SBV a)
forall (m :: * -> *) a.
(HasKind a, MonadIO m) =>
State -> Quantifier -> m (SBV a)
mkQArg State
st Quantifier
EX m (SBV a) -> (SBV a -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> r -> m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st (r -> m ()) -> (SBV a -> r) -> SBV a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exists nm a -> r
fn (Exists nm a -> r) -> (SBV a -> Exists nm a) -> SBV a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> Exists nm a
forall (nm :: Symbol) a. SBV a -> Exists nm a
Exists

-- | Functions of a unique single existential
instance (SymVal a, Constraint m r, EqSymbolic (SBV a), QuantifiedBool r) => Constraint m (ExistsUnique nm a -> r) where
  mkConstraint :: State -> (ExistsUnique nm a -> r) -> m ()
mkConstraint State
st = State
-> (Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool)
-> m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st ((Exists nm a
  -> Forall (AppendSymbol nm "_eu1") a
  -> Forall (AppendSymbol nm "_eu2") a
  -> SBool)
 -> m ())
-> ((ExistsUnique nm a -> r)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool)
-> (ExistsUnique nm a -> r)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExistsUnique nm a -> r)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
forall b a (nm :: Symbol).
(QuantifiedBool b, EqSymbolic (SBV a)) =>
(ExistsUnique nm a -> b)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
rewriteExistsUnique

-- | Functions of a number of existentials
instance (KnownNat n, SymVal a, Constraint m r) => Constraint m (ExistsN n nm a -> r) where
  mkConstraint :: State -> (ExistsN n nm a -> r) -> m ()
mkConstraint State
st ExistsN n nm a -> r
fn = Int -> m (SBV a) -> m [SBV a]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) (State -> Quantifier -> m (SBV a)
forall (m :: * -> *) a.
(HasKind a, MonadIO m) =>
State -> Quantifier -> m (SBV a)
mkQArg State
st Quantifier
EX) m [SBV a] -> ([SBV a] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> r -> m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st (r -> m ()) -> ([SBV a] -> r) -> [SBV a] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExistsN n nm a -> r
fn (ExistsN n nm a -> r)
-> ([SBV a] -> ExistsN n nm a) -> [SBV a] -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SBV a] -> ExistsN n nm a
forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ExistsN n nm a
ExistsN

-- | Functions of a single universal
instance (SymVal a, Constraint m r) => Constraint m (Forall nm a -> r) where
  mkConstraint :: State -> (Forall nm a -> r) -> m ()
mkConstraint State
st Forall nm a -> r
fn = State -> Quantifier -> m (SBV a)
forall (m :: * -> *) a.
(HasKind a, MonadIO m) =>
State -> Quantifier -> m (SBV a)
mkQArg State
st Quantifier
ALL m (SBV a) -> (SBV a -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> r -> m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st (r -> m ()) -> (SBV a -> r) -> SBV a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Forall nm a -> r
fn (Forall nm a -> r) -> (SBV a -> Forall nm a) -> SBV a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> Forall nm a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall

-- | Functions of a number of universals
instance (KnownNat n, SymVal a, Constraint m r) => Constraint m (ForallN n nm a -> r) where
  mkConstraint :: State -> (ForallN n nm a -> r) -> m ()
mkConstraint State
st ForallN n nm a -> r
fn = Int -> m (SBV a) -> m [SBV a]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) (State -> Quantifier -> m (SBV a)
forall (m :: * -> *) a.
(HasKind a, MonadIO m) =>
State -> Quantifier -> m (SBV a)
mkQArg State
st Quantifier
ALL) m [SBV a] -> ([SBV a] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> r -> m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st (r -> m ()) -> ([SBV a] -> r) -> [SBV a] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ForallN n nm a -> r
fn (ForallN n nm a -> r)
-> ([SBV a] -> ForallN n nm a) -> [SBV a] -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SBV a] -> ForallN n nm a
forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ForallN n nm a
ForallN

-- | Values that we can turn into a lambda abstraction
class MonadSymbolic m => Lambda m a where
  mkLambda :: State -> a -> m ()

-- | Base case, simple values
instance MonadSymbolic m => Lambda m (SBV a) where
  mkLambda :: State -> SBV a -> m ()
mkLambda State
_ SBV a
out = m (SBV a) -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m (SBV a) -> m ()) -> m (SBV a) -> m ()
forall a b. (a -> b) -> a -> b
$ SBV a -> m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
out

-- | Functions
instance (SymVal a, Lambda m r) => Lambda m (SBV a -> r) where
  mkLambda :: State -> (SBV a -> r) -> m ()
mkLambda State
st SBV a -> r
fn = m (SBV a)
mkArg m (SBV a) -> (SBV a -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> r -> m ()
forall (m :: * -> *) a. Lambda m a => State -> a -> m ()
mkLambda State
st (r -> m ()) -> (SBV a -> r) -> SBV a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> r
fn
    where mkArg :: m (SBV a)
mkArg = do let k :: Kind
k = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
                     sv <- IO SV -> m SV
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> Kind -> IO SV
lambdaVar State
st Kind
k
                     pure $ SBV $ SVal k (Right (cache (const (return sv))))

-- | A value that can be used as a quantified boolean
class QuantifiedBool a where
  -- | Turn a quantified boolean into a regular boolean. That is, this function turns an exists/forall quantified
  -- formula to a simple boolean that can be used as a regular boolean value. An example is:
  --
  -- @
  --   quantifiedBool $ \\(Forall x) (Exists y) -> y .> (x :: SInteger)
  -- @
  --
  -- is equivalent to `sTrue`. You can think of this function as performing quantifier-elimination: It takes
  -- a quantified formula, and reduces it to a simple boolean that is equivalent to it, but has no quantifiers.
  quantifiedBool :: a -> SBool

-- | Base case of quantification, simple booleans
instance {-# OVERLAPPING #-} QuantifiedBool SBool where
  quantifiedBool :: SBool -> SBool
quantifiedBool = SBool -> SBool
forall a. a -> a
id

-- | Actions we can do in a context: Either at problem description
-- time or while we are dynamically querying. 'Symbolic' and 'Query' are
-- two instances of this class. Note that we use this mechanism
-- internally and do not export it from SBV.
class SolverContext m where
   -- | Add a constraint, any satisfying instance must satisfy this condition.
   constrain :: QuantifiedBool a => a -> m ()

   -- | Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.
   softConstrain :: QuantifiedBool a => a -> m ()

   -- | Add a named constraint. The name is used in unsat-core extraction.
   namedConstraint :: QuantifiedBool a => String -> a -> m ()

   -- | Add a constraint, with arbitrary attributes.
   constrainWithAttribute :: QuantifiedBool a => [(String, String)] -> a -> m ()

   -- | Set info. Example: @setInfo ":status" ["unsat"]@.
   setInfo :: String -> [String] -> m ()

   -- | Set an option.
   setOption :: SMTOption -> m ()

   -- | Set the logic.
   setLogic :: Logic -> m ()

   -- | Set a solver time-out value, in milli-seconds. This function
   -- essentially translates to the SMTLib call @(set-info :timeout val)@,
   -- and your backend solver may or may not support it! The amount given
   -- is in milliseconds. Also see the function 'Data.SBV.Control.timeOut' for finer level
   -- control of time-outs, directly from SBV.
   setTimeOut :: Integer -> m ()

   -- | Get the state associated with this context
   contextState :: m State

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

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

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

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

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

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

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

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

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

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

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

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

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

-------------------------------------------------------------------------------
-- * Symbolic Values
-------------------------------------------------------------------------------
-- | A 'SymVal' is a potential symbolic value that can be created instances of to be fed to a symbolic program.
class (HasKind a, Typeable a) => SymVal a where
  -- | Generalization of 'Data.SBV.mkSymVal'
  mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV a)

  -- | Turn a literal constant to symbolic
  literal :: a -> SBV a

  -- | Extract a literal, from a CV representation
  fromCV :: CV -> a

  -- | Does it concretely satisfy the given predicate?
  isConcretely :: SBV a -> (a -> Bool) -> Bool

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Symbolic 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.
--
-- NB. Equality is a built-in notion in SMTLib, and is object-equality. While this mostly matches Haskell's
-- notion of equality, the correspondence isn't exact. This mostly shows up in containers with floats inside,
-- such as sequences of floats, sets of doubles, and arrays of doubles. While SBV tries to maintain Haskell
-- semantics, it does resort to container equality for compound types. For instance, for an IEEE-float,
-- -0 == 0. But for an SMTLib sequence, equals is done over objects. i.e., @[0] == [-0]@ in Haskell, but
-- @literal [0] ./= literal [-0]@ when used as SMTLib sequences. The rabbit-hole goes deep here, especially
-- when @NaN@ is involved, which does not compare equal to itself per IEEE-semantics.
--
-- If you are not using floats, then you can ignore all this. If you do, then SBV will do the right thing for
-- them when checking equality directly, but not when you use containers with floating-point elements. In the
-- latter case, object-equality will be used.
--
-- Minimal complete definition: None, if the type is instance of @Generic@. Otherwise '(.==)'.
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.
  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

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

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

  -- Default implementation of 'distinct'. Note that we override
  -- this method for the base types to generate better code.
  distinct []     = SBool
sTrue
  distinct (a
x:[a]
xs) = (a -> SBool) -> [a] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll (a
x a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./=) [a]
xs SBool -> SBool -> SBool
.&& [a] -> SBool
forall a. EqSymbolic a => [a] -> SBool
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] -> SBool
go [a]
es
    where isIgnored :: a -> SBool
isIgnored = (a -> [a] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [a]
ignored)

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

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

  -- Default implementation for '(.==)' if the type is 'Generic'
  default (.==) :: (G.Generic a, GEqSymbolic (G.Rep a)) => a -> a -> SBool
  (.==) = a -> a -> SBool
forall a. (Generic a, GEqSymbolic (Rep a)) => a -> a -> SBool
symbolicEqDefault

-- | Default implementation of symbolic equality, when the underlying type is generic
-- Not exported, used with automatic deriving.
symbolicEqDefault :: (G.Generic a, GEqSymbolic (G.Rep a)) => a -> a -> SBool
symbolicEqDefault :: forall a. (Generic a, GEqSymbolic (Rep a)) => a -> a -> SBool
symbolicEqDefault a
x a
y = Rep a Any -> Rep a Any -> SBool
forall a. Rep a a -> Rep a a -> SBool
forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
symbolicEq (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
G.from a
x) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
G.from a
y)

-- | Not exported, used for implementing generic equality.
class GEqSymbolic f where
  symbolicEq :: f a -> f a -> SBool

{-
 - N.B. A V1 instance like the below would be wrong!
 - Why? Because in SBV, we use empty data to mean "uninterpreted" sort; not
 - something that has no constructors. Perhaps that was a bad design
 - decision. So, do not allow equality checking of such values.
instance GEqSymbolic V1 where
  symbolicEq _ _ = sTrue
-}

instance GEqSymbolic U1 where
  symbolicEq :: forall a. U1 a -> U1 a -> SBool
symbolicEq U1 a
_ U1 a
_ = SBool
sTrue

instance (EqSymbolic c) => GEqSymbolic (K1 i c) where
  symbolicEq :: forall a. K1 i c a -> K1 i c a -> SBool
symbolicEq (K1 c
x) (K1 c
y) = c
x c -> c -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== c
y

instance (GEqSymbolic f) => GEqSymbolic (M1 i c f) where
  symbolicEq :: forall a. M1 i c f a -> M1 i c f a -> SBool
symbolicEq (M1 f a
x) (M1 f a
y) = f a -> f a -> SBool
forall a. f a -> f a -> SBool
forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
symbolicEq f a
x f a
y

instance (GEqSymbolic f, GEqSymbolic g) => GEqSymbolic (f :*: g) where
  symbolicEq :: forall a. (:*:) f g a -> (:*:) f g a -> SBool
symbolicEq (f a
x1 :*: g a
y1) (f a
x2 :*: g a
y2) = f a -> f a -> SBool
forall a. f a -> f a -> SBool
forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
symbolicEq f a
x1 f a
x2 SBool -> SBool -> SBool
.&& g a -> g a -> SBool
forall a. g a -> g a -> SBool
forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
symbolicEq g a
y1 g a
y2

instance (GEqSymbolic f, GEqSymbolic g) => GEqSymbolic (f :+: g) where
  symbolicEq :: forall a. (:+:) f g a -> (:+:) f g a -> SBool
symbolicEq (L1 f a
l) (L1 f a
r) = f a -> f a -> SBool
forall a. f a -> f a -> SBool
forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
symbolicEq f a
l f a
r
  symbolicEq (R1 g a
l) (R1 g a
r) = g a -> g a -> SBool
forall a. g a -> g a -> SBool
forall (f :: * -> *) a. GEqSymbolic f => f a -> f a -> SBool
symbolicEq g a
l g a
r
  symbolicEq (L1 f a
_) (R1 g a
_) = SBool
sFalse
  symbolicEq (R1 g a
_) (L1 f a
_) = SBool
sFalse

-- We don't want to do a generic Num a => Num (SBV a) instance; since that would be dangerous. Liftings
-- would only work for types we already handle. If a user defines his own type and makes an instance
-- of it, it would do the wrong thing. See https://github.com/LeventErkok/sbv/issues/706 for a discussion.
-- So, we have to declare the instances individually. I played around doing this via iso-deriving and
-- other generic mechanisms, but failed to do so. The CPP solution here is crude, but it avoids the
-- code duplication.
#define MKSNUM(CSTR, TYPE, KIND)                                                            \
instance (CSTR) => Num (TYPE) where {                                                       \
  fromInteger i  = SBV $ SVal (KIND) $ Left $ mkConstCV (KIND) (fromIntegral i :: Integer); \
  SBV a + SBV b  = SBV $ a `svPlus`  b;                                                     \
  SBV a * SBV b  = SBV $ a `svTimes` b;                                                     \
  SBV a - SBV b  = SBV $ a `svMinus` b;                                                     \
  abs    (SBV a) = SBV $ svAbs    a;                                                        \
  signum (SBV a) = SBV $ svSignum a;                                                        \
  negate (SBV a) = SBV $ svUNeg   a;                                                        \
}

-- Derive basic instances we need
MKSNUM((),               SInteger,             KUnbounded)
MKSNUM((),               SWord8,               KBounded False  8)
MKSNUM((),               SWord16,              KBounded False 16)
MKSNUM((),               SWord32,              KBounded False 32)
MKSNUM((),               SWord64,              KBounded False 64)
MKSNUM((),               SInt8,                KBounded True   8)
MKSNUM((),               SInt16,               KBounded True  16)
MKSNUM((),               SInt32,               KBounded True  32)
MKSNUM((),               SInt64,               KBounded True  64)
MKSNUM((),               SFloat,               KFloat)
MKSNUM((),               SDouble,              KDouble)
MKSNUM((),               SReal,                KReal)
MKSNUM(KnownNat n,       SWord n,              KBounded False (intOfProxy (Proxy @n)))
MKSNUM(KnownNat n,       SInt  n,              KBounded True  (intOfProxy (Proxy @n)))
MKSNUM(ValidFloat eb sb, SFloatingPoint eb sb, KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)))

-- | Extract a portion of bits to form a smaller bit-vector.
bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                    , KnownNat i
                                    , KnownNat j
                                    , i + 1 <= n
                                    , j <= i
                                    , BVIsNonZero (i - j + 1)
                                    ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@
                                      -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold
                                      -> SBV (bv n)             -- ^ Input bit vector of size @n@
                                      -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@
bvExtract :: forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract proxy i
start proxy j
end = SVal -> SBV (bv ((i - j) + 1))
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv ((i - j) + 1)))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv ((i - j) + 1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
i Int
j (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
   where i :: Int
i  = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
start)
         j :: Int
j  = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy j -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy j
end)

-- | Join two bitvectors.
(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)
       , KnownNat m, BVIsNonZero m, SymVal (bv m)
       ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side
         -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side
         -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@
SBV (bv n)
n # :: forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SBV (bv m)
m = SVal -> SBV (bv (n + m))
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv (n + m))) -> SVal -> SBV (bv (n + m))
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
svJoin (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n) (SBV (bv m) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv m)
m)
infixr 5 #

-- | Drop bits from the top of a bit-vector.
bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n
                                 , KnownNat i
                                 , i + 1 <= n
                                 , i + m - n <= 0
                                 , BVIsNonZero (n - i)
                                 ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.
                                   -> SBV (bv n)                 -- ^ Input, of size @n@
                                   -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.
bvDrop :: forall (i :: Nat) (n :: Nat) (m :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n,
 ((i + m) - n) <= 0, BVIsNonZero (n - i)) =>
proxy i -> SBV (bv n) -> SBV (bv m)
bvDrop proxy i
i = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
0 (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

-- | Take bits from the top of a bit-vector.
bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n
                               , KnownNat i, BVIsNonZero i
                               , i <= n
                               ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.
                                 -> SBV (bv n)               -- ^ Input, of size @n@
                                 -> SBV (bv i)               -- ^ Output, of size @i@
bvTake :: forall (i :: Nat) (n :: Nat) (bv :: Nat -> *) (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) =>
proxy i -> SBV (bv n) -> SBV (bv i)
bvTake proxy i
i = SVal -> SBV (bv i)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv i))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
end (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
        end :: Int
end   = Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

-- | A class of values that can be skolemized. Note that we don't export this class. Use
-- the 'skolemize' function instead.
class Skolemize a where
  type SkolemsTo a :: Type
  skolem :: String -> [(SVal, String)] -> a -> SkolemsTo a

  -- | Skolemization. For any formula, skolemization gives back an equisatisfiable formula that
  -- has no existential quantifiers in it. You have to provide enough names for all the
  -- existentials in the argument. (Extras OK, so you can pass an infinite list if you like.)
  -- The names should be distinct, and also different from any other uninterpreted name
  -- you might have elsewhere.
  skolemize :: (Constraint Symbolic (SkolemsTo a), Skolemize a) => a -> SkolemsTo a
  skolemize = [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem [Char]
"" []

  -- | If you use the same names for skolemized arguments in different functions, they will
  -- collide; which is undesirable. Unfortunately there's no easy way for SBV to detect this.
  -- In such cases, use 'taggedSkolemize' to add a scope to the skolem-function names generated.
  taggedSkolemize :: (Constraint Symbolic (SkolemsTo a), Skolemize a) => String -> a -> SkolemsTo a
  taggedSkolemize [Char]
scope = [Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem ([Char]
scope [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"_") []

-- | Base case; pure symbolic values
instance Skolemize (SBV a) where
  type SkolemsTo (SBV a) = SBV a
  skolem :: [Char] -> [(SVal, [Char])] -> SBV a -> SkolemsTo (SBV a)
skolem [Char]
_ [(SVal, [Char])]
_ = SBV a -> SkolemsTo (SBV a)
SBV a -> SBV a
forall a. a -> a
id

-- | Skolemize over a universal quantifier
instance (KnownSymbol nm, Skolemize r) => Skolemize (Forall nm a -> r) where
  type SkolemsTo (Forall nm a -> r) = Forall nm a -> SkolemsTo r
  skolem :: [Char]
-> [(SVal, [Char])]
-> (Forall nm a -> r)
-> SkolemsTo (Forall nm a -> r)
skolem [Char]
scope [(SVal, [Char])]
args Forall nm a -> r
f arg :: Forall nm a
arg@(Forall SBV a
a) = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem [Char]
scope ([(SVal, [Char])]
args [(SVal, [Char])] -> [(SVal, [Char])] -> [(SVal, [Char])]
forall a. [a] -> [a] -> [a]
++ [(SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
a, Proxy nm -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nm))]) (Forall nm a -> r
f Forall nm a
arg)

-- | Skolemize over a number of universal quantifiers
instance (KnownSymbol nm, Skolemize r) => Skolemize (ForallN n nm a -> r) where
  type SkolemsTo (ForallN n nm a -> r) = ForallN n nm a -> SkolemsTo r
  skolem :: [Char]
-> [(SVal, [Char])]
-> (ForallN n nm a -> r)
-> SkolemsTo (ForallN n nm a -> r)
skolem [Char]
scope [(SVal, [Char])]
args ForallN n nm a -> r
f arg :: ForallN n nm a
arg@(ForallN [SBV a]
xs) = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem [Char]
scope ([(SVal, [Char])]
args [(SVal, [Char])] -> [(SVal, [Char])] -> [(SVal, [Char])]
forall a. [a] -> [a] -> [a]
++ (SBV a -> Int -> (SVal, [Char]))
-> [SBV a] -> [Int] -> [(SVal, [Char])]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SBV a -> Int -> (SVal, [Char])
grab [SBV a]
xs [(Int
1::Int)..]) (ForallN n nm a -> r
f ForallN n nm a
arg)
    where pre :: [Char]
pre = Proxy nm -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nm)
          grab :: SBV a -> Int -> (SVal, [Char])
grab SBV a
x Int
i = (SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
x, [Char]
pre [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)

-- | Skolemize over an existential quantifier
instance (HasKind a, KnownSymbol nm, Skolemize r) => Skolemize (Exists nm a -> r) where
  type SkolemsTo (Exists nm a -> r) = SkolemsTo r
  skolem :: [Char]
-> [(SVal, [Char])]
-> (Exists nm a -> r)
-> SkolemsTo (Exists nm a -> r)
skolem [Char]
scope [(SVal, [Char])]
args Exists nm a -> r
f = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem [Char]
scope [(SVal, [Char])]
args (Exists nm a -> r
f (SBV a -> Exists nm a
forall (nm :: Symbol) a. SBV a -> Exists nm a
Exists SBV a
skolemized))
    where skolemized :: SBV a
skolemized = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> [Char] -> UICodeKind -> [(SVal, [Char])] -> SVal
svUninterpretedNamedArgs (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) ([Char]
scope [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy nm -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nm)) (Bool -> UICodeKind
UINone Bool
True) [(SVal, [Char])]
args

-- | Skolemize over a number of existential quantifiers
instance (HasKind a, KnownNat n, KnownSymbol nm, Skolemize r) => Skolemize (ExistsN n nm a -> r) where
  type SkolemsTo (ExistsN n nm a -> r) = SkolemsTo r
  skolem :: [Char]
-> [(SVal, [Char])]
-> (ExistsN n nm a -> r)
-> SkolemsTo (ExistsN n nm a -> r)
skolem [Char]
scope [(SVal, [Char])]
args ExistsN n nm a -> r
f = [Char] -> [(SVal, [Char])] -> r -> SkolemsTo r
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem [Char]
scope [(SVal, [Char])]
args (ExistsN n nm a -> r
f ([SBV a] -> ExistsN n nm a
forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ExistsN n nm a
ExistsN [SBV a]
skolemized))
    where need :: Int
need   = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
          prefix :: [Char]
prefix = Proxy nm -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nm)
          fs :: [[Char]]
fs     = [[Char]
prefix [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i | Int
i <- [Int
1 .. Int
need]]
          skolemized :: [SBV a]
skolemized = [SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> [Char] -> UICodeKind -> [(SVal, [Char])] -> SVal
svUninterpretedNamedArgs (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) ([Char]
scope [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
n) (Bool -> UICodeKind
UINone Bool
True) [(SVal, [Char])]
args | [Char]
n <- [[Char]]
fs]

-- | Skolemize over a unique existential quantifier
instance (  HasKind a
          , EqSymbolic (SBV a)
          , KnownSymbol nm
          , QuantifiedBool r
          , Skolemize (Forall (AppendSymbol nm "_eu1") a -> Forall (AppendSymbol nm "_eu2") a -> SBool)
         ) => Skolemize (ExistsUnique nm a -> r) where
  type SkolemsTo (ExistsUnique nm a -> r) =  Forall (AppendSymbol nm "_eu1") a
                                          -> Forall (AppendSymbol nm "_eu2") a
                                          -> SBool
  skolem :: [Char]
-> [(SVal, [Char])]
-> (ExistsUnique nm a -> r)
-> SkolemsTo (ExistsUnique nm a -> r)
skolem [Char]
scope [(SVal, [Char])]
args ExistsUnique nm a -> r
f = [Char]
-> [(SVal, [Char])]
-> (Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a -> SBool)
-> SkolemsTo
     (Forall (AppendSymbol nm "_eu1") a
      -> Forall (AppendSymbol nm "_eu2") a -> SBool)
forall a.
Skolemize a =>
[Char] -> [(SVal, [Char])] -> a -> SkolemsTo a
skolem [Char]
scope [(SVal, [Char])]
args ((ExistsUnique nm a -> r)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
forall b a (nm :: Symbol).
(QuantifiedBool b, EqSymbolic (SBV a)) =>
(ExistsUnique nm a -> b)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
rewriteExistsUnique ExistsUnique nm a -> r
f (SBV a -> Exists nm a
forall (nm :: Symbol) a. SBV a -> Exists nm a
Exists SBV a
skolemized))
    where skolemized :: SBV a
skolemized = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> [Char] -> UICodeKind -> [(SVal, [Char])] -> SVal
svUninterpretedNamedArgs (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) ([Char]
scope [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy nm -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nm)) (Bool -> UICodeKind
UINone Bool
True) [(SVal, [Char])]
args

-- | Class of things that we can logically negate
class QNot a where
  type NegatesTo a :: Type
  -- | Negation of a quantified formula. This operation essentially lifts 'sNot' to quantified formulae.
  -- Note that you can achieve the same using @'sNot' . 'quantifiedBool'@, but that will hide the
  -- quantifiers, so prefer this version if you want to keep them around.
  qNot :: a -> NegatesTo a

-- | Base case; pure symbolic boolean
instance QNot SBool where
  type NegatesTo SBool = SBool
  qNot :: SBool -> NegatesTo SBool
qNot = SBool -> NegatesTo SBool
SBool -> SBool
sNot

-- | Negate over a universal quantifier. Switches to existential.
instance QNot r => QNot (Forall nm a -> r) where
  type NegatesTo (Forall nm a -> r) = Exists nm a -> NegatesTo r
  qNot :: (Forall nm a -> r) -> NegatesTo (Forall nm a -> r)
qNot Forall nm a -> r
f (Exists SBV a
a) = r -> NegatesTo r
forall a. QNot a => a -> NegatesTo a
qNot (Forall nm a -> r
f (SBV a -> Forall nm a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a))

-- | Negate over a number of universal quantifiers
instance QNot r => QNot (ForallN nm n a -> r) where
  type NegatesTo (ForallN nm n a -> r) = ExistsN nm n a -> NegatesTo r
  qNot :: (ForallN nm n a -> r) -> NegatesTo (ForallN nm n a -> r)
qNot ForallN nm n a -> r
f (ExistsN [SBV a]
xs) = r -> NegatesTo r
forall a. QNot a => a -> NegatesTo a
qNot (ForallN nm n a -> r
f ([SBV a] -> ForallN nm n a
forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ForallN n nm a
ForallN [SBV a]
xs))

-- | Negate over an existential quantifier. Switches to universal.
instance QNot r => QNot (Exists nm a -> r) where
  type NegatesTo (Exists nm a -> r) = Forall nm a -> NegatesTo r
  qNot :: (Exists nm a -> r) -> NegatesTo (Exists nm a -> r)
qNot Exists nm a -> r
f (Forall SBV a
a) = r -> NegatesTo r
forall a. QNot a => a -> NegatesTo a
qNot (Exists nm a -> r
f (SBV a -> Exists nm a
forall (nm :: Symbol) a. SBV a -> Exists nm a
Exists SBV a
a))

-- | Negate over a number of existential quantifiers
instance QNot r => QNot (ExistsN nm n a -> r) where
  type NegatesTo (ExistsN nm n a -> r) = ForallN nm n a -> NegatesTo r
  qNot :: (ExistsN nm n a -> r) -> NegatesTo (ExistsN nm n a -> r)
qNot ExistsN nm n a -> r
f (ForallN [SBV a]
xs) = r -> NegatesTo r
forall a. QNot a => a -> NegatesTo a
qNot (ExistsN nm n a -> r
f ([SBV a] -> ExistsN nm n a
forall (n :: Nat) (nm :: Symbol) a. [SBV a] -> ExistsN n nm a
ExistsN [SBV a]
xs))

-- | Negate over an unique existential quantifier
instance (QNot r, QuantifiedBool r, EqSymbolic (SBV a)) => QNot (ExistsUnique nm a -> r) where
  type NegatesTo (ExistsUnique nm a -> r) =  Forall nm a
                                          -> Exists (AppendSymbol nm "_eu1") a
                                          -> Exists (AppendSymbol nm "_eu2") a
                                          -> SBool
  qNot :: (ExistsUnique nm a -> r) -> NegatesTo (ExistsUnique nm a -> r)
qNot = (Exists nm a
 -> Forall (AppendSymbol nm "_eu1") a
 -> Forall (AppendSymbol nm "_eu2") a
 -> SBool)
-> NegatesTo
     (Exists nm a
      -> Forall (AppendSymbol nm "_eu1") a
      -> Forall (AppendSymbol nm "_eu2") a
      -> SBool)
(Exists nm a
 -> Forall (AppendSymbol nm "_eu1") a
 -> Forall (AppendSymbol nm "_eu2") a
 -> SBool)
-> Forall nm a
-> Exists (AppendSymbol nm "_eu1") a
-> Exists (AppendSymbol nm "_eu2") a
-> SBool
forall a. QNot a => a -> NegatesTo a
qNot ((Exists nm a
  -> Forall (AppendSymbol nm "_eu1") a
  -> Forall (AppendSymbol nm "_eu2") a
  -> SBool)
 -> Forall nm a
 -> Exists (AppendSymbol nm "_eu1") a
 -> Exists (AppendSymbol nm "_eu2") a
 -> SBool)
-> ((ExistsUnique nm a -> r)
    -> Exists nm a
    -> Forall (AppendSymbol nm "_eu1") a
    -> Forall (AppendSymbol nm "_eu2") a
    -> SBool)
-> (ExistsUnique nm a -> r)
-> Forall nm a
-> Exists (AppendSymbol nm "_eu1") a
-> Exists (AppendSymbol nm "_eu2") a
-> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExistsUnique nm a -> r)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
forall b a (nm :: Symbol).
(QuantifiedBool b, EqSymbolic (SBV a)) =>
(ExistsUnique nm a -> b)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
rewriteExistsUnique

-- | Get rid of exists unique.
rewriteExistsUnique :: ( QuantifiedBool b                 -- If b can be turned into a boolean
                       , EqSymbolic (SBV a)               -- If we can do equality on symbolic a's
                       )                                  -- THEN
                    => (ExistsUnique nm a -> b)           -- Given an unique-existential, we can
                    -> Exists nm a                        -- Turn it into an existential
                    -> Forall (AppendSymbol nm "_eu1") a  -- A universal
                    -> Forall (AppendSymbol nm "_eu2") a  -- Another universal
                    -> SBool                                  -- Making sure given holds, and if both univers hold, they're the same
rewriteExistsUnique :: forall b a (nm :: Symbol).
(QuantifiedBool b, EqSymbolic (SBV a)) =>
(ExistsUnique nm a -> b)
-> Exists nm a
-> Forall (AppendSymbol nm "_eu1") a
-> Forall (AppendSymbol nm "_eu2") a
-> SBool
rewriteExistsUnique ExistsUnique nm a -> b
f (Exists SBV a
x) (Forall SBV a
x1) (Forall SBV a
x2) = SBool
fx SBool -> SBool -> SBool
.&& SBool
unique
  where fx :: SBool
fx    = b -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (b -> SBool) -> b -> SBool
forall a b. (a -> b) -> a -> b
$ ExistsUnique nm a -> b
f (SBV a -> ExistsUnique nm a
forall (nm :: Symbol) a. SBV a -> ExistsUnique nm a
ExistsUnique SBV a
x)
        fx1 :: b
fx1   = ExistsUnique nm a -> b
f (SBV a -> ExistsUnique nm a
forall (nm :: Symbol) a. SBV a -> ExistsUnique nm a
ExistsUnique SBV a
x1)
        fx2 :: b
fx2   = ExistsUnique nm a -> b
f (SBV a -> ExistsUnique nm a
forall (nm :: Symbol) a. SBV a -> ExistsUnique nm a
ExistsUnique SBV a
x2)

        bothHolds :: SBool
bothHolds  = b -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool b
fx1 SBool -> SBool -> SBool
.&& b -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool b
fx2
        mustEqual :: SBool
mustEqual  = SBV a
x1 SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x2
        unique :: SBool
unique     = SBool
bothHolds SBool -> SBool -> SBool
.=> SBool
mustEqual