{-# 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.
    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 <- ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
    (newSymBiMap, lowered, dummyConstraint) <-
      lowerSinglePrimCached formula symBiMap
    lift $ lift $ SBV.constrain dummyConstraint
    lift $ lift $ SBV.constrain (lowered emptyQuantifiedStack)
    put newSymBiMap
  monadicSolverCheckSat :: SBVIncrementalT m (Either SolvingFailure Model)
monadicSolverCheckSat = do
    checkSatResult <- ReaderT
  GrisetteSMTConfig (StateT SymBiMap (QueryT m)) CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
SBVTC.checkSat
    config <- ask
    symBiMap <- get
    case checkSatResult of
      CheckSatResult
SBVC.Sat -> do
        sbvModel <- ReaderT GrisetteSMTConfig (StateT SymBiMap (QueryT m)) SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
SBVTC.getModel
        let model = GrisetteSMTConfig -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig
config SMTModel
sbvModel SymBiMap
symBiMap
        return $ Right 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
  _ <- TMVar SBVSolverStatus -> STM (Maybe SBVSolverStatus)
forall a. TMVar a -> STM (Maybe a)
tryTakeTMVar TMVar SBVSolverStatus
status
  putTMVar status SBVSolverTerminated

instance ConfigurableSolver GrisetteSMTConfig SBVSolverHandle where
  newSolver :: GrisetteSMTConfig -> IO SBVSolverHandle
newSolver GrisetteSMTConfig
config = do
    sbvSolverHandleInChan <- STM (TChan SolverCommand) -> IO (TChan SolverCommand)
forall a. STM a -> IO a
atomically STM (TChan SolverCommand)
forall a. STM (TChan a)
newTChan
    sbvSolverHandleOutChan <- atomically newTChan
    sbvSolverHandleStatus <- newTMVarIO SBVSolverNormal
    sbvSolverHandleMonad <- async $ do
      let handler (SomeException
e :: SomeException) =
            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 (Text -> SolvingFailure
SolvingError (Text -> SolvingFailure) -> Text -> SolvingFailure
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException SomeException
e))
      handle handler $ runSBVIncremental config $ do
        let loop = do
              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 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
                  r <- ReaderT
  GrisetteSMTConfig
  (StateT SymBiMap (QueryT IO))
  (Either SolvingFailure Model)
forall (m :: * -> *).
MonadicSolver m =>
m (Either SolvingFailure Model)
monadicSolverCheckSat
                  liftIO $ atomically $ writeTChan sbvSolverHandleOutChan r
                  loop
        loop
        liftIO $ atomically $ do
          setTerminated sbvSolverHandleStatus
          writeTChan sbvSolverHandleOutChan $ Left Terminated
    return $ SBVSolverHandle {..}

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
    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 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
        r <- SBVSolverHandle -> IO (Either SolvingFailure a)
f SBVSolverHandle
handle
        liftIO $ atomically $ do
          currStatus <- tryReadTMVar status
          case 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 ()
        return 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

sbvForall,
  sbvExists ::
    forall t.
    (SupportedNonFuncPrim t) =>
    TypedConstantSymbol t ->
    (QuantifiedStack -> SBV.SBool) ->
    QuantifiedStack ->
    SBV.SBool
