{-# 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
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Backend.SBV.Data.SMT.Solving
  ( -- * Term type computation
    TermTy,

    -- * SBV backend configuration
    ApproximationConfig (..),
    ExtraConfig (..),
    precise,
    approx,
    withTimeout,
    clearTimeout,
    withApprox,
    clearApprox,
    GrisetteSMTConfig (..),

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

    -- * SBV solver handle
    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 (=->))

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

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

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

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

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

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

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

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

-- | An approximate reasoning configuration with the given SBV solver
-- configuration.
approx ::
  forall p n.
  (KnownNat n, 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)

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

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

-- | Set the reasoning precision for the solver configuration.
withApprox ::
  (KnownNat n, 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}}

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

sbvCheckSatResult :: SBVC.CheckSatResult -> SolvingFailure
sbvCheckSatResult :: CheckSatResult -> SolvingFailure
sbvCheckSatResult CheckSatResult
SBVC.Sat = [Char] -> SolvingFailure
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
sbvCheckSatResult (SBVC.DSat Maybe [Char]
_) = [Char] -> SolvingFailure
forall a. HasCallStack => [Char] -> a
error [Char]
"DSat is currently not supported"
sbvCheckSatResult CheckSatResult
SBVC.Unsat = SolvingFailure
Unsat
sbvCheckSatResult CheckSatResult
SBVC.Unk = SolvingFailure
Unk

-- | Apply the timeout to the configuration.
applyTimeout ::
  (MonadIO m, SBVTC.MonadQuery m) => GrisetteSMTConfig i -> m a -> m a
applyTimeout :: forall (m :: * -> *) (i :: Nat) a.
(MonadIO m, MonadQuery m) =>
GrisetteSMTConfig i -> m a -> m a
applyTimeout GrisetteSMTConfig i
config m a
q = case ExtraConfig i -> Maybe Int
forall (i :: Nat). ExtraConfig i -> Maybe Int
timeout (GrisetteSMTConfig i -> ExtraConfig i
forall (i :: Nat). GrisetteSMTConfig i -> ExtraConfig i
extraConfig GrisetteSMTConfig i
config) of
  Maybe Int
Nothing -> m a
q
  Just Int
t -> Int -> m a -> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
Int -> m a -> m a
SBVTC.timeout Int
t m a
q

-- | Incremental solver monad transformer with the SBV backend.
type SBVIncrementalT n m =
  ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (SBVTC.QueryT m))

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

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

-- | Run the incremental solver monad transformer with a given configuration.
runSBVIncrementalT ::
  (SBVTC.ExtractIO m) =>
  GrisetteSMTConfig n ->
  SBVIncrementalT n m a ->
  m a
runSBVIncrementalT :: forall (m :: * -> *) (n :: Nat) a.
ExtractIO m =>
GrisetteSMTConfig n -> SBVIncrementalT n m a -> m a
runSBVIncrementalT GrisetteSMTConfig n
config SBVIncrementalT n m a
sbvIncrementalT =
  SMTConfig -> SymbolicT m a -> m a
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
SBVT.runSMTWith (GrisetteSMTConfig n -> SMTConfig
forall (i :: Nat). GrisetteSMTConfig i -> SMTConfig
sbvConfig GrisetteSMTConfig n
config) (SymbolicT m a -> m a) -> SymbolicT m a -> m a
forall a b. (a -> b) -> a -> b
$
    QueryT m a -> SymbolicT m a
forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
SBVTC.query (QueryT m a -> SymbolicT m a) -> QueryT m a -> SymbolicT m a
forall a b. (a -> b) -> a -> b
$
      GrisetteSMTConfig n -> QueryT m a -> QueryT m a
forall (m :: * -> *) (i :: Nat) a.
(MonadIO m, MonadQuery m) =>
GrisetteSMTConfig i -> m a -> m a
applyTimeout GrisetteSMTConfig n
config (QueryT m a -> QueryT m a) -> QueryT m a -> QueryT m a
forall a b. (a -> b) -> a -> b
$
        (StateT SymBiMap (QueryT m) a -> SymBiMap -> QueryT m a)
-> SymBiMap -> StateT SymBiMap (QueryT m) a -> QueryT m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT SymBiMap (QueryT m) a -> SymBiMap -> QueryT m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT SymBiMap
emptySymBiMap (StateT SymBiMap (QueryT m) a -> QueryT m a)
-> StateT SymBiMap (QueryT m) a -> QueryT m a
forall a b. (a -> b) -> a -> b
$
          SBVIncrementalT n m a
-> GrisetteSMTConfig n -> StateT SymBiMap (QueryT m) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT SBVIncrementalT n m a
sbvIncrementalT GrisetteSMTConfig n
config

instance (MonadIO m) => MonadicSolver (SBVIncrementalT n m) where
  monadicSolverSolve :: SymBool -> SBVIncrementalT n m (Either SolvingFailure Model)
monadicSolverSolve (SymBool Term Bool
formula) = do
    SymBiMap
symBiMap <- ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (QueryT m)) SymBiMap
forall s (m :: * -> *). MonadState s m => m s
get
    GrisetteSMTConfig n
config <- ReaderT
  (GrisetteSMTConfig n)
  (StateT SymBiMap (QueryT m))
  (GrisetteSMTConfig n)
