content: {-# LANGUAGE BangPatterns #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE RecordWildCards #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE Strict #-}
  {-# 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
    ( Exception (displayException),
      SomeException,
      handle,
      throwTo,
    )
  import Control.Monad.IO.Class (MonadIO, liftIO)
  import Control.Monad.Reader
    ( MonadReader (ask),
      MonadTrans (lift),
      ReaderT (runReaderT),
      ask,
    )
  import Control.Monad.STM (STM)
  import Control.Monad.State.Strict
    ( MonadState (get, put),
      StateT,
      evalStateT,
    )
  import Data.Dynamic (fromDyn, toDyn)
  import qualified Data.HashSet as HS
  import Data.IORef (modifyIORef', newIORef, readIORef, writeIORef)
  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 qualified Data.Text as T
  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.Core.Data.MemoUtils (htmemo)
  import Grisette.Internal.SymPrim.GeneralFun (substTerm)
  import Grisette.Internal.SymPrim.Prim.Model as PM
    ( Model,
    )
  import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
  import Grisette.Internal.SymPrim.Prim.Term
    ( PEvalApplyTerm (sbvApplyTerm),
      PEvalBVTerm (sbvBVConcatTerm, sbvBVExtendTerm, sbvBVSelectTerm),
      PEvalBitCastOrTerm (sbvBitCastOr),
      PEvalBitCastTerm (sbvBitCast),
      PEvalBitwiseTerm
        ( sbvAndBitsTerm,
          sbvComplementBitsTerm,
          sbvOrBitsTerm,
          sbvXorBitsTerm
        ),
      PEvalDivModIntegralTerm
        ( sbvDivIntegralTerm,
          sbvModIntegralTerm,
          sbvQuotIntegralTerm,
          sbvRemIntegralTerm
        ),
      PEvalFPTerm
        ( sbvFPBinaryTerm,
          sbvFPFMATerm,
          sbvFPRoundingBinaryTerm,
          sbvFPRoundingUnaryTerm,
          sbvFPTraitTerm,
          sbvFPUnaryTerm
        ),
      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,
          parseSMTModelResult,
          sbvDistinct,
          sbvEq,
          sbvIte,
          symSBVName,
          symSBVTerm,
          withPrim
        ),
      SymbolKind (AnyKind),
      Term,
      TypedConstantSymbol,
      TypedSymbol (TypedSymbol),
      someTypedSymbol,
      symTerm,
      pattern AbsNumTerm,
      pattern AddNumTerm,
      pattern AndBitsTerm,
      pattern AndTerm,
      pattern ApplyTerm,
      pattern BVConcatTerm,
      pattern BVExtendTerm,
      pattern BVSelectTerm,
      pattern BitCastOrTerm,
      pattern BitCastTerm,
      pattern ComplementBitsTerm,
      pattern ConTerm,
      pattern DistinctTerm,
      pattern DivIntegralTerm,
      pattern EqTerm,
      pattern ExistsTerm,
      pattern FPBinaryTerm,
      pattern FPFMATerm,
      pattern FPRoundingBinaryTerm,
      pattern FPRoundingUnaryTerm,
      pattern FPTraitTerm,
      pattern FPUnaryTerm,
      pattern FdivTerm,
      pattern FloatingUnaryTerm,
      pattern ForallTerm,
      pattern FromFPOrTerm,
      pattern FromIntegralTerm,
      pattern ITETerm,
      pattern LeOrdTerm,
      pattern LtOrdTerm,
      pattern ModIntegralTerm,
      pattern MulNumTerm,
      pattern NegNumTerm,
      pattern NotTerm,
      pattern OrBitsTerm,
      pattern OrTerm,
      pattern PowerTerm,
      pattern QuotIntegralTerm,
      pattern RecipTerm,
      pattern RemIntegralTerm,
      pattern RotateLeftTerm,
      pattern RotateRightTerm,
      pattern ShiftLeftTerm,
      pattern ShiftRightTerm,
      pattern SignumNumTerm,
      pattern SupportedTerm,
      pattern SymTerm,
      pattern ToFPTerm,
      pattern XorBitsTerm,
    )
  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.
      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
    { sbvConfig :: SBV.SMTConfig,
      extraConfig :: ExtraConfig
    }
  
  preciseExtraConfig :: ExtraConfig
  preciseExtraConfig = ExtraConfig {timeout = Nothing}
  
  -- | Solver configuration for Boolector. <https://boolector.github.io/>
  boolector :: GrisetteSMTConfig
  boolector = GrisetteSMTConfig SBV.boolector preciseExtraConfig
  
  -- | Solver configuration for Bitwuzla. <https://bitwuzla.github.io/>
  bitwuzla :: GrisetteSMTConfig
  bitwuzla = GrisetteSMTConfig SBV.bitwuzla preciseExtraConfig
  
  -- | Solver configuration for CVC4. <https://cvc4.github.io/>
  cvc4 :: GrisetteSMTConfig
  cvc4 = GrisetteSMTConfig SBV.cvc4 preciseExtraConfig
  
  -- | Solver configuration for CVC5. <https://cvc5.github.io/>
  cvc5 :: GrisetteSMTConfig
  cvc5 = GrisetteSMTConfig SBV.cvc5 preciseExtraConfig
  
  -- | Solver configuration for Yices. <https://yices.csl.sri.com/>
  yices :: GrisetteSMTConfig
  yices = GrisetteSMTConfig SBV.yices preciseExtraConfig
  
  -- | Solver configuration for DReal. <http://dreal.github.io/>
  dReal :: GrisetteSMTConfig
  dReal = GrisetteSMTConfig SBV.dReal preciseExtraConfig
  
  -- | Solver configuration for Z3. <https://github.com/Z3Prover/z3/>
  z3 :: GrisetteSMTConfig
  z3 = GrisetteSMTConfig SBV.z3 preciseExtraConfig
  
  -- | Solver configuration for MathSAT. <http://mathsat.fbk.eu/>
  mathSAT :: GrisetteSMTConfig
  mathSAT = GrisetteSMTConfig SBV.mathSAT preciseExtraConfig
  
  -- | Solver configuration for ABC. <http://www.eecs.berkeley.edu/~alanmi/abc/>
  abc :: GrisetteSMTConfig
  abc = GrisetteSMTConfig SBV.abc 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 t config =
    config {extraConfig = (extraConfig config) {timeout = Just t}}
  
  -- | Clear the timeout for the solver configuration.
  clearTimeout :: GrisetteSMTConfig -> GrisetteSMTConfig
  clearTimeout config =
    config {extraConfig = (extraConfig config) {timeout = Nothing}}
  
  sbvCheckSatResult :: SBVC.CheckSatResult -> SolvingFailure
  sbvCheckSatResult SBVC.Sat = error "Should not happen"
  sbvCheckSatResult (SBVC.DSat _) = error "DSat is currently not supported"
  sbvCheckSatResult SBVC.Unsat = Unsat
  sbvCheckSatResult SBVC.Unk = Unk
  
  -- | Apply the timeout to the configuration.
  applyTimeout ::
    (MonadIO m, SBVTC.MonadQuery m) => GrisetteSMTConfig -> m a -> m a
  applyTimeout config q = case timeout (extraConfig config) of
    Nothing -> q
    Just t -> SBVTC.timeout t 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 = runSBVIncrementalT
  
  -- | Run the incremental solver monad transformer with a given configuration.
  runSBVIncrementalT ::
    (SBVTC.ExtractIO m) =>
    GrisetteSMTConfig ->
    SBVIncrementalT m a ->
    m a
  runSBVIncrementalT config sbvIncrementalT =
    SBVT.runSMTWith (sbvConfig config) $
      SBVTC.query $
        applyTimeout config $
          flip evalStateT emptySymBiMap $
            runReaderT sbvIncrementalT config
  
  instance (MonadIO m) => MonadicSolver (SBVIncrementalT m) where
    monadicSolverAssert (SymBool formula) = do
      symBiMap <- get
      (newSymBiMap, lowered, dummyConstraint) <-
        lowerSinglePrimCached formula symBiMap
      lift $ lift $ SBV.constrain dummyConstraint
      lift $ lift $ SBV.constrain (lowered emptyQuantifiedStack)
      put newSymBiMap
    monadicSolverCheckSat = do
      checkSatResult <- SBVTC.checkSat
      config <- ask
      symBiMap <- get
      case checkSatResult of
        SBVC.Sat -> do
          sbvModel <- SBVTC.getModel
          let model = parseModel config sbvModel symBiMap
          return $ Right model
        r -> return $ Left $ sbvCheckSatResult r
    monadicSolverResetAssertions = SBVTC.resetAssertions
    monadicSolverPush = SBVTC.push
    monadicSolverPop = SBVTC.pop
  
  data SBVSolverStatus = SBVSolverNormal | SBVSolverTerminated
  
  -- | The handle type for the SBV solver.
  --
  -- See 'ConfigurableSolver' and 'Solver' for the interfaces.
  data SBVSolverHandle = SBVSolverHandle
    { sbvSolverHandleMonad :: Async (),
      sbvSolverHandleStatus :: TMVar SBVSolverStatus,
      sbvSolverHandleInChan :: TChan SolverCommand,
      sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
    }
  
  setTerminated :: TMVar SBVSolverStatus -> STM ()
  setTerminated status = do
    _ <- tryTakeTMVar status
    putTMVar status SBVSolverTerminated
  
  instance ConfigurableSolver GrisetteSMTConfig SBVSolverHandle where
    newSolver config = do
      sbvSolverHandleInChan <- atomically newTChan
      sbvSolverHandleOutChan <- atomically newTChan
      sbvSolverHandleStatus <- newTMVarIO SBVSolverNormal
      sbvSolverHandleMonad <- async $ do
        let handler (e :: SomeException) =
              liftIO $
                atomically $ do
                  setTerminated sbvSolverHandleStatus
                  writeTChan
                    sbvSolverHandleOutChan
                    (Left (SolvingError $ T.pack $ displayException e))
        handle handler $ runSBVIncremental config $ do
          let loop = do
                nextFormula <-
                  liftIO $ atomically $ readTChan sbvSolverHandleInChan
                case nextFormula of
                  SolverPush n -> monadicSolverPush n >> loop
                  SolverPop n -> monadicSolverPop n >> loop
                  SolverTerminate -> return ()
                  SolverResetAssertions -> monadicSolverResetAssertions >> loop
                  SolverAssert formula -> do
                    monadicSolverAssert formula
                    loop
                  SolverCheckSat -> do
                    r <- monadicSolverCheckSat
                    liftIO $ atomically $ writeTChan sbvSolverHandleOutChan r
                    loop
          loop
          liftIO $ atomically $ do
            setTerminated sbvSolverHandleStatus
            writeTChan sbvSolverHandleOutChan $ Left Terminated
      return $ SBVSolverHandle {..}
  
  instance Solver SBVSolverHandle where
    solverRunCommand f handle@(SBVSolverHandle _ status inChan _) !command = do
      st <- liftIO $ atomically $ takeTMVar status
      case st of
        SBVSolverNormal -> do
          liftIO $ atomically $ writeTChan inChan command
          r <- f handle
          liftIO $ atomically $ do
            currStatus <- tryReadTMVar status
            case currStatus of
              Nothing -> putTMVar status SBVSolverNormal
              Just _ -> return ()
          return r
        SBVSolverTerminated -> do
          liftIO $ atomically $ setTerminated status
          return $ Left Terminated
    solverCheckSat handle =
      solverRunCommand
        ( \(SBVSolverHandle _ _ _ outChan) ->
            liftIO $ atomically $ readTChan outChan
        )
        handle
        SolverCheckSat
    solverTerminate (SBVSolverHandle thread status inChan _) = do
      liftIO $ atomically $ do
        setTerminated status
        writeTChan inChan SolverTerminate
      wait thread
    solverForceTerminate (SBVSolverHandle thread status _ outChan) = do
      liftIO $ atomically $ do
        setTerminated status
        writeTChan outChan (Left Terminated)
      throwTo (asyncThreadId thread) ExitSuccess
      wait thread
  
  sbvForall,
    sbvExists ::
      forall t.
      (SupportedNonFuncPrim t) =>
      TypedConstantSymbol t ->
      (QuantifiedStack -> SBV.SBool) ->
      QuantifiedStack ->
      SBV.SBool
  #if MIN_VERSION_sbv(10,1,0)
  sbvForall sb r qst = withNonFuncPrim @t $
    SBV.quantifiedBool $
      \(SBV.Forall (a :: SBVType t)) ->
        r $ addQuantified sb (toDyn a) qst
  sbvExists sb r qst = withNonFuncPrim @t $
    SBV.quantifiedBool $
      \(SBV.Exists (a :: SBVType t)) ->
        r $ addQuantified sb (toDyn a) qst
  #else
  sbvForall =
    error "Quantifiers are only available when you build with SBV 10.1.0 or later"
  sbvExists =
    error "Quantifiers are only available when you build with SBV 10.1.0 or later"
  #endif
  
  -- | Lower a single primitive term to SBV. With an explicitly provided
  -- 'SymBiMap' cache.
  lowerSinglePrimCached ::
    forall t m.
    (HasCallStack, SBVFreshMonad m) =>
    Term t ->
    SymBiMap ->
    m (SymBiMap, QuantifiedStack -> SBVType t, SBV.SBool)
  lowerSinglePrimCached t' m' = do
    mapState <- liftIO $ newIORef m'
    accumulatedDummyConstraints <- liftIO $ newIORef SBV.sTrue
    -- quantifiedSymbols <- liftIO $ newIORef emptyQuantifiedSymbols
    let goCached ::
          forall x.
          QuantifiedSymbols ->
          Term x ->
          m (QuantifiedStack -> SBVType x)
        goCached qs t@SupportedTerm = do
          mp <- liftIO $ readIORef mapState
          case lookupTerm (SomeTerm t) mp of
            Just x -> return (\qst -> withPrim @x $ fromDyn (x qst) undefined)
            Nothing -> goCachedImpl qs t
        goCachedImpl ::
          forall a.
          (SupportedPrim a) =>
          QuantifiedSymbols ->
          Term a ->
          m (QuantifiedStack -> SBVType a)
        goCachedImpl _ (ConTerm v) =
          return $ const $ conSBVTerm v
        goCachedImpl qs t@(SymTerm ts) = do
          if isQuantifiedSymbol ts qs
            then withPrim @a $ do
              let retDyn qst =
                    case lookupQuantified (someTypedSymbol ts) qst of
                      Just v -> v
                      Nothing ->
                        error "BUG: Symbol not found in the quantified stack"
              liftIO $
                modifyIORef' mapState $
                  \m -> addBiMapIntermediate (SomeTerm t) retDyn m
              return $
                \x ->
                  fromDyn
                    (retDyn x)
                    (error "BUG: Symbol not found in the quantified stack")
            else withPrim @a $ do
              m <- liftIO $ readIORef mapState
              let name = symSBVName ts (sizeBiMap m)
              g <- symSBVTerm @a name
              liftIO $
                modifyIORef' accumulatedDummyConstraints $
                  \c -> c SBV..&& funcDummyConstraint @a g
              liftIO $
                modifyIORef' mapState $
                  addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts)
              return $ const g
        goCachedImpl qs t@(ForallTerm (ts :: TypedConstantSymbol t1) v) =
          withNonFuncPrim @t1 $ do
            do
              m <- liftIO $ readIORef mapState
              let (newm, sb) =
                    attachNextQuantifiedSymbolInfo m ts
              liftIO $ writeIORef mapState newm
              let substedTerm = substTerm ts (symTerm sb) HS.empty v
              r <- goCached (addQuantifiedSymbol sb qs) substedTerm
              let ret = sbvForall sb r
              liftIO $
                modifyIORef' mapState $
                  addBiMapIntermediate (SomeTerm t) (toDyn . ret)
              return ret
        goCachedImpl qs t@(ExistsTerm (ts :: TypedConstantSymbol t1) v) =
          withNonFuncPrim @t1 $ do
            do
              m <- liftIO $ readIORef mapState
              let (newm, sb) =
                    attachNextQuantifiedSymbolInfo m ts
              liftIO $ writeIORef mapState newm
              let substedTerm = substTerm ts (symTerm sb) HS.empty v
              r <- goCached (addQuantifiedSymbol sb qs) substedTerm
              let ret = sbvExists sb r
              liftIO $
                modifyIORef' mapState $
                  addBiMapIntermediate (SomeTerm t) (toDyn . ret)
              return ret
        goCachedImpl qs t =
          withPrim @a $ do
            r <- goCachedIntermediate qs t
            let memoed = htmemo r
                {-# NOINLINE memoed #-}
            liftIO $
              modifyIORef' mapState $
                addBiMapIntermediate (SomeTerm t) (toDyn . memoed)
            return memoed
        goCachedIntermediate ::
          forall a.
          (SupportedPrim a) =>
          QuantifiedSymbols ->
          Term a ->
          m (QuantifiedStack -> SBVType a)
        goCachedIntermediate qs (NotTerm t) = do
          r <- goCached qs t
          return $ \qst -> SBV.sNot (r qst)
        goCachedIntermediate qs (OrTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> a' qst SBV..|| b' qst
        goCachedIntermediate qs (AndTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> a' qst SBV..&& b' qst
        goCachedIntermediate qs (EqTerm (a :: Term v) b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $
            \qst -> sbvEq @v (a' qst) (b' qst)
        goCachedIntermediate
          qs
          (DistinctTerm (args :: NonEmpty (Term t0))) = do
            args' <- traverse (goCached qs) args
            return $ \qst -> sbvDistinct @t0 (fmap ($ qst) args')
        goCachedIntermediate qs (ITETerm c a b) = do
          c' <- goCached qs c
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvIte @a (c' qst) (a' qst) (b' qst)
        goCachedIntermediate qs (AddNumTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvAddNumTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (NegNumTerm a) = do
          a' <- goCached qs a
          return $ sbvNegNumTerm @a . a'
        goCachedIntermediate qs (MulNumTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvMulNumTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (AbsNumTerm a) = do
          a' <- goCached qs a
          return $ sbvAbsNumTerm @a . a'
        goCachedIntermediate qs (SignumNumTerm a) = do
          a' <- goCached qs a
          return $ sbvSignumNumTerm @a . a'
        goCachedIntermediate qs (LtOrdTerm (a :: Term v) b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvLtOrdTerm @v (a' qst) (b' qst)
        goCachedIntermediate qs (LeOrdTerm (a :: Term v) b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvLeOrdTerm @v (a' qst) (b' qst)
        goCachedIntermediate qs (AndBitsTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvAndBitsTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (OrBitsTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvOrBitsTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (XorBitsTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvXorBitsTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (ComplementBitsTerm a) = do
          a' <- goCached qs a
          return $ sbvComplementBitsTerm @a . a'
        goCachedIntermediate qs (ShiftLeftTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvShiftLeftTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (ShiftRightTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvShiftRightTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (RotateLeftTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvRotateLeftTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (RotateRightTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvRotateRightTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (ApplyTerm (f :: Term f) a) = do
          l1 <- goCached qs f
          l2 <- goCached qs a
          return $ \qst -> sbvApplyTerm @f (l1 qst) (l2 qst)
        goCachedIntermediate qs (BitCastTerm (a :: Term x)) = do
          a' <- goCached qs a
          return $ sbvBitCast @x @a . a'
        goCachedIntermediate
          qs
          (BitCastOrTerm (d :: Term a) (a :: Term x)) = do
            d' <- goCached qs d
            a' <- goCached qs a
            return $ \qst -> sbvBitCastOr @x @a (d' qst) (a' qst)
        goCachedIntermediate
          qs
          (BVConcatTerm (a :: Term (bv l)) (b :: Term (bv r))) =
            do
              a' <- goCached qs a
              b' <- goCached qs b
              return $
                \qst ->
                  sbvBVConcatTerm @bv (Proxy @l) (Proxy @r) (a' qst) (b' qst)
        goCachedIntermediate
          qs
          (BVExtendTerm signed (pr :: p r) (a :: Term (bv l))) =
            do
              a' <- goCached qs a
              return $ sbvBVExtendTerm @bv (Proxy @l) pr signed . a'
        goCachedIntermediate
          qs
          (BVSelectTerm (pix :: p ix) (pw :: q w) (a :: Term (bv n))) =
            do
              a' <- goCached qs a
              return $ sbvBVSelectTerm @bv pix pw (Proxy @n) . a'
        goCachedIntermediate qs (DivIntegralTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvDivIntegralTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (ModIntegralTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvModIntegralTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (QuotIntegralTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvQuotIntegralTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (RemIntegralTerm a b) = do
          a' <- goCached qs a
          b' <- goCached qs b
          return $ \qst -> sbvRemIntegralTerm @a (a' qst) (b' qst)
        goCachedIntermediate qs (FPTraitTerm trait (a :: Term (fp eb sb))) = do
          a' <- goCached qs a
          return $ sbvFPTraitTerm @fp @eb @sb trait . a'
        goCachedIntermediate qs (FdivTerm a b) = do
          a <- goCached qs a
          b <- goCached qs b
          return $ \qst -> sbvFdivTerm @a (a qst) (b qst)
        goCachedIntermediate qs (RecipTerm a) = do
          a <- goCached qs a
          return $ sbvRecipTerm @a . a
        goCachedIntermediate qs (FloatingUnaryTerm op a) = do
          a <- goCached qs a
          return $ sbvFloatingUnaryTerm @a op . a
        goCachedIntermediate qs (PowerTerm a b) = do
          a <- goCached qs a
          b <- goCached qs b
          return $ \qst -> sbvPowerTerm @a (a qst) (b qst)
        goCachedIntermediate qs (FPUnaryTerm op (a :: Term (fp eb sb))) = do
          a <- goCached qs a
          return $ sbvFPUnaryTerm @fp @eb @sb op . a
        goCachedIntermediate qs (FPBinaryTerm op (a :: Term (fp eb sb)) b) = do
          a <- goCached qs a
          b <- goCached qs b
          return $ \qst -> sbvFPBinaryTerm @fp @eb @sb op (a qst) (b qst)
        goCachedIntermediate qs (FPRoundingUnaryTerm op round (a :: Term (fp eb sb))) = do
          round <- goCached qs round
          a <- goCached qs a
          return $ \qst -> sbvFPRoundingUnaryTerm @fp @eb @sb op (round qst) (a qst)
        goCachedIntermediate qs (FPRoundingBinaryTerm op round (a :: Term (fp eb sb)) b) = do
          round <- goCached qs round
          a <- goCached qs a
          b <- goCached qs b
          return $ \qst -> sbvFPRoundingBinaryTerm @fp @eb @sb op (round qst) (a qst) (b qst)
        goCachedIntermediate qs (FPFMATerm round (a :: Term (fp eb sb)) b c) = do
          round <- goCached qs round
          a <- goCached qs a
          b <- goCached qs b
          c <- goCached qs c
          return $ \qst -> sbvFPFMATerm @fp @eb @sb (round qst) (a qst) (b qst) (c qst)
        goCachedIntermediate qs (FromIntegralTerm (b :: Term b)) = do
          b <- goCached qs b
          return $ sbvFromIntegralTerm @b @a . b
        goCachedIntermediate qs (FromFPOrTerm d mode arg) = do
          d <- goCached qs d
          mode <- goCached qs mode
          arg <- goCached qs arg
          return $ \qst -> sbvFromFPOrTerm @a (d qst) (mode qst) (arg qst)
        goCachedIntermediate qs (ToFPTerm mode (arg :: Term b) _ _) = do
          mode <- goCached qs mode
          arg <- goCached qs arg
          return $ \qst -> sbvToFPTerm @b (mode qst) (arg qst)
        goCachedIntermediate _ ConTerm {} = error "Should not happen"
        goCachedIntermediate _ SymTerm {} = error "Should not happen"
        goCachedIntermediate _ ForallTerm {} = error "Should not happen"
        goCachedIntermediate _ ExistsTerm {} = error "Should not happen"
    r <- goCached emptyQuantifiedSymbols t'
    m <- liftIO $ readIORef mapState
    constraint <- liftIO $ readIORef accumulatedDummyConstraints
    return (m, r, constraint)
  
  -- | Lower a single primitive term to SBV.
  lowerSinglePrim ::
    forall a m.
    (HasCallStack, SBVFreshMonad m) =>
    Term a ->
    m (SymBiMap, QuantifiedStack -> SBVType a, SBV.SBool)
  lowerSinglePrim t =
    lowerSinglePrimCached t emptySymBiMap
  
  #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 =
    traverse
      (\v -> case v of
        (a, (_, _, Right c)) -> Just (a, c)
        _ -> 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 _ model@(SBVI.SMTModel _ _ assoc origFuncs) mp =
    case preprocessUIFuncs origFuncs of
      Just funcs -> foldr goSingle emptyModel $ funcs ++ assocFuncs
      _ -> error "SBV Failed to parse model"
    where
      assocFuncs = (\(s, v) -> (s, ([], v))) <$> assoc
      goSingle :: (String, ([([SBVD.CV], SBVD.CV)], SBVD.CV)) -> PM.Model -> PM.Model
      goSingle (name, cv) m = case findStringToSymbol name mp of
        Just (SomeTypedSymbol (s@TypedSymbol {} :: TypedSymbol 'AnyKind r)) ->
          insertValue
            s
            (parseSMTModelResult 0 cv :: r)
            m
        Nothing ->
          error $
            "BUG: Please send a bug report. The model is not consistent with the "
              <> "list of symbols that have been defined. The map is "
              <> show mp
              <> ". The model is "
              <> show model
  