#if MIN_VERSION_sbv(10,1,0)
sbvForall :: forall t.
SupportedNonFuncPrim t =>
TypedConstantSymbol t
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
sbvForall TypedConstantSymbol t
sb QuantifiedStack -> SBool
r QuantifiedStack
qst = forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t ((NonFuncPrimConstraint t => SBool) -> SBool)
-> (NonFuncPrimConstraint t => SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
  (Forall Any (NonFuncSBVBaseType t) -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
SBV.quantifiedBool ((Forall Any (NonFuncSBVBaseType t) -> SBool) -> SBool)
-> (Forall Any (NonFuncSBVBaseType t) -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
    \(SBV.Forall (SBVType t
a :: SBVType t)) ->
      QuantifiedStack -> SBool
r (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol t
-> Dynamic -> QuantifiedStack -> QuantifiedStack
forall a.
TypedConstantSymbol a
-> Dynamic -> QuantifiedStack -> QuantifiedStack
addQuantified TypedConstantSymbol t
sb (SBV (NonFuncSBVBaseType t) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV (NonFuncSBVBaseType t)
SBVType t
a) QuantifiedStack
qst
sbvExists :: forall t.
SupportedNonFuncPrim t =>
TypedConstantSymbol t
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
sbvExists TypedConstantSymbol t
sb QuantifiedStack -> SBool
r QuantifiedStack
qst = forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t ((NonFuncPrimConstraint t => SBool) -> SBool)
-> (NonFuncPrimConstraint t => SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
  (Exists Any (NonFuncSBVBaseType t) -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
SBV.quantifiedBool ((Exists Any (NonFuncSBVBaseType t) -> SBool) -> SBool)
-> (Exists Any (NonFuncSBVBaseType t) -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
    \(SBV.Exists (SBVType t
a :: SBVType t)) ->
      QuantifiedStack -> SBool
r (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol t
-> Dynamic -> QuantifiedStack -> QuantifiedStack
forall a.
TypedConstantSymbol a
-> Dynamic -> QuantifiedStack -> QuantifiedStack
addQuantified TypedConstantSymbol t
sb (SBV (NonFuncSBVBaseType t) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBV (NonFuncSBVBaseType t)
SBVType t
a) QuantifiedStack
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 :: forall t (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
Term t
-> SymBiMap -> m (SymBiMap, QuantifiedStack -> SBVType t, SBool)
lowerSinglePrimCached Term t
t' SymBiMap
m' = do
  mapState <- IO (IORef SymBiMap) -> m (IORef SymBiMap)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef SymBiMap) -> m (IORef SymBiMap))
-> IO (IORef SymBiMap) -> m (IORef SymBiMap)
forall a b. (a -> b) -> a -> b
$ SymBiMap -> IO (IORef SymBiMap)
forall a. a -> IO (IORef a)
newIORef SymBiMap
m'
  accumulatedDummyConstraints <- liftIO $ newIORef SBV.sTrue
  -- quantifiedSymbols <- liftIO $ newIORef emptyQuantifiedSymbols
  let goCached ::
        forall x.
        QuantifiedSymbols ->
        Term x ->
        m (QuantifiedStack -> SBVType x)
      goCached QuantifiedSymbols
qs t :: Term x
t@Term x
SupportedTerm = do
        mp <- IO SymBiMap -> m SymBiMap
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SymBiMap -> m SymBiMap) -> IO SymBiMap -> m SymBiMap
forall a b. (a -> b) -> a -> b
$ IORef SymBiMap -> IO SymBiMap
forall a. IORef a -> IO a
readIORef IORef SymBiMap
mapState
        case lookupTerm (SomeTerm t) mp of
          Just QuantifiedStack -> Dynamic
x -> (QuantifiedStack -> SBVType x) -> m (QuantifiedStack -> SBVType x)
forall a. a -> 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 @x (((PrimConstraint x, SMTDefinable (SBVType x),
   Mergeable (SBVType x), Typeable (SBVType x)) =>
  SBVType x)
 -> SBVType x)
-> ((PrimConstraint x, SMTDefinable (SBVType x),
     Mergeable (SBVType x), Typeable (SBVType x)) =>
    SBVType x)
-> SBVType x
forall a b. (a -> b) -> a -> b
$ Dynamic -> SBVType x -> SBVType x
forall a. Typeable a => Dynamic -> a -> a
fromDyn (QuantifiedStack -> Dynamic
x QuantifiedStack
qst) SBVType x
forall a. HasCallStack => a
undefined)
          Maybe (QuantifiedStack -> Dynamic)
Nothing -> QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
forall a.
SupportedPrim a =>
QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
goCachedImpl QuantifiedSymbols
qs Term x
t
      goCachedImpl ::
        forall a.
        (SupportedPrim a) =>
        QuantifiedSymbols ->
        Term a ->
        m (QuantifiedStack -> SBVType a)
      goCachedImpl QuantifiedSymbols
_ (ConTerm a
v) =
        (QuantifiedStack -> SBVType a) -> m (QuantifiedStack -> SBVType a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
 -> m (QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> 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
      goCachedImpl QuantifiedSymbols
qs t :: Term a
t@(SymTerm TypedSymbol 'AnyKind a
ts) = do
        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)) =>
  m (QuantifiedStack -> SBVType a))
 -> m (QuantifiedStack -> SBVType a))
-> ((PrimConstraint a, SMTDefinable (SBVType a),
     Mergeable (SBVType a), Typeable (SBVType a)) =>
    m (QuantifiedStack -> SBVType a))
-> 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"
            IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$
              IORef SymBiMap -> (SymBiMap -> SymBiMap) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef SymBiMap
mapState ((SymBiMap -> SymBiMap) -> IO ())
-> (SymBiMap -> SymBiMap) -> IO ()
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) -> m (QuantifiedStack -> SBVType a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QuantifiedStack -> SBVType a)
 -> m (QuantifiedStack -> SBVType a))
-> (QuantifiedStack -> SBVType a)
-> 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)) =>
  m (QuantifiedStack -> SBVType a))
 -> m (QuantifiedStack -> SBVType a))
