{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Backend.Solving
-- Copyright   :   (c) Sirui Lu 2021-2023
-- 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
    ApproximationConfig (..),
    ExtraConfig (..),
    precise,
    approx,
    withTimeout,
    clearTimeout,
    withApprox,
    clearApprox,
    GrisetteSMTConfig (..),

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

    -- * SBV solver handle
    SBVSolverHandle,

    -- * Internal lowering functions
    lowerSinglePrimCached,
    lowerSinglePrim,
    parseModel,
  )
where

import Control.Concurrent.Async (Async (asyncThreadId), async, wait)
import Control.Concurrent.STM
  ( TMVar,
    atomically,
    newTMVarIO,
    putTMVar,
    takeTMVar,
    tryReadTMVar,
    tryTakeTMVar,
  )
import Control.Concurrent.STM.TChan (TChan, newTChan, readTChan, writeTChan)
import Control.Exception (handle, throwTo)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.Reader
  ( MonadReader (ask),
    MonadTrans (lift),
    ReaderT (runReaderT),
  )
import Control.Monad.STM (STM)
import Control.Monad.State (MonadState (get, put), StateT, evalStateT)
import Data.Dynamic (fromDyn, toDyn)
import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import qualified Data.SBV.Control as SBVC
import qualified Data.SBV.Dynamic as SBVD
import qualified Data.SBV.Internals as SBVI
import qualified Data.SBV.Trans as SBVT
import qualified Data.SBV.Trans.Control as SBVTC
import GHC.IO.Exception (ExitCode (ExitSuccess))
import GHC.Stack (HasCallStack)
import GHC.TypeNats (KnownNat, Nat)
import Grisette.Internal.Backend.SymBiMap
  ( SymBiMap,
    addBiMap,
    addBiMapIntermediate,
    emptySymBiMap,
    findStringToSymbol,
    lookupTerm,
    sizeBiMap,
  )
import Grisette.Internal.Core.Data.Class.ModelOps (ModelOps (emptyModel, insertValue))
import Grisette.Internal.Core.Data.Class.Solver
  ( ConfigurableSolver (newSolver),
    MonadicSolver
      ( monadicSolverPop,
        monadicSolverPush,
        monadicSolverSolve
      ),
    Solver
      ( solverForceTerminate,
        solverRunCommand,
        solverSolve,
        solverTerminate
      ),
    SolverCommand (SolverPop, SolverPush, SolverSolve, SolverTerminate),
    SolvingFailure (SolvingError, Terminated, Unk, Unsat),
  )
import Grisette.Internal.SymPrim.Prim.Internal.IsZero (KnownIsZero)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalApplyTerm (sbvApplyTerm),
    PEvalBVSignConversionTerm (sbvToSigned, sbvToUnsigned),
    PEvalBVTerm (sbvBVConcatTerm, sbvBVExtendTerm, sbvBVSelectTerm),
    PEvalBitwiseTerm
      ( sbvAndBitsTerm,
        sbvComplementBitsTerm,
        sbvOrBitsTerm,
        sbvXorBitsTerm
      ),
    PEvalDivModIntegralTerm
      ( sbvDivIntegralTerm,
        sbvModIntegralTerm,
        sbvQuotIntegralTerm,
        sbvRemIntegralTerm
      ),
    PEvalNumTerm
      ( sbvAbsNumTerm,
        sbvAddNumTerm,
        sbvMulNumTerm,
        sbvNegNumTerm,
        sbvSignumNumTerm
      ),
    PEvalOrdTerm (sbvLeOrdTerm, sbvLtOrdTerm),
    PEvalRotateTerm (sbvRotateLeftTerm, sbvRotateRightTerm),
    PEvalShiftTerm (sbvShiftLeftTerm, sbvShiftRightTerm),
    SBVFreshMonad,
    SBVRep (SBVType),
    SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim
      ( conSBVTerm,
        parseSMTModelResult,
        sbvEq,
        sbvIte,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        ComplementBitsTerm,
        ConTerm,
        DivIntegralTerm,
        EqTerm,
        ITETerm,
        LeOrdTerm,
        LtOrdTerm,
        ModIntegralTerm,
        MulNumTerm,
        NegNumTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotIntegralTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        ToSignedTerm,
        ToUnsignedTerm,
        XorBitsTerm
      ),
    introSupportedPrimConstraint,
    someTypedSymbol,
    withSymbolSupported,
  )
import Grisette.Internal.SymPrim.Prim.Model as PM
  ( Model,
  )
import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))

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

