-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Dynamic
-- Copyright : (c) Brian Huffman
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Dynamically typed low-level API to the SBV library, for users who
-- want to generate symbolic values at run-time. Note that with this
-- API it is possible to create terms that are not type correct; use
-- at your own risk!
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Dynamic
  (
  -- * Programming with symbolic values
  -- ** Symbolic types
  -- *** Abstract symbolic value type
    SVal
  , HasKind(..), Kind(..), CV(..), CVal(..), cvToBool
  -- ** Creating a symbolic variable
  , Symbolic
  , Quantifier(..)
  , svMkSymVar, svNewVar_, svNewVar
  , sWordN, sWordN_, sIntN, sIntN_
  -- ** Operations on symbolic values
  -- *** Boolean literals
  , svTrue, svFalse, svBool, svAsBool
  -- *** Integer literals
  , svInteger, svAsInteger
  -- *** Float literals
  , svFloat, svDouble, svFloatingPoint
  -- *** Algebraic reals (only from rationals)
  , svReal, svNumerator, svDenominator
  -- *** Symbolic equality
  , svEqual, svNotEqual, svStrongEqual
  -- *** Constructing concrete lists
  , svEnumFromThenTo
  -- *** Symbolic ordering
  , svLessThan, svGreaterThan, svLessEq, svGreaterEq, svStructuralLessThan
  -- *** Arithmetic operations
  , svPlus, svTimes, svMinus, svUNeg, svAbs
  , svDivide, svQuot, svRem, svQuotRem, svExp
  , svAddConstant, svIncrement, svDecrement
  -- *** Logical operations
  , svAnd, svOr, svXOr, svNot
  , svShl, svShr, svRol, svRor
  -- *** Splitting, joining, and extending
  , svExtract, svJoin, svZeroExtend, svSignExtend
  -- *** Sign-casting
  , svSign, svUnsign
  -- *** Numeric conversions
  , svFromIntegral
  -- *** Indexed lookups
  , svSelect
  -- *** Word-level operations
  , svToWord1, svFromWord1, svTestBit, svSetBit
  , svShiftLeft, svShiftRight
  , svRotateLeft, svRotateRight
  , svBarrelRotateLeft, svBarrelRotateRight
  , svWordFromBE, svWordFromLE
  , svBlastLE, svBlastBE
  -- ** Conditionals: Mergeable values
  , svIte, svLazyIte, svSymbolicMerge
  -- * Uninterpreted sorts, constants, and functions
  , svUninterpreted
  -- * Properties, proofs, and satisfiability
  -- ** Proving properties
  , proveWith
  -- ** Checking satisfiability
  , satWith, allSatWith
  -- ** Checking safety
  , safeWith
  -- * Proving properties using multiple solvers
  , proveWithAll, proveWithAny, satWithAll, satWithAny
  -- * Proving properties using multiple threads
  , proveConcurrentWithAll, proveConcurrentWithAny
  , satConcurrentWithAny, satConcurrentWithAll
  -- * Quick-check
  , svQuickCheck

  -- * Model extraction

  -- ** Inspecting proof results
  , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)

  -- ** Programmable model extraction
  , genParse, getModelAssignment, getModelDictionary
  -- * SMT Interface: Configurations and solvers
  , SMTConfig(..), SMTLibVersion(..), Solver(..), SMTSolver(..), boolector, bitwuzla, cvc4, cvc5, dReal, yices, z3, mathSAT, abc, defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers

  -- * Symbolic computations
  , outputSVal

  -- * Code generation from symbolic programs
  , SBVCodeGen

  -- ** Setting code-generation options
  , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile

  -- ** Designating inputs
  , svCgInput, svCgInputArr

  -- ** Designating outputs
  , svCgOutput, svCgOutputArr

  -- ** Designating return values
  , svCgReturn, svCgReturnArr

  -- ** Code generation with uninterpreted functions
  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert

  -- ** Code generation with 'Data.SBV.SInteger' and 'Data.SBV.SReal' types
  , cgIntegerSize, cgSRealType, CgSRealType(..)

  -- ** Compilation to C
  , compileToC, compileToCLib

  -- ** Compilation to SMTLib
  , generateSMTBenchmarkSat, generateSMTBenchmarkProof
  ) where

import Control.Monad.Trans (liftIO)

import Data.Map.Strict (Map)

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

import Data.SBV.Compilers.CodeGen ( SBVCodeGen
                                  , svCgInput, svCgInputArr
                                  , svCgOutput, svCgOutputArr
                                  , svCgReturn, svCgReturnArr
                                  , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
                                  , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert
                                  , cgIntegerSize, cgSRealType, CgSRealType(..)
                                  )