-> ((PrimConstraint a, SMTDefinable (SBVType a),
     Mergeable (SBVType a), Typeable (SBVType a)) =>
    m (QuantifiedStack -> SBVType a))
-> m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
            m <- IO SymBiMap -> m SymBiMap
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SymBiMap -> m SymBiMap) -> IO SymBiMap -> m SymBiMap
forall a b. (a -> b) -> a -> b
$ IORef SymBiMap -> IO SymBiMap
forall a. IORef a -> IO a
readIORef IORef SymBiMap
mapState
            let 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)
            g <- symSBVTerm @a name
            liftIO $
              modifyIORef' accumulatedDummyConstraints $
                \SBool
c -> SBool
c SBool -> SBool -> SBool
SBV..&& forall t. SupportedPrim t => SBVType t -> SBool
funcDummyConstraint @a SBVType a
g
            liftIO $
              modifyIORef' mapState $
                addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts)
            return $ const g
      goCachedImpl QuantifiedSymbols
qs t :: Term a
t@(ForallTerm (TypedConstantSymbol t
ts :: TypedConstantSymbol t1) Term Bool
v) =
        forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t1 ((NonFuncPrimConstraint t => m (QuantifiedStack -> SBVType a))
 -> m (QuantifiedStack -> SBVType a))
-> (NonFuncPrimConstraint t => m (QuantifiedStack -> SBVType a))
-> m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
          do
            m <- IO SymBiMap -> m SymBiMap
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SymBiMap -> m SymBiMap) -> IO SymBiMap -> m SymBiMap
forall a b. (a -> b) -> a -> b
$ IORef SymBiMap -> IO SymBiMap
forall a. IORef a -> IO a
readIORef IORef SymBiMap
mapState
            let (newm, sb) =
                  attachNextQuantifiedSymbolInfo m ts
            liftIO $ writeIORef mapState newm
            let substedTerm = TypedConstantSymbol t
-> Term t
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term Bool
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a
-> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
substTerm TypedConstantSymbol t
ts (TypedConstantSymbol t -> Term t
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedConstantSymbol t
sb) HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term Bool
v
            r <- goCached (addQuantifiedSymbol sb qs) substedTerm
            let ret = TypedConstantSymbol t
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall t.
SupportedNonFuncPrim t =>
TypedConstantSymbol t
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
sbvForall TypedConstantSymbol t
sb QuantifiedStack -> SBool
r
            liftIO $
              modifyIORef' mapState $
                addBiMapIntermediate (SomeTerm t) (toDyn . ret)
            return ret
      goCachedImpl QuantifiedSymbols
qs t :: Term a
t@(ExistsTerm (TypedConstantSymbol t
ts :: TypedConstantSymbol t1) Term Bool
v) =
        forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @t1 ((NonFuncPrimConstraint t => m (QuantifiedStack -> SBVType a))
 -> m (QuantifiedStack -> SBVType a))