-- | Configures how to approximate unbounded values.
--
-- For example, if we use @'Approx' ('Data.Proxy' :: 'Data.Proxy' 4)@ to
-- approximate the following unbounded integer:
--
-- > (+ a 9)
--
-- We will get
--
-- > (bvadd a #x9)
--
-- Here the value 9 will be approximated to a 4-bit bit vector, and the
-- operation `bvadd` will be used instead of `+`.
--
-- Note that this approximation may not be sound. See 'GrisetteSMTConfig' for
-- more details.
data ApproximationConfig (n :: Nat) where
  NoApprox :: ApproximationConfig 0
  Approx ::
    (KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>
    p n ->
    ApproximationConfig n

-- | Grisette specific extra configurations for the SBV backend.
data ExtraConfig (i :: Nat) = ExtraConfig
  { -- | Timeout in milliseconds for each solver call. CEGIS may call the
    -- solver multiple times and each call has its own timeout.
    forall (i :: Nat). ExtraConfig i -> Maybe Int
timeout :: Maybe Int,
    -- | Configures how to approximate unbounded integer values.
    forall (i :: Nat). ExtraConfig i -> ApproximationConfig i
integerApprox :: ApproximationConfig i
  }

preciseExtraConfig :: ExtraConfig 0
preciseExtraConfig :: ExtraConfig 0
preciseExtraConfig =
  ExtraConfig
    { timeout :: Maybe Int
timeout = Maybe Int
forall a. Maybe a
Nothing,
      integerApprox :: ApproximationConfig 0
integerApprox = ApproximationConfig 0
NoApprox
    }

approximateExtraConfig ::
  (KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>
  p n ->
  ExtraConfig n
approximateExtraConfig :: forall (n :: Nat) (p :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownIsZero n) =>
p n -> ExtraConfig n
approximateExtraConfig p n
p =
  ExtraConfig
    { timeout :: Maybe Int
timeout = Maybe Int
forall a. Maybe a
Nothing,
      integerApprox :: ApproximationConfig n
integerApprox = p n -> ApproximationConfig n
forall (n :: Nat) (p :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownIsZero n) =>
p n -> ApproximationConfig n
Approx p n
p
    }

-- | Solver configuration for the Grisette SBV backend.
-- A Grisette solver configuration consists of a SBV solver configuration and
-- the reasoning precision.
--
-- Integers can be unbounded (mathematical integer) or bounded (machine
-- integer/bit vector). The two types of integers have their own use cases,
-- and should be used to model different systems.
-- However, the solvers are known to have bad performance on some unbounded
-- integer operations, for example, when reason about non-linear integer
-- algebraic (e.g., multiplication or division),
-- the solver may not be able to get a result in a reasonable time.
-- In contrast, reasoning about bounded integers is usually more efficient.
--
-- To bridge the performance gap between the two types of integers, Grisette
-- allows to model the system with unbounded integers, and evaluate them with
-- infinite precision during the symbolic evaluation, but when solving the
-- queries, they are translated to bit vectors for better performance.
--
-- For example, the Grisette term @5 * "a" :: 'SymInteger'@ should be translated
-- to the following SMT with the unbounded reasoning configuration (the term
-- is @t1@):
--
-- > (declare-fun a () Int)           ; declare symbolic constant a
-- > (define-fun c1 () Int 5)         ; define the concrete value 5
-- > (define-fun t1 () Int (* c1 a))  ; define the term
--
-- While with reasoning precision 4, it would be translated to the following
-- SMT (the term is @t1@):
--
-- > ; declare symbolic constant a, the type is a bit vector with bit width 4
-- > (declare-fun a () (_ BitVec 4))
-- > ; define the concrete value 1, translated to the bit vector #x1
-- > (define-fun c1 () (_ BitVec 4) #x5)
-- > ; define the term, using bit vector addition rather than integer addition
-- > (define-fun t1 () (_ BitVec 4) (bvmul c1 a))
--
-- This bounded translation can usually be solved faster than the unbounded
-- one, and should work well when no overflow is possible, in which case the
-- performance can be improved with almost no cost.
--
-- We must note that the bounded translation is an approximation and is
-- __/not sound/__. As the approximation happens only during the final
-- translation, the symbolic evaluation may aggressively optimize the term based
-- on the properties of mathematical integer arithmetic. This may cause the
-- solver yield results that is incorrect under both unbounded or bounded
-- semantics.
--
-- The following is an example that is correct under bounded semantics, while is
-- incorrect under the unbounded semantics:
--
-- >>> :set -XTypeApplications -XOverloadedStrings -XDataKinds
-- >>> let a = "a" :: SymInteger
-- >>> solve (precise z3) $ a .> 7 .&& a .< 9
-- Right (Model {a -> 8 :: Integer})
-- >>> solve (approx (Proxy @4) z3) $ a .> 7 .&& a .< 9
-- Left Unsat
--
-- This may be avoided by setting an large enough reasoning precision to prevent
-- overflows.
data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig
  { forall (i :: Nat). GrisetteSMTConfig i -> SMTConfig
sbvConfig :: SBV.SMTConfig,
    forall (i :: Nat). GrisetteSMTConfig i -> ExtraConfig i
extraConfig :: ExtraConfig i
  }

-- | A precise reasoning configuration with the given SBV solver configuration.
precise :: SBV.SMTConfig -> GrisetteSMTConfig 0
precise :: SMTConfig -> GrisetteSMTConfig 0
precise SMTConfig
config = SMTConfig -> ExtraConfig 0 -> GrisetteSMTConfig 0
forall (i :: Nat).
SMTConfig -> ExtraConfig i -> GrisetteSMTConfig i
GrisetteSMTConfig SMTConfig
config ExtraConfig 0
preciseExtraConfig

-- | An approximate reasoning configuration with the given SBV solver
-- configuration.
approx ::
  forall p n.
  (KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>
  p n ->
  SBV.SMTConfig ->
  GrisetteSMTConfig n
approx :: forall (p :: Nat -> *) (n :: Nat).
(KnownNat n, BVIsNonZero n, KnownIsZero n) =>
p n -> SMTConfig -> GrisetteSMTConfig n
approx p n
p SMTConfig
config = SMTConfig -> ExtraConfig n -> GrisetteSMTConfig n
forall (i :: Nat).
SMTConfig -> ExtraConfig i -> GrisetteSMTConfig i
GrisetteSMTConfig SMTConfig
config (p n -> ExtraConfig n
forall (n :: Nat) (p :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownIsZero n) =>
p n -> ExtraConfig n
approximateExtraConfig p n
p)

-- | Set the timeout for the solver configuration.
withTimeout :: Int -> GrisetteSMTConfig i -> GrisetteSMTConfig i
withTimeout :: forall (i :: Nat).
Int -> GrisetteSMTConfig i -> GrisetteSMTConfig i
withTimeout Int
t GrisetteSMTConfig i
config =
  GrisetteSMTConfig i
config {extraConfig = (extraConfig config) {timeout = Just t}}

-- | Clear the timeout for the solver configuration.
clearTimeout :: GrisetteSMTConfig i -> GrisetteSMTConfig i
clearTimeout :: forall (i :: Nat). GrisetteSMTConfig i -> GrisetteSMTConfig i
clearTimeout GrisetteSMTConfig i
config =
  GrisetteSMTConfig i
config {extraConfig = (extraConfig config) {timeout = Nothing}}

-- | Set the reasoning precision for the solver configuration.
withApprox ::
  (KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>
  p n ->
  GrisetteSMTConfig i ->
  GrisetteSMTConfig n
withApprox :: forall (n :: Nat) (p :: Nat -> *) (i :: Nat).
(KnownNat n, BVIsNonZero n, KnownIsZero n) =>
p n -> GrisetteSMTConfig i -> GrisetteSMTConfig n
withApprox p n
p GrisetteSMTConfig i
config =
  GrisetteSMTConfig i
config {extraConfig = (extraConfig config) {integerApprox = Approx p}}

-- | Clear the reasoning precision and perform precise reasoning with the
-- solver configuration.
clearApprox :: GrisetteSMTConfig i -> GrisetteSMTConfig 0
clearApprox :: forall (i :: Nat). GrisetteSMTConfig i -> GrisetteSMTConfig 0
clearApprox GrisetteSMTConfig i
config =
  GrisetteSMTConfig i
config {extraConfig = (extraConfig config) {integerApprox = NoApprox}}

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 i -> m a -> m a
applyTimeout :: forall (m :: * -> *) (i :: Nat) a.
(MonadIO m, MonadQuery m) =>
GrisetteSMTConfig i -> m a -> m a
applyTimeout GrisetteSMTConfig i
config m a
q = case ExtraConfig i -> Maybe Int
forall (i :: Nat). ExtraConfig i -> Maybe Int
timeout (GrisetteSMTConfig i -> ExtraConfig i
forall (i :: Nat). GrisetteSMTConfig i -> ExtraConfig i
extraConfig GrisetteSMTConfig i
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 n m =
  ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (SBVTC.QueryT m))

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

-- | Run the incremental solver monad with a given configuration.
runSBVIncremental :: GrisetteSMTConfig n -> SBVIncremental n a -> IO a
runSBVIncremental :: forall (n :: Nat) a.
GrisetteSMTConfig n -> SBVIncremental n a -> IO a
runSBVIncremental = GrisetteSMTConfig n -> SBVIncrementalT n IO a -> IO a
forall (m :: * -> *) (n :: Nat) a.
ExtractIO m =>
GrisetteSMTConfig n -> SBVIncrementalT n m a -> m a
runSBVIncrementalT

-- | Run the incremental solver monad transformer with a given configuration.
runSBVIncrementalT ::
  (SBVTC.ExtractIO m) =>
  GrisetteSMTConfig n ->
  SBVIncrementalT n m a ->
  m a
runSBVIncrementalT :: forall (m :: * -> *) (n :: Nat) a.
ExtractIO m =>
GrisetteSMTConfig n -> SBVIncrementalT n m a -> m a
runSBVIncrementalT GrisetteSMTConfig n
config SBVIncrementalT n m a
sbvIncrementalT =
  SMTConfig -> SymbolicT m a -> m a
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
SBVT.runSMTWith (GrisetteSMTConfig n -> SMTConfig
forall (i :: Nat). GrisetteSMTConfig i -> SMTConfig
sbvConfig GrisetteSMTConfig n
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 n -> QueryT m a -> QueryT m a
forall (m :: * -> *) (i :: Nat) a.
(MonadIO m, MonadQuery m) =>
GrisetteSMTConfig i -> m a -> m a
applyTimeout GrisetteSMTConfig n
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 n m a
-> GrisetteSMTConfig n -> StateT SymBiMap (QueryT m) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT SBVIncrementalT n m a
sbvIncrementalT GrisetteSMTConfig n
config

instance (MonadIO m) => MonadicSolver (SBVIncrementalT n m) where
  monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model)
monadicSolverSolve (SymBool Term Bool
formula) = do
    SymBiMap
symBiMap <- ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT m)) SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
    GrisetteSMTConfig n
config <- ReaderT
  (GrisetteSMTConfig n)
  (StateT SymBiMap (QueryT m))
  (GrisetteSMTConfig n)
forall r (m :: * -> *). MonadReader r m => m r
ask
    (SymBiMap
newSymBiMap, SBV Bool
lowered) <- GrisetteSMTConfig n
-> Term Bool
-> SymBiMap
-> ReaderT
     (GrisetteSMTConfig n)
     (StateT SymBiMap (QueryT m))
     (SymBiMap, SBVType n Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig n
config Term Bool
formula SymBiMap
symBiMap
    StateT SymBiMap (QueryT m) () -> SBVIncrementalT n m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT (GrisetteSMTConfig n) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT SymBiMap (QueryT m) () -> SBVIncrementalT n m ())
-> StateT SymBiMap (QueryT m) () -> SBVIncrementalT n m ()
forall a b. (a -> b) -> a -> b
$ QueryT m () -> StateT SymBiMap (QueryT m) ()
forall (m :: * -> *) a. Monad m => m a -> StateT SymBiMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QueryT m () -> StateT SymBiMap (QueryT m) ())
-> QueryT m () -> StateT SymBiMap (QueryT m) ()
forall a b. (a -> b) -> a -> b
$ SBV Bool -> QueryT m ()
forall a. QuantifiedBool a => a -> QueryT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
SBV.constrain SBV Bool
lowered
    SymBiMap -> SBVIncrementalT n m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SymBiMap
newSymBiMap
    CheckSatResult
checkSatResult <- ReaderT
  (GrisetteSMTConfig n) (StateT SymBiMap (QueryT m)) CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
SBVTC.checkSat
    case CheckSatResult
checkSatResult of
      CheckSatResult
SBVC.Sat -> do
        SMTModel
sbvModel <- ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT m)) SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
SBVTC.getModel
        let model :: Model
model = GrisetteSMTConfig n -> SMTModel -> SymBiMap -> Model
forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig n
config SMTModel
sbvModel SymBiMap
newSymBiMap
        Either SolvingFailure Model
-> SBVIncrementalT n m (Either SolvingFailure Model)
forall a.
a -> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure Model
 -> SBVIncrementalT n m (Either SolvingFailure Model))
