module Language.Hasmtlib.Type.Solver where

import Language.Hasmtlib.Type.Pipe
import Language.Hasmtlib.Type.Option
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Codec
import qualified SMTLIB.Backends as B
import qualified SMTLIB.Backends.Process as P
import Data.Default
import Control.Monad.State

-- | Data that can have a 'B.Solver'.
class WithSolver a where
  withSolver :: B.Solver -> a

instance WithSolver Pipe where
  withSolver :: Solver -> Pipe
withSolver = Int -> Maybe String -> Solver -> Pipe
Pipe Int
0 Maybe String
forall a. Maybe a
Nothing

-- | @'solveWith' solver prob@ solves a SMT problem @prob@ with the given
-- @solver@. It returns a pair consisting of:
--
-- 1. A 'Result' that indicates if @prob@ is satisfiable ('Sat'),
--    unsatisfiable ('Unsat'), or if the solver could not determine any
--    results ('Unknown').
--
-- 2. A 'Decoded' answer that was decoded using the solution to @prob@. Note
--    that this answer is only meaningful if the 'Result' is 'Sat' or 'Unknown' and
--    the answer value is in a 'Just'.
--
-- Here is a small example of how to use 'solveWith':
--
-- @
-- import Language.Hasmtlib
--
-- main :: IO ()
-- main = do
--   res <- solveWith (solver cvc5) $ do
--     setLogic \"QF_LIA\"
-- 
--     x <- var @IntSort
-- 
--     assert $ x >? 0
--     
--     return x
-- 
--   print res
-- @
solveWith :: (Monad m, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
solveWith :: forall (m :: * -> *) s a.
(Monad m, Default s, Codec a) =>
Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
solveWith Solver s m
solver StateT s m a
m = do
  (a
a, s
problem) <- StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT s m a
m s
forall a. Default a => a
def
  (Result
result, Solution
solution) <- Solver s m
solver s
problem
    
  (Result, Maybe (Decoded a)) -> m (Result, Maybe (Decoded a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
result, Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
solution a
a)

-- | Pipes an SMT-problem interactively to the solver.
--   Enables incremental solving by default.
--   Here is a small example of how to use it for solving a problem utilizing the solvers incremental stack:
-- 
-- @
-- import Language.Hasmtlib
-- import Control.Monad.IO.Class
-- 
-- main :: IO ()
-- main = do
--   cvc5Living <- interactiveSolver cvc5
--   interactiveWith cvc5Living $ do
--     setOption $ ProduceModels True
--     setLogic \"QF_LIA\"
-- 
--     x <- var @IntSort
-- 
--     assert $ x >? 0
-- 
--     (res, sol) <- solve
--     liftIO $ print res
--     liftIO $ print $ decode sol x
-- 
--     push
--     y <- var @IntSort
-- 
--     assert $ y <? 0
--     assert $ x === y
-- 
--     res' <- checkSat
--     liftIO $ print res'
--     pop
-- 
--     res'' <- checkSat
--     liftIO $ print res''
-- 
--   return ()
-- @
interactiveWith :: (MonadIO m, WithSolver s) => (B.Solver, P.Handle) -> StateT s m () -> m ()
interactiveWith :: forall (m :: * -> *) s.
(MonadIO m, WithSolver s) =>
(Solver, Handle) -> StateT s m () -> m ()
interactiveWith (Solver
solver, Handle
handle) StateT s m ()
m = do
   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_ Solver
solver (Builder -> IO ()) -> Builder -> IO ()
forall a b. (a -> b) -> a -> b
$ SMTOption -> Builder
forall a. Render a => a -> Builder
render (Bool -> SMTOption
Incremental Bool
True)
   ((), s)
_ <- StateT s m () -> s -> m ((), s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT s m ()
m (s -> m ((), s)) -> s -> m ((), s)
forall a b. (a -> b) -> a -> b
$ Solver -> s
forall a. WithSolver a => Solver -> a
withSolver Solver
solver
   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
$ Handle -> IO ()
P.close Handle
handle