import Data.SBV.Compilers.C       (compileToC, compileToCLib)

import Data.SBV.Provers.Prover (boolector, bitwuzla, cvc4, cvc5, dReal, yices, z3, mathSAT, abc, defaultSMTCfg)
import Data.SBV.SMT.SMT        (ThmResult(..), SatResult(..), SafeResult(..), OptimizeResult(..), AllSatResult(..), genParse)
import Data.SBV                (sbvCheckSolverInstallation, defaultSolverConfig, getAvailableSolvers)

import qualified Data.SBV                as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny
                                                , proveConcurrentWithAll, proveConcurrentWithAny
                                                , satConcurrentWithAny, satConcurrentWithAll
                                                )
import qualified Data.SBV.Core.Data      as SBV (SBV(..))
import qualified Data.SBV.Core.Model     as SBV (sbvQuickCheck)
import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, safeWith, allSatWith, generateSMTBenchmarkSat, generateSMTBenchmarkProof)
import qualified Data.SBV.SMT.SMT        as SBV (Modelable(getModelAssignment, getModelDictionary))

import Data.Time (NominalDiffTime)

-- | Dynamic variant of quick-check
svQuickCheck :: Symbolic SVal -> IO Bool
svQuickCheck :: Symbolic SVal -> IO Bool
svQuickCheck = SymbolicT IO SBool -> IO Bool
SBV.sbvQuickCheck (SymbolicT IO SBool -> IO Bool)
-> (Symbolic SVal -> SymbolicT IO SBool)
-> Symbolic SVal
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool

toSBool :: SVal -> SBV.SBool
toSBool :: SVal -> SBool
toSBool = SVal -> SBool
forall a. SVal -> SBV a
SBV.SBV