-> Either SolvingFailure Model
-> SBVIncrementalT n m (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ Model -> Either SolvingFailure Model
forall a b. b -> Either a b
Right Model
model
      CheckSatResult
r -> Either SolvingFailure Model
-> SBVIncrementalT n m (Either SolvingFailure Model)
forall a.
a -> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure Model
 -> SBVIncrementalT n m (Either SolvingFailure Model))
-> Either SolvingFailure Model
-> SBVIncrementalT n 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
  monadicSolverPush :: Int -> SBVIncrementalT n m ()
monadicSolverPush = Int -> SBVIncrementalT n m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
SBVTC.push
  monadicSolverPop :: Int -> SBVIncrementalT n m ()
monadicSolverPop = Int -> SBVIncrementalT n m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
SBVTC.pop

data SBVSolverStatus = SBVSolverNormal | SBVSolverTerminated

-- | The handle type for the SBV solver.
--
-- See 'ConfigurableSolver' and 'Solver' for the interfaces.
data SBVSolverHandle = SBVSolverHandle
  { SBVSolverHandle -> Async ()
sbvSolverHandleMonad :: Async (),
    SBVSolverHandle -> TMVar SBVSolverStatus
sbvSolverHandleStatus :: TMVar SBVSolverStatus,
    SBVSolverHandle -> TChan SolverCommand
sbvSolverHandleInChan :: TChan SolverCommand,
    SBVSolverHandle -> TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
  }

