module Language.Hasmtlib.Solver.Common where

import Language.Hasmtlib.Type.SMT
import Language.Hasmtlib.Type.OMT
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Internal.Parser
import Data.Default
import Data.Sequence as Seq hiding ((|>), filter)
import Data.ByteString.Lazy hiding (singleton)
import Data.ByteString.Lazy.UTF8 (toString)
import Data.ByteString.Builder
import Data.Attoparsec.ByteString
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import qualified SMTLIB.Backends.Process as Process
import qualified SMTLIB.Backends as Backend

-- | Creates a 'Solver' from a 'Process.Config'.
solver :: (RenderSeq s, MonadIO m) => Process.Config -> Solver s m
solver :: forall s (m :: * -> *).
(RenderSeq s, MonadIO m) =>
Config -> Solver s m
solver Config
cfg = Config -> Maybe (Debugger s) -> Solver s m
forall s (m :: * -> *).
(RenderSeq s, MonadIO m) =>
Config -> Maybe (Debugger s) -> Solver s m
processSolver Config
cfg Maybe (Debugger s)
forall a. Maybe a
Nothing

-- | Creates a debugging 'Solver' from a 'Process.Config'.
debug :: (RenderSeq s, MonadIO m) => Process.Config -> Debugger s -> Solver s m
debug :: forall s (m :: * -> *).
(RenderSeq s, MonadIO m) =>
Config -> Debugger s -> Solver s m
debug Config
cfg = Config -> Maybe (Debugger s) -> Solver s m
forall s (m :: * -> *).
(RenderSeq s, MonadIO m) =>
Config -> Maybe (Debugger s) -> Solver s m
processSolver Config
cfg (Maybe (Debugger s) -> Solver s m)
-> (Debugger s -> Maybe (Debugger s)) -> Debugger s -> Solver s m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Maybe (Debugger s)
forall a. a -> Maybe a
Just

-- | Creates an interactive session with a solver by creating and returning an alive process-handle 'Process.Handle'.
--   Queues commands by default, see 'Backend.Queuing'.
interactiveSolver :: MonadIO m => Process.Config -> m (Backend.Solver, Process.Handle)
interactiveSolver :: forall (m :: * -> *). MonadIO m => Config -> m (Solver, Handle)
interactiveSolver Config
cfg = IO (Solver, Handle) -> m (Solver, Handle)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Solver, Handle) -> m (Solver, Handle))
-> IO (Solver, Handle) -> m (Solver, Handle)
forall a b. (a -> b) -> a -> b
$ do
  Handle
handle  <- Config -> IO Handle
Process.new Config
cfg
  (Solver -> Handle -> (Solver, Handle))
-> IO Solver -> IO Handle -> IO (Solver, Handle)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (QueuingFlag -> Backend -> IO Solver
Backend.initSolver QueuingFlag
Backend.Queuing (Backend -> IO Solver) -> Backend -> IO Solver
forall a b. (a -> b) -> a -> b
$ Handle -> Backend
Process.toBackend Handle
handle) (Handle -> IO Handle
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Handle
handle)

-- | A type holding actions for debugging states.
data Debugger s = Debugger
  { forall s. Debugger s -> s -> IO ()
debugState          :: s -> IO ()               -- ^ Debug the entire state
  , forall s. Debugger s -> Seq Builder -> IO ()
debugProblem        :: Seq Builder -> IO ()     -- ^ Debug the linewise-rendered problem
  , forall s. Debugger s -> ByteString -> IO ()
debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@
  , forall s. Debugger s -> ByteString -> IO ()
debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@
  }

instance Default (Debugger SMT) where
  def :: Debugger SMT
def = Debugger
    { debugState :: SMT -> IO ()
debugState            = \SMT
s -> IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Vars: "       [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq (SomeKnownSMTSort SMTVar) -> Int
forall a. Seq a -> Int
Seq.length (SMT
sSMT
-> Getting
     (Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
-> Seq (SomeKnownSMTSort SMTVar)
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
vars))
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Assertions: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq (Expr 'BoolSort) -> Int
forall a. Seq a -> Int
Seq.length (SMT
sSMT
-> Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
-> Seq (Expr 'BoolSort)
forall s a. s -> Getting a s a -> a
^.Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas))
    , debugProblem :: Seq Builder -> IO ()
debugProblem        = IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> (Seq Builder -> IO ()) -> Seq Builder -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Builder -> IO ()) -> Seq Builder -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (Builder -> [Char]) -> Builder -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Char]
toString (ByteString -> [Char])
-> (Builder -> ByteString) -> Builder -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString)
    , debugResultResponse :: ByteString -> IO ()