-> (NonFuncPrimConstraint t => m (QuantifiedStack -> SBVType a))
-> m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
          do
            m <- IO SymBiMap -> m SymBiMap
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SymBiMap -> m SymBiMap) -> IO SymBiMap -> m SymBiMap
forall a b. (a -> b) -> a -> b
$ IORef SymBiMap -> IO SymBiMap
forall a. IORef a -> IO a
readIORef IORef SymBiMap
mapState
            let (newm, sb) =
                  attachNextQuantifiedSymbolInfo m ts
            liftIO $ writeIORef mapState newm
            let substedTerm = TypedConstantSymbol t
-> Term t
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term Bool
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a
-> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
substTerm TypedConstantSymbol t
ts (TypedConstantSymbol t -> Term t
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedConstantSymbol t
sb) HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term Bool
v
            r <- goCached (addQuantifiedSymbol sb qs) substedTerm
            let ret = TypedConstantSymbol t
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
forall t.
SupportedNonFuncPrim t =>
TypedConstantSymbol t
-> (QuantifiedStack -> SBool) -> QuantifiedStack -> SBool
sbvExists TypedConstantSymbol t
sb QuantifiedStack -> SBool
r
            liftIO $
              modifyIORef' mapState $
                addBiMapIntermediate (SomeTerm t) (toDyn . ret)
            return ret
      goCachedImpl QuantifiedSymbols
qs Term a
t =
        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)) =>
  m (QuantifiedStack -> SBVType a))
 -> m (QuantifiedStack -> SBVType a))
-> ((PrimConstraint a, SMTDefinable (SBVType a),
     Mergeable (SBVType a), Typeable (SBVType a)) =>
    m (QuantifiedStack -> SBVType a))
-> m (QuantifiedStack -> SBVType a)
forall a b. (a -> b) -> a -> b
$ do
          r <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall a.
SupportedPrim a =>
QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
goCachedIntermediate QuantifiedSymbols
qs Term a
t
          let memoed = (QuantifiedStack -> SBVType a) -> QuantifiedStack -> SBVType a
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo QuantifiedStack -> SBVType a
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 QuantifiedSymbols
qs (NotTerm Term Bool
t) = do
        r <- QuantifiedSymbols
-> Term Bool -> m (QuantifiedStack -> SBVType Bool)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term Bool
t
        return $ \QuantifiedStack
qst -> SBool -> SBool
SBV.sNot (QuantifiedStack -> SBool
r QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (OrTerm Term Bool
a Term Bool
b) = do
        a' <- QuantifiedSymbols
-> Term Bool -> m (QuantifiedStack -> SBVType Bool)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term Bool
a
        b' <- goCached qs b
        return $ \QuantifiedStack
qst -> QuantifiedStack -> SBool
a' QuantifiedStack
qst SBool -> SBool -> SBool
SBV..|| QuantifiedStack -> SBool
b' QuantifiedStack
qst
      goCachedIntermediate QuantifiedSymbols
qs (AndTerm Term Bool
a Term Bool
b) = do
        a' <- QuantifiedSymbols
-> Term Bool -> m (QuantifiedStack -> SBVType Bool)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term Bool
a
        b' <- goCached qs b
        return $ \QuantifiedStack
qst -> QuantifiedStack -> SBool
a' QuantifiedStack
qst SBool -> SBool -> SBool
SBV..&& QuantifiedStack -> SBool
b' QuantifiedStack
qst
      goCachedIntermediate QuantifiedSymbols
qs (EqTerm (Term t
a :: Term v) Term t
b) = do
        a' <- QuantifiedSymbols -> Term t -> m (QuantifiedStack -> SBVType t)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term t
a
        b' <- goCached qs b
        return $
          \QuantifiedStack
qst -> forall t. SupportedPrim t => SBVType t -> SBVType t -> SBool
sbvEq @v (QuantifiedStack -> SBVType t
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType t
b' QuantifiedStack
qst)
      goCachedIntermediate
        QuantifiedSymbols
qs
        (DistinctTerm (NonEmpty (Term t)
args :: NonEmpty (Term t0))) = do
          args' <- (Term t -> m (QuantifiedStack -> SBVType t))
-> NonEmpty (Term t) -> m (NonEmpty (QuantifiedStack -> SBVType t))
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 (QuantifiedSymbols -> Term t -> m (QuantifiedStack -> SBVType t)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs) NonEmpty (Term t)
args
          return $ \QuantifiedStack
qst -> forall t. SupportedPrim t => NonEmpty (SBVType t) -> SBool
sbvDistinct @t0 (((QuantifiedStack -> SBVType t) -> SBVType t)
-> NonEmpty (QuantifiedStack -> SBVType t) -> NonEmpty (SBVType t)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QuantifiedStack -> SBVType t) -> QuantifiedStack -> SBVType t
forall a b. (a -> b) -> a -> b
$ QuantifiedStack
qst) NonEmpty (QuantifiedStack -> SBVType t)
args')
      goCachedIntermediate QuantifiedSymbols