setTerminated :: TMVar SBVSolverStatus -> STM ()
setTerminated :: TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status = do
  Maybe SBVSolverStatus
_ <- TMVar SBVSolverStatus -> STM (Maybe SBVSolverStatus)
forall a. TMVar a -> STM (Maybe a)
tryTakeTMVar TMVar SBVSolverStatus
status
  TMVar SBVSolverStatus -> SBVSolverStatus -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar SBVSolverStatus
status SBVSolverStatus
SBVSolverTerminated

instance ConfigurableSolver (GrisetteSMTConfig n) SBVSolverHandle where
  newSolver :: GrisetteSMTConfig n -> IO SBVSolverHandle
newSolver GrisetteSMTConfig n
config = do
    TChan SolverCommand
sbvSolverHandleInChan <- STM (TChan SolverCommand) -> IO (TChan SolverCommand)
forall a. STM a -> IO a
atomically STM (TChan SolverCommand)
forall a. STM (TChan a)
newTChan
    TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan <- STM (TChan (Either SolvingFailure Model))
-> IO (TChan (Either SolvingFailure Model))
forall a. STM a -> IO a
atomically STM (TChan (Either SolvingFailure Model))
forall a. STM (TChan a)
newTChan
    TMVar SBVSolverStatus
sbvSolverHandleStatus <- SBVSolverStatus -> IO (TMVar SBVSolverStatus)
forall a. a -> IO (TMVar a)
newTMVarIO SBVSolverStatus
SBVSolverNormal
    Async ()
sbvSolverHandleMonad <- IO () -> IO (Async ())
forall a. IO a -> IO (Async a)
async (IO () -> IO (Async ())) -> IO () -> IO (Async ())
forall a b. (a -> b) -> a -> b
$ do
      let handler :: SomeException -> IO ()
handler SomeException
e =
            IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
              STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
sbvSolverHandleStatus
                TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan (SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left (SomeException -> SolvingFailure
SolvingError SomeException
e))
      (SomeException -> IO ()) -> IO () -> IO ()
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle SomeException -> IO ()
handler (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GrisetteSMTConfig n -> SBVIncremental n () -> IO ()
forall (n :: Nat) a.
GrisetteSMTConfig n -> SBVIncremental n a -> IO a
runSBVIncremental GrisetteSMTConfig n
config (SBVIncremental n () -> IO ()) -> SBVIncremental n () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        let loop :: SBVIncremental n ()
loop = do
              SolverCommand
nextFormula <- IO SolverCommand
-> ReaderT
     (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) SolverCommand
forall a.
IO a
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SolverCommand
 -> ReaderT
      (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) SolverCommand)
-> IO SolverCommand
-> ReaderT
     (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) SolverCommand
forall a b. (a -> b) -> a -> b
$ STM SolverCommand -> IO SolverCommand
forall a. STM a -> IO a
atomically (STM SolverCommand -> IO SolverCommand)
-> STM SolverCommand -> IO SolverCommand
forall a b. (a -> b) -> a -> b
$ TChan SolverCommand -> STM SolverCommand
forall a. TChan a -> STM a
readTChan TChan SolverCommand
sbvSolverHandleInChan
              case SolverCommand
nextFormula of
                SolverPush Int
n -> Int -> SBVIncremental n ()
forall (m :: * -> *). MonadicSolver m => Int -> m ()
monadicSolverPush Int
n SBVIncremental n () -> SBVIncremental n () -> SBVIncremental n ()
forall a b.
ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) a
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) b
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBVIncremental n ()
loop
                SolverPop Int
n -> Int -> SBVIncremental n ()
forall (m :: * -> *). MonadicSolver m => Int -> m ()
monadicSolverPop Int
n SBVIncremental n () -> SBVIncremental n () -> SBVIncremental n ()
forall a b.
ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) a
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) b
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBVIncremental n ()
loop
                SolverCommand
SolverTerminate -> () -> SBVIncremental n ()
forall a.
a -> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                SolverSolve SymBool
formula -> do
                  Either SolvingFailure Model
r <- SymBool
-> ReaderT
     (GrisetteSMTConfig n)
     (StateT SymBiMap (QueryT IO))
     (Either SolvingFailure Model)
forall (m :: * -> *).
MonadicSolver m =>
SymBool -> m (Either SolvingFailure Model)
monadicSolverSolve SymBool
formula
                  IO () -> SBVIncremental n ()
forall a.
IO a
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SBVIncremental n ()) -> IO () -> SBVIncremental n ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan Either SolvingFailure Model
r
                  SBVIncremental n ()
loop
        SBVIncremental n ()
loop
        IO () -> SBVIncremental n ()
forall a.
IO a
-> ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SBVIncremental n ()) -> IO () -> SBVIncremental n ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
sbvSolverHandleStatus
          TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
sbvSolverHandleOutChan (Either SolvingFailure Model -> STM ())
-> Either SolvingFailure Model -> STM ()
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left SolvingFailure
Terminated
    SBVSolverHandle -> IO SBVSolverHandle
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBVSolverHandle -> IO SBVSolverHandle)
-> SBVSolverHandle -> IO SBVSolverHandle
forall a b. (a -> b) -> a -> b
$ SBVSolverHandle {Async ()
TChan (Either SolvingFailure Model)
TChan SolverCommand
TMVar SBVSolverStatus
sbvSolverHandleMonad :: Async ()
sbvSolverHandleStatus :: TMVar SBVSolverStatus
sbvSolverHandleInChan :: TChan SolverCommand
sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
sbvSolverHandleInChan :: TChan SolverCommand
sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)
sbvSolverHandleStatus :: TMVar SBVSolverStatus
sbvSolverHandleMonad :: Async ()
..}

instance Solver SBVSolverHandle where
  solverRunCommand :: forall a.
(SBVSolverHandle -> IO (Either SolvingFailure a))
-> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand SBVSolverHandle -> IO (Either SolvingFailure a)
f handle :: SBVSolverHandle
handle@(SBVSolverHandle Async ()
_ TMVar SBVSolverStatus
status TChan SolverCommand
inChan TChan (Either SolvingFailure Model)
_) SolverCommand
command = do
    SBVSolverStatus