forall r (m :: * -> *). MonadReader r m => m r
ask
    (SymBiMap
newSymBiMap, 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

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

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

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

instance Solver SBVSolverHandle where
  solverRunCommand :: forall a.
(SBVSolverHandle -> IO (Either SolvingFailure a))
-> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand SBVSolverHandle -> IO (Either SolvingFailure a)
f handle :: SBVSolverHandle
handle@(SBVSolverHandle Async ()
_ TMVar SBVSolverStatus
status TChan SolverCommand
inChan TChan (Either SolvingFailure Model)
_) SolverCommand
command = do
    SBVSolverStatus
st <- IO SBVSolverStatus -> IO SBVSolverStatus
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVSolverStatus -> IO SBVSolverStatus)
-> IO SBVSolverStatus -> IO SBVSolverStatus
forall a b. (a -> b) -> a -> b
$ STM SBVSolverStatus -> IO SBVSolverStatus
forall a. STM a -> IO a
atomically (STM SBVSolverStatus -> IO SBVSolverStatus)
-> STM SBVSolverStatus -> IO SBVSolverStatus
forall a b. (a -> b) -> a -> b
$ TMVar SBVSolverStatus -> STM SBVSolverStatus
forall a. TMVar a -> STM a
takeTMVar TMVar SBVSolverStatus
status
    case SBVSolverStatus
st of
      SBVSolverStatus
SBVSolverNormal -> do
        IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan SolverCommand -> SolverCommand -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan SolverCommand
inChan SolverCommand
command
        Either SolvingFailure a
r <- SBVSolverHandle -> IO (Either SolvingFailure a)
f SBVSolverHandle
handle
        IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Maybe SBVSolverStatus
currStatus <- TMVar SBVSolverStatus -> STM (Maybe SBVSolverStatus)
forall a. TMVar a -> STM (Maybe a)
tryReadTMVar TMVar SBVSolverStatus
status
          case Maybe SBVSolverStatus
currStatus of
            Maybe SBVSolverStatus
Nothing -> TMVar SBVSolverStatus -> SBVSolverStatus -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar SBVSolverStatus
status SBVSolverStatus
SBVSolverNormal
            Just SBVSolverStatus
_ -> () -> STM ()
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Either SolvingFailure a
r
      SBVSolverStatus
SBVSolverTerminated -> do
        IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
        Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SolvingFailure a -> IO (Either SolvingFailure a))
-> Either SolvingFailure a -> IO (Either SolvingFailure a)
forall a b. (a -> b) -> a -> b
$ SolvingFailure -> Either SolvingFailure a
forall a b. a -> Either a b
Left SolvingFailure
Terminated
  solverSolve :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure Model)
solverSolve SBVSolverHandle
handle SymBool
nextFormula =
    (SBVSolverHandle -> IO (Either SolvingFailure Model))
-> SBVSolverHandle
-> SolverCommand
-> IO (Either SolvingFailure Model)
forall handle a.
Solver handle =>
(handle -> IO (Either SolvingFailure a))
-> handle -> SolverCommand -> IO (Either SolvingFailure a)
forall a.
(SBVSolverHandle -> IO (Either SolvingFailure a))
-> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a)
solverRunCommand
      ( \(SBVSolverHandle Async ()
_ TMVar SBVSolverStatus
_ TChan SolverCommand
_ TChan (Either SolvingFailure Model)
outChan) ->
          IO (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either SolvingFailure Model)
 -> IO (Either SolvingFailure Model))
-> IO (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ STM (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a. STM a -> IO a
atomically (STM (Either SolvingFailure Model)
 -> IO (Either SolvingFailure Model))
-> STM (Either SolvingFailure Model)
-> IO (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ TChan (Either SolvingFailure Model)
-> STM (Either SolvingFailure Model)
forall a. TChan a -> STM a
readTChan TChan (Either SolvingFailure Model)
outChan
      )
      SBVSolverHandle
handle
      (SolverCommand -> IO (Either SolvingFailure Model))
-> SolverCommand -> IO (Either SolvingFailure Model)
forall a b. (a -> b) -> a -> b
$ SymBool -> SolverCommand
SolverSolve SymBool
nextFormula
  solverTerminate :: SBVSolverHandle -> IO ()
solverTerminate (SBVSolverHandle Async ()
thread TMVar SBVSolverStatus
status TChan SolverCommand
inChan TChan (Either SolvingFailure Model)
_) = do
    IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
      TChan SolverCommand -> SolverCommand -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan SolverCommand
inChan SolverCommand
SolverTerminate
    Async () -> IO ()
forall a. Async a -> IO a
wait Async ()
thread
  solverForceTerminate :: SBVSolverHandle -> IO ()
solverForceTerminate (SBVSolverHandle Async ()
thread TMVar SBVSolverStatus
status TChan SolverCommand
_ TChan (Either SolvingFailure Model)
outChan) = do
    IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      TMVar SBVSolverStatus -> STM ()
setTerminated TMVar SBVSolverStatus
status
      TChan (Either SolvingFailure Model)
-> Either SolvingFailure Model -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Either SolvingFailure Model)
outChan (SolvingFailure -> Either SolvingFailure Model
forall a b. a -> Either a b
Left SolvingFailure
Terminated)
    ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async () -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async ()
thread) ExitCode
ExitSuccess
    Async () -> IO ()
forall a. Async a -> IO a
wait Async ()
thread