{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Backend.SBV.Data.SMT.Solving
(
TermTy,
ApproximationConfig (..),
ExtraConfig (..),
precise,
approx,
withTimeout,
clearTimeout,
withApprox,
clearApprox,
GrisetteSMTConfig (..),
SBVIncrementalT,
SBVIncremental,
runSBVIncrementalT,
runSBVIncremental,
SBVSolverHandle,
)
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.Kind (Type)
import qualified Data.SBV as SBV
import qualified Data.SBV.Control as SBVC
import qualified Data.SBV.Trans as SBVT
import qualified Data.SBV.Trans.Control as SBVTC
import GHC.IO.Exception (ExitCode (ExitSuccess))
import GHC.TypeNats (KnownNat, Nat)
import Grisette.Backend.SBV.Data.SMT.Lowering
( SymBiMap,
lowerSinglePrimCached,
parseModel,
)
import Grisette.Backend.SBV.Data.SMT.SymBiMap (emptySymBiMap)
import Grisette.Core.Data.BV (IntN, WordN)
import Grisette.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.IR.SymPrim.Data.Prim.InternedTerm.Term
( type (-->),
)
import Grisette.IR.SymPrim.Data.Prim.Model as PM
( Model,
)
import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))
import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
type Aux :: Bool -> Nat -> Type
type family Aux o n where
Aux 'True _ = SBV.SInteger
Aux 'False n = SBV.SInt n
type IsZero :: Nat -> Bool
type family IsZero n where
IsZero 0 = 'True
IsZero _ = 'False
type TermTy :: Nat -> Type -> Type
type family TermTy bitWidth b where
TermTy _ Bool = SBV.SBool
TermTy n Integer = Aux (IsZero n) n
TermTy _ (IntN x) = SBV.SBV (SBV.IntN x)
TermTy _ (WordN x) = SBV.SBV (SBV.WordN x)
TermTy n (a =-> b) = TermTy n a -> TermTy n b
TermTy n (a --> b) = TermTy n a -> TermTy n b
TermTy _ v = v
data ApproximationConfig (n :: Nat) where
NoApprox :: ApproximationConfig 0
Approx ::
(KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero 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, IsZero n ~ 'False, SBV.BVIsNonZero 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, IsZero n ~ 'False, BVIsNonZero 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, IsZero n ~ 'False, SBV.BVIsNonZero n) =>
p n ->
SBV.SMTConfig ->
GrisetteSMTConfig n
approx :: forall (p :: Nat -> *) (n :: Nat).
(KnownNat n, IsZero n ~ 'False, BVIsNonZero 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, IsZero n ~ 'False, BVIsNonZero 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, IsZero n ~ 'False, SBV.BVIsNonZero n) =>
p n ->
GrisetteSMTConfig i ->
GrisetteSMTConfig n
withApprox :: forall (n :: Nat) (p :: Nat -> *) (i :: Nat).
(KnownNat n, IsZero n ~ 'False, BVIsNonZero 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, SBool
lowered) <- GrisetteSMTConfig n
-> Term Bool
-> SymBiMap
-> ReaderT
(GrisetteSMTConfig n)
(StateT SymBiMap (QueryT m))
(SymBiMap, TermTy n Bool)
forall (integerBitWidth :: Nat) a (m :: * -> *).
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth
-> Term a -> SymBiMap -> m (SymBiMap, TermTy 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
$ SBool -> QueryT m ()
forall a. QuantifiedBool a => a -> QueryT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
SBV.constrain SBool
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