st <- IO SBVSolverStatus -> IO SBVSolverStatus
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVSolverStatus -> IO SBVSolverStatus)
-> IO SBVSolverStatus -> IO SBVSolverStatus
forall a b. (a -> b) -> a -> b
$ STM SBVSolverStatus -> IO SBVSolverStatus
forall a. STM a -> IO a
atomically (STM SBVSolverStatus -> IO SBVSolverStatus)
-> STM SBVSolverStatus -> IO SBVSolverStatus
forall a b. (a -> b) -> a -> b
$ TMVar SBVSolverStatus -> STM SBVSolverStatus
forall a. TMVar a -> STM a
takeTMVar TMVar SBVSolverStatus
status
    case SBVSolverStatus
st of
      SBVSolverStatus
SBVSolverNormal -> do
        IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan SolverCommand -> SolverCommand -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan SolverCommand
inChan SolverCommand
command
        Either SolvingFailure a
r <- SBVSolverHandle -> IO (Either SolvingFailure a)
f SBVSolverHandle
handle
        IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Maybe SBVSolverStatus
currStatus <- TMVar SBVSolverStatus -> STM (Maybe SBVSolverStatus)
forall a. TMVar a -> STM (Maybe a)
tryReadTMVar TMVar SBVSolverStatus
status
          case Maybe SBVSolverStatus
currStatus of
            Maybe SBVSolverStatus
Nothing -> TMVar SBVSolverStatus -> SBVSolverStatus -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar SBVSolverStatus
status SBVSolverStatus
SBVSolverNormal
            Just SBVSolverStatus
_ -> () -> STM ()
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Either SolvingFailure a
r
      SBVSolverStatus
SBVSolverTerminated -> do
        IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
        Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure a -> IO (Either SolvingFailure a))
-> Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> Either SolvingFailure a
forall a b. a -> Either a b
Left SolvingFailure
Terminated
  solverSolve :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve SBVSolverHandle
handle SymBool
nextFormula =
    (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 -> IO (Either SolvingFailure Model))
-> SolverCommand -> IO (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ SymBool -> SolverCommand
SolverSolve SymBool
nextFormula
  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

configIntroKnownIsZero :: GrisetteSMTConfig n -> ((KnownIsZero n) => r) -> r
configIntroKnownIsZero :: forall (n :: Nat) r.
GrisetteSMTConfig n -> (KnownIsZero n => r) -> r
configIntroKnownIsZero (GrisetteSMTConfig SMTConfig
_ (ExtraConfig Maybe Int
_ (Approx p n
_))) KnownIsZero n => r
r = r
KnownIsZero n => r
r
configIntroKnownIsZero (GrisetteSMTConfig SMTConfig
_ (ExtraConfig Maybe Int
_ ApproximationConfig n
NoApprox)) KnownIsZero n => r
r = r
KnownIsZero n => r
r

lowerSinglePrimCached ::
  forall integerBitWidth a m.
  (HasCallStack, SBVFreshMonad m) =>
  GrisetteSMTConfig integerBitWidth ->
  Term a ->
  SymBiMap ->
  m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached :: forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m =
  Term a
-> (SupportedPrim a => m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a => m (SymBiMap, SBVType integerBitWidth a))
 -> m (SymBiMap, SBVType integerBitWidth a))
