{-# 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
(
ApproximationConfig (..),
ExtraConfig (..),
precise,
approx,
withTimeout,
clearTimeout,
withApprox,
clearApprox,
GrisetteSMTConfig (..),
SBVIncrementalT,
SBVIncremental,
runSBVIncrementalT,
runSBVIncremental,
SBVSolverHandle,
lowerSinglePrimCached,
lowerSinglePrim,
parseModel,
)
where
import Control.Concurrent.Async (Async (asyncThreadId), async, wait)
import Control.Concurrent.STM
( TMVar,
atomically,
newTMVarIO,
putTMVar,
takeTMVar,
tryReadTMVar,
tryTakeTMVar,
)
import Control.Concurrent.STM.TChan (TChan, newTChan, readTChan, writeTChan)
import Control.Exception (handle, throwTo)
import Control.Monad.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))
data ApproximationConfig (n :: Nat) where
NoApprox :: ApproximationConfig 0
Approx ::
(KnownNat n, SBV.BVIsNonZero n, KnownIsZero n) =>
p n ->
ApproximationConfig n
data (i :: Nat) =
{
forall (i :: Nat). ExtraConfig i -> Maybe Int
timeout :: Maybe Int,
forall (i :: Nat). ExtraConfig i -> ApproximationConfig i
integerApprox :: ApproximationConfig i
}
preciseExtraConfig :: ExtraConfig 0
=
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
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
}
data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig
{ forall (i :: Nat). GrisetteSMTConfig i -> SMTConfig
sbvConfig :: SBV.SMTConfig,
:: ExtraConfig i
}
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
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)
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}}
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}}
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}}
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
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
type SBVIncrementalT n m =
ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (SBVTC.QueryT m))
type SBVIncremental n = SBVIncrementalT n IO
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
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
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."