{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Backend.Solving
(
GrisetteSMTConfig (..),
boolector,
bitwuzla,
cvc4,
cvc5,
yices,
dReal,
z3,
mathSAT,
abc,
ExtraConfig (..),
withTimeout,
clearTimeout,
SBVIncrementalT,
SBVIncremental,
runSBVIncrementalT,
runSBVIncremental,
SBVSolverHandle,
lowerSinglePrimCached,
lowerSinglePrim,
parseModel,
)
where
import Control.Concurrent.Async (Async (asyncThreadId), async, wait)
import Control.Concurrent.STM
( TMVar,
atomically,
newTMVarIO,
putTMVar,
takeTMVar,
tryReadTMVar,
tryTakeTMVar,
)
import Control.Concurrent.STM.TChan (TChan, newTChan, readTChan, writeTChan)
import Control.Exception (handle, throwTo)
import Control.Monad (when)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.RWS (RWST (runRWST))
import Control.Monad.Reader
( MonadReader (ask),
MonadTrans (lift),
ReaderT (runReaderT),
ask,
local,
)
import Control.Monad.STM (STM)
import Control.Monad.State (MonadState (get, put), StateT, evalStateT, modify)
import Control.Monad.Writer (tell)
import Data.Dynamic (fromDyn, toDyn)
import Data.List.NonEmpty (NonEmpty)
import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import qualified Data.SBV.Control as SBVC
import qualified Data.SBV.Dynamic as SBVD
import qualified Data.SBV.Internals as SBVI
import qualified Data.SBV.Trans as SBVT
import qualified Data.SBV.Trans.Control as SBVTC
import GHC.IO.Exception (ExitCode (ExitSuccess))
import GHC.Stack (HasCallStack)
import Grisette.Internal.Backend.QuantifiedStack
( QuantifiedStack,
QuantifiedSymbols,
addQuantified,
addQuantifiedSymbol,
emptyQuantifiedStack,
emptyQuantifiedSymbols,
isQuantifiedSymbol,
lookupQuantified,
)
import Grisette.Internal.Backend.SymBiMap
( SymBiMap,
addBiMap,
addBiMapIntermediate,
attachNextQuantifiedSymbolInfo,
emptySymBiMap,
findStringToSymbol,
lookupTerm,
sizeBiMap,
)
import Grisette.Internal.Core.Data.Class.ModelOps
( ModelOps (emptyModel, insertValue),
)
import Grisette.Internal.Core.Data.Class.Solver
( ConfigurableSolver (newSolver),
MonadicSolver
( monadicSolverAssert,
monadicSolverCheckSat,
monadicSolverPop,
monadicSolverPush,
monadicSolverResetAssertions
),
Solver
( solverCheckSat,
solverForceTerminate,
solverRunCommand,
solverTerminate
),
SolverCommand
( SolverAssert,
SolverCheckSat,
SolverPop,
SolverPush,
SolverResetAssertions,
SolverTerminate
),
SolvingFailure (SolvingError, Terminated, Unk, Unsat),
)
import Grisette.Internal.SymPrim.GeneralFun (substTerm)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
( sbvFPBinaryTerm,
sbvFPFMATerm,
sbvFPRoundingBinaryTerm,
sbvFPRoundingUnaryTerm,
sbvFPTraitTerm,
sbvFPUnaryTerm,
)
import Grisette.Internal.SymPrim.Prim.Internal.Term
( PEvalApplyTerm (sbvApplyTerm),
PEvalBVTerm (sbvBVConcatTerm, sbvBVExtendTerm, sbvBVSelectTerm),
PEvalBitCastOrTerm (sbvBitCastOr),
PEvalBitCastTerm (sbvBitCast),
PEvalBitwiseTerm
( sbvAndBitsTerm,
sbvComplementBitsTerm,
sbvOrBitsTerm,
sbvXorBitsTerm
),
PEvalDivModIntegralTerm
( sbvDivIntegralTerm,
sbvModIntegralTerm,
sbvQuotIntegralTerm,
sbvRemIntegralTerm
),
PEvalFloatingTerm (sbvFloatingUnaryTerm, sbvPowerTerm),
PEvalFractionalTerm (sbvFdivTerm, sbvRecipTerm),
PEvalFromIntegralTerm (sbvFromIntegralTerm),
PEvalIEEEFPConvertibleTerm (sbvFromFPOrTerm, sbvToFPTerm),
PEvalNumTerm
( sbvAbsNumTerm,
sbvAddNumTerm,
sbvMulNumTerm,
sbvNegNumTerm,
sbvSignumNumTerm
),
PEvalOrdTerm (sbvLeOrdTerm, sbvLtOrdTerm),
PEvalRotateTerm (sbvRotateLeftTerm, sbvRotateRightTerm),
PEvalShiftTerm (sbvShiftLeftTerm, sbvShiftRightTerm),
SBVFreshMonad,
SBVRep (SBVType),
SomeTypedSymbol (SomeTypedSymbol),
SupportedNonFuncPrim (withNonFuncPrim),
SupportedPrim
( conSBVTerm,
funcDummyConstraint,
isFuncType,
parseSMTModelResult,
sbvDistinct,
sbvEq,
sbvIte,
symSBVName,
symSBVTerm,
withPrim
),
Term
( AbsNumTerm,
AddNumTerm,
AndBitsTerm,
AndTerm,
ApplyTerm,
BVConcatTerm,
BVExtendTerm,
BVSelectTerm,
BinaryTerm,
BitCastOrTerm,
BitCastTerm,
ComplementBitsTerm,
ConTerm,
DistinctTerm,
DivIntegralTerm,
EqTerm,
ExistsTerm,
FPBinaryTerm,
FPFMATerm,
FPRoundingBinaryTerm,
FPRoundingUnaryTerm,
FPTraitTerm,
FPUnaryTerm,
FdivTerm,
FloatingUnaryTerm,
ForallTerm,
FromFPOrTerm,
FromIntegralTerm,
ITETerm,
LeOrdTerm,
LtOrdTerm,
ModIntegralTerm,
MulNumTerm,
NegNumTerm,
NotTerm,
OrBitsTerm,
OrTerm,
PowerTerm,
QuotIntegralTerm,
RecipTerm,
RemIntegralTerm,
RotateLeftTerm,
RotateRightTerm,
ShiftLeftTerm,
ShiftRightTerm,
SignumNumTerm,
SymTerm,
TernaryTerm,
ToFPTerm,
UnaryTerm,
XorBitsTerm
),
TypedConstantSymbol,
TypedSymbol (TypedSymbol),
introSupportedPrimConstraint,
someTypedSymbol,
symTerm,
withSymbolSupported,
)
import Grisette.Internal.SymPrim.Prim.Model as PM
( Model,
)
import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
newtype =
{
ExtraConfig -> Maybe Int
timeout :: Maybe Int
}
data GrisetteSMTConfig = GrisetteSMTConfig
{ GrisetteSMTConfig -> SMTConfig
sbvConfig :: SBV.SMTConfig,
:: ExtraConfig
}
preciseExtraConfig :: ExtraConfig
= ExtraConfig {timeout :: Maybe Int
timeout = Maybe Int
forall a. Maybe a
Nothing}
boolector :: GrisetteSMTConfig
boolector :: GrisetteSMTConfig
boolector = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.boolector ExtraConfig
preciseExtraConfig
bitwuzla :: GrisetteSMTConfig
bitwuzla :: GrisetteSMTConfig
bitwuzla = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.bitwuzla ExtraConfig
preciseExtraConfig
cvc4 :: GrisetteSMTConfig
cvc4 :: GrisetteSMTConfig
cvc4 = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.cvc4 ExtraConfig
preciseExtraConfig
cvc5 :: GrisetteSMTConfig
cvc5 :: GrisetteSMTConfig
cvc5 = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.cvc5 ExtraConfig
preciseExtraConfig
yices :: GrisetteSMTConfig
yices :: GrisetteSMTConfig
yices = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.yices ExtraConfig
preciseExtraConfig
dReal :: GrisetteSMTConfig
dReal :: GrisetteSMTConfig
dReal = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.dReal ExtraConfig
preciseExtraConfig
z3 :: GrisetteSMTConfig
z3 :: GrisetteSMTConfig
z3 = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.z3 ExtraConfig
preciseExtraConfig
mathSAT :: GrisetteSMTConfig
mathSAT :: GrisetteSMTConfig
mathSAT = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.mathSAT ExtraConfig
preciseExtraConfig
abc :: GrisetteSMTConfig
abc :: GrisetteSMTConfig
abc = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.abc ExtraConfig
preciseExtraConfig
withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig
withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig
withTimeout Int
t GrisetteSMTConfig
config =
GrisetteSMTConfig
config {extraConfig = (extraConfig config) {timeout = Just t}}
clearTimeout :: GrisetteSMTConfig -> GrisetteSMTConfig
clearTimeout :: GrisetteSMTConfig -> GrisetteSMTConfig
clearTimeout GrisetteSMTConfig
config =
GrisetteSMTConfig
config {extraConfig = (extraConfig config) {timeout = Nothing}}
sbvCheckSatResult :: SBVC.CheckSatResult -> SolvingFailure
sbvCheckSatResult :: CheckSatResult -> SolvingFailure
sbvCheckSatResult CheckSatResult
SBVC.Sat = [Char] -> SolvingFailure
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
sbvCheckSatResult (SBVC.DSat Maybe [Char]
_) = [Char] -> SolvingFailure
forall a. HasCallStack => [Char] -> a
error [Char]
"DSat is currently not supported"
sbvCheckSatResult CheckSatResult
SBVC.Unsat = SolvingFailure
Unsat
sbvCheckSatResult CheckSatResult
SBVC.Unk = SolvingFailure
Unk
applyTimeout ::
(MonadIO m, SBVTC.MonadQuery m) => GrisetteSMTConfig -> m a -> m a
applyTimeout :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
GrisetteSMTConfig -> m a -> m a
applyTimeout GrisetteSMTConfig
config m a
q = case ExtraConfig -> Maybe Int
timeout (GrisetteSMTConfig -> ExtraConfig
extraConfig GrisetteSMTConfig
config) of
Maybe Int
Nothing -> m a
q
Just Int
t -> Int -> m a -> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
Int -> m a -> m a
SBVTC.timeout Int
t m a
q
type SBVIncrementalT m =
ReaderT GrisetteSMTConfig (StateT SymBiMap (SBVTC.QueryT m))
type SBVIncremental = SBVIncrementalT IO
runSBVIncremental :: GrisetteSMTConfig -> SBVIncremental a -> IO a
runSBVIncremental :: forall a. GrisetteSMTConfig -> SBVIncremental a -> IO a
runSBVIncremental = GrisetteSMTConfig -> SBVIncrementalT IO a -> IO a
forall (m :: * -> *) a.
ExtractIO m =>
GrisetteSMTConfig -> SBVIncrementalT m a -> m a
runSBVIncrementalT
runSBVIncrementalT ::
(SBVTC.ExtractIO m) =>
GrisetteSMTConfig ->
SBVIncrementalT m a ->
m a
runSBVIncrementalT :: forall (m :: * -> *) a.
ExtractIO m =>
GrisetteSMTConfig -> SBVIncrementalT m a -> m a
runSBVIncrementalT GrisetteSMTConfig
config SBVIncrementalT m a
sbvIncrementalT =
SMTConfig -> SymbolicT m a -> m a
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
SBVT.runSMTWith (GrisetteSMTConfig -> SMTConfig
sbvConfig GrisetteSMTConfig
config) (SymbolicT m a -> m a) -> SymbolicT m a -> m a
forall a b. (a -> b) -> a -> b
$
QueryT m a -> SymbolicT m a
forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
SBVTC.query (QueryT m a -> SymbolicT m a) -> QueryT m a -> SymbolicT m a
forall a b. (a -> b) -> a -> b
$
GrisetteSMTConfig -> QueryT m a -> QueryT m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
GrisetteSMTConfig -> m a -> m a
applyTimeout GrisetteSMTConfig
config (QueryT m a -> QueryT m a) -> QueryT m a -> QueryT m a
forall a b. (a -> b) -> a -> b
$
(StateT SymBiMap (QueryT m) a -> SymBiMap -> QueryT m a)
-> SymBiMap -> StateT SymBiMap (QueryT m) a -> QueryT m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT SymBiMap (QueryT m) a -> SymBiMap -> QueryT m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT SymBiMap
emptySymBiMap (StateT SymBiMap (QueryT m) a -> QueryT m a)
-> StateT SymBiMap (QueryT m) a -> QueryT m a
forall a b. (a -> b) -> a -> b
$
SBVIncrementalT m a
-> GrisetteSMTConfig -> StateT SymBiMap (QueryT m) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT SBVIncrementalT m a
sbvIncrementalT GrisetteSMTConfig
config
instance (MonadIO m) => MonadicSolver (SBVIncrementalT m) where
monadicSolverAssert :: SymBool -> SBVIncrementalT m ()
monadicSolverAssert (SymBool Term Bool
formula) = do
SymBiMap
symBiMap <- ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
GrisetteSMTConfig
config <- ReaderT
GrisetteSMTConfig (StateT SymBiMap (QueryT m)) GrisetteSMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
(SymBiMap
newSymBiMap, QuantifiedStack -> SBool
lowered, SBool
dummyConstraint) <-
GrisetteSMTConfig
-> Term Bool
-> SymBiMap
-> ReaderT
GrisetteSMTConfig
(StateT SymBiMap (QueryT m))
(SymBiMap, QuantifiedStack -> SBVType Bool, SBool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> SymBiMap
-> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
lowerSinglePrimCached GrisetteSMTConfig
config Term Bool
formula SymBiMap
symBiMap
StateT SymBiMap (QueryT m) () -> SBVIncrementalT m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT GrisetteSMTConfig m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT SymBiMap (QueryT m) () -> SBVIncrementalT m ())
-> StateT SymBiMap (QueryT m) () -> SBVIncrementalT m ()
forall a b. (a -> b) -> a -> b
$ QueryT m () -> StateT SymBiMap (QueryT m) ()
forall (m :: * -> *) a. Monad m => m a -> StateT SymBiMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QueryT m () -> StateT SymBiMap (QueryT m) ())
-> QueryT m () -> StateT SymBiMap (QueryT m) ()
forall a b. (a -> b) -> a -> b
$ SBool -> QueryT m ()
forall a. QuantifiedBool a => a -> QueryT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
SBV.constrain SBool
dummyConstraint
StateT SymBiMap (QueryT m) () -> SBVIncrementalT m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT GrisetteSMTConfig m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT SymBiMap (QueryT m) () -> SBVIncrementalT m ())
-> StateT SymBiMap (QueryT m) () -> SBVIncrementalT m ()
forall a b. (a -> b) -> a -> b
$ QueryT m () -> StateT SymBiMap (QueryT m) ()
forall (m :: * -> *) a. Monad m => m a -> StateT SymBiMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QueryT m () -> StateT SymBiMap (QueryT m) ())
-> QueryT m () -> StateT SymBiMap (QueryT m) ()
forall a b. (a -> b) -> a -> b
$ SBool -> QueryT m ()
forall a. QuantifiedBool a => a -> QueryT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
SBV.constrain (QuantifiedStack -> SBool
lowered QuantifiedStack
emptyQuantifiedStack)
SymBiMap -> SBVIncrementalT m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SymBiMap
newSymBiMap
monadicSolverCheckSat :: SBVIncrementalT m (Either SolvingFailure Model)
monadicSolverCheckSat = do
CheckSatResult
checkSatResult <- ReaderT
GrisetteSMTConfig (StateT SymBiMap (QueryT m)) CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
SBVTC.checkSat
GrisetteSMTConfig
config <- ReaderT
GrisetteSMTConfig (StateT SymBiMap (QueryT m)) GrisetteSMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
SymBiMap
symBiMap <- ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
case CheckSatResult
checkSatResult of
CheckSatResult
SBVC.Sat -> do
SMTModel
sbvModel <- ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
SBVTC.getModel
let model :: Model
model = GrisetteSMTConfig -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig
config SMTModel
sbvModel SymBiMap
symBiMap
Either SolvingFailure Model
-> SBVIncrementalT m (Either SolvingFailure Model)
forall a.
a -> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure Model
-> SBVIncrementalT m (Either SolvingFailure Model))
-> Either SolvingFailure Model
-> SBVIncrementalT m (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ Model -> Either SolvingFailure Model
forall a b. b -> Either a b
Right Model
model
CheckSatResult
r -> Either SolvingFailure Model
-> SBVIncrementalT m (Either SolvingFailure Model)
forall a.
a -> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure Model
-> SBVIncrementalT m (Either SolvingFailure Model))
-> Either SolvingFailure Model
-> SBVIncrementalT m (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left (SolvingFailure -> Either SolvingFailure Model)
-> SolvingFailure -> Either SolvingFailure Model
forall a b. (a -> b) -> a -> b
$ CheckSatResult -> SolvingFailure
sbvCheckSatResult CheckSatResult
r
monadicSolverResetAssertions :: SBVIncrementalT m ()
monadicSolverResetAssertions = SBVIncrementalT m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
SBVTC.resetAssertions
monadicSolverPush :: Int -> SBVIncrementalT m ()
monadicSolverPush = Int -> SBVIncrementalT m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
SBVTC.push
monadicSolverPop :: Int -> SBVIncrementalT m ()
monadicSolverPop = Int -> SBVIncrementalT m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
SBVTC.pop
data SBVSolverStatus = SBVSolverNormal | SBVSolverTerminated
data SBVSolverHandle = SBVSolverHandle
{ SBVSolverHandle -> Async ()
sbvSolverHandleMonad :: Async (),
SBVSolverHandle -> TMVar SBVSolverStatus
sbvSolverHandleStatus :: TMVar SBVSolverStatus,
SBVSolverHandle -> TChan SolverCommand
sbvSolverHandleInChan :: TChan SolverCommand,
SBVSolverHandle -> TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
}
setTerminated :: TMVar SBVSolverStatus -> STM ()
setTerminated :: TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status = do
Maybe SBVSolverStatus
_ <- TMVar SBVSolverStatus -> STM (Maybe SBVSolverStatus)
forall a. TMVar a -> STM (Maybe a)
tryTakeTMVar TMVar SBVSolverStatus
status
TMVar SBVSolverStatus -> SBVSolverStatus -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar SBVSolverStatus
status SBVSolverStatus
SBVSolverTerminated
instance ConfigurableSolver GrisetteSMTConfig SBVSolverHandle where
newSolver :: GrisetteSMTConfig -> IO SBVSolverHandle
newSolver GrisetteSMTConfig
config = do
TChan SolverCommand
sbvSolverHandleInChan <- STM (TChan SolverCommand) -> IO (TChan SolverCommand)
forall a. STM a -> IO a
atomically STM (TChan SolverCommand)
forall a. STM (TChan a)
newTChan
TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan <- STM (TChan (Either SolvingFailure Model))
-> IO (TChan (Either SolvingFailure Model))
forall a. STM a -> IO a
atomically STM (TChan (Either SolvingFailure Model))
forall a. STM (TChan a)
newTChan
TMVar SBVSolverStatus
sbvSolverHandleStatus <- SBVSolverStatus -> IO (TMVar SBVSolverStatus)
forall a. a -> IO (TMVar a)
newTMVarIO SBVSolverStatus
SBVSolverNormal
Async ()
sbvSolverHandleMonad <- IO () -> IO (Async ())
forall a. IO a -> IO (Async a)
async (IO () -> IO (Async ())) -> IO () -> IO (Async ())
forall a b. (a -> b) -> a -> b
$ do
let handler :: SomeException -> IO ()
handler SomeException
e =
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
sbvSolverHandleStatus
TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan (SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left (SomeException -> SolvingFailure
SolvingError SomeException
e))
(SomeException -> IO ()) -> IO () -> IO ()
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle SomeException -> IO ()
handler (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GrisetteSMTConfig -> SBVIncremental () -> IO ()
forall a. GrisetteSMTConfig -> SBVIncremental a -> IO a
runSBVIncremental GrisetteSMTConfig
config (SBVIncremental () -> IO ()) -> SBVIncremental () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let loop :: SBVIncremental ()
loop = do
SolverCommand
nextFormula <-
IO SolverCommand
-> ReaderT
GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) SolverCommand
forall a.
IO a -> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SolverCommand
-> ReaderT
GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) SolverCommand)
-> IO SolverCommand
-> ReaderT
GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) SolverCommand
forall a b. (a -> b) -> a -> b
$ STM SolverCommand -> IO SolverCommand
forall a. STM a -> IO a
atomically (STM SolverCommand -> IO SolverCommand)
-> STM SolverCommand -> IO SolverCommand
forall a b. (a -> b) -> a -> b
$ TChan SolverCommand -> STM SolverCommand
forall a. TChan a -> STM a
readTChan TChan SolverCommand
sbvSolverHandleInChan
case SolverCommand
nextFormula of
SolverPush Int
n -> Int -> SBVIncremental ()
forall (m :: * -> *). MonadicSolver m => Int -> m ()
monadicSolverPush Int
n SBVIncremental () -> SBVIncremental () -> SBVIncremental ()
forall a b.
ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
-> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) b
-> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBVIncremental ()
loop
SolverPop Int
n -> Int -> SBVIncremental ()
forall (m :: * -> *). MonadicSolver m => Int -> m ()
monadicSolverPop Int
n SBVIncremental () -> SBVIncremental () -> SBVIncremental ()
forall a b.
ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
-> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) b
-> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBVIncremental ()
loop
SolverCommand
SolverTerminate -> () -> SBVIncremental ()
forall a.
a -> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
SolverCommand
SolverResetAssertions -> SBVIncremental ()
forall (m :: * -> *). MonadicSolver m => m ()
monadicSolverResetAssertions SBVIncremental () -> SBVIncremental () -> SBVIncremental ()
forall a b.
ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
-> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) b
-> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBVIncremental ()
loop
SolverAssert SymBool
formula -> do
SymBool -> SBVIncremental ()
forall (m :: * -> *). MonadicSolver m => SymBool -> m ()
monadicSolverAssert SymBool
formula
SBVIncremental ()
loop
SolverCommand
SolverCheckSat -> do
Either SolvingFailure Model
r <- ReaderT
GrisetteSMTConfig
(StateT SymBiMap (QueryT IO))
(Either SolvingFailure Model)
forall (m :: * -> *).
MonadicSolver m =>
m (Either SolvingFailure Model)
monadicSolverCheckSat
IO () -> SBVIncremental ()
forall a.
IO a -> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SBVIncremental ()) -> IO () -> SBVIncremental ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan Either SolvingFailure Model
r
SBVIncremental ()
loop
SBVIncremental ()
loop
IO () -> SBVIncremental ()
forall a.
IO a -> ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SBVIncremental ()) -> IO () -> SBVIncremental ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
sbvSolverHandleStatus
TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan (Either SolvingFailure Model -> STM ())
-> Either SolvingFailure Model -> STM ()
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left SolvingFailure
Terminated
SBVSolverHandle -> IO SBVSolverHandle
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVSolverHandle -> IO SBVSolverHandle)
-> SBVSolverHandle -> IO SBVSolverHandle
forall a b. (a -> b) -> a -> b
$ SBVSolverHandle {Async ()
TChan (Either SolvingFailure Model)
TChan SolverCommand
TMVar SBVSolverStatus
sbvSolverHandleMonad :: Async ()
sbvSolverHandleStatus :: TMVar SBVSolverStatus
sbvSolverHandleInChan :: TChan SolverCommand
sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
sbvSolverHandleInChan :: TChan SolverCommand
sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
sbvSolverHandleStatus :: TMVar SBVSolverStatus
sbvSolverHandleMonad :: Async ()
..}
instance Solver SBVSolverHandle where
solverRunCommand :: forall a.
(SBVSolverHandle -> IO (Either SolvingFailure a))
-> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand SBVSolverHandle -> IO (Either SolvingFailure a)
f handle :: SBVSolverHandle
handle@(SBVSolverHandle Async ()
_ TMVar SBVSolverStatus
status TChan SolverCommand
inChan TChan (Either SolvingFailure Model)
_) SolverCommand
command = do
SBVSolverStatus
st <- IO SBVSolverStatus -> IO SBVSolverStatus
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVSolverStatus -> IO SBVSolverStatus)
-> IO SBVSolverStatus -> IO SBVSolverStatus
forall a b. (a -> b) -> a -> b
$ STM SBVSolverStatus -> IO SBVSolverStatus
forall a. STM a -> IO a
atomically (STM SBVSolverStatus -> IO SBVSolverStatus)
-> STM SBVSolverStatus -> IO SBVSolverStatus
forall a b. (a -> b) -> a -> b
$ TMVar SBVSolverStatus -> STM SBVSolverStatus
forall a. TMVar a -> STM a
takeTMVar TMVar SBVSolverStatus
status
case SBVSolverStatus
st of
SBVSolverStatus
SBVSolverNormal -> do
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan SolverCommand -> SolverCommand -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan SolverCommand
inChan SolverCommand
command
Either SolvingFailure a
r <- SBVSolverHandle -> IO (Either SolvingFailure a)
f SBVSolverHandle
handle
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Maybe SBVSolverStatus
currStatus <- TMVar SBVSolverStatus -> STM (Maybe SBVSolverStatus)
forall a. TMVar a -> STM (Maybe a)
tryReadTMVar TMVar SBVSolverStatus
status
case Maybe SBVSolverStatus
currStatus of
Maybe SBVSolverStatus
Nothing -> TMVar SBVSolverStatus -> SBVSolverStatus -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar SBVSolverStatus
status SBVSolverStatus
SBVSolverNormal
Just SBVSolverStatus
_ -> () -> STM ()
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Either SolvingFailure a
r
SBVSolverStatus
SBVSolverTerminated -> do
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure a -> IO (Either SolvingFailure a))
-> Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> Either SolvingFailure a
forall a b. a -> Either a b
Left SolvingFailure
Terminated
solverCheckSat :: SBVSolverHandle -> IO (Either SolvingFailure Model)
solverCheckSat SBVSolverHandle
handle =
(SBVSolverHandle -> IO (Either SolvingFailure Model))
-> SBVSolverHandle
-> SolverCommand
-> IO (Either SolvingFailure Model)
forall handle a.
Solver handle =>
(handle -> IO (Either SolvingFailure a))
-> handle -> SolverCommand -> IO (Either SolvingFailure a)
forall a.
(SBVSolverHandle -> IO (Either SolvingFailure a))
-> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand
( \(SBVSolverHandle Async ()
_ TMVar SBVSolverStatus
_ TChan SolverCommand
_ TChan (Either SolvingFailure Model)
outChan) ->
IO (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model))
-> IO (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ STM (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a. STM a -> IO a
atomically (STM (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model))
-> STM (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ TChan (Either SolvingFailure Model)
-> STM (Either SolvingFailure Model)
forall a. TChan a -> STM a
readTChan TChan (Either SolvingFailure Model)
outChan
)
SBVSolverHandle
handle
SolverCommand
SolverCheckSat
solverTerminate :: SBVSolverHandle -> IO ()
solverTerminate (SBVSolverHandle Async ()
thread TMVar SBVSolverStatus
status TChan SolverCommand
inChan TChan (Either SolvingFailure Model)
_) = do
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
TChan SolverCommand -> SolverCommand -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan SolverCommand
inChan SolverCommand
SolverTerminate
Async () -> IO ()
forall a. Async a -> IO a
wait Async ()
thread
solverForceTerminate :: SBVSolverHandle -> IO ()
solverForceTerminate (SBVSolverHandle Async ()
thread TMVar SBVSolverStatus
status TChan SolverCommand
_ TChan (Either SolvingFailure Model)
outChan) = do
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
outChan (SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left SolvingFailure
Terminated)
ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async () -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async ()
thread) ExitCode
ExitSuccess
Async () -> IO ()
forall a. Async a -> IO a
wait Async ()
thread
newtype TermAll = TermAll SBV.SBool
instance Semigroup TermAll where
TermAll SBool
a <> :: TermAll -> TermAll -> TermAll
<> TermAll SBool
b = SBool -> TermAll
TermAll (SBool
a SBool -> SBool -> SBool
SBV..&& SBool
b)
instance Monoid TermAll where
mempty :: TermAll
mempty = SBool -> TermAll
TermAll SBool
SBV.sTrue
lowerSinglePrimCached ::
forall a m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig ->
Term a ->
SymBiMap ->
m (SymBiMap, QuantifiedStack -> SBVType a, SBV.SBool)
lowerSinglePrimCached :: forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> SymBiMap
-> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
lowerSinglePrimCached GrisetteSMTConfig
config Term a
t SymBiMap
m = do
(QuantifiedStack -> SBVType a
r, SymBiMap
finalm, TermAll SBool
dummy) <-
RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
-> QuantifiedSymbols
-> SymBiMap
-> m (QuantifiedStack -> SBVType a, SymBiMap, TermAll)
forall r w s (m :: * -> *) a.
RWST r w s m a -> r -> s -> m (a, s, w)
runRWST (GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
t) QuantifiedSymbols
emptyQuantifiedSymbols SymBiMap
m
(SymBiMap, QuantifiedStack -> SBVType a, SBool)
-> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
finalm, QuantifiedStack -> SBVType a
r, SBool
dummy)
lowerSinglePrim ::
forall a m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig ->
Term a ->
m (SymBiMap, QuantifiedStack -> SBVType a, SBV.SBool)
lowerSinglePrim :: forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a -> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
lowerSinglePrim GrisetteSMTConfig
config Term a
t =
GrisetteSMTConfig
-> Term a
-> SymBiMap
-> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> SymBiMap
-> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
lowerSinglePrimCached GrisetteSMTConfig
config Term a
t SymBiMap
emptySymBiMap
lowerSinglePrimCached' ::
forall a m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig ->
Term a ->
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a)
lowerSinglePrimCached' :: forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
t = do
SymBiMap
m <- RWST QuantifiedSymbols TermAll SymBiMap m SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
Term a
-> (SupportedPrim a =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (SupportedPrim a =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$
case HasCallStack =>
SomeTerm -> SymBiMap -> Maybe (QuantifiedStack -> Dynamic)
SomeTerm -> SymBiMap -> Maybe (QuantifiedStack -> Dynamic)
lookupTerm (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) SymBiMap
m of
Just QuantifiedStack -> Dynamic
x ->
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return
( \QuantifiedStack
qst ->
forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
Mergeable (SBVType t), Typeable (SBVType t)) =>
a)
-> a
withPrim @a (((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
SBVType a)
-> SBVType a)
-> ((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
SBVType a)
-> SBVType a
forall a b. (a -> b) -> a -> b
$
Dynamic -> SBVType a -> SBVType a
forall a. Typeable a => Dynamic -> a -> a
fromDyn (QuantifiedStack -> Dynamic
x QuantifiedStack
qst) SBVType a
forall a. HasCallStack => a
undefined
)
Maybe (QuantifiedStack -> Dynamic)
Nothing -> do
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimImpl GrisetteSMTConfig
config Term a
t
lowerSinglePrimImpl ::
forall a m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig ->
Term a ->
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a)
lowerSinglePrimImpl :: forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimImpl GrisetteSMTConfig
_ (ConTerm Int
_ a
v) =
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ SBVType a -> QuantifiedStack -> SBVType a
forall a b. a -> b -> a
const (SBVType a -> QuantifiedStack -> SBVType a)
-> SBVType a -> QuantifiedStack -> SBVType a
forall a b. (a -> b) -> a -> b
$ a -> SBVType a
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm a
v
lowerSinglePrimImpl GrisetteSMTConfig
_ t :: Term a
t@(SymTerm Int
_ TypedSymbol 'AnyKind a
ts) = do
QuantifiedSymbols
qs <- RWST QuantifiedSymbols TermAll SymBiMap m QuantifiedSymbols
forall r (m :: * -> *). MonadReader r m => m r
ask
if TypedSymbol 'AnyKind a -> QuantifiedSymbols -> Bool
forall a (knd :: SymbolKind).
(SupportedPrim a, IsSymbolKind knd) =>
TypedSymbol knd a -> QuantifiedSymbols -> Bool
isQuantifiedSymbol TypedSymbol 'AnyKind a
ts QuantifiedSymbols
qs
then forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
Mergeable (SBVType t), Typeable (SBVType t)) =>
a)
-> a
withPrim @a (((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> ((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
let retDyn :: QuantifiedStack -> Dynamic
retDyn QuantifiedStack
qst =
case SomeTypedSymbol 'AnyKind -> QuantifiedStack -> Maybe Dynamic
forall (knd :: SymbolKind).
(HasCallStack, IsSymbolKind knd) =>
SomeTypedSymbol knd -> QuantifiedStack -> Maybe Dynamic
lookupQuantified (TypedSymbol 'AnyKind a -> SomeTypedSymbol 'AnyKind
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'AnyKind a
ts) QuantifiedStack
qst of
Just Dynamic
v -> Dynamic
v
Maybe Dynamic
Nothing -> [Char] -> Dynamic
forall a. HasCallStack => [Char] -> a
error [Char]
"BUG: Symbol not found in the quantified stack"
(SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> (SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ \SymBiMap
m -> HasCallStack =>
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) QuantifiedStack -> Dynamic
retDyn SymBiMap
m
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$
\QuantifiedStack
x ->
Dynamic -> SBVType a -> SBVType a
forall a. Typeable a => Dynamic -> a -> a
fromDyn
(QuantifiedStack -> Dynamic
retDyn QuantifiedStack
x)
([Char] -> SBVType a
forall a. HasCallStack => [Char] -> a
error [Char]
"BUG: Symbol not found in the quantified stack")
else forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
Mergeable (SBVType t), Typeable (SBVType t)) =>
a)
-> a
withPrim @a (((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> ((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
SymBiMap
m <- RWST QuantifiedSymbols TermAll SymBiMap m SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
let name :: [Char]
name = TypedSymbol 'AnyKind a -> Int -> [Char]
forall t.
SupportedPrim t =>
TypedSymbol 'AnyKind t -> Int -> [Char]
symSBVName TypedSymbol 'AnyKind a
ts (SymBiMap -> Int
sizeBiMap SymBiMap
m)
SBVType a
g <- forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
[Char] -> m (SBVType t)
symSBVTerm @a [Char]
name
Bool
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall t. SupportedPrim t => Bool
isFuncType @a) (RWST QuantifiedSymbols TermAll SymBiMap m ()
-> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ TermAll -> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (TermAll -> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> TermAll -> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ SBool -> TermAll
TermAll (SBool -> TermAll) -> SBool -> TermAll
forall a b. (a -> b) -> a -> b
$ forall t. SupportedPrim t => SBVType t -> SBool
funcDummyConstraint @a SBVType a
g
SymBiMap -> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (SymBiMap -> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> SymBiMap -> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ SomeTerm
-> Dynamic
-> [Char]
-> SomeTypedSymbol 'AnyKind
-> SymBiMap
-> SymBiMap
forall (knd :: SymbolKind).
HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol knd -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBVType a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBVType a
g) [Char]
name (TypedSymbol 'AnyKind a -> SomeTypedSymbol 'AnyKind
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'AnyKind a
ts) SymBiMap
m
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ SBVType a -> QuantifiedStack -> SBVType a
forall a b. a -> b -> a
const SBVType a
g
#if MIN_VERSION_sbv(10,1,0)
lowerSinglePrimImpl GrisetteSMTConfig
config t :: Term a
t@(ForallTerm Int
_ (TypedConstantSymbol t1
ts :: TypedConstantSymbol t1) Term Bool
v) =
forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t1 ((NonFuncPrimConstraint t1 =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (NonFuncPrimConstraint t1 =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
do
SymBiMap
m <- RWST QuantifiedSymbols TermAll SymBiMap m SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
let (SymBiMap
newm, sb :: TypedConstantSymbol t1
sb@(TypedSymbol Symbol
sbs)) = SymBiMap
-> TypedConstantSymbol t1 -> (SymBiMap, TypedConstantSymbol t1)
forall a.
SymBiMap
-> TypedConstantSymbol a -> (SymBiMap, TypedConstantSymbol a)
attachNextQuantifiedSymbolInfo SymBiMap
m TypedConstantSymbol t1
ts
SymBiMap -> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SymBiMap
newm
let substedTerm :: Term Bool
substedTerm = TypedConstantSymbol t1 -> Term t1 -> Term Bool -> Term Bool
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol t1
ts (Symbol -> Term t1
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
sbs) Term Bool
v
QuantifiedStack -> SBool
r <-
(QuantifiedSymbols -> QuantifiedSymbols)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a.
(QuantifiedSymbols -> QuantifiedSymbols)
-> RWST QuantifiedSymbols TermAll SymBiMap m a
-> RWST QuantifiedSymbols TermAll SymBiMap m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (TypedConstantSymbol t1 -> QuantifiedSymbols -> QuantifiedSymbols
forall a.
TypedConstantSymbol a -> QuantifiedSymbols -> QuantifiedSymbols
addQuantifiedSymbol TypedConstantSymbol t1
sb) (RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$
GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached'
GrisetteSMTConfig
config
Term Bool
substedTerm
let ret :: QuantifiedStack -> SBool
ret QuantifiedStack
qst = (Forall Any (NonFuncSBVBaseType t1) -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
SBV.quantifiedBool ((Forall Any (NonFuncSBVBaseType t1) -> SBool) -> SBool)
-> (Forall Any (NonFuncSBVBaseType t1) -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
\(SBV.Forall (SBVType t1
a :: SBVType t1)) ->
QuantifiedStack -> SBool
r (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol t1
-> Dynamic -> QuantifiedStack -> QuantifiedStack
forall a.
TypedConstantSymbol a
-> Dynamic -> QuantifiedStack -> QuantifiedStack
addQuantified TypedConstantSymbol t1
sb (SBV (NonFuncSBVBaseType t1) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV (NonFuncSBVBaseType t1)
SBVType t1
a) QuantifiedStack
qst
(SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> (SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBool -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (SBool -> Dynamic)
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBool
ret)
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return QuantifiedStack -> SBool
ret
lowerSinglePrimImpl GrisetteSMTConfig
config t :: Term a
t@(ExistsTerm Int
_ (TypedConstantSymbol t1
ts :: TypedConstantSymbol t1) Term Bool
v) =
forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t1 ((NonFuncPrimConstraint t1 =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (NonFuncPrimConstraint t1 =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
do
SymBiMap
m <- RWST QuantifiedSymbols TermAll SymBiMap m SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
let (SymBiMap
newm, sb :: TypedConstantSymbol t1
sb@(TypedSymbol Symbol
sbs)) = SymBiMap
-> TypedConstantSymbol t1 -> (SymBiMap, TypedConstantSymbol t1)
forall a.
SymBiMap
-> TypedConstantSymbol a -> (SymBiMap, TypedConstantSymbol a)
attachNextQuantifiedSymbolInfo SymBiMap
m TypedConstantSymbol t1
ts
SymBiMap -> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SymBiMap
newm
let substedTerm :: Term Bool
substedTerm = TypedConstantSymbol t1 -> Term t1 -> Term Bool -> Term Bool
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol t1
ts (Symbol -> Term t1
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
sbs) Term Bool
v
QuantifiedStack -> SBool
r <-
(QuantifiedSymbols -> QuantifiedSymbols)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a.
(QuantifiedSymbols -> QuantifiedSymbols)
-> RWST QuantifiedSymbols TermAll SymBiMap m a
-> RWST QuantifiedSymbols TermAll SymBiMap m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (TypedConstantSymbol t1 -> QuantifiedSymbols -> QuantifiedSymbols
forall a.
TypedConstantSymbol a -> QuantifiedSymbols -> QuantifiedSymbols
addQuantifiedSymbol TypedConstantSymbol t1
sb) (RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$
GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached'
GrisetteSMTConfig
config
Term Bool
substedTerm
let ret :: QuantifiedStack -> SBool
ret QuantifiedStack
qst = (Exists Any (NonFuncSBVBaseType t1) -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
SBV.quantifiedBool ((Exists Any (NonFuncSBVBaseType t1) -> SBool) -> SBool)
-> (Exists Any (NonFuncSBVBaseType t1) -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
\(SBV.Exists (SBVType t1
a :: SBVType t1)) ->
QuantifiedStack -> SBool
r (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol t1
-> Dynamic -> QuantifiedStack -> QuantifiedStack
forall a.
TypedConstantSymbol a
-> Dynamic -> QuantifiedStack -> QuantifiedStack
addQuantified TypedConstantSymbol t1
sb (SBV (NonFuncSBVBaseType t1) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV (NonFuncSBVBaseType t1)
SBVType t1
a) QuantifiedStack
qst
(SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> (SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBool -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (SBool -> Dynamic)
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBool
ret)
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return QuantifiedStack -> SBool
ret
#else
lowerSinglePrimImpl _ ForallTerm {} =
error "Quantifiers are only available when you build with SBV 10.1.0 or later"
lowerSinglePrimImpl _ ExistsTerm {} =
error "Quantifiers are only available when you build with SBV 10.1.0 or later"
#endif
lowerSinglePrimImpl GrisetteSMTConfig
config Term a
t =
Term a
-> (SupportedPrim a =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (SupportedPrim a =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$
forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
Mergeable (SBVType t), Typeable (SBVType t)) =>
a)
-> a
withPrim @a (((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> ((PrimConstraint a, SMTDefinable (SBVType a),
Mergeable (SBVType a), Typeable (SBVType a)) =>
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
QuantifiedStack -> SBVType a
r <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimIntermediate GrisetteSMTConfig
config Term a
t
(SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ())
-> (SymBiMap -> SymBiMap)
-> RWST QuantifiedSymbols TermAll SymBiMap m ()
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
SomeTerm -> (QuantifiedStack -> Dynamic) -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBVType a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (SBVType a -> Dynamic)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
r)
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return QuantifiedStack -> SBVType a
r
lowerSinglePrimIntermediate ::
forall a m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig ->
Term a ->
RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a)
lowerSinglePrimIntermediate :: forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (NotTerm Int
_ Term Bool
a) = do
QuantifiedStack -> SBool
a' <- GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term Bool
a
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
SBV.sNot (SBool -> SBool)
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBool
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (OrTerm Int
_ Term Bool
a Term Bool
b) = do
QuantifiedStack -> SBool
a' <- GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term Bool
a
QuantifiedStack -> SBool
b' <- GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term Bool
b
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> QuantifiedStack -> SBool
a' QuantifiedStack
qst SBool -> SBool -> SBool
SBV..|| QuantifiedStack -> SBool
b' QuantifiedStack
qst
lowerSinglePrimIntermediate GrisetteSMTConfig
config (AndTerm Int
_ Term Bool
a Term Bool
b) = do
QuantifiedStack -> SBool
a' <- GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term Bool
a
QuantifiedStack -> SBool
b' <- GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term Bool
b
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> QuantifiedStack -> SBool
a' QuantifiedStack
qst SBool -> SBool -> SBool
SBV..&& QuantifiedStack -> SBool
b' QuantifiedStack
qst
lowerSinglePrimIntermediate GrisetteSMTConfig
config (EqTerm Int
_ (Term t1
a :: Term v) Term t1
b) = do
QuantifiedStack -> SBVType t1
a' <- GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term t1
a
QuantifiedStack -> SBVType t1
b' <- GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term t1
b
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. SupportedPrim t => SBVType t -> SBVType t -> SBool
sbvEq @v (QuantifiedStack -> SBVType t1
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType t1
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (DistinctTerm Int
_ (NonEmpty (Term t1)
args :: NonEmpty (Term t))) = do
NonEmpty (QuantifiedStack -> SBVType t1)
args' <- (Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1))
-> NonEmpty (Term t1)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(NonEmpty (QuantifiedStack -> SBVType t1))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse (GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config) NonEmpty (Term t1)
args
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. SupportedPrim t => NonEmpty (SBVType t) -> SBool
sbvDistinct @t (((QuantifiedStack -> SBVType t1) -> SBVType t1)
-> NonEmpty (QuantifiedStack -> SBVType t1)
-> NonEmpty (SBVType t1)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QuantifiedStack -> SBVType t1) -> QuantifiedStack -> SBVType t1
forall a b. (a -> b) -> a -> b
$ QuantifiedStack
qst) NonEmpty (QuantifiedStack -> SBVType t1)
args')
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ITETerm Int
_ Term Bool
c Term a
a Term a
b) = do
QuantifiedStack -> SBool
c' <- GrisetteSMTConfig
-> Term Bool
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType Bool)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term Bool
c
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
SupportedPrim t =>
SBool -> SBVType t -> SBVType t -> SBVType t
sbvIte @a (QuantifiedStack -> SBool
c' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (AddNumTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalNumTerm t => SBVType t -> SBVType t -> SBVType t
sbvAddNumTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (NegNumTerm Int
_ Term a
a) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall t. PEvalNumTerm t => SBVType t -> SBVType t
sbvNegNumTerm @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (MulNumTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalNumTerm t => SBVType t -> SBVType t -> SBVType t
sbvMulNumTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (AbsNumTerm Int
_ Term a
a) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall t. PEvalNumTerm t => SBVType t -> SBVType t
sbvAbsNumTerm @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (SignumNumTerm Int
_ Term a
a) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall t. PEvalNumTerm t => SBVType t -> SBVType t
sbvSignumNumTerm @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (LtOrdTerm Int
_ (Term t1
a :: Term v) Term t1
b) = do
QuantifiedStack -> SBVType t1
a' <- GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term t1
a
QuantifiedStack -> SBVType t1
b' <- GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term t1
b
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalOrdTerm t => SBVType t -> SBVType t -> SBool
sbvLtOrdTerm @v (QuantifiedStack -> SBVType t1
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType t1
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (LeOrdTerm Int
_ (Term t1
a :: Term v) Term t1
b) = do
QuantifiedStack -> SBVType t1
a' <- GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term t1
a
QuantifiedStack -> SBVType t1
b' <- GrisetteSMTConfig
-> Term t1
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType t1)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term t1
b
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalOrdTerm t => SBVType t -> SBVType t -> SBool
sbvLeOrdTerm @v (QuantifiedStack -> SBVType t1
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType t1
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (AndBitsTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalBitwiseTerm t => SBVType t -> SBVType t -> SBVType t
sbvAndBitsTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (OrBitsTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalBitwiseTerm t => SBVType t -> SBVType t -> SBVType t
sbvOrBitsTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (XorBitsTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalBitwiseTerm t => SBVType t -> SBVType t -> SBVType t
sbvXorBitsTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ComplementBitsTerm Int
_ Term a
a) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall t. PEvalBitwiseTerm t => SBVType t -> SBVType t
sbvComplementBitsTerm @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ShiftLeftTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalShiftTerm t => SBVType t -> SBVType t -> SBVType t
sbvShiftLeftTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ShiftRightTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalShiftTerm t => SBVType t -> SBVType t -> SBVType t
sbvShiftRightTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (RotateLeftTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalRotateTerm t => SBVType t -> SBVType t -> SBVType t
sbvRotateLeftTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (RotateRightTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t. PEvalRotateTerm t => SBVType t -> SBVType t -> SBVType t
sbvRotateRightTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ApplyTerm Int
_ (Term f
f :: Term f) Term a
a) = do
QuantifiedStack -> SBVType f
l1 <- GrisetteSMTConfig
-> Term f
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType f)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term f
f
QuantifiedStack -> SBVType a
l2 <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall f a b.
PEvalApplyTerm f a b =>
SBVType f -> SBVType a -> SBVType b
sbvApplyTerm @f (QuantifiedStack -> SBVType f
l1 QuantifiedStack
qst) (QuantifiedStack -> SBVType a
l2 QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (BitCastTerm Int
_ (Term a
a :: Term x)) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall a b. PEvalBitCastTerm a b => SBVType a -> SBVType b
sbvBitCast @x @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a'
lowerSinglePrimIntermediate
GrisetteSMTConfig
config
(BitCastOrTerm Int
_ (Term a
d :: Term a) (Term a
a :: Term x)) = do
QuantifiedStack -> SBVType a
d' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
d
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall a b.
PEvalBitCastOrTerm a b =>
SBVType b -> SBVType a -> SBVType b
sbvBitCastOr @x @a (QuantifiedStack -> SBVType a
d' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst)
lowerSinglePrimIntermediate
GrisetteSMTConfig
config
(BVConcatTerm Int
_ (Term (bv l)
a :: Term (bv l)) (Term (bv r)
b :: Term (bv r))) =
do
QuantifiedStack -> SBVType (bv l)
a' <- GrisetteSMTConfig
-> Term (bv l)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv l))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (bv l)
a
QuantifiedStack -> SBVType (bv r)
b' <- GrisetteSMTConfig
-> Term (bv r)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv r))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (bv r)
b
(QuantifiedStack -> SBVType (bv (l + r)))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv (l + r)))
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType (bv (l + r)))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv (l + r))))
-> (QuantifiedStack -> SBVType (bv (l + r)))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv (l + r)))
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
(p1 :: Natural -> *) (p2 :: Natural -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
p1 l
-> p2 r -> SBVType (bv l) -> SBVType (bv r) -> SBVType (bv (l + r))
sbvBVConcatTerm @bv (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) (QuantifiedStack -> SBVType (bv l)
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType (bv r)
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate
GrisetteSMTConfig
config
(BVExtendTerm Int
_ Bool
signed (TypeRep r
pr :: p r) (Term (bv l)
a :: Term (bv l))) =
do
QuantifiedStack -> SBVType (bv l)
a' <- GrisetteSMTConfig
-> Term (bv l)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv l))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (bv l)
a
(QuantifiedStack -> SBVType (bv r))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv r))
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType (bv r))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv r)))
-> (QuantifiedStack -> SBVType (bv r))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv r))
forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
(p1 :: Natural -> *) (p2 :: Natural -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
p1 l -> p2 r -> Bool -> SBVType (bv l) -> SBVType (bv r)
sbvBVExtendTerm @bv (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) TypeRep r
pr Bool
signed (SBVType (bv l) -> SBVType (bv r))
-> (QuantifiedStack -> SBVType (bv l))
-> QuantifiedStack
-> SBVType (bv r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType (bv l)
a'
lowerSinglePrimIntermediate
GrisetteSMTConfig
config
(BVSelectTerm Int
_ (TypeRep ix
pix :: p ix) (TypeRep w
pw :: q w) (Term (bv n)
a :: Term (bv n))) =
do
QuantifiedStack -> SBVType (bv n)
a' <- GrisetteSMTConfig
-> Term (bv n)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv n))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (bv n)
a
(QuantifiedStack -> SBVType (bv w))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv w))
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType (bv w))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv w)))
-> (QuantifiedStack -> SBVType (bv w))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (bv w))
forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (ix :: Natural) (w :: Natural)
(n :: Natural) (p1 :: Natural -> *) (p2 :: Natural -> *)
(p3 :: Natural -> *).
(PEvalBVTerm bv, KnownNat ix, KnownNat w, KnownNat n, 1 <= n,
1 <= w, (ix + w) <= n) =>
p1 ix -> p2 w -> p3 n -> SBVType (bv n) -> SBVType (bv w)
sbvBVSelectTerm @bv TypeRep ix
pix TypeRep w
pw (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (SBVType (bv n) -> SBVType (bv w))
-> (QuantifiedStack -> SBVType (bv n))
-> QuantifiedStack
-> SBVType (bv w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType (bv n)
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (DivIntegralTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
PEvalDivModIntegralTerm t =>
SBVType t -> SBVType t -> SBVType t
sbvDivIntegralTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ModIntegralTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
PEvalDivModIntegralTerm t =>
SBVType t -> SBVType t -> SBVType t
sbvModIntegralTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (QuotIntegralTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
PEvalDivModIntegralTerm t =>
SBVType t -> SBVType t -> SBVType t
sbvQuotIntegralTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (RemIntegralTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b' <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
PEvalDivModIntegralTerm t =>
SBVType t -> SBVType t -> SBVType t
sbvRemIntegralTerm @a (QuantifiedStack -> SBVType a
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b' QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FPTraitTerm Int
_ FPTrait
trait Term (FP eb sb)
a) = do
QuantifiedStack -> SFloatingPoint eb sb
a' <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
a
(QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool))
-> (QuantifiedStack -> SBool)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a b. (a -> b) -> a -> b
$ FPTrait -> SFloatingPoint eb sb -> SBool
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPTrait -> SFloatingPoint eb sb -> SBool
sbvFPTraitTerm FPTrait
trait (SFloatingPoint eb sb -> SBool)
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> QuantifiedStack
-> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SFloatingPoint eb sb
a'
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FdivTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
PEvalFractionalTerm t =>
SBVType t -> SBVType t -> SBVType t
sbvFdivTerm @a (QuantifiedStack -> SBVType a
a QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (RecipTerm Int
_ Term a
a) = do
QuantifiedStack -> SBVType a
a <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall t. PEvalFractionalTerm t => SBVType t -> SBVType t
sbvRecipTerm @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FloatingUnaryTerm Int
_ FloatingUnaryOp
op Term a
a) = do
QuantifiedStack -> SBVType a
a <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> SBVType t -> SBVType t
sbvFloatingUnaryTerm @a FloatingUnaryOp
op (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
a
lowerSinglePrimIntermediate GrisetteSMTConfig
config (PowerTerm Int
_ Term a
a Term a
b) = do
QuantifiedStack -> SBVType a
a <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
a
QuantifiedStack -> SBVType a
b <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall t.
PEvalFloatingTerm t =>
SBVType t -> SBVType t -> SBVType t
sbvPowerTerm @a (QuantifiedStack -> SBVType a
a QuantifiedStack
qst) (QuantifiedStack -> SBVType a
b QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FPUnaryTerm Int
_ FPUnaryOp
op Term (FP eb sb)
a) = do
QuantifiedStack -> SFloatingPoint eb sb
a <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
a
(QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb))
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ FPUnaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPUnaryOp -> SFloatingPoint eb sb -> SFloatingPoint eb sb
sbvFPUnaryTerm FPUnaryOp
op (SFloatingPoint eb sb -> SFloatingPoint eb sb)
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> QuantifiedStack
-> SFloatingPoint eb sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SFloatingPoint eb sb
a
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FPBinaryTerm Int
_ FPBinaryOp
op Term (FP eb sb)
a Term (FP eb sb)
b) = do
QuantifiedStack -> SFloatingPoint eb sb
a <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
a
QuantifiedStack -> SFloatingPoint eb sb
b <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
b
(QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb))
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> FPBinaryOp
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPBinaryOp
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPBinaryTerm FPBinaryOp
op (QuantifiedStack -> SFloatingPoint eb sb
a QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
b QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FPRoundingUnaryTerm Int
_ FPRoundingUnaryOp
op Term FPRoundingMode
round Term (FP eb sb)
a) = do
QuantifiedStack -> SRoundingMode
round <- GrisetteSMTConfig
-> Term FPRoundingMode
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType FPRoundingMode)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term FPRoundingMode
round
QuantifiedStack -> SFloatingPoint eb sb
a <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
a
(QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb))
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> FPRoundingUnaryOp
-> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingUnaryOp
-> SRoundingMode -> SFloatingPoint eb sb -> SFloatingPoint eb sb
sbvFPRoundingUnaryTerm FPRoundingUnaryOp
op (QuantifiedStack -> SRoundingMode
round QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
a QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FPRoundingBinaryTerm Int
_ FPRoundingBinaryOp
op Term FPRoundingMode
round Term (FP eb sb)
a Term (FP eb sb)
b) = do
QuantifiedStack -> SRoundingMode
round <- GrisetteSMTConfig
-> Term FPRoundingMode
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType FPRoundingMode)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term FPRoundingMode
round
QuantifiedStack -> SFloatingPoint eb sb
a <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
a
QuantifiedStack -> SFloatingPoint eb sb
b <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
b
(QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb))
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> FPRoundingBinaryOp
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
FPRoundingBinaryOp
-> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPRoundingBinaryTerm FPRoundingBinaryOp
op (QuantifiedStack -> SRoundingMode
round QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
a QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
b QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FPFMATerm Int
_ Term FPRoundingMode
round Term (FP eb sb)
a Term (FP eb sb)
b Term (FP eb sb)
c) = do
QuantifiedStack -> SRoundingMode
round <- GrisetteSMTConfig
-> Term FPRoundingMode
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType FPRoundingMode)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term FPRoundingMode
round
QuantifiedStack -> SFloatingPoint eb sb
a <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
a
QuantifiedStack -> SFloatingPoint eb sb
b <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
b
QuantifiedStack -> SFloatingPoint eb sb
c <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
c
(QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb))
-> (QuantifiedStack -> SFloatingPoint eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SFloatingPoint eb sb)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
SRoundingMode
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
-> SFloatingPoint eb sb
sbvFPFMATerm (QuantifiedStack -> SRoundingMode
round QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
a QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
b QuantifiedStack
qst) (QuantifiedStack -> SFloatingPoint eb sb
c QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FromIntegralTerm Int
_ (Term a
b :: Term b)) = do
QuantifiedStack -> SBVType a
b <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
b
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ forall a b. PEvalFromIntegralTerm a b => SBVType a -> SBVType b
sbvFromIntegralTerm @b @a (SBVType a -> SBVType a)
-> (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuantifiedStack -> SBVType a
b
lowerSinglePrimIntermediate GrisetteSMTConfig
config (FromFPOrTerm Int
_ Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg) = do
QuantifiedStack -> SBVType a
d <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
d
QuantifiedStack -> SRoundingMode
mode <- GrisetteSMTConfig
-> Term FPRoundingMode
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType FPRoundingMode)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term FPRoundingMode
mode
QuantifiedStack -> SBV (FloatingPoint eb sb)
arg <- GrisetteSMTConfig
-> Term (FP eb sb)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType (FP eb sb))
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term (FP eb sb)
arg
(QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
SBVType a
-> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType a
sbvFromFPOrTerm @a (QuantifiedStack -> SBVType a
d QuantifiedStack
qst) (QuantifiedStack -> SRoundingMode
mode QuantifiedStack
qst) (QuantifiedStack -> SBV (FloatingPoint eb sb)
arg QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
config (ToFPTerm Int
_ Term FPRoundingMode
mode (Term a
arg :: Term b) Proxy eb
_ Proxy sb
_) = do
QuantifiedStack -> SRoundingMode
mode <- GrisetteSMTConfig
-> Term FPRoundingMode
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBVType FPRoundingMode)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term FPRoundingMode
mode
QuantifiedStack -> SBVType a
arg <- GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig
-> Term a
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
lowerSinglePrimCached' GrisetteSMTConfig
config Term a
arg
(QuantifiedStack -> SBV (FloatingPoint eb sb))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBV (FloatingPoint eb sb))
forall a. a -> RWST QuantifiedSymbols TermAll SymBiMap m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBV (FloatingPoint eb sb))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBV (FloatingPoint eb sb)))
-> (QuantifiedStack -> SBV (FloatingPoint eb sb))
-> RWST
QuantifiedSymbols
TermAll
SymBiMap
m
(QuantifiedStack -> SBV (FloatingPoint eb sb))
forall a b. (a -> b) -> a -> b
$ \QuantifiedStack
qst -> forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
SBVType FPRoundingMode -> SBVType a -> SBVType (FP eb sb)
sbvToFPTerm @b (QuantifiedStack -> SRoundingMode
mode QuantifiedStack
qst) (QuantifiedStack -> SBVType a
arg QuantifiedStack
qst)
lowerSinglePrimIntermediate GrisetteSMTConfig
_ ConTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
lowerSinglePrimIntermediate GrisetteSMTConfig
_ SymTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
lowerSinglePrimIntermediate GrisetteSMTConfig
_ ForallTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
lowerSinglePrimIntermediate GrisetteSMTConfig
_ ExistsTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
lowerSinglePrimIntermediate GrisetteSMTConfig
_ UnaryTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Not implemented"
lowerSinglePrimIntermediate GrisetteSMTConfig
_ BinaryTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Not implemented"
lowerSinglePrimIntermediate GrisetteSMTConfig
_ TernaryTerm {} = [Char]
-> RWST
QuantifiedSymbols TermAll SymBiMap m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Not implemented"
#if MIN_VERSION_sbv(10,3,0)
preprocessUIFuncs ::
[(String, (Bool, ty, Either String ([([SBVD.CV], SBVD.CV)], SBVD.CV)))] ->
Maybe [(String, ([([SBVD.CV], SBVD.CV)], SBVD.CV))]
preprocessUIFuncs :: forall ty.
[([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))]
-> Maybe [([Char], ([([CV], CV)], CV))]
preprocessUIFuncs =
(([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
-> Maybe ([Char], ([([CV], CV)], CV)))
-> [([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))]
-> Maybe [([Char], ([([CV], CV)], CV))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
(\([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
v -> case ([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
v of
([Char]
a, (Bool
_, ty
_, Right ([([CV], CV)], CV)
c)) -> ([Char], ([([CV], CV)], CV)) -> Maybe ([Char], ([([CV], CV)], CV))
forall a. a -> Maybe a
Just ([Char]
a, ([([CV], CV)], CV)
c)
([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
_ -> Maybe ([Char], ([([CV], CV)], CV))
forall a. Maybe a
Nothing)
#elif MIN_VERSION_sbv(10,0,0)
preprocessUIFuncs ::
[(String, (ty, Either String ([([SBVD.CV], SBVD.CV)], SBVD.CV)))] ->
Maybe [(String, ([([SBVD.CV], SBVD.CV)], SBVD.CV))]
preprocessUIFuncs =
traverse
(\v -> case v of
(a, (_, Right c)) -> Just (a, c)
_ -> Nothing)
#else
preprocessUIFuncs ::
[(String, (ty, ([([SBVD.CV], SBVD.CV)], SBVD.CV)))] ->
Maybe [(String, ([([SBVD.CV], SBVD.CV)], SBVD.CV))]
preprocessUIFuncs = Just . fmap (\(a, (_, c)) -> (a, c))
#endif
parseModel ::
GrisetteSMTConfig ->
SBVI.SMTModel ->
SymBiMap ->
PM.Model
parseModel :: GrisetteSMTConfig -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig
_ (SBVI.SMTModel [([Char], GeneralizedCV)]
_ Maybe [(NamedSymVar, CV)]
_ [([Char], CV)]
assoc [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
origFuncs) SymBiMap
mp =
case [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> Maybe [([Char], ([([CV], CV)], CV))]
forall ty.
[([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))]
-> Maybe [([Char], ([([CV], CV)], CV))]
preprocessUIFuncs [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
origFuncs of
Just [([Char], ([([CV], CV)], CV))]
funcs -> (([Char], ([([CV], CV)], CV)) -> Model -> Model)
-> Model -> [([Char], ([([CV], CV)], CV))] -> Model
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Char], ([([CV], CV)], CV)) -> Model -> Model
goSingle Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel ([([Char], ([([CV], CV)], CV))] -> Model)
-> [([Char], ([([CV], CV)], CV))] -> Model
forall a b. (a -> b) -> a -> b
$ [([Char], ([([CV], CV)], CV))]
funcs [([Char], ([([CV], CV)], CV))]
-> [([Char], ([([CV], CV)], CV))] -> [([Char], ([([CV], CV)], CV))]
forall a. [a] -> [a] -> [a]
++ [([Char], ([([CV], CV)], CV))]
assocFuncs
Maybe [([Char], ([([CV], CV)], CV))]
_ -> [Char] -> Model
forall a. HasCallStack => [Char] -> a
error [Char]
"SBV Failed to parse model"
where
assocFuncs :: [([Char], ([([CV], CV)], CV))]
assocFuncs = (\([Char]
s, CV
v) -> ([Char]
s, ([], CV
v))) (([Char], CV) -> ([Char], ([([CV], CV)], CV)))
-> [([Char], CV)] -> [([Char], ([([CV], CV)], CV))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Char], CV)]
assoc
goSingle :: (String, ([([SBVD.CV], SBVD.CV)], SBVD.CV)) -> PM.Model -> PM.Model
goSingle :: ([Char], ([([CV], CV)], CV)) -> Model -> Model
goSingle ([Char]
name, ([([CV], CV)], CV)
cv) Model
m = case [Char] -> SymBiMap -> Maybe (SomeTypedSymbol 'AnyKind)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
[Char] -> SymBiMap -> Maybe (SomeTypedSymbol knd)
findStringToSymbol [Char]
name SymBiMap
mp of
Just (SomeTypedSymbol (TypeRep t
_ :: p r) TypedSymbol 'AnyKind t
s) ->
TypedSymbol 'AnyKind t -> (SupportedPrim t => Model) -> Model
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol 'AnyKind t
s ((SupportedPrim t => Model) -> Model)
-> (SupportedPrim t => Model) -> Model
forall a b. (a -> b) -> a -> b
$
TypedSymbol 'AnyKind t -> t -> Model -> Model
forall t. TypedSymbol 'AnyKind t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol 'AnyKind t
s (Int -> ([([CV], CV)], CV) -> t
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult Int
0 ([([CV], CV)], CV)
cv :: r) Model
m
Maybe (SomeTypedSymbol 'AnyKind)
Nothing ->
[Char] -> Model
forall a. HasCallStack => [Char] -> a
error ([Char] -> Model) -> [Char] -> Model
forall a b. (a -> b) -> a -> b
$
[Char]
"BUG: Please send a bug report. The model is not consistent with the "
[Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"list of symbols that have been defined."