-> (SupportedPrim a => m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall a b. (a -> b) -> a -> b
$
    GrisetteSMTConfig integerBitWidth
-> (KnownIsZero integerBitWidth =>
    m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall (n :: Nat) r.
GrisetteSMTConfig n -> (KnownIsZero n => r) -> r
configIntroKnownIsZero GrisetteSMTConfig integerBitWidth
config ((KnownIsZero integerBitWidth =>
  m (SymBiMap, SBVType integerBitWidth a))
 -> m (SymBiMap, SBVType integerBitWidth a))
-> (KnownIsZero integerBitWidth =>
    m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall a b. (a -> b) -> a -> b
$
      case HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) SymBiMap
m of
        Just Dynamic
x ->
          (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
            ( SymBiMap
m,
              forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @a (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @integerBitWidth) (((PrimConstraint integerBitWidth a,
   SMTDefinable (SBVType integerBitWidth a),
   Mergeable (SBVType integerBitWidth a),
   Typeable (SBVType integerBitWidth a)) =>
  SBVType integerBitWidth a)
 -> SBVType integerBitWidth a)
-> ((PrimConstraint integerBitWidth a,
     SMTDefinable (SBVType integerBitWidth a),
     Mergeable (SBVType integerBitWidth a),
     Typeable (SBVType integerBitWidth a)) =>
    SBVType integerBitWidth a)
-> SBVType integerBitWidth a
forall a b. (a -> b) -> a -> b
$ Dynamic -> SBVType integerBitWidth a -> SBVType integerBitWidth a
forall a. Typeable a => Dynamic -> a -> a
fromDyn Dynamic
x SBVType integerBitWidth a
forall a. HasCallStack => a
undefined
            )
        Maybe Dynamic
Nothing -> GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m

lowerSinglePrim ::
  forall integerBitWidth a m.
  (HasCallStack, SBVFreshMonad m) =>
  GrisetteSMTConfig integerBitWidth ->
  Term a ->
  m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrim :: forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrim GrisetteSMTConfig integerBitWidth
config Term a
t = GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
emptySymBiMap

lowerSinglePrimImpl ::
  forall integerBitWidth a m.
  (HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>
  GrisetteSMTConfig integerBitWidth ->
  Term a ->
  SymBiMap ->
  m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimImpl :: forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config (ConTerm Int
_ a
v) SymBiMap
m =
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m, GrisetteSMTConfig integerBitWidth -> a -> SBVType integerBitWidth a
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> a -> SBVType n a
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm GrisetteSMTConfig integerBitWidth
config a
v)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config t :: Term a
t@(SymTerm Int
_ TypedSymbol a
ts) SymBiMap
m =
  forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @a GrisetteSMTConfig integerBitWidth
config (((PrimConstraint integerBitWidth a,
   SMTDefinable (SBVType integerBitWidth a),
   Mergeable (SBVType integerBitWidth a),
   Typeable (SBVType integerBitWidth a)) =>
  m (SymBiMap, SBVType integerBitWidth a))
 -> m (SymBiMap, SBVType integerBitWidth a))
-> ((PrimConstraint integerBitWidth a,
     SMTDefinable (SBVType integerBitWidth a),
     Mergeable (SBVType integerBitWidth a),
     Typeable (SBVType integerBitWidth a)) =>
    m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall a b. (a -> b) -> a -> b
$ do
    let name :: [Char]
name = TypedSymbol a -> Int -> [Char]
forall t. SupportedPrim t => TypedSymbol t -> Int -> [Char]
symSBVName TypedSymbol a
ts (SymBiMap -> Int
sizeBiMap SymBiMap
m)
    SBVType integerBitWidth a
g <- forall t (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, SBVFreshMonad m, KnownIsZero n) =>
proxy n -> [Char] -> m (SBVType n t)
symSBVTerm @a GrisetteSMTConfig integerBitWidth
config [Char]
name
    (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack =>
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
SomeTerm
-> Dynamic -> [Char] -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBVType integerBitWidth a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBVType integerBitWidth a
g) [Char]
name (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts) SymBiMap
m, SBVType integerBitWidth a
g)
lowerSinglePrimImpl GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m =
  Term a
-> (SupportedPrim a => m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a => m (SymBiMap, SBVType integerBitWidth a))
 -> m (SymBiMap, SBVType integerBitWidth a))
-> (SupportedPrim a => m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall a b. (a -> b) -> a -> b
$
    forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @a GrisetteSMTConfig integerBitWidth
config (((PrimConstraint integerBitWidth a,
   SMTDefinable (SBVType integerBitWidth a),
   Mergeable (SBVType integerBitWidth a),
   Typeable (SBVType integerBitWidth a)) =>
  m (SymBiMap, SBVType integerBitWidth a))
 -> m (SymBiMap, SBVType integerBitWidth a))
-> ((PrimConstraint integerBitWidth a,
     SMTDefinable (SBVType integerBitWidth a),
     Mergeable (SBVType integerBitWidth a),
     Typeable (SBVType integerBitWidth a)) =>
    m (SymBiMap, SBVType integerBitWidth a))
-> m (SymBiMap, SBVType integerBitWidth a)
forall a b. (a -> b) -> a -> b
$ do
      (SymBiMap
m, SBVType integerBitWidth a
r) <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config Term a
t SymBiMap
m
      (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t) (SBVType integerBitWidth a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn SBVType integerBitWidth a
r) SymBiMap
m, SBVType integerBitWidth a
r)

lowerSinglePrimIntermediate ::
  forall integerBitWidth a m.
  (HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>
  GrisetteSMTConfig integerBitWidth ->
  Term a ->
  SymBiMap ->
  m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimIntermediate :: forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m, KnownIsZero integerBitWidth) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (NotTerm Int
_ Term Bool
a) SymBiMap
m = do
  (SymBiMap
m1, SBV Bool
a') <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
a SymBiMap
m
  (SymBiMap, SBV Bool) -> m (SymBiMap, SBV Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, SBV Bool -> SBV Bool
SBV.sNot SBV Bool
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (OrTerm Int
_ Term Bool
a Term Bool
b) SymBiMap
m = do
  (SymBiMap
m1, SBV Bool
a') <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
a SymBiMap
m
  (SymBiMap
m2, SBV Bool
b') <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
b SymBiMap
m1
  (SymBiMap, SBV Bool) -> m (SymBiMap, SBV Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, SBV Bool
a' SBV Bool -> SBV Bool -> SBV Bool
SBV..|| SBV Bool
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (AndTerm Int
_ Term Bool
a Term Bool
b) SymBiMap
m = do
  (SymBiMap
m1, SBV Bool
a') <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
a SymBiMap
m
  (SymBiMap
m2, SBV Bool
b') <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
b SymBiMap
m1
  (SymBiMap, SBV Bool) -> m (SymBiMap, SBV Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, SBV Bool
a' SBV Bool -> SBV Bool -> SBV Bool
SBV..&& SBV Bool
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (EqTerm Int
_ (Term t1
a :: Term v) Term t1
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth t1
a') <- GrisetteSMTConfig integerBitWidth
-> Term t1 -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth t1)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term t1
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth t1
b') <- GrisetteSMTConfig integerBitWidth
-> Term t1 -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth t1)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term t1
b SymBiMap
m1
  (SymBiMap, SBV Bool) -> m (SymBiMap, SBV Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBV Bool
sbvEq @v GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth t1
a' SBVType integerBitWidth t1
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ITETerm Int
_ Term Bool
c Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBV Bool
c') <- GrisetteSMTConfig integerBitWidth
-> Term Bool
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term Bool
c SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m1
  (SymBiMap
m3, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m2
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m3, forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> SBV Bool -> SBVType n t -> SBVType n t -> SBVType n t
sbvIte @a GrisetteSMTConfig integerBitWidth
config SBV Bool
c' SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (AddNumTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalNumTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvAddNumTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (NegNumTerm Int
_ Term a
a) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalNumTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t
sbvNegNumTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (MulNumTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalNumTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvMulNumTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (AbsNumTerm Int
_ Term a
a) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalNumTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t
sbvAbsNumTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (SignumNumTerm Int
_ Term a
a) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalNumTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t
sbvSignumNumTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (LtOrdTerm Int
_ (Term t1
a :: Term v) Term t1
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth t1
a') <- GrisetteSMTConfig integerBitWidth
-> Term t1 -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth t1)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term t1
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth t1
b') <- GrisetteSMTConfig integerBitWidth
-> Term t1 -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth t1)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term t1
b SymBiMap
m1
  (SymBiMap, SBV Bool) -> m (SymBiMap, SBV Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (n :: Nat) (proxy :: Nat -> *).
(PEvalOrdTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBV Bool
sbvLtOrdTerm @v GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth t1
a' SBVType integerBitWidth t1
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (LeOrdTerm Int
_ (Term t1
a :: Term v) Term t1
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth t1
a') <- GrisetteSMTConfig integerBitWidth
-> Term t1 -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth t1)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term t1
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth t1
b') <- GrisetteSMTConfig integerBitWidth
-> Term t1 -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth t1)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term t1
b SymBiMap
m1
  (SymBiMap, SBV Bool) -> m (SymBiMap, SBV Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (n :: Nat) (proxy :: Nat -> *).
(PEvalOrdTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBV Bool
sbvLeOrdTerm @v GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth t1
a' SBVType integerBitWidth t1
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (AndBitsTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (n :: Nat) (proxy :: Nat -> *).
(PEvalBitwiseTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvAndBitsTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (OrBitsTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (n :: Nat) (proxy :: Nat -> *).
(PEvalBitwiseTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvOrBitsTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (XorBitsTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (n :: Nat) (proxy :: Nat -> *).
(PEvalBitwiseTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvXorBitsTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ComplementBitsTerm Int
_ Term a
a) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, forall t (n :: Nat) (proxy :: Nat -> *).
(PEvalBitwiseTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t
sbvComplementBitsTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ShiftLeftTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalShiftTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvShiftLeftTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ShiftRightTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalShiftTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvShiftRightTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (RotateLeftTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalRotateTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvRotateLeftTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (RotateRightTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalRotateTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvRotateRightTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ApplyTerm Int
_ (Term f
f :: Term f) Term a
a) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth f
l1) <- GrisetteSMTConfig integerBitWidth
-> Term f -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth f)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term f
f SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
l2) <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall f a b (n :: Nat) (proxy :: Nat -> *).
(PEvalApplyTerm f a b, KnownIsZero n) =>
proxy n -> SBVType n f -> SBVType n a -> SBVType n b
sbvApplyTerm @f GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth f
l1 SBVType integerBitWidth a
l2)
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ToSignedTerm Int
_ (Term (u n)
a :: Term (u n))) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth (u n)
a') <- GrisetteSMTConfig integerBitWidth
-> Term (u n)
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth (u n))
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (u n)
a SymBiMap
m
  (SymBiMap, SBVType integerBitWidth (s n))
-> m (SymBiMap, SBVType integerBitWidth (s n))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, Proxy u
-> Proxy n
-> GrisetteSMTConfig integerBitWidth
-> SBVType integerBitWidth (u n)
-> SBVType integerBitWidth (s n)
forall (n :: Nat) (integerBitwidth :: Nat) (o :: (Nat -> *) -> *)
       (p :: Nat -> *) (q :: Nat -> *).
(KnownIsZero integerBitwidth, KnownNat n, 1 <= n) =>
o u
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (u n)
-> SBVType integerBitwidth (s n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat)
       (integerBitwidth :: Nat) (o :: (Nat -> *) -> *) (p :: Nat -> *)
       (q :: Nat -> *).
(PEvalBVSignConversionTerm u s, KnownIsZero integerBitwidth,
 KnownNat n, 1 <= n) =>
o u
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (u n)
-> SBVType integerBitwidth (s n)
sbvToSigned (forall {k} (t :: k). Proxy t
forall (t :: Nat -> *). Proxy t
Proxy @u) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth (u n)
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ToUnsignedTerm Int
_ (Term (s n)
a :: Term (s n))) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth (s n)
a') <- GrisetteSMTConfig integerBitWidth
-> Term (s n)
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth (s n))
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (s n)
a SymBiMap
m
  (SymBiMap, SBVType integerBitWidth (u n))
-> m (SymBiMap, SBVType integerBitWidth (u n))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, Proxy s
-> Proxy n
-> GrisetteSMTConfig integerBitWidth
-> SBVType integerBitWidth (s n)
-> SBVType integerBitWidth (u n)
forall (n :: Nat) (integerBitwidth :: Nat) (o :: (Nat -> *) -> *)
       (p :: Nat -> *) (q :: Nat -> *).
(KnownIsZero integerBitwidth, KnownNat n, 1 <= n) =>
o s
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (s n)
-> SBVType integerBitwidth (u n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat)
       (integerBitwidth :: Nat) (o :: (Nat -> *) -> *) (p :: Nat -> *)
       (q :: Nat -> *).
(PEvalBVSignConversionTerm u s, KnownIsZero integerBitwidth,
 KnownNat n, 1 <= n) =>
o s
-> p n
-> q integerBitwidth
-> SBVType integerBitwidth (s n)
-> SBVType integerBitwidth (u n)
sbvToUnsigned (forall {k} (t :: k). Proxy t
forall (t :: Nat -> *). Proxy t
Proxy @s) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth (s n)
a')
lowerSinglePrimIntermediate
  GrisetteSMTConfig integerBitWidth
config
  (BVConcatTerm Int
_ (Term (bv l)
a :: Term (bv l)) (Term (bv r)
b :: Term (bv r)))
  SymBiMap
m = do
    (SymBiMap
m1, SBVType integerBitWidth (bv l)
a') <- GrisetteSMTConfig integerBitWidth
-> Term (bv l)
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth (bv l))
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (bv l)
a SymBiMap
m
    (SymBiMap
m2, SBVType integerBitWidth (bv r)
b') <- GrisetteSMTConfig integerBitWidth
-> Term (bv r)
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth (bv r))
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (bv r)
b SymBiMap
m1
    (SymBiMap, SBVType integerBitWidth (bv (l + r)))
-> m (SymBiMap, SBVType integerBitWidth (bv (l + r)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall (bv :: Nat -> *) (n :: Nat) (l :: Nat) (r :: Nat)
       (p0 :: Nat -> *) (p1 :: Nat -> *) (p2 :: Nat -> *).
(PEvalBVTerm bv, KnownIsZero n, KnownNat l, KnownNat r, 1 <= l,
 1 <= r) =>
p0 n
-> p1 l
-> p2 r
-> SBVType n (bv l)
-> SBVType n (bv r)
-> SBVType n (bv (l + r))
sbvBVConcatTerm @bv GrisetteSMTConfig integerBitWidth
config (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) SBVType integerBitWidth (bv l)
a' SBVType integerBitWidth (bv r)
b')
lowerSinglePrimIntermediate
  GrisetteSMTConfig integerBitWidth
config
  (BVExtendTerm Int
_ Bool
signed (TypeRep r
pr :: p r) (Term (bv l)
a :: Term (bv l)))
  SymBiMap
m = do
    (SymBiMap
m1, SBVType integerBitWidth (bv l)
a') <- GrisetteSMTConfig integerBitWidth
-> Term (bv l)
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth (bv l))
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (bv l)
a SymBiMap
m
    (SymBiMap, SBVType integerBitWidth (bv r))
-> m (SymBiMap, SBVType integerBitWidth (bv r))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, forall (bv :: Nat -> *) (n :: Nat) (l :: Nat) (r :: Nat)
       (p0 :: Nat -> *) (p1 :: Nat -> *) (p2 :: Nat -> *).
(PEvalBVTerm bv, KnownIsZero n, KnownNat l, KnownNat r, 1 <= l,
 1 <= r, l <= r) =>
p0 n
-> p1 l -> p2 r -> Bool -> SBVType n (bv l) -> SBVType n (bv r)
sbvBVExtendTerm @bv GrisetteSMTConfig integerBitWidth
config (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) TypeRep r
pr Bool
signed SBVType integerBitWidth (bv l)
a')
lowerSinglePrimIntermediate
  GrisetteSMTConfig integerBitWidth
config
  (BVSelectTerm Int
_ (TypeRep ix
pix :: p ix) (TypeRep w
pw :: q w) (Term (bv n)
a :: Term (bv n)))
  SymBiMap
m = do
    (SymBiMap
m1, SBVType integerBitWidth (bv n)
a') <- GrisetteSMTConfig integerBitWidth
-> Term (bv n)
-> SymBiMap
-> m (SymBiMap, SBVType integerBitWidth (bv n))
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term (bv n)
a SymBiMap
m
    (SymBiMap, SBVType integerBitWidth (bv w))
-> m (SymBiMap, SBVType integerBitWidth (bv w))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m1, forall (bv :: Nat -> *) (int :: Nat) (ix :: Nat) (w :: Nat)
       (n :: Nat) (p0 :: Nat -> *) (p1 :: Nat -> *) (p2 :: Nat -> *)
       (p3 :: Nat -> *).
(PEvalBVTerm bv, KnownIsZero int, KnownNat ix, KnownNat w,
 KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) =>
p0 int
-> p1 ix
-> p2 w
-> p3 n
-> SBVType int (bv n)
-> SBVType int (bv w)
sbvBVSelectTerm @bv GrisetteSMTConfig integerBitWidth
config TypeRep ix
pix TypeRep w
pw (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) SBVType integerBitWidth (bv n)
a')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (DivIntegralTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalDivModIntegralTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvDivIntegralTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (ModIntegralTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalDivModIntegralTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvModIntegralTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (QuotIntegralTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalDivModIntegralTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvQuotIntegralTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
config (RemIntegralTerm Int
_ Term a
a Term a
b) SymBiMap
m = do
  (SymBiMap
m1, SBVType integerBitWidth a
a') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
a SymBiMap
m
  (SymBiMap
m2, SBVType integerBitWidth a
b') <- GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, SBVType integerBitWidth a)
lowerSinglePrimCached GrisetteSMTConfig integerBitWidth
config Term a
b SymBiMap
m1
  (SymBiMap, SBVType integerBitWidth a)
-> m (SymBiMap, SBVType integerBitWidth a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymBiMap
m2, forall t (proxy :: Nat -> *) (n :: Nat).
(PEvalDivModIntegralTerm t, KnownIsZero n) =>
proxy n -> SBVType n t -> SBVType n t -> SBVType n t
sbvRemIntegralTerm @a GrisetteSMTConfig integerBitWidth
config SBVType integerBitWidth a
a' SBVType integerBitWidth a
b')
lowerSinglePrimIntermediate GrisetteSMTConfig integerBitWidth
_ Term a
_ SymBiMap
_ = m (SymBiMap, SBVType integerBitWidth a)
forall a. HasCallStack => a
undefined

#if MIN_VERSION_sbv(10,3,0)
preprocessUIFuncs ::
  [(String, (Bool, ty, Either String ([([SBVD.CV], SBVD.CV)], SBVD.CV)))] ->
  Maybe [(String, ([([SBVD.CV], SBVD.CV)], SBVD.CV))]
preprocessUIFuncs :: forall ty.
[([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))]
-> Maybe [([Char], ([([CV], CV)], CV))]
preprocessUIFuncs =
  (([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
 -> Maybe ([Char], ([([CV], CV)], CV)))
-> [([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))]
-> Maybe [([Char], ([([CV], CV)], CV))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
    (\([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
v -> case ([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
v of
      ([Char]
a, (Bool
_, ty
_, Right ([([CV], CV)], CV)
c)) -> ([Char], ([([CV], CV)], CV)) -> Maybe ([Char], ([([CV], CV)], CV))
forall a. a -> Maybe a
Just ([Char]
a, ([([CV], CV)], CV)
c)
      ([Char], (Bool, ty, Either [Char] ([([CV], CV)], CV)))
_ -> Maybe ([Char], ([([CV], CV)], CV))
forall a. Maybe a
Nothing)
#elif MIN_VERSION_sbv(10,0,0)
preprocessUIFuncs ::
  [(String, (ty, Either String ([([SBVD.CV], SBVD.CV)], SBVD.CV)))] ->
  Maybe [(String, ([([SBVD.CV], SBVD.CV)], SBVD.CV))]
preprocessUIFuncs =
  traverse
    (\v -> case v of
      (a, (_, Right c)) -> Just (a, c)
      _ -> Nothing)
#else
preprocessUIFuncs ::
  [(String, (ty, ([([SBVD.CV], SBVD.CV)], SBVD.CV)))] ->
  Maybe [(String, ([([SBVD.CV], SBVD.CV)], SBVD.CV))]
preprocessUIFuncs = Just . fmap (\(a, (_, c)) -> (a, c))
#endif

parseModel ::
  forall integerBitWidth.
  GrisetteSMTConfig integerBitWidth ->
  SBVI.SMTModel ->
  SymBiMap ->
  PM.Model
parseModel :: forall (integerBitWidth :: Nat).
GrisetteSMTConfig integerBitWidth -> SMTModel -> SymBiMap -> Model
parseModel GrisetteSMTConfig integerBitWidth
_ (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)], 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
findStringToSymbol [Char]
name SymBiMap
mp of
      Just (SomeTypedSymbol (TypeRep t
_ :: p r) TypedSymbol t
s) ->
        TypedSymbol t -> (SupportedPrim t => Model) -> Model
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
s ((SupportedPrim t => Model) -> Model)
-> (SupportedPrim t => Model) -> Model
forall a b. (a -> b) -> a -> b
$
          TypedSymbol t -> t -> Model -> Model
forall t. TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol 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
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."