qs (ITETerm Term Bool
c Term a
a Term a
b) = do
        c' <- QuantifiedSymbols
-> Term Bool -> m (QuantifiedStack -> SBVType Bool)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term Bool
c
        a' <- goCached qs a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (AddNumTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (NegNumTerm Term a
a) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvNegNumTerm @a . a'
      goCachedIntermediate QuantifiedSymbols
qs (MulNumTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (AbsNumTerm Term a
a) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvAbsNumTerm @a . a'
      goCachedIntermediate QuantifiedSymbols
qs (SignumNumTerm Term a
a) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvSignumNumTerm @a . a'
      goCachedIntermediate QuantifiedSymbols
qs (LtOrdTerm (Term t
a :: Term v) Term t
b) = do
        a' <- QuantifiedSymbols -> Term t -> m (QuantifiedStack -> SBVType t)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term t
a
        b' <- goCached qs b
        return $ \QuantifiedStack
qst -> forall t. PEvalOrdTerm t => SBVType t -> SBVType t -> SBool
sbvLtOrdTerm @v (QuantifiedStack -> SBVType t
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType t
b' QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (LeOrdTerm (Term t
a :: Term v) Term t
b) = do
        a' <- QuantifiedSymbols -> Term t -> m (QuantifiedStack -> SBVType t)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term t
a
        b' <- goCached qs b
        return $ \QuantifiedStack
qst -> forall t. PEvalOrdTerm t => SBVType t -> SBVType t -> SBool
sbvLeOrdTerm @v (QuantifiedStack -> SBVType t
a' QuantifiedStack
qst) (QuantifiedStack -> SBVType t
b' QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (AndBitsTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (OrBitsTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (XorBitsTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (ComplementBitsTerm Term a
a) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvComplementBitsTerm @a . a'
      goCachedIntermediate QuantifiedSymbols
