{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}

{- |
This module provides an IO-'Pipe' to external SMT-Solvers and ships with implementations for 'MonadSMT', 'MonadOMT' and 'MonadIncrSMT'.

The 'Pipe' is based on a 'B.Solver' from Tweag's package @smtlib-backends@ and in reality is just an IO-Handle.
-}
module Language.Hasmtlib.Type.Pipe
(
  -- * Type
  Pipe(..)

  -- * Lens
, 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

-- | A pipe to the solver.
--   If 'B.Solver' is 'B.Queuing' then all commands that do not expect an answer are sent to the queue.
--   All commands that expect an answer have the queue to be sent to the solver before sending the command itself.
--   If 'B.Solver' is not 'B.Queuing', all commands are sent to the solver immediately.
data Pipe = Pipe
  { Pipe -> Int
_lastPipeVarId     :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var
  , Pipe -> Maybe String
_mPipeLogic        :: Maybe String                                        -- ^ Logic for the SMT-Solver
  , Pipe -> SharingMode
_pipeSharingMode   :: !SharingMode                                        -- ^ How to share common expressions
  , Pipe -> HashMap (StableName ()) (SomeKnownSMTSort Expr)
_pipeStableMap     :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share
  , Pipe -> Seq (Seq (StableName ()))
_incrSharedAuxs    :: !(Seq (Seq (StableName ())))                        -- ^ Index of each 'Seq' ('StableName' ()) is incremental stack height where 'StableName' representing auxiliary var that has been shared
  , Pipe -> Solver
_pipeSolver        :: !B.Solver                                           -- ^ Active pipe to the backend
  , Pipe -> Maybe (Debugger Pipe)
_mPipeDebugger      :: Maybe (Debugger Pipe)                                 -- ^ Debugger for communication with the external solver
  }
$(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 #-}