debugResultResponse = IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> (ByteString -> IO ()) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (ByteString -> [Char]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[Char]
s -> [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n") ([Char] -> [Char])
-> (ByteString -> [Char]) -> ByteString -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Char]
toString
    , debugModelResponse :: ByteString -> IO ()
debugModelResponse  = IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> (ByteString -> IO ()) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString -> IO ()) -> [ByteString] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (ByteString -> [Char]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Char]
toString) ([ByteString] -> IO ())
-> (ByteString -> [ByteString]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> ByteString -> [ByteString]
split Word8
13
    }

instance Default (Debugger OMT) where
  def :: Debugger OMT
def = Debugger
    { debugState :: OMT -> IO ()
debugState          = \OMT
omt -> IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Vars: "                 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq (SomeKnownSMTSort SMTVar) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting
     (Seq (SomeKnownSMTSort SMTVar)) OMT (Seq (SomeKnownSMTSort SMTVar))
-> Seq (SomeKnownSMTSort SMTVar)
forall s a. s -> Getting a s a -> a
^.(SMT -> Const (Seq (SomeKnownSMTSort SMTVar)) SMT)
-> OMT -> Const (Seq (SomeKnownSMTSort SMTVar)) OMT
Lens' OMT SMT
smt((SMT -> Const (Seq (SomeKnownSMTSort SMTVar)) SMT)
 -> OMT -> Const (Seq (SomeKnownSMTSort SMTVar)) OMT)
-> Getting
     (Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
-> Getting
     (Seq (SomeKnownSMTSort SMTVar)) OMT (Seq (SomeKnownSMTSort SMTVar))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Getting
  (Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
vars))
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Hard assertions: "      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq (Expr 'BoolSort) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting (Seq (Expr 'BoolSort)) OMT (Seq (Expr 'BoolSort))
-> Seq (Expr 'BoolSort)
forall s a. s -> Getting a s a -> a
^.(SMT -> Const (Seq (Expr 'BoolSort)) SMT)
-> OMT -> Const (Seq (Expr 'BoolSort)) OMT
Lens' OMT SMT
smt((SMT -> Const (Seq (Expr 'BoolSort)) SMT)
 -> OMT -> Const (Seq (Expr 'BoolSort)) OMT)
-> Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
-> Getting (Seq (Expr 'BoolSort)) OMT (Seq (Expr 'BoolSort))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas))
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Soft assertions: "      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq SoftFormula -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting (Seq SoftFormula) OMT (Seq SoftFormula)
-> Seq SoftFormula
forall s a. s -> Getting a s a -> a
^.Getting (Seq SoftFormula) OMT (Seq SoftFormula)
Lens' OMT (Seq SoftFormula)
softFormulas))
        [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Optimization targets: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq (SomeKnownSMTSort Minimize) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting
     (Seq (SomeKnownSMTSort Minimize))
     OMT
     (Seq (SomeKnownSMTSort Minimize))
-> Seq (SomeKnownSMTSort Minimize)
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (SomeKnownSMTSort Minimize))
  OMT
  (Seq (SomeKnownSMTSort Minimize))
Lens' OMT (Seq (SomeKnownSMTSort Minimize))
targetMinimize) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq (SomeKnownSMTSort Maximize) -> Int
forall a. Seq a -> Int
Seq.length (OMT
omtOMT
-> Getting
     (Seq (SomeKnownSMTSort Maximize))
     OMT
     (Seq (SomeKnownSMTSort Maximize))
-> Seq (SomeKnownSMTSort Maximize)
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (SomeKnownSMTSort Maximize))
  OMT
  (Seq (SomeKnownSMTSort Maximize))
Lens' OMT (Seq (SomeKnownSMTSort Maximize))
targetMaximize))
    , debugProblem :: Seq Builder -> IO ()
debugProblem        = IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> (Seq Builder -> IO ()) -> Seq Builder -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Builder -> IO ()) -> Seq Builder -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (Builder -> [Char]) -> Builder -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Char]
toString (ByteString -> [Char])
-> (Builder -> ByteString) -> Builder -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString)
    , debugResultResponse :: ByteString -> IO ()
debugResultResponse = IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> (ByteString -> IO ()) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (ByteString -> [Char]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[Char]
s -> [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n") ([Char] -> [Char])
-> (ByteString -> [Char]) -> ByteString -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Char]
toString
    , debugModelResponse :: ByteString -> IO ()
debugModelResponse  = IO () -> IO ()
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> (ByteString -> IO ()) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString -> IO ()) -> [ByteString] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn ([Char] -> IO ()) -> (ByteString -> [Char]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Char]
toString) ([ByteString] -> IO ())
-> (ByteString -> [ByteString]) -> ByteString -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> ByteString -> [ByteString]
split Word8
13
    }

-- | A 'Solver' which holds an external process with a SMT-Solver.
--   This will:
--
-- 1. Encode the 'SMT'-problem,
--
-- 2. Start a new external process for the SMT-Solver,
--
-- 3. Send the problem to the SMT-Solver,
--
-- 4. Wait for an answer and parse it and
--
-- 5. close the process and clean up all resources.
--
processSolver :: (RenderSeq s, MonadIO m) => Process.Config -> Maybe (Debugger s) -> Solver s m
processSolver :: forall s (m :: * -> *).
(RenderSeq s, MonadIO m) =>
Config -> Maybe (Debugger s) -> Solver s m
processSolver Config
cfg Maybe (Debugger s)
debugger s
s = do
  IO (Result, Solution) -> m (Result, Solution)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Result, Solution) -> m (Result, Solution))
