{-# 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
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Backend.Solving
  ( -- * SBV backend configuration
    GrisetteSMTConfig (..),
    boolector,
    bitwuzla,
    cvc4,
    cvc5,
    yices,
    dReal,
    z3,
    mathSAT,
    abc,

    -- * Changing the extra configurations
    ExtraConfig (..),
    withTimeout,
    clearTimeout,

    -- * SBV monadic solver interface
    SBVIncrementalT,
    SBVIncremental,
    runSBVIncrementalT,
    runSBVIncremental,

    -- * SBV solver handle
    SBVSolverHandle,

    -- * Internal lowering functions
    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))

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- | Grisette specific extra configurations for the SBV backend.
newtype ExtraConfig = ExtraConfig
  { -- | Timeout in microseconds for each solver call. CEGIS may call the
    -- solver multiple times and each call has its own timeout.
    ExtraConfig -> Maybe Int
timeout :: Maybe Int
  }

-- | Solver configuration for the Grisette SBV backend.
--
-- A Grisette solver configuration consists of a SBV solver configuration and
-- some extra configurations.
--
-- You should start with the predefined configurations.
data GrisetteSMTConfig = GrisetteSMTConfig
  { GrisetteSMTConfig -> SMTConfig
sbvConfig :: SBV.SMTConfig,
    GrisetteSMTConfig -> ExtraConfig
extraConfig :: ExtraConfig
  }

preciseExtraConfig :: ExtraConfig
preciseExtraConfig :: ExtraConfig
preciseExtraConfig = ExtraConfig {timeout :: Maybe Int
timeout = Maybe Int
forall a. Maybe a
Nothing}

-- | Solver configuration for Boolector. <https://boolector.github.io/>
boolector :: GrisetteSMTConfig
boolector :: GrisetteSMTConfig
boolector = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.boolector ExtraConfig
preciseExtraConfig

-- | Solver configuration for Bitwuzla. <https://bitwuzla.github.io/>
bitwuzla :: GrisetteSMTConfig
bitwuzla :: GrisetteSMTConfig
bitwuzla = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.bitwuzla ExtraConfig
preciseExtraConfig

-- | Solver configuration for CVC4. <https://cvc4.github.io/>
cvc4 :: GrisetteSMTConfig
cvc4 :: GrisetteSMTConfig
cvc4 = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.cvc4 ExtraConfig
preciseExtraConfig

-- | Solver configuration for CVC5. <https://cvc5.github.io/>
cvc5 :: GrisetteSMTConfig
cvc5 :: GrisetteSMTConfig
cvc5 = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.cvc5 ExtraConfig
preciseExtraConfig

-- | Solver configuration for Yices. <https://yices.csl.sri.com/>
yices :: GrisetteSMTConfig
yices :: GrisetteSMTConfig
yices = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.yices ExtraConfig
preciseExtraConfig

-- | Solver configuration for DReal. <http://dreal.github.io/>
dReal :: GrisetteSMTConfig
dReal :: GrisetteSMTConfig
dReal = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.dReal ExtraConfig
preciseExtraConfig

-- | Solver configuration for Z3. <https://github.com/Z3Prover/z3/>
z3 :: GrisetteSMTConfig
z3 :: GrisetteSMTConfig
z3 = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.z3 ExtraConfig
preciseExtraConfig

-- | Solver configuration for MathSAT. <http://mathsat.fbk.eu/>
mathSAT :: GrisetteSMTConfig
mathSAT :: GrisetteSMTConfig
mathSAT = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.mathSAT ExtraConfig
preciseExtraConfig

-- | Solver configuration for ABC. <http://www.eecs.berkeley.edu/~alanmi/abc/>
abc :: GrisetteSMTConfig
abc :: GrisetteSMTConfig
abc = SMTConfig -> ExtraConfig -> GrisetteSMTConfig
GrisetteSMTConfig SMTConfig
SBV.abc ExtraConfig
preciseExtraConfig

-- | Set the timeout for the solver configuration.
--
-- The timeout is in microseconds (1e-6 seconds). The timeout is applied to each
-- individual solver query.
withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig
withTimeout :: Int -> GrisetteSMTConfig -> GrisetteSMTConfig
withTimeout Int
t GrisetteSMTConfig
config =
  GrisetteSMTConfig
config {extraConfig = (extraConfig config) {timeout = Just t}}

-- | Clear the timeout for the solver configuration.
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

-- | Apply the timeout to the configuration.
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

-- | Incremental solver monad transformer with the SBV backend.
type SBVIncrementalT m =
  ReaderT GrisetteSMTConfig (StateT SymBiMap (SBVTC.QueryT m))

-- | Incremental solver monad with the SBV backend.
type SBVIncremental = SBVIncrementalT IO

-- | Run the incremental solver monad with a given configuration.
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

-- | Run the incremental solver monad transformer with a given configuration.
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

-- | The handle type for the SBV solver.
--
-- See 'ConfigurableSolver' and 'Solver' for the interfaces.
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

-- | Lower a single primitive term to SBV. With an explicitly provided
-- 'SymBiMap' cache.
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
  -- (_, newm, dummy) <- declareAllUFuncsImpl config t HS.empty m
  (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)

-- | Lower a single primitive term to SBV.
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

-- | Parse an SBV model to a Grisette model.
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."