{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Client.BaseIO where
import Data.SBV.Core.Data (HasKind, Kind, Outputtable, Penalty, SymArray,
SymVal, SBool, SBV, SChar, SDouble, SFloat,
SInt8, SInt16, SInt32, SInt64, SInteger, SList,
SReal, SString, SV, SWord8, SWord16, SWord32,
SWord64, SEither, SMaybe, SSet)
import Data.SBV.Core.Sized (SInt, SWord, IntN, WordN, IsNonZero)
import Data.SBV.Core.Model (Metric(..), SymTuple)
import Data.SBV.Core.Symbolic (Objective, OptimizeStyle, Result, VarContext,
Symbolic, SBVRunMode, SMTConfig, SVal)
import Data.SBV.Control.Types (SMTOption)
import Data.SBV.Provers.Prover (Provable, SExecutable, ThmResult)
import Data.SBV.SMT.SMT (AllSatResult, SafeResult, SatResult,
OptimizeResult)
import GHC.TypeLits
import Data.Kind
import Data.Int
import Data.Word
import qualified Data.SBV.Core.Data as Trans
import qualified Data.SBV.Core.Sized as Trans
import qualified Data.SBV.Core.Model as Trans
import qualified Data.SBV.Core.Symbolic as Trans
import qualified Data.SBV.Provers.Prover as Trans
forAll_ :: Provable a => a -> Symbolic SBool
forAll_ :: a -> Symbolic SBool
forAll_ = a -> Symbolic SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
Trans.forAll_
forAll :: Provable a => [String] -> a -> Symbolic SBool
forAll :: [String] -> a -> Symbolic SBool
forAll = [String] -> a -> Symbolic SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
Trans.forAll
forSome_ :: Provable a => a -> Symbolic SBool
forSome_ :: a -> Symbolic SBool
forSome_ = a -> Symbolic SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
Trans.forSome_
forSome :: Provable a => [String] -> a -> Symbolic SBool
forSome :: [String] -> a -> Symbolic SBool
forSome = [String] -> a -> Symbolic SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
Trans.forSome
prove :: Provable a => a -> IO ThmResult
prove :: a -> IO ThmResult
prove = a -> IO ThmResult
forall (m :: * -> *) a. MProvable m a => a -> m ThmResult
Trans.prove
proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
proveWith :: SMTConfig -> a -> IO ThmResult
proveWith = SMTConfig -> a -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
Trans.proveWith
dprove :: Provable a => a -> IO ThmResult
dprove :: a -> IO ThmResult
dprove = a -> IO ThmResult
forall (m :: * -> *) a. MProvable m a => a -> m ThmResult
Trans.dprove
dproveWith :: Provable a => SMTConfig -> a -> IO ThmResult
dproveWith :: SMTConfig -> a -> IO ThmResult
dproveWith = SMTConfig -> a -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
Trans.dproveWith
sat :: Provable a => a -> IO SatResult
sat :: a -> IO SatResult
sat = a -> IO SatResult
forall (m :: * -> *) a. MProvable m a => a -> m SatResult
Trans.sat
satWith :: Provable a => SMTConfig -> a -> IO SatResult
satWith :: SMTConfig -> a -> IO SatResult
satWith = SMTConfig -> a -> IO SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
Trans.satWith
dsat :: Provable a => a -> IO SatResult
dsat :: a -> IO SatResult
dsat = a -> IO SatResult
forall (m :: * -> *) a. MProvable m a => a -> m SatResult
Trans.dsat
dsatWith :: Provable a => SMTConfig -> a -> IO SatResult
dsatWith :: SMTConfig -> a -> IO SatResult
dsatWith = SMTConfig -> a -> IO SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
Trans.dsatWith
allSat :: Provable a => a -> IO AllSatResult
allSat :: a -> IO AllSatResult
allSat = a -> IO AllSatResult
forall (m :: * -> *) a. MProvable m a => a -> m AllSatResult
Trans.allSat
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
allSatWith :: SMTConfig -> a -> IO AllSatResult
allSatWith = SMTConfig -> a -> IO AllSatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m AllSatResult
Trans.allSatWith
optimize :: Provable a => OptimizeStyle -> a -> IO OptimizeResult
optimize :: OptimizeStyle -> a -> IO OptimizeResult
optimize = OptimizeStyle -> a -> IO OptimizeResult
forall (m :: * -> *) a.
MProvable m a =>
OptimizeStyle -> a -> m OptimizeResult
Trans.optimize
optimizeWith :: Provable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith :: SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith = SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
Trans.optimizeWith
isVacuous :: Provable a => a -> IO Bool
isVacuous :: a -> IO Bool
isVacuous = a -> IO Bool
forall (m :: * -> *) a. MProvable m a => a -> m Bool
Trans.isVacuous
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
isVacuousWith :: SMTConfig -> a -> IO Bool
isVacuousWith = SMTConfig -> a -> IO Bool
forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
Trans.isVacuousWith
isTheorem :: Provable a => a -> IO Bool
isTheorem :: a -> IO Bool
isTheorem = a -> IO Bool
forall (m :: * -> *) a. MProvable m a => a -> m Bool
Trans.isTheorem
isTheoremWith :: Provable a => SMTConfig -> a -> IO Bool
isTheoremWith :: SMTConfig -> a -> IO Bool
isTheoremWith = SMTConfig -> a -> IO Bool
forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
Trans.isTheoremWith
isSatisfiable :: Provable a => a -> IO Bool
isSatisfiable :: a -> IO Bool
isSatisfiable = a -> IO Bool
forall (m :: * -> *) a. MProvable m a => a -> m Bool
Trans.isSatisfiable
isSatisfiableWith :: Provable a => SMTConfig -> a -> IO Bool
isSatisfiableWith :: SMTConfig -> a -> IO Bool
isSatisfiableWith = SMTConfig -> a -> IO Bool
forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
Trans.isSatisfiableWith
runSMT :: Symbolic a -> IO a
runSMT :: Symbolic a -> IO a
runSMT = Symbolic a -> IO a
forall (m :: * -> *) a. MonadIO m => SymbolicT m a -> m a
Trans.runSMT
runSMTWith :: SMTConfig -> Symbolic a -> IO a
runSMTWith :: SMTConfig -> Symbolic a -> IO a
runSMTWith = SMTConfig -> Symbolic a -> IO a
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
Trans.runSMTWith
sName_ :: SExecutable IO a => a -> Symbolic ()
sName_ :: a -> Symbolic ()
sName_ = a -> Symbolic ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
Trans.sName_
sName :: SExecutable IO a => [String] -> a -> Symbolic ()
sName :: [String] -> a -> Symbolic ()
sName = [String] -> a -> Symbolic ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
Trans.sName
safe :: SExecutable IO a => a -> IO [SafeResult]
safe :: a -> IO [SafeResult]
safe = a -> IO [SafeResult]
forall (m :: * -> *) a. SExecutable m a => a -> m [SafeResult]
Trans.safe
safeWith :: SExecutable IO a => SMTConfig -> a -> IO [SafeResult]
safeWith :: SMTConfig -> a -> IO [SafeResult]
safeWith = SMTConfig -> a -> IO [SafeResult]
forall (m :: * -> *) a.
SExecutable m a =>
SMTConfig -> a -> m [SafeResult]
Trans.safeWith
mkSymSBV :: VarContext -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBV :: VarContext -> Kind -> Maybe String -> Symbolic (SBV a)
mkSymSBV = VarContext -> Kind -> Maybe String -> Symbolic (SBV a)
forall a (m :: * -> *).
MonadSymbolic m =>
VarContext -> Kind -> Maybe String -> m (SBV a)
Trans.mkSymSBV
sbvToSymSV :: SBV a -> Symbolic SV
sbvToSymSV :: SBV a -> Symbolic SV
sbvToSymSV = SBV a -> Symbolic SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
Trans.sbvToSymSV
output :: Outputtable a => a -> Symbolic a
output :: a -> Symbolic a
output = a -> Symbolic a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
Trans.output
forall :: SymVal a => String -> Symbolic (SBV a)
forall :: String -> Symbolic (SBV a)
forall = String -> Symbolic (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
Trans.forall
forall_ :: SymVal a => Symbolic (SBV a)
forall_ :: Symbolic (SBV a)
forall_ = Symbolic (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
Trans.forall_
mkForallVars :: SymVal a => Int -> Symbolic [SBV a]
mkForallVars :: Int -> Symbolic [SBV a]
mkForallVars = Int -> Symbolic [SBV a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Int -> m [SBV a]
Trans.mkForallVars
exists :: SymVal a => String -> Symbolic (SBV a)
exists :: String -> Symbolic (SBV a)
exists = String -> Symbolic (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
Trans.exists
exists_ :: SymVal a => Symbolic (SBV a)
exists_ :: Symbolic (SBV a)
exists_ = Symbolic (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
Trans.exists_
mkExistVars :: SymVal a => Int -> Symbolic [SBV a]
mkExistVars :: Int -> Symbolic [SBV a]
mkExistVars = Int -> Symbolic [SBV a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Int -> m [SBV a]
Trans.mkExistVars
free :: SymVal a => String -> Symbolic (SBV a)
free :: String -> Symbolic (SBV a)
free = String -> Symbolic (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
Trans.free
free_ :: SymVal a => Symbolic (SBV a)
free_ :: Symbolic (SBV a)
free_ = Symbolic (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
Trans.free_
mkFreeVars :: SymVal a => Int -> Symbolic [SBV a]
mkFreeVars :: Int -> Symbolic [SBV a]
mkFreeVars = Int -> Symbolic [SBV a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Int -> m [SBV a]
Trans.mkFreeVars
symbolic :: SymVal a => String -> Symbolic (SBV a)
symbolic :: String -> Symbolic (SBV a)
symbolic = String -> Symbolic (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
Trans.symbolic
symbolics :: SymVal a => [String] -> Symbolic [SBV a]
symbolics :: [String] -> Symbolic [SBV a]
symbolics = [String] -> Symbolic [SBV a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
Trans.symbolics
mkSymVal :: SymVal a => VarContext -> Maybe String -> Symbolic (SBV a)
mkSymVal :: VarContext -> Maybe String -> Symbolic (SBV a)
mkSymVal = VarContext -> Maybe String -> Symbolic (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe String -> m (SBV a)
Trans.mkSymVal
newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)
newArray_ :: Maybe (SBV b) -> Symbolic (array a b)
newArray_ = Maybe (SBV b) -> Symbolic (array a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
Trans.newArray_
newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)
newArray :: String -> Maybe (SBV b) -> Symbolic (array a b)
newArray = String -> Maybe (SBV b) -> Symbolic (array a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
Trans.newArray
genMkSymVar :: Kind -> VarContext -> Maybe String -> Symbolic (SBV a)
genMkSymVar :: Kind -> VarContext -> Maybe String -> Symbolic (SBV a)
genMkSymVar = Kind -> VarContext -> Maybe String -> Symbolic (SBV a)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
Trans.genMkSymVar
sBool :: String -> Symbolic SBool
sBool :: String -> Symbolic SBool
sBool = String -> Symbolic SBool
forall (m :: * -> *). MonadSymbolic m => String -> m SBool
Trans.sBool
sBool_ :: Symbolic SBool
sBool_ :: Symbolic SBool
sBool_ = Symbolic SBool
forall (m :: * -> *). MonadSymbolic m => m SBool
Trans.sBool_
sBools :: [String] -> Symbolic [SBool]
sBools :: [String] -> Symbolic [SBool]
sBools = [String] -> Symbolic [SBool]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SBool]
Trans.sBools
sWord8 :: String -> Symbolic SWord8
sWord8 :: String -> Symbolic SWord8
sWord8 = String -> Symbolic SWord8
forall (m :: * -> *). MonadSymbolic m => String -> m SWord8
Trans.sWord8
sWord8_ :: Symbolic SWord8
sWord8_ :: Symbolic SWord8
sWord8_ = Symbolic SWord8
forall (m :: * -> *). MonadSymbolic m => m SWord8
Trans.sWord8_
sWord8s :: [String] -> Symbolic [SWord8]
sWord8s :: [String] -> Symbolic [SWord8]
sWord8s = [String] -> Symbolic [SWord8]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord8]
Trans.sWord8s
sWord16 :: String -> Symbolic SWord16
sWord16 :: String -> Symbolic SWord16
sWord16 = String -> Symbolic SWord16
forall (m :: * -> *). MonadSymbolic m => String -> m SWord16
Trans.sWord16
sWord16_ :: Symbolic SWord16
sWord16_ :: Symbolic SWord16
sWord16_ = Symbolic SWord16
forall (m :: * -> *). MonadSymbolic m => m SWord16
Trans.sWord16_
sWord16s :: [String] -> Symbolic [SWord16]
sWord16s :: [String] -> Symbolic [SWord16]
sWord16s = [String] -> Symbolic [SWord16]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord16]
Trans.sWord16s
sWord32 :: String -> Symbolic SWord32
sWord32 :: String -> Symbolic SWord32
sWord32 = String -> Symbolic SWord32
forall (m :: * -> *). MonadSymbolic m => String -> m SWord32
Trans.sWord32
sWord32_ :: Symbolic SWord32
sWord32_ :: Symbolic SWord32
sWord32_ = Symbolic SWord32
forall (m :: * -> *). MonadSymbolic m => m SWord32
Trans.sWord32_
sWord32s :: [String] -> Symbolic [SWord32]
sWord32s :: [String] -> Symbolic [SWord32]
sWord32s = [String] -> Symbolic [SWord32]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord32]
Trans.sWord32s
sWord64 :: String -> Symbolic SWord64
sWord64 :: String -> Symbolic SWord64
sWord64 = String -> Symbolic SWord64
forall (m :: * -> *). MonadSymbolic m => String -> m SWord64
Trans.sWord64
sWord64_ :: Symbolic SWord64
sWord64_ :: Symbolic SWord64
sWord64_ = Symbolic SWord64
forall (m :: * -> *). MonadSymbolic m => m SWord64
Trans.sWord64_
sWord64s :: [String] -> Symbolic [SWord64]
sWord64s :: [String] -> Symbolic [SWord64]
sWord64s = [String] -> Symbolic [SWord64]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SWord64]
Trans.sWord64s
sWord :: (KnownNat n, IsNonZero n) => String -> Symbolic (SWord n)
sWord :: String -> Symbolic (SWord n)
sWord = String -> Symbolic (SWord n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, IsNonZero n, MonadSymbolic m) =>
String -> m (SWord n)
Trans.sWord
sWord_ :: (KnownNat n, IsNonZero n) => Symbolic (SWord n)
sWord_ :: Symbolic (SWord n)
sWord_ = Symbolic (SWord n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, IsNonZero n, MonadSymbolic m) =>
m (SWord n)
Trans.sWord_
sWords :: (KnownNat n, IsNonZero n) => [String] -> Symbolic [SWord n]
sWords :: [String] -> Symbolic [SWord n]
sWords = [String] -> Symbolic [SWord n]
forall (n :: Nat) (m :: * -> *).
(KnownNat n, IsNonZero n, MonadSymbolic m) =>
[String] -> m [SWord n]
Trans.sWords
sInt8 :: String -> Symbolic SInt8
sInt8 :: String -> Symbolic SInt8
sInt8 = String -> Symbolic SInt8
forall (m :: * -> *). MonadSymbolic m => String -> m SInt8
Trans.sInt8
sInt8_ :: Symbolic SInt8
sInt8_ :: Symbolic SInt8
sInt8_ = Symbolic SInt8
forall (m :: * -> *). MonadSymbolic m => m SInt8
Trans.sInt8_
sInt8s :: [String] -> Symbolic [SInt8]
sInt8s :: [String] -> Symbolic [SInt8]
sInt8s = [String] -> Symbolic [SInt8]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt8]
Trans.sInt8s
sInt16 :: String -> Symbolic SInt16
sInt16 :: String -> Symbolic SInt16
sInt16 = String -> Symbolic SInt16
forall (m :: * -> *). MonadSymbolic m => String -> m SInt16
Trans.sInt16
sInt16_ :: Symbolic SInt16
sInt16_ :: Symbolic SInt16
sInt16_ = Symbolic SInt16
forall (m :: * -> *). MonadSymbolic m => m SInt16
Trans.sInt16_
sInt16s :: [String] -> Symbolic [SInt16]
sInt16s :: [String] -> Symbolic [SInt16]
sInt16s = [String] -> Symbolic [SInt16]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt16]
Trans.sInt16s
sInt32 :: String -> Symbolic SInt32
sInt32 :: String -> Symbolic SInt32
sInt32 = String -> Symbolic SInt32
forall (m :: * -> *). MonadSymbolic m => String -> m SInt32
Trans.sInt32
sInt32_ :: Symbolic SInt32
sInt32_ :: Symbolic SInt32
sInt32_ = Symbolic SInt32
forall (m :: * -> *). MonadSymbolic m => m SInt32
Trans.sInt32_
sInt32s :: [String] -> Symbolic [SInt32]
sInt32s :: [String] -> Symbolic [SInt32]
sInt32s = [String] -> Symbolic [SInt32]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt32]
Trans.sInt32s
sInt64 :: String -> Symbolic SInt64
sInt64 :: String -> Symbolic SInt64
sInt64 = String -> Symbolic SInt64
forall (m :: * -> *). MonadSymbolic m => String -> m SInt64
Trans.sInt64
sInt64_ :: Symbolic SInt64
sInt64_ :: Symbolic SInt64
sInt64_ = Symbolic SInt64
forall (m :: * -> *). MonadSymbolic m => m SInt64
Trans.sInt64_
sInt64s :: [String] -> Symbolic [SInt64]
sInt64s :: [String] -> Symbolic [SInt64]
sInt64s = [String] -> Symbolic [SInt64]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInt64]
Trans.sInt64s
sInt :: (KnownNat n, IsNonZero n) => String -> Symbolic (SInt n)
sInt :: String -> Symbolic (SInt n)
sInt = String -> Symbolic (SInt n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, IsNonZero n, MonadSymbolic m) =>
String -> m (SInt n)
Trans.sInt
sInt_ :: (KnownNat n, IsNonZero n) => Symbolic (SInt n)
sInt_ :: Symbolic (SInt n)
sInt_ = Symbolic (SInt n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, IsNonZero n, MonadSymbolic m) =>
m (SInt n)
Trans.sInt_
sInts :: (KnownNat n, IsNonZero n) => [String] -> Symbolic [SInt n]
sInts :: [String] -> Symbolic [SInt n]
sInts = [String] -> Symbolic [SInt n]
forall (n :: Nat) (m :: * -> *).
(KnownNat n, IsNonZero n, MonadSymbolic m) =>
[String] -> m [SInt n]
Trans.sInts
sInteger :: String -> Symbolic SInteger
sInteger :: String -> Symbolic SInteger
sInteger = String -> Symbolic SInteger
forall (m :: * -> *). MonadSymbolic m => String -> m SInteger
Trans.sInteger
sInteger_ :: Symbolic SInteger
sInteger_ :: Symbolic SInteger
sInteger_ = Symbolic SInteger
forall (m :: * -> *). MonadSymbolic m => m SInteger
Trans.sInteger_
sIntegers :: [String] -> Symbolic [SInteger]
sIntegers :: [String] -> Symbolic [SInteger]
sIntegers = [String] -> Symbolic [SInteger]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SInteger]
Trans.sIntegers
sReal :: String -> Symbolic SReal
sReal :: String -> Symbolic SReal
sReal = String -> Symbolic SReal
forall (m :: * -> *). MonadSymbolic m => String -> m SReal
Trans.sReal
sReal_ :: Symbolic SReal
sReal_ :: Symbolic SReal
sReal_ = Symbolic SReal
forall (m :: * -> *). MonadSymbolic m => m SReal
Trans.sReal_
sReals :: [String] -> Symbolic [SReal]
sReals :: [String] -> Symbolic [SReal]
sReals = [String] -> Symbolic [SReal]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SReal]
Trans.sReals
sFloat :: String -> Symbolic SFloat
sFloat :: String -> Symbolic SFloat
sFloat = String -> Symbolic SFloat
forall (m :: * -> *). MonadSymbolic m => String -> m SFloat
Trans.sFloat
sFloat_ :: Symbolic SFloat
sFloat_ :: Symbolic SFloat
sFloat_ = Symbolic SFloat
forall (m :: * -> *). MonadSymbolic m => m SFloat
Trans.sFloat_
sFloats :: [String] -> Symbolic [SFloat]
sFloats :: [String] -> Symbolic [SFloat]
sFloats = [String] -> Symbolic [SFloat]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SFloat]
Trans.sFloats
sDouble :: String -> Symbolic SDouble
sDouble :: String -> Symbolic SDouble
sDouble = String -> Symbolic SDouble
forall (m :: * -> *). MonadSymbolic m => String -> m SDouble
Trans.sDouble
sDouble_ :: Symbolic SDouble
sDouble_ :: Symbolic SDouble
sDouble_ = Symbolic SDouble
forall (m :: * -> *). MonadSymbolic m => m SDouble
Trans.sDouble_
sDoubles :: [String] -> Symbolic [SDouble]
sDoubles :: [String] -> Symbolic [SDouble]
sDoubles = [String] -> Symbolic [SDouble]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SDouble]
Trans.sDoubles
sChar :: String -> Symbolic SChar
sChar :: String -> Symbolic SChar
sChar = String -> Symbolic SChar
forall (m :: * -> *). MonadSymbolic m => String -> m SChar
Trans.sChar
sChar_ :: Symbolic SChar
sChar_ :: Symbolic SChar
sChar_ = Symbolic SChar
forall (m :: * -> *). MonadSymbolic m => m SChar
Trans.sChar_
sChars :: [String] -> Symbolic [SChar]
sChars :: [String] -> Symbolic [SChar]
sChars = [String] -> Symbolic [SChar]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SChar]
Trans.sChars
sString :: String -> Symbolic SString
sString :: String -> Symbolic SString
sString = String -> Symbolic SString
forall (m :: * -> *). MonadSymbolic m => String -> m SString
Trans.sString
sString_ :: Symbolic SString
sString_ :: Symbolic SString
sString_ = Symbolic SString
forall (m :: * -> *). MonadSymbolic m => m SString
Trans.sString_
sStrings :: [String] -> Symbolic [SString]
sStrings :: [String] -> Symbolic [SString]
sStrings = [String] -> Symbolic [SString]
forall (m :: * -> *). MonadSymbolic m => [String] -> m [SString]
Trans.sStrings
sList :: SymVal a => String -> Symbolic (SList a)
sList :: String -> Symbolic (SList a)
sList = String -> Symbolic (SList a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SList a)
Trans.sList
sList_ :: SymVal a => Symbolic (SList a)
sList_ :: Symbolic (SList a)
sList_ = Symbolic (SList a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SList a)
Trans.sList_
sLists :: SymVal a => [String] -> Symbolic [SList a]
sLists :: [String] -> Symbolic [SList a]
sLists = [String] -> Symbolic [SList a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SList a]
Trans.sLists
sTuple :: (SymTuple tup, SymVal tup) => String -> Symbolic (SBV tup)
sTuple :: String -> Symbolic (SBV tup)
sTuple = String -> Symbolic (SBV tup)
forall tup (m :: * -> *).
(SymTuple tup, SymVal tup, MonadSymbolic m) =>
String -> m (SBV tup)
Trans.sTuple
sTuple_ :: (SymTuple tup, SymVal tup) => Symbolic (SBV tup)
sTuple_ :: Symbolic (SBV tup)
sTuple_ = Symbolic (SBV tup)
forall tup (m :: * -> *).
(SymTuple tup, SymVal tup, MonadSymbolic m) =>
m (SBV tup)
Trans.sTuple_
sTuples :: (SymTuple tup, SymVal tup) => [String] -> Symbolic [SBV tup]
sTuples :: [String] -> Symbolic [SBV tup]
sTuples = [String] -> Symbolic [SBV tup]
forall tup (m :: * -> *).
(SymTuple tup, SymVal tup, MonadSymbolic m) =>
[String] -> m [SBV tup]
Trans.sTuples
sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b)
sEither :: String -> Symbolic (SEither a b)
sEither = String -> Symbolic (SEither a b)
forall a b (m :: * -> *).
(SymVal a, SymVal b, MonadSymbolic m) =>
String -> m (SEither a b)
Trans.sEither
sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b)
sEither_ :: Symbolic (SEither a b)
sEither_ = Symbolic (SEither a b)
forall a b (m :: * -> *).
(SymVal a, SymVal b, MonadSymbolic m) =>
m (SEither a b)
Trans.sEither_
sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b]
sEithers :: [String] -> Symbolic [SEither a b]
sEithers = [String] -> Symbolic [SEither a b]
forall a b (m :: * -> *).
(SymVal a, SymVal b, MonadSymbolic m) =>
[String] -> m [SEither a b]
Trans.sEithers
sMaybe :: SymVal a => String -> Symbolic (SMaybe a)
sMaybe :: String -> Symbolic (SMaybe a)
sMaybe = String -> Symbolic (SMaybe a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SMaybe a)
Trans.sMaybe
sMaybe_ :: SymVal a => Symbolic (SMaybe a)
sMaybe_ :: Symbolic (SMaybe a)
sMaybe_ = Symbolic (SMaybe a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SMaybe a)
Trans.sMaybe_
sMaybes :: SymVal a => [String] -> Symbolic [SMaybe a]
sMaybes :: [String] -> Symbolic [SMaybe a]
sMaybes = [String] -> Symbolic [SMaybe a]
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SMaybe a]
Trans.sMaybes
sSet :: (Ord a, SymVal a) => String -> Symbolic (SSet a)
sSet :: String -> Symbolic (SSet a)
sSet = String -> Symbolic (SSet a)
forall a (m :: * -> *).
(Ord a, SymVal a, MonadSymbolic m) =>
String -> m (SSet a)
Trans.sSet
sSet_ :: (Ord a, SymVal a) => Symbolic (SSet a)
sSet_ :: Symbolic (SSet a)
sSet_ = Symbolic (SSet a)
forall a (m :: * -> *).
(Ord a, SymVal a, MonadSymbolic m) =>
m (SSet a)
Trans.sSet_
sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a]
sSets :: [String] -> Symbolic [SSet a]
sSets = [String] -> Symbolic [SSet a]
forall a (m :: * -> *).
(Ord a, SymVal a, MonadSymbolic m) =>
[String] -> m [SSet a]
Trans.sSets
solve :: [SBool] -> Symbolic SBool
solve :: [SBool] -> Symbolic SBool
solve = [SBool] -> Symbolic SBool
forall (m :: * -> *). MonadSymbolic m => [SBool] -> m SBool
Trans.solve
assertWithPenalty :: String -> SBool -> Penalty -> Symbolic ()
assertWithPenalty :: String -> SBool -> Penalty -> Symbolic ()
assertWithPenalty = String -> SBool -> Penalty -> Symbolic ()
forall (m :: * -> *).
MonadSymbolic m =>
String -> SBool -> Penalty -> m ()
Trans.assertWithPenalty
minimize :: Metric a => String -> SBV a -> Symbolic ()
minimize :: String -> SBV a -> Symbolic ()
minimize = String -> SBV a -> Symbolic ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
Trans.minimize
maximize :: Metric a => String -> SBV a -> Symbolic ()
maximize :: String -> SBV a -> Symbolic ()
maximize = String -> SBV a -> Symbolic ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
Trans.maximize
svToSymSV :: SVal -> Symbolic SV
svToSymSV :: SVal -> Symbolic SV
svToSymSV = SVal -> Symbolic SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
Trans.svToSymSV
runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
runSymbolic = SBVRunMode -> Symbolic a -> IO (a, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
Trans.runSymbolic
addNewSMTOption :: SMTOption -> Symbolic ()
addNewSMTOption :: SMTOption -> Symbolic ()
addNewSMTOption = SMTOption -> Symbolic ()
forall (m :: * -> *). MonadSymbolic m => SMTOption -> m ()
Trans.addNewSMTOption
imposeConstraint :: Bool -> [(String, String)] -> SVal -> Symbolic ()
imposeConstraint :: Bool -> [(String, String)] -> SVal -> Symbolic ()
imposeConstraint = Bool -> [(String, String)] -> SVal -> Symbolic ()
forall (m :: * -> *).
MonadSymbolic m =>
Bool -> [(String, String)] -> SVal -> m ()
Trans.imposeConstraint
addSValOptGoal :: Objective SVal -> Symbolic ()
addSValOptGoal :: Objective SVal -> Symbolic ()
addSValOptGoal = Objective SVal -> Symbolic ()
forall (m :: * -> *). MonadSymbolic m => Objective SVal -> m ()
Trans.addSValOptGoal
outputSVal :: SVal -> Symbolic ()
outputSVal :: SVal -> Symbolic ()
outputSVal = SVal -> Symbolic ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
Trans.outputSVal
type FromSizedErr (arg :: Type) = 'Text "fromSized: Cannot convert from type: " ':<>: 'ShowType arg
':$$: 'Text " Source type must be one of SInt N, SWord N, IntN N, WordN N"
':$$: 'Text " where N is 8, 16, 32, or 64."
type ToSizedErr (arg :: Type) = 'Text "toSized: Cannot convert from type: " ':<>: 'ShowType arg
':$$: 'Text " Source type must be one of Int8/16/32/64"
':$$: 'Text " OR Word8/16/32/64"
':$$: 'Text " OR their symbolic variants."
type family FromSized (t :: Type) :: Type where
FromSized (WordN 8) = Word8
FromSized (WordN 16) = Word16
FromSized (WordN 32) = Word32
FromSized (WordN 64) = Word64
FromSized (IntN 8) = Int8
FromSized (IntN 16) = Int16
FromSized (IntN 32) = Int32
FromSized (IntN 64) = Int64
FromSized (SWord 8) = SWord8
FromSized (SWord 16) = SWord16
FromSized (SWord 32) = SWord32
FromSized (SWord 64) = SWord64
FromSized (SInt 8) = SInt8
FromSized (SInt 16) = SInt16
FromSized (SInt 32) = SInt32
FromSized (SInt 64) = SInt64
type family FromSizedCstr (t :: Type) :: Constraint where
FromSizedCstr (WordN 8) = ()
FromSizedCstr (WordN 16) = ()
FromSizedCstr (WordN 32) = ()
FromSizedCstr (WordN 64) = ()
FromSizedCstr (IntN 8) = ()
FromSizedCstr (IntN 16) = ()
FromSizedCstr (IntN 32) = ()
FromSizedCstr (IntN 64) = ()
FromSizedCstr (SWord 8) = ()
FromSizedCstr (SWord 16) = ()
FromSizedCstr (SWord 32) = ()
FromSizedCstr (SWord 64) = ()
FromSizedCstr (SInt 8) = ()
FromSizedCstr (SInt 16) = ()
FromSizedCstr (SInt 32) = ()
FromSizedCstr (SInt 64) = ()
FromSizedCstr arg = TypeError (FromSizedErr arg)
class FromSizedBV a where
fromSized :: a -> FromSized a
default fromSized :: (Num (FromSized a), Integral a) => a -> FromSized a
fromSized = a -> FromSized a
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (WordN 8)
instance {-# OVERLAPPING #-} FromSizedBV (WordN 16)
instance {-# OVERLAPPING #-} FromSizedBV (WordN 32)
instance {-# OVERLAPPING #-} FromSizedBV (WordN 64)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 8)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 16)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 32)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 64)
instance {-# OVERLAPPING #-} FromSizedBV (SWord 8) where fromSized :: SWord 8 -> FromSized (SWord 8)
fromSized = SWord 8 -> FromSized (SWord 8)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SWord 16) where fromSized :: SWord 16 -> FromSized (SWord 16)
fromSized = SWord 16 -> FromSized (SWord 16)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SWord 32) where fromSized :: SWord 32 -> FromSized (SWord 32)
fromSized = SWord 32 -> FromSized (SWord 32)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SWord 64) where fromSized :: SWord 64 -> FromSized (SWord 64)
fromSized = SWord 64 -> FromSized (SWord 64)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 8) where fromSized :: SInt 8 -> FromSized (SInt 8)
fromSized = SInt 8 -> FromSized (SInt 8)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 16) where fromSized :: SInt 16 -> FromSized (SInt 16)
fromSized = SInt 16 -> FromSized (SInt 16)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 32) where fromSized :: SInt 32 -> FromSized (SInt 32)
fromSized = SInt 32 -> FromSized (SInt 32)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 64) where fromSized :: SInt 64 -> FromSized (SInt 64)
fromSized = SInt 64 -> FromSized (SInt 64)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPABLE #-} FromSizedCstr arg => FromSizedBV arg where fromSized :: arg -> FromSized arg
fromSized = String -> arg -> FromSized arg
forall a. HasCallStack => String -> a
error String
"unreachable"
type family ToSized (t :: Type) :: Type where
ToSized Word8 = WordN 8
ToSized Word16 = WordN 16
ToSized Word32 = WordN 32
ToSized Word64 = WordN 64
ToSized Int8 = IntN 8
ToSized Int16 = IntN 16
ToSized Int32 = IntN 32
ToSized Int64 = IntN 64
ToSized SWord8 = SWord 8
ToSized SWord16 = SWord 16
ToSized SWord32 = SWord 32
ToSized SWord64 = SWord 64
ToSized SInt8 = SInt 8
ToSized SInt16 = SInt 16
ToSized SInt32 = SInt 32
ToSized SInt64 = SInt 64
type family ToSizedCstr (t :: Type) :: Constraint where
ToSizedCstr Word8 = ()
ToSizedCstr Word16 = ()
ToSizedCstr Word32 = ()
ToSizedCstr Word64 = ()
ToSizedCstr Int8 = ()
ToSizedCstr Int16 = ()
ToSizedCstr Int32 = ()
ToSizedCstr Int64 = ()
ToSizedCstr SWord8 = ()
ToSizedCstr SWord16 = ()
ToSizedCstr SWord32 = ()
ToSizedCstr SWord64 = ()
ToSizedCstr SInt8 = ()
ToSizedCstr SInt16 = ()
ToSizedCstr SInt32 = ()
ToSizedCstr SInt64 = ()
ToSizedCstr arg = TypeError (ToSizedErr arg)
class ToSizedBV a where
toSized :: a -> ToSized a
default toSized :: (Num (ToSized a), Integral a) => (a -> ToSized a)
toSized = a -> ToSized a
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance {-# OVERLAPPING #-} ToSizedBV Word8
instance {-# OVERLAPPING #-} ToSizedBV Word16
instance {-# OVERLAPPING #-} ToSizedBV Word32
instance {-# OVERLAPPING #-} ToSizedBV Word64
instance {-# OVERLAPPING #-} ToSizedBV Int8
instance {-# OVERLAPPING #-} ToSizedBV Int16
instance {-# OVERLAPPING #-} ToSizedBV Int32
instance {-# OVERLAPPING #-} ToSizedBV Int64
instance {-# OVERLAPPING #-} ToSizedBV SWord8 where toSized :: SWord8 -> ToSized SWord8
toSized = SWord8 -> ToSized SWord8
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SWord16 where toSized :: SWord16 -> ToSized SWord16
toSized = SWord16 -> ToSized SWord16
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SWord32 where toSized :: SWord32 -> ToSized SWord32
toSized = SWord32 -> ToSized SWord32
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SWord64 where toSized :: SWord64 -> ToSized SWord64
toSized = SWord64 -> ToSized SWord64
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt8 where toSized :: SInt8 -> ToSized SInt8
toSized = SInt8 -> ToSized SInt8
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt16 where toSized :: SInt16 -> ToSized SInt16
toSized = SInt16 -> ToSized SInt16
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt32 where toSized :: SInt32 -> ToSized SInt32
toSized = SInt32 -> ToSized SInt32
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt64 where toSized :: SInt64 -> ToSized SInt64
toSized = SInt64 -> ToSized SInt64
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
SymVal b) =>
SBV a -> SBV b
Trans.sFromIntegral
instance {-# OVERLAPPABLE #-} ToSizedCstr arg => ToSizedBV arg where toSized :: arg -> ToSized arg
toSized = String -> arg -> ToSized arg
forall a. HasCallStack => String -> a
error String
"unreachable"