-> IO (Result, Solution) -> m (Result, Solution)
forall a b. (a -> b) -> a -> b
$ Config
-> (Handle -> IO (Result, Solution)) -> IO (Result, Solution)
forall a. Config -> (Handle -> IO a) -> IO a
Process.with Config
cfg ((Handle -> IO (Result, Solution)) -> IO (Result, Solution))
-> (Handle -> IO (Result, Solution)) -> IO (Result, Solution)
forall a b. (a -> b) -> a -> b
$ \Handle
handle -> do
    IO () -> (Debugger s -> IO ()) -> Maybe (Debugger s) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger s -> s -> IO ()
forall s. Debugger s -> s -> IO ()
`debugState` s
s) Maybe (Debugger s)
debugger
    Solver
pSolver <- QueuingFlag -> Backend -> IO Solver
Backend.initSolver QueuingFlag
Backend.Queuing (Backend -> IO Solver) -> Backend -> IO Solver
forall a b. (a -> b) -> a -> b
$ Handle -> Backend
Process.toBackend Handle
handle

    let problem :: Seq Builder
problem = s -> Seq Builder
forall a. RenderSeq a => a -> Seq Builder
renderSeq s
s
    IO () -> (Debugger s -> IO ()) -> Maybe (Debugger s) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger s -> Seq Builder -> IO ()
forall s. Debugger s -> Seq Builder -> IO ()
`debugProblem` Seq Builder
problem) Maybe (Debugger s)
debugger

    Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
problem (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)
    ByteString
resultResponse <- Solver -> Builder -> IO ByteString
Backend.command Solver
pSolver Builder
"(check-sat)"
    IO () -> (Debugger s -> IO ()) -> Maybe (Debugger s) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger s -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
`debugResultResponse` ByteString
resultResponse) Maybe (Debugger s)
debugger

    ByteString
modelResponse  <- Solver -> Builder -> IO ByteString
Backend.command Solver
pSolver Builder
"(get-model)"
    IO () -> (Debugger s -> IO ()) -> Maybe (Debugger s) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger s -> ByteString -> IO ()
forall s. Debugger s -> ByteString -> IO ()
`debugModelResponse` ByteString
modelResponse) Maybe (Debugger s)
debugger

    case Parser Result -> ByteString -> Either [Char] Result
forall a. Parser a -> ByteString -> Either [Char] a
parseOnly Parser Result
resultParser (ByteString -> ByteString
toStrict ByteString
resultResponse) of
      Left [Char]
e    -> [Char] -> IO (Result, Solution)
forall a. [Char] -> IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
e
      Right Result
res -> case Result
res of
        Result
Unsat -> (Result, Solution) -> IO (Result, Solution)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
res, Solution
forall a. Monoid a => a
mempty)
        Result
_     -> case Parser Solution -> ByteString -> Either [Char] Solution
forall a. Parser a -> ByteString -> Either [Char] a
parseOnly Parser Solution
anyModelParser (ByteString -> ByteString
toStrict ByteString
modelResponse) of
          Left [Char]
e    -> [Char] -> IO (Result, Solution)
forall a. [Char] -> IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
e
          Right Solution
sol -> (Result, Solution) -> IO (Result, Solution)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
res, Solution
sol)