qs (ShiftLeftTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (ShiftRightTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (RotateLeftTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (RotateRightTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (ApplyTerm (Term f
f :: Term f) Term a
a) = do
        l1 <- QuantifiedSymbols -> Term f -> m (QuantifiedStack -> SBVType f)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term f
f
        l2 <- goCached qs a
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (BitCastTerm (Term a
a :: Term x)) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvBitCast @x @a . a'
      goCachedIntermediate
        QuantifiedSymbols
qs
        (BitCastOrTerm (Term a
d :: Term a) (Term a
a :: Term x)) = do
          d' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
d
          a' <- goCached qs a
          return $ \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)
      goCachedIntermediate
        QuantifiedSymbols
qs
        (BVConcatTerm (Term (bv l)
a :: Term (bv l)) (Term (bv r)
b :: Term (bv r))) =
          do
            a' <- QuantifiedSymbols
-> Term (bv l) -> m (QuantifiedStack -> SBVType (bv l))
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term (bv l)
a
            b' <- goCached qs b
            return $
              \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)
      goCachedIntermediate
        QuantifiedSymbols
qs
        (BVExtendTerm Bool
signed (Proxy r
pr :: p r) (Term (bv l)
a :: Term (bv l))) =
          do
            a' <- QuantifiedSymbols
-> Term (bv l) -> m (QuantifiedStack -> SBVType (bv l))
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term (bv l)
a
            return $ sbvBVExtendTerm @bv (Proxy @l) pr signed . a'
      goCachedIntermediate
        QuantifiedSymbols
qs
        (BVSelectTerm (Proxy ix
pix :: p ix) (Proxy w
pw :: q w) (Term (bv n)
a :: Term (bv n))) =
          do
            a' <- QuantifiedSymbols
-> Term (bv n) -> m (QuantifiedStack -> SBVType (bv n))
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term (bv n)
a
            return $ sbvBVSelectTerm @bv pix pw (Proxy @n) . a'
      goCachedIntermediate QuantifiedSymbols
qs (DivIntegralTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (ModIntegralTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (QuotIntegralTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (RemIntegralTerm Term a
a Term a
b) = do
        a' <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b' <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (FPTraitTerm FPTrait
trait (Term (fp eb sb)
a :: Term (fp eb sb))) = do
        a' <- QuantifiedSymbols
-> Term (fp eb sb) -> m (QuantifiedStack -> SBVType (fp eb sb))
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term (fp eb sb)
a
        return $ sbvFPTraitTerm @fp @eb @sb trait . a'
      goCachedIntermediate QuantifiedSymbols
qs (FdivTerm Term a
a Term a
b) = do
        a <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (RecipTerm Term a
a) = do
        a <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvRecipTerm @a . a
      goCachedIntermediate QuantifiedSymbols
qs (FloatingUnaryTerm FloatingUnaryOp
op Term a
a) = do
        a <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        return $ sbvFloatingUnaryTerm @a op . a
      goCachedIntermediate QuantifiedSymbols
qs (PowerTerm Term a
a Term a
b) = do
        a <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
a
        b <- goCached qs b
        return $ \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)
      goCachedIntermediate QuantifiedSymbols
qs (FPUnaryTerm FPUnaryOp
op (Term (fp eb sb)
a :: Term (fp eb sb))) = do
        a <- QuantifiedSymbols
-> Term (fp eb sb) -> m (QuantifiedStack -> SBVType (fp eb sb))
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term (fp eb sb)
a
        return $ sbvFPUnaryTerm @fp @eb @sb op . a
      goCachedIntermediate QuantifiedSymbols
qs (FPBinaryTerm FPBinaryOp
op (Term (fp eb sb)
a :: Term (fp eb sb)) Term (fp eb sb)
b) = do
        a <- QuantifiedSymbols
-> Term (fp eb sb) -> m (QuantifiedStack -> SBVType (fp eb sb))
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term (fp eb sb)
a
        b <- goCached qs b
        return $ \QuantifiedStack
qst -> forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP eb sb) =>
FPBinaryOp
-> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb)
sbvFPBinaryTerm @fp @eb @sb FPBinaryOp
op (QuantifiedStack -> SBVType (fp eb sb)
a QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
b QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (FPRoundingUnaryTerm FPRoundingUnaryOp
op Term FPRoundingMode
round (Term (fp eb sb)
a :: Term (fp eb sb))) = do
        round <- QuantifiedSymbols
-> Term FPRoundingMode
-> m (QuantifiedStack -> SBVType FPRoundingMode)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term FPRoundingMode
round
        a <- goCached qs a
        return $ \QuantifiedStack
qst -> forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP eb sb) =>
FPRoundingUnaryOp
-> SBVType FPRoundingMode
-> SBVType (fp eb sb)
-> SBVType (fp eb sb)
sbvFPRoundingUnaryTerm @fp @eb @sb FPRoundingUnaryOp
op (QuantifiedStack -> SBV RoundingMode
round QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
a QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (FPRoundingBinaryTerm FPRoundingBinaryOp
op Term FPRoundingMode
round (Term (fp eb sb)
a :: Term (fp eb sb)) Term (fp eb sb)
b) = do
        round <- QuantifiedSymbols
-> Term FPRoundingMode
-> m (QuantifiedStack -> SBVType FPRoundingMode)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term FPRoundingMode
round
        a <- goCached qs a
        b <- goCached qs b
        return $ \QuantifiedStack
qst -> forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP eb sb) =>
FPRoundingBinaryOp
-> SBVType FPRoundingMode
-> SBVType (fp eb sb)
-> SBVType (fp eb sb)
-> SBVType (fp eb sb)
sbvFPRoundingBinaryTerm @fp @eb @sb FPRoundingBinaryOp
op (QuantifiedStack -> SBV RoundingMode
round QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
a QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
b QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (FPFMATerm Term FPRoundingMode
round (Term (fp eb sb)
a :: Term (fp eb sb)) Term (fp eb sb)
b Term (fp eb sb)
c) = do
        round <- QuantifiedSymbols
-> Term FPRoundingMode
-> m (QuantifiedStack -> SBVType FPRoundingMode)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term FPRoundingMode
round
        a <- goCached qs a
        b <- goCached qs b
        c <- goCached qs c
        return $ \QuantifiedStack
qst -> forall (fp :: Natural -> Natural -> *) (eb :: Natural)
       (sb :: Natural).
(PEvalFPTerm fp, ValidFP eb sb) =>
SBVType FPRoundingMode
-> SBVType (fp eb sb)
-> SBVType (fp eb sb)
-> SBVType (fp eb sb)
-> SBVType (fp eb sb)
sbvFPFMATerm @fp @eb @sb (QuantifiedStack -> SBV RoundingMode
round QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
a QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
b QuantifiedStack
qst) (QuantifiedStack -> SBVType (fp eb sb)
c QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (FromIntegralTerm (Term a
b :: Term b)) = do
        b <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
b
        return $ sbvFromIntegralTerm @b @a . b
      goCachedIntermediate QuantifiedSymbols
qs (FromFPOrTerm Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg) = do
        d <- QuantifiedSymbols -> Term a -> m (QuantifiedStack -> SBVType a)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term a
d
        mode <- goCached qs mode
        arg <- goCached qs arg
        return $ \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 -> SBV RoundingMode
mode QuantifiedStack
qst) (QuantifiedStack -> SBV (FloatingPoint eb sb)
arg QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
qs (ToFPTerm Term FPRoundingMode
mode (Term a
arg :: Term b) Proxy eb
_ Proxy sb
_) = do
        mode <- QuantifiedSymbols
-> Term FPRoundingMode
-> m (QuantifiedStack -> SBVType FPRoundingMode)
forall x.
QuantifiedSymbols -> Term x -> m (QuantifiedStack -> SBVType x)
goCached QuantifiedSymbols
qs Term FPRoundingMode
mode
        arg <- goCached qs arg
        return $ \QuantifiedStack
qst -> forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
SBVType FPRoundingMode -> SBVType a -> SBVType (FP eb sb)
sbvToFPTerm @b (QuantifiedStack -> SBV RoundingMode
mode QuantifiedStack
qst) (QuantifiedStack -> SBVType a
arg QuantifiedStack
qst)
      goCachedIntermediate QuantifiedSymbols
_ ConTerm {} = [Char] -> m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
      goCachedIntermediate QuantifiedSymbols
_ SymTerm {} = [Char] -> m (QuantifiedStack -> SBVType a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
      goCachedIntermediate QuantifiedSymbols
_ ForallTerm {} = [Char] -> m (QuantifiedStack -> SBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
      goCachedIntermediate QuantifiedSymbols
_ ExistsTerm {} = [Char] -> m (QuantifiedStack -> SBool)
forall a. HasCallStack => [Char] -> a
error [Char]
"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 :: forall a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
Term a -> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
lowerSinglePrim Term a
t =
  Term a
-> SymBiMap -> m (SymBiMap, QuantifiedStack -> SBVType a, SBool)
forall t (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
Term t
-> SymBiMap -> m (SymBiMap, QuantifiedStack -> SBVType t, SBool)
lowerSinglePrimCached Term a
t SymBiMap
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 :: 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
_ model :: SMTModel
model@(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 (s :: TypedSymbol 'AnyKind t
s@TypedSymbol {} :: TypedSymbol 'AnyKind r)) ->
        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. The map is "
            [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> SymBiMap -> [Char]
forall a. Show a => a -> [Char]
show SymBiMap
mp
            [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
". The model is "
            [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> SMTModel -> [Char]
forall a. Show a => a -> [Char]
show SMTModel
model