{-# 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, isDebugging
)
where

import Language.Hasmtlib.Internal.Sharing
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.SMT
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 qualified Data.ByteString.Lazy.Char8 as ByteString.Char8
import Data.ByteString.Builder
import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf)
import Data.Attoparsec.ByteString hiding (Result)
import Control.Monad.State
import Control.Monad
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 -> Bool
_isDebugging       :: !Bool                                               -- ^ Flag if pipe shall debug
  }
$(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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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)
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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 = Builder
"(push 1)"
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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 = Builder
"(pop 1)"
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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
"(check-sat)"
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString Builder
cmd
    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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn ByteString
result
    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
"(get-model)"
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString Builder
cmd
    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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn ByteString
model
    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 = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"get-value" (Builder -> Builder) -> Builder -> Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> SMTVar t -> Builder
forall a. Render a => a -> Builder
render SMTVar t
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString Builder
cmd
    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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn ByteString
model
    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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Pipe
pipePipe -> Getting Bool Pipe Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Pipe Bool
Lens' Pipe Bool
isDebugging) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ 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
$ ByteString -> IO ()
ByteString.Char8.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString 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
$ 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 #-}