{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}
module Language.Hasmtlib.Type.Pipe
(
Pipe(..)
, lastPipeVarId, mPipeLogic
, pipeSharingMode, pipeStableMap, incrSharedAuxs
, pipeSolver
)
where
import Language.Hasmtlib.Internal.Sharing
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Type.Debugger
import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..))
import Language.Hasmtlib.Type.MonadSMT
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Codec
import Language.Hasmtlib.Internal.Parser hiding (var, constant)
import qualified SMTLIB.Backends as B
import Data.HashMap.Lazy
import Data.Sequence hiding ((|>), (:>))
import Data.List (isPrefixOf)
import Data.IntMap as IntMap (singleton)
import Data.Dependent.Map as DMap
import Data.Coerce
import Data.ByteString.Builder
import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf)
import Data.Attoparsec.ByteString hiding (Result)
import Control.Monad.State
import Control.Lens hiding (List)
import System.Mem.StableName
data Pipe = Pipe
{ Pipe -> Int
_lastPipeVarId :: {-# UNPACK #-} !Int
, Pipe -> Maybe String
_mPipeLogic :: Maybe String
, Pipe -> SharingMode
_pipeSharingMode :: !SharingMode
, Pipe -> HashMap (StableName ()) (SomeKnownSMTSort Expr)
_pipeStableMap :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))
, Pipe -> Seq (Seq (StableName ()))
_incrSharedAuxs :: !(Seq (Seq (StableName ())))
, Pipe -> Solver
_pipeSolver :: !B.Solver
, Pipe -> Maybe (Debugger Pipe)
_mPipeDebugger :: Maybe (Debugger Pipe)
}
$(makeLenses ''Pipe)
instance Sharing Pipe where
type SharingMonad Pipe = MonadIO
stableMap :: Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))
stableMap = (HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> f (HashMap (StableName ()) (SomeKnownSMTSort Expr)))
-> Pipe -> f Pipe
Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))
pipeStableMap
assertSharedNode :: forall (m :: * -> *).
(MonadState Pipe m, SharingMonad Pipe m) =>
StableName () -> Expr 'BoolSort -> m ()
assertSharedNode StableName ()
sn Expr 'BoolSort
expr = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
ASetter Pipe Pipe (Seq (StableName ())) (Seq (StableName ()))
-> (Seq (StableName ()) -> Seq (StableName ())) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ((Seq (Seq (StableName ())) -> Identity (Seq (Seq (StableName ()))))
-> Pipe -> Identity Pipe
Lens' Pipe (Seq (Seq (StableName ())))
incrSharedAuxs((Seq (Seq (StableName ()))
-> Identity (Seq (Seq (StableName ()))))
-> Pipe -> Identity Pipe)
-> ((Seq (StableName ()) -> Identity (Seq (StableName ())))
-> Seq (Seq (StableName ()))
-> Identity (Seq (Seq (StableName ()))))
-> ASetter Pipe Pipe (Seq (StableName ())) (Seq (StableName ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Seq (StableName ()) -> Identity (Seq (StableName ())))
-> Seq (Seq (StableName ()))
-> Identity (Seq (Seq (StableName ())))
forall s a. Snoc s s a a => Traversal' s a
Traversal' (Seq (Seq (StableName ()))) (Seq (StableName ()))
_last) (Seq (StableName ()) -> StableName () -> Seq (StableName ())
forall s a. Snoc s s a a => s -> a -> s
|> StableName ()
sn)
let cmd :: Builder
cmd = Expr 'BoolSort -> Builder
renderAssert Expr 'BoolSort
expr
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugAssert` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
setSharingMode :: forall (m :: * -> *). MonadState Pipe m => SharingMode -> m ()
setSharingMode SharingMode
sm = (SharingMode -> Identity SharingMode) -> Pipe -> Identity Pipe
Lens' Pipe SharingMode
pipeSharingMode ((SharingMode -> Identity SharingMode) -> Pipe -> Identity Pipe)
-> SharingMode -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SharingMode
sm
instance (MonadState Pipe m, MonadIO m) => MonadSMT Pipe m where
smtvar' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (SMTVar t)
smtvar' Proxy t
_ = (Int -> SMTVar t) -> m Int -> m (SMTVar t)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> SMTVar t
forall a b. Coercible a b => a -> b
coerce (m Int -> m (SMTVar t)) -> m Int -> m (SMTVar t)
forall a b. (a -> b) -> a -> b
$ (Int -> (Int, Int)) -> Pipe -> (Int, Pipe)
Lens' Pipe Int
lastPipeVarId ((Int -> (Int, Int)) -> Pipe -> (Int, Pipe)) -> Int -> m Int
forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
<+= Int
1
{-# INLINE smtvar' #-}
var' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (Expr t)
var' Proxy t
p = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
SMTVar t
newVar <- Proxy t -> m (SMTVar t)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Proxy t -> m (SMTVar t)
forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (SMTVar t)
smtvar' Proxy t
p
let cmd :: Builder
cmd = SMTVar t -> Builder
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Builder
renderDeclareVar SMTVar t
newVar
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugVar` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
Expr t -> m (Expr t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> m (Expr t)) -> Expr t -> m (Expr t)
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Expr t
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Expr t
Var SMTVar t
newVar
{-# INLINEABLE var' #-}
assert :: Expr 'BoolSort -> m ()
assert Expr 'BoolSort
expr = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
Expr 'BoolSort
sExpr <- SharingMode -> Expr 'BoolSort -> m (Expr 'BoolSort)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) =>
SharingMode -> Expr t -> m (Expr t)
runSharing (Pipe
pipePipe -> Getting SharingMode Pipe SharingMode -> SharingMode
forall s a. s -> Getting a s a -> a
^.Getting SharingMode Pipe SharingMode
Lens' Pipe SharingMode
pipeSharingMode) Expr 'BoolSort
expr
Expr 'BoolSort
qExpr <- case Pipe
pipePipe -> Getting (Maybe String) Pipe (Maybe String) -> Maybe String
forall s a. s -> Getting a s a -> a
^.Getting (Maybe String) Pipe (Maybe String)
Lens' Pipe (Maybe String)
mPipeLogic of
Maybe String
Nothing -> Expr 'BoolSort -> m (Expr 'BoolSort)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr 'BoolSort
sExpr
Just String
logic -> if String
"QF" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
logic then Expr 'BoolSort -> m (Expr 'BoolSort)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr 'BoolSort
sExpr else Expr 'BoolSort -> m (Expr 'BoolSort)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Expr t -> m (Expr t)
quantify Expr 'BoolSort
sExpr
let cmd :: Builder
cmd = Expr 'BoolSort -> Builder
renderAssert Expr 'BoolSort
qExpr
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugAssert` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
{-# INLINEABLE assert #-}
setOption :: SMTOption -> m ()
setOption SMTOption
opt = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = SMTOption -> Builder
forall a. Render a => a -> Builder
render SMTOption
opt
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugOption` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
setLogic :: String -> m ()
setLogic String
l = do
(Maybe String -> Identity (Maybe String)) -> Pipe -> Identity Pipe
Lens' Pipe (Maybe String)
mPipeLogic ((Maybe String -> Identity (Maybe String))
-> Pipe -> Identity Pipe)
-> String -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= String
l
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = Builder -> Builder
renderSetLogic (String -> Builder
stringUtf8 String
l)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugLogic` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
push :: m ()
push = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = Integer -> Builder
renderPush Integer
1
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugPush` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
(Seq (Seq (StableName ())) -> Identity (Seq (Seq (StableName ()))))
-> Pipe -> Identity Pipe
Lens' Pipe (Seq (Seq (StableName ())))
incrSharedAuxs ((Seq (Seq (StableName ()))
-> Identity (Seq (Seq (StableName ()))))
-> Pipe -> Identity Pipe)
-> Seq (Seq (StableName ())) -> m ()
forall s (m :: * -> *) a.
(MonadState s m, Semigroup a) =>
ASetter' s a -> a -> m ()
<>= Seq (Seq (StableName ()))
forall a. Monoid a => a
mempty
pop :: m ()
pop = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = Integer -> Builder
renderPop Integer
1
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugPop` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
Getting (Sequenced () m) Pipe (StableName ())
-> Pipe -> (StableName () -> m ()) -> m ()
forall (m :: * -> *) r s a.
Monad m =>
Getting (Sequenced r m) s a -> s -> (a -> m r) -> m ()
forMOf_ ((Seq (Seq (StableName ()))
-> Const (Sequenced () m) (Seq (Seq (StableName ()))))
-> Pipe -> Const (Sequenced () m) Pipe
Lens' Pipe (Seq (Seq (StableName ())))
incrSharedAuxs((Seq (Seq (StableName ()))
-> Const (Sequenced () m) (Seq (Seq (StableName ()))))
-> Pipe -> Const (Sequenced () m) Pipe)
-> ((StableName () -> Const (Sequenced () m) (StableName ()))
-> Seq (Seq (StableName ()))
-> Const (Sequenced () m) (Seq (Seq (StableName ()))))
-> Getting (Sequenced () m) Pipe (StableName ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Seq (StableName ())
-> Const (Sequenced () m) (Seq (StableName ())))
-> Seq (Seq (StableName ()))
-> Const (Sequenced () m) (Seq (Seq (StableName ())))
forall s a. Snoc s s a a => Traversal' s a
Traversal' (Seq (Seq (StableName ()))) (Seq (StableName ()))
_last((Seq (StableName ())
-> Const (Sequenced () m) (Seq (StableName ())))
-> Seq (Seq (StableName ()))
-> Const (Sequenced () m) (Seq (Seq (StableName ()))))
-> ((StableName () -> Const (Sequenced () m) (StableName ()))
-> Seq (StableName ())
-> Const (Sequenced () m) (Seq (StableName ())))
-> (StableName () -> Const (Sequenced () m) (StableName ()))
-> Seq (Seq (StableName ()))
-> Const (Sequenced () m) (Seq (Seq (StableName ())))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(StableName () -> Const (Sequenced () m) (StableName ()))
-> Seq (StableName ())
-> Const (Sequenced () m) (Seq (StableName ()))
forall (f :: * -> *) a. Foldable f => IndexedFold Int (f a) a
IndexedFold Int (Seq (StableName ())) (StableName ())
folded) Pipe
pipe (\StableName ()
sn -> (HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> Identity (HashMap (StableName ()) (SomeKnownSMTSort Expr)))
-> Pipe -> Identity Pipe
Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))
pipeStableMap((HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> Identity (HashMap (StableName ()) (SomeKnownSMTSort Expr)))
-> Pipe -> Identity Pipe)
-> ((Maybe (SomeKnownSMTSort Expr)
-> Identity (Maybe (SomeKnownSMTSort Expr)))
-> HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> Identity (HashMap (StableName ()) (SomeKnownSMTSort Expr)))
-> (Maybe (SomeKnownSMTSort Expr)
-> Identity (Maybe (SomeKnownSMTSort Expr)))
-> Pipe
-> Identity Pipe
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (HashMap (StableName ()) (SomeKnownSMTSort Expr))
-> Lens'
(HashMap (StableName ()) (SomeKnownSMTSort Expr))
(Maybe (IxValue (HashMap (StableName ()) (SomeKnownSMTSort Expr))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at StableName ()
Index (HashMap (StableName ()) (SomeKnownSMTSort Expr))
sn ((Maybe (SomeKnownSMTSort Expr)
-> Identity (Maybe (SomeKnownSMTSort Expr)))
-> Pipe -> Identity Pipe)
-> Maybe (SomeKnownSMTSort Expr) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Maybe (SomeKnownSMTSort Expr)
forall a. Maybe a
Nothing)
((Seq (Seq (StableName ()))
-> Identity (Seq (Seq (StableName ()))))
-> Pipe -> Identity Pipe)
-> (Seq (Seq (StableName ())) -> Seq (Seq (StableName ()))) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying (Seq (Seq (StableName ())) -> Identity (Seq (Seq (StableName ()))))
-> Pipe -> Identity Pipe
Lens' Pipe (Seq (Seq (StableName ())))
incrSharedAuxs ((Seq (Seq (StableName ())) -> Seq (Seq (StableName ()))) -> m ())
-> (Seq (Seq (StableName ())) -> Seq (Seq (StableName ()))) -> m ()
forall a b. (a -> b) -> a -> b
$ \case (Seq (Seq (StableName ()))
auxs:>Seq (StableName ())
_) -> Seq (Seq (StableName ()))
auxs ; Seq (Seq (StableName ()))
auxs -> Seq (Seq (StableName ()))
auxs
checkSat :: m Result
checkSat = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = Builder
renderCheckSat
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugCheckSat` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
ByteString
result <- IO ByteString -> m ByteString
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ByteString -> m ByteString) -> IO ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ByteString
B.command (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
`debugResultResponse` ByteString
result) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
case Parser Result -> ByteString -> Either String Result
forall a. Parser a -> ByteString -> Either String a
parseOnly Parser Result
resultParser (ByteString -> ByteString
toStrict ByteString
result) of
Left String
e -> IO Result -> m Result
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Result -> m Result) -> IO Result -> m Result
forall a b. (a -> b) -> a -> b
$ do
ByteString -> IO ()
forall a. Show a => a -> IO ()
print ByteString
result
String -> IO Result
forall a. HasCallStack => String -> a
error String
e
Right Result
res -> Result -> m Result
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
res
getModel :: m Solution
getModel = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = Builder
renderGetModel
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugGetModel` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
ByteString
model <- IO ByteString -> m ByteString
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ByteString -> m ByteString) -> IO ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ByteString
B.command (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
`debugModelResponse` ByteString
model) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
case Parser Solution -> ByteString -> Either String Solution
forall a. Parser a -> ByteString -> Either String a
parseOnly Parser Solution
anyModelParser (ByteString -> ByteString
toStrict ByteString
model) of
Left String
e -> IO Solution -> m Solution
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Solution -> m Solution) -> IO Solution -> m Solution
forall a b. (a -> b) -> a -> b
$ do
ByteString -> IO ()
forall a. Show a => a -> IO ()
print ByteString
model
String -> IO Solution
forall a. HasCallStack => String -> a
error String
e
Right Solution
sol -> Solution -> m Solution
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Solution
sol
getValue :: forall t. KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))
getValue :: forall (t :: SMTSort).
KnownSMTSort t =>
Expr t -> m (Maybe (Decoded (Expr t)))
getValue v :: Expr t
v@(Var SMTVar t
x) = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
let cmd :: Builder
cmd = SMTVar t -> Builder
forall (t :: SMTSort). SMTVar t -> Builder
renderGetValue SMTVar t
x
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugGetValue` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
ByteString
model <- IO ByteString -> m ByteString
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ByteString -> m ByteString) -> IO ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ByteString
B.command (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
`debugModelResponse` ByteString
model) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
case Parser (SMTVarSol t) -> ByteString -> Either String (SMTVarSol t)
forall a. Parser a -> ByteString -> Either String a
parseOnly (forall (t :: SMTSort).
KnownSMTSort t =>
SMTVar t -> Parser (SMTVarSol t)
getValueParser @t SMTVar t
x) (ByteString -> ByteString
toStrict ByteString
model) of
Left String
e -> IO (Maybe (HaskellType t)) -> m (Maybe (HaskellType t))
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (HaskellType t)) -> m (Maybe (HaskellType t)))
-> IO (Maybe (HaskellType t)) -> m (Maybe (HaskellType t))
forall a b. (a -> b) -> a -> b
$ do
ByteString -> IO ()
forall a. Show a => a -> IO ()
print ByteString
model
String -> IO (Maybe (HaskellType t))
forall a. HasCallStack => String -> a
error String
e
Right SMTVarSol t
sol ->
Maybe (HaskellType t) -> m (Maybe (HaskellType t))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (HaskellType t) -> m (Maybe (HaskellType t)))
-> Maybe (HaskellType t) -> m (Maybe (HaskellType t))
forall a b. (a -> b) -> a -> b
$
Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode
(SSMTSort t -> IntValueMap t -> Solution
forall {k1} (k2 :: k1 -> *) (v :: k1) (f :: k1 -> *).
k2 v -> f v -> DMap k2 f
DMap.singleton
(forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t)
(IntMap (Value t) -> IntValueMap t
forall (t :: SMTSort). IntMap (Value t) -> IntValueMap t
IntValueMap (IntMap (Value t) -> IntValueMap t)
-> IntMap (Value t) -> IntValueMap t
forall a b. (a -> b) -> a -> b
$ Int -> Value t -> IntMap (Value t)
forall a. Int -> a -> IntMap a
IntMap.singleton (SMTVarSol t
solSMTVarSol t -> Getting Int (SMTVarSol t) Int -> Int
forall s a. s -> Getting a s a -> a
^.(SMTVar t -> Const Int (SMTVar t))
-> SMTVarSol t -> Const Int (SMTVarSol t)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(SMTVar t -> f (SMTVar t)) -> SMTVarSol t -> f (SMTVarSol t)
solVar((SMTVar t -> Const Int (SMTVar t))
-> SMTVarSol t -> Const Int (SMTVarSol t))
-> ((Int -> Const Int Int) -> SMTVar t -> Const Int (SMTVar t))
-> Getting Int (SMTVarSol t) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Const Int Int) -> SMTVar t -> Const Int (SMTVar t)
forall (t1 :: SMTSort) (t2 :: SMTSort) (p :: * -> * -> *)
(f :: * -> *).
(Profunctor p, Functor f) =>
p Int (f Int) -> p (SMTVar t1) (f (SMTVar t2))
varId) (SMTVarSol t
solSMTVarSol t -> Getting (Value t) (SMTVarSol t) (Value t) -> Value t
forall s a. s -> Getting a s a -> a
^.Getting (Value t) (SMTVarSol t) (Value t)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(Value t -> f (Value t)) -> SMTVarSol t -> f (SMTVarSol t)
solVal)))
Expr t
v
getValue Expr t
expr = do
Solution
model <- m Solution
forall s (m :: * -> *). MonadIncrSMT s m => m Solution
getModel
Maybe (HaskellType t) -> m (Maybe (HaskellType t))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (HaskellType t) -> m (Maybe (HaskellType t)))
-> Maybe (HaskellType t) -> m (Maybe (HaskellType t))
forall a b. (a -> b) -> a -> b
$ Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
model Expr t
expr
instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where
minimize :: forall (t :: SMTSort).
(KnownSMTSort t, Num (Expr t)) =>
Expr t -> m ()
minimize Expr t
expr = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
Expr t
sExpr <- SharingMode -> Expr t -> m (Expr t)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) =>
SharingMode -> Expr t -> m (Expr t)
runSharing (Pipe
pipePipe -> Getting SharingMode Pipe SharingMode -> SharingMode
forall s a. s -> Getting a s a -> a
^.Getting SharingMode Pipe SharingMode
Lens' Pipe SharingMode
pipeSharingMode) Expr t
expr
let cmd :: Builder
cmd = Minimize t -> Builder
forall a. Render a => a -> Builder
render (Minimize t -> Builder) -> Minimize t -> Builder
forall a b. (a -> b) -> a -> b
$ Expr t -> Minimize t
forall (t :: SMTSort). Expr t -> Minimize t
Minimize Expr t
sExpr
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugMinimize` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
{-# INLINEABLE minimize #-}
maximize :: forall (t :: SMTSort).
(KnownSMTSort t, Num (Expr t)) =>
Expr t -> m ()
maximize Expr t
expr = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
Expr t
sExpr <- SharingMode -> Expr t -> m (Expr t)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) =>
SharingMode -> Expr t -> m (Expr t)
runSharing (Pipe
pipePipe -> Getting SharingMode Pipe SharingMode -> SharingMode
forall s a. s -> Getting a s a -> a
^.Getting SharingMode Pipe SharingMode
Lens' Pipe SharingMode
pipeSharingMode) Expr t
expr
let cmd :: Builder
cmd = Maximize t -> Builder
forall a. Render a => a -> Builder
render (Maximize t -> Builder) -> Maximize t -> Builder
forall a b. (a -> b) -> a -> b
$ Expr t -> Maximize t
forall (t :: SMTSort). Expr t -> Maximize t
Maximize Expr t
sExpr
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugMaximize` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
{-# INLINEABLE maximize #-}
assertSoft :: Expr 'BoolSort -> Maybe Double -> Maybe String -> m ()
assertSoft Expr 'BoolSort
expr Maybe Double
w Maybe String
gid = do
Pipe
pipe <- m Pipe
forall s (m :: * -> *). MonadState s m => m s
get
Expr 'BoolSort
sExpr <- SharingMode -> Expr 'BoolSort -> m (Expr 'BoolSort)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) =>
SharingMode -> Expr t -> m (Expr t)
runSharing (Pipe
pipePipe -> Getting SharingMode Pipe SharingMode -> SharingMode
forall s a. s -> Getting a s a -> a
^.Getting SharingMode Pipe SharingMode
Lens' Pipe SharingMode
pipeSharingMode) Expr 'BoolSort
expr
let cmd :: Builder
cmd = SoftFormula -> Builder
forall a. Render a => a -> Builder
render (SoftFormula -> Builder) -> SoftFormula -> Builder
forall a b. (a -> b) -> a -> b
$ Expr 'BoolSort -> Maybe Double -> Maybe String -> SoftFormula
SoftFormula Expr 'BoolSort
sExpr Maybe Double
w Maybe String
gid
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> (Debugger Pipe -> IO ()) -> Maybe (Debugger Pipe) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Debugger Pipe -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugAssertSoft` Builder
cmd) (Pipe
pipePipe
-> Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting (Maybe (Debugger Pipe)) Pipe (Maybe (Debugger Pipe))
Lens' Pipe (Maybe (Debugger Pipe))
mPipeDebugger)
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
B.command_ (Pipe
pipePipe -> Getting Solver Pipe Solver -> Solver
forall s a. s -> Getting a s a -> a
^.Getting Solver Pipe Solver
Lens' Pipe Solver
pipeSolver) Builder
cmd
{-# INLINEABLE assertSoft #-}