module Language.Hasmtlib.Solver.Common where

import Language.Hasmtlib.Type.SMT
import Language.Hasmtlib.Type.Solution
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 P
import qualified SMTLIB.Backends as B

-- | A newtype-wrapper for 'P.Config' which configures a solver via external process.
newtype ProcessSolver = ProcessSolver { ProcessSolver -> Config
conf :: P.Config }

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

-- | Creates a debugging 'Solver' from a 'ProcessSolver'
debug :: MonadIO m => ProcessSolver -> Solver SMT m
debug :: forall (m :: * -> *). MonadIO m => ProcessSolver -> Solver SMT m
debug (ProcessSolver Config
cfg) = Config -> Maybe Debugger -> Solver SMT m
forall (m :: * -> *).
MonadIO m =>
Config -> Maybe Debugger -> Solver SMT m
processSolver Config
cfg (Maybe Debugger -> Solver SMT m) -> Maybe Debugger -> Solver SMT m
forall a b. (a -> b) -> a -> b
$ Debugger -> Maybe Debugger
forall a. a -> Maybe a
Just Debugger
forall a. Default a => a
def

-- | Creates an interactive session with a solver by creating and returning an alive process-handle 'P.Handle'.
interactiveSolver :: MonadIO m => ProcessSolver -> m (B.Solver, P.Handle)
interactiveSolver :: forall (m :: * -> *).
MonadIO m =>
ProcessSolver -> m (Solver, Handle)
interactiveSolver (ProcessSolver 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
P.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
B.initSolver QueuingFlag
B.Queuing (Backend -> IO Solver) -> Backend -> IO Solver
forall a b. (a -> b) -> a -> b
$ Handle -> Backend
P.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 to execute for debugging 'SMT' solving.
data Debugger = Debugger
  { Debugger -> SMT -> IO ()
debugSMT            :: SMT -> IO ()
  , Debugger -> Seq Builder -> IO ()
debugProblem        :: Seq Builder -> IO ()
  , Debugger -> ByteString -> IO ()
debugResultResponse :: ByteString -> IO ()
  , Debugger -> ByteString -> IO ()
debugModelResponse  :: ByteString -> IO ()
  }

instance Default Debugger where
  def :: Debugger
def = Debugger
    { debugSMT :: SMT -> IO ()
debugSMT            = \SMT
smt -> 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
smtSMT
-> 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
smtSMT
-> 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
    }

-- | 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 :: MonadIO m => P.Config -> Maybe Debugger -> Solver SMT m
processSolver :: forall (m :: * -> *).
MonadIO m =>
Config -> Maybe Debugger -> Solver SMT m
processSolver Config
cfg Maybe Debugger
debugger SMT
smt = 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
P.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 -> IO ()) -> Maybe Debugger -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger -> SMT -> IO ()
`debugSMT` SMT
smt) Maybe Debugger
debugger
    Solver
pSolver <- QueuingFlag -> Backend -> IO Solver
B.initSolver QueuingFlag
B.Queuing (Backend -> IO Solver) -> Backend -> IO Solver
forall a b. (a -> b) -> a -> b
$ Handle -> Backend
P.toBackend Handle
handle

    let problem :: Seq Builder
problem = SMT -> Seq Builder
renderSMT SMT
smt
    IO () -> (Debugger -> IO ()) -> Maybe Debugger -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger -> Seq Builder -> IO ()
`debugProblem` Seq Builder
problem) Maybe Debugger
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 ()
B.command_ Solver
pSolver)
    ByteString
resultResponse <- Solver -> Builder -> IO ByteString
B.command Solver
pSolver Builder
"(check-sat)"
    IO () -> (Debugger -> IO ()) -> Maybe Debugger -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger -> ByteString -> IO ()
`debugResultResponse` ByteString
resultResponse) Maybe Debugger
debugger

    ByteString
modelResponse  <- Solver -> Builder -> IO ByteString
B.command Solver
pSolver Builder
"(get-model)"
    IO () -> (Debugger -> IO ()) -> Maybe Debugger -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty (Debugger -> ByteString -> IO ()
`debugModelResponse` ByteString
modelResponse) Maybe Debugger
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)