-- | Create SMT-Lib benchmark for a sat call
generateSMTBenchmarkSat :: Symbolic SVal -> IO String
generateSMTBenchmarkSat :: Symbolic SVal -> IO String
generateSMTBenchmarkSat Symbolic SVal
s = SymbolicT IO SBool -> IO String
forall (m :: * -> *) a. SatisfiableM m a => a -> m String
SBV.generateSMTBenchmarkSat ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Create SMT-Lib benchmark for a proof call
generateSMTBenchmarkProof :: Symbolic SVal -> IO String
generateSMTBenchmarkProof :: Symbolic SVal -> IO String
generateSMTBenchmarkProof Symbolic SVal
s = SymbolicT IO SBool -> IO String
forall (m :: * -> *) a. ProvableM m a => a -> m String
SBV.generateSMTBenchmarkProof ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Proves the predicate using the given SMT-solver
proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
proveWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> SymbolicT IO SBool -> IO ThmResult
forall (m :: * -> *) a.
ProvableM m a =>
SMTConfig -> a -> m ThmResult
SBV.proveWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Find a satisfying assignment using the given SMT-solver
satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
satWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> SymbolicT IO SBool -> IO SatResult
forall (m :: * -> *) a.
SatisfiableM m a =>
SMTConfig -> a -> m SatResult
SBV.satWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Check safety using the given SMT-solver
safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
safeWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> SymbolicT IO SBool -> IO [SafeResult]
forall (m :: * -> *) a.
SExecutable m a =>
SMTConfig -> a -> m [SafeResult]
SBV.safeWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Find all satisfying assignments using the given SMT-solver
allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
allSatWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> SymbolicT IO SBool -> IO AllSatResult
forall (m :: * -> *) a.
SatisfiableM m a =>
SMTConfig -> a -> m AllSatResult
SBV.allSatWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Prove a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll :: [SMTConfig]
-> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> SymbolicT IO SBool -> IO [(Solver, NominalDiffTime, ThmResult)]
forall a.
Provable a =>
[SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
SBV.proveWithAll [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Prove a property with multiple solvers, running them in separate
-- threads. Only the result of the first one to finish will be
-- returned, remaining threads will be killed.
proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny :: [SMTConfig]
-> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> SymbolicT IO SBool -> IO (Solver, NominalDiffTime, ThmResult)
forall a.
Provable a =>
[SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
SBV.proveWithAny [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Prove a property with query mode using multiple threads. Each query
-- computation will spawn a thread and a unique instance of your solver to run
-- asynchronously. The 'Symbolic' t'SVal' is duplicated for each thread. This
-- function will block until all child threads return.
proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll :: SMTConfig
-> Symbolic SVal
-> [Query SVal]
-> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll SMTConfig
cfg Symbolic SVal
s [Query SVal]
queries = SMTConfig
-> [Query SVal]
-> SymbolicT IO SBool
-> IO [(Solver, NominalDiffTime, ThmResult)]
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
SBV.proveConcurrentWithAll SMTConfig
cfg [Query SVal]
queries ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Prove a property with query mode using multiple threads. Each query
-- computation will spawn a thread and a unique instance of your solver to run
-- asynchronously. The 'Symbolic' t'SVal' is duplicated for each thread. This
-- function will return the first query computation that completes, killing the others.
proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny :: SMTConfig
-> Symbolic SVal
-> [Query SVal]
-> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny SMTConfig
cfg Symbolic SVal
s [Query SVal]
queries = SMTConfig
-> [Query SVal]
-> SymbolicT IO SBool
-> IO (Solver, NominalDiffTime, ThmResult)
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
SBV.proveConcurrentWithAny SMTConfig
cfg [Query SVal]
queries ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Find a satisfying assignment to a property with multiple solvers,
-- running them in separate threads. The results will be returned in
-- the order produced.
satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll :: [SMTConfig]
-> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> SymbolicT IO SBool -> IO [(Solver, NominalDiffTime, SatResult)]
forall a.
Satisfiable a =>
[SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
SBV.satWithAll [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Find a satisfying assignment to a property with multiple solvers,
-- running them in separate threads. Only the result of the first one
-- to finish will be returned, remaining threads will be killed.
satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
satWithAny :: [SMTConfig]
-> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
satWithAny [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> SymbolicT IO SBool -> IO (Solver, NominalDiffTime, SatResult)
forall a.
Satisfiable a =>
[SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
SBV.satWithAny [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Find a satisfying assignment to a property with multiple threads in query
-- mode. The 'Symbolic' t'SVal' represents what is known to all child query threads.
-- Each query thread will spawn a unique instance of the solver. Only the first
-- one to finish will be returned and the other threads will be killed.
satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny :: forall b.
SMTConfig
-> [Query b]
-> Symbolic SVal
-> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny SMTConfig
cfg [Query b]
qs Symbolic SVal
s = SMTConfig
-> [Query b]
-> SymbolicT IO SBool
-> IO (Solver, NominalDiffTime, SatResult)
forall a b.
Satisfiable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
SBV.satConcurrentWithAny SMTConfig
cfg [Query b]
qs ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Find a satisfying assignment to a property with multiple threads in query
-- mode. The 'Symbolic' t'SVal' represents what is known to all child query threads.
-- Each query thread will spawn a unique instance of the solver. This function
-- will block until all child threads have completed.
satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll :: forall b.
SMTConfig
-> [Query b]
-> Symbolic SVal
-> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
cfg [Query b]
qs Symbolic SVal
s = SMTConfig
-> [Query b]
-> SymbolicT IO SBool
-> IO [(Solver, NominalDiffTime, SatResult)]
forall a b.
Satisfiable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
SBV.satConcurrentWithAll SMTConfig
cfg [Query b]
qs ((SVal -> SBool) -> Symbolic SVal -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)

-- | Extract a model, the result is a tuple where the first argument (if True)
-- indicates whether the model was "probable". (i.e., if the solver returned unknown.)
getModelAssignment :: SMTResult -> Either String (Bool, [CV])
getModelAssignment :: SMTResult -> Either String (Bool, [CV])
getModelAssignment = SMTResult -> Either String (Bool, [CV])
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
forall b. SatModel b => SMTResult -> Either String (Bool, b)
SBV.getModelAssignment

-- | Extract a model dictionary. Extract a dictionary mapping the variables to
-- their respective values as returned by the SMT solver. Also see `Data.SBV.SMT.getModelDictionaries`.
getModelDictionary :: SMTResult -> Map String CV
getModelDictionary :: SMTResult -> Map String CV
getModelDictionary = SMTResult -> Map String CV
forall a. Modelable a => a -> Map String CV
SBV.getModelDictionary

-- | Create a named fresh existential variable in the current context
svNewVar :: MonadSymbolic m => Kind -> String -> m SVal
svNewVar :: forall (m :: * -> *). MonadSymbolic m => Kind -> String -> m SVal
svNewVar Kind
k String
n = 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 String -> State -> IO SVal
svMkSymVar (Maybe Quantifier -> VarContext
NonQueryVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX)) Kind
k (String -> Maybe String
forall a. a -> Maybe a
Just String
n)

-- | Create an unnamed fresh existential variable in the current context
svNewVar_ :: MonadSymbolic m => Kind -> m SVal
svNewVar_ :: forall (m :: * -> *). MonadSymbolic m => Kind -> m SVal
svNewVar_ Kind
k = 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 String -> State -> IO SVal
svMkSymVar (Maybe Quantifier -> VarContext
NonQueryVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX)) Kind
k Maybe String
forall a. Maybe a
Nothing