{- |
This module provides functions for having SMT-Problems solved by external solvers.
-}
module Language.Hasmtlib.Type.Solver
  (
  -- * WithSolver
  WithSolver(..)

  -- * Stateful solving
  , solveWith

  -- * Interactive solving
  , interactiveWith, debugInteractiveWith

  -- ** Minimzation
  , solveMinimized

  -- ** Maximization
  , solveMaximized
  )
where

import Language.Hasmtlib.Type.MonadSMT
import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Type.Pipe
import Language.Hasmtlib.Codec
import qualified SMTLIB.Backends as Backend
import qualified SMTLIB.Backends.Process as Process
import Data.Default
import Data.Maybe
import Control.Monad.State

-- | Data that can have a 'Backend.Solver' which may be debugged.
class WithSolver a where
  -- | Create a value with a 'Backend.Solver' and a 'Bool' for whether to debug the 'Backend.Solver'.
  withSolver :: Backend.Solver -> Bool -> a

instance WithSolver Pipe where
  withSolver :: Solver -> Bool -> Pipe
withSolver = Int
-> Maybe String
-> SharingMode
-> HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> Seq (Seq (StableName ()))
-> Solver
-> Bool
-> Pipe
Pipe Int
0 Maybe String
forall a. Maybe a
Nothing SharingMode
forall a. Default a => a
def HashMap (StableName ()) (SomeKnownSMTSort Expr)
forall a. Monoid a => a
mempty Seq (Seq (StableName ()))
forall a. Monoid a => a
mempty

-- | @'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'.
--
-- ==== __Example__
--
-- @
-- import Language.Hasmtlib
--
-- main :: IO ()
-- main = do
--   res <- solveWith @SMT (solver cvc5) $ do
--     setLogic \"QF_LIA\"
--
--     x <- var \@IntSort
--
--     assert $ x >? 0
--
--     return x
--
--   print res
-- @
--
-- The solver will probably answer with @x := 1@.
solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
solveWith :: forall s (m :: * -> *) a.
(Default s, Monad m, 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.
--
-- ==== __Example__
--
-- @
-- import Language.Hasmtlib
-- import Control.Monad.IO.Class
--
-- main :: IO ()
-- main = do
--   cvc5Living <- interactiveSolver cvc5
--   interactiveWith @Pipe cvc5Living $ do
--     setOption $ Incremental True
--     setOption $ ProduceModels True
--     setLogic \"QF_LRA\"
--
--     x <- var \@RealSort
--
--     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 :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()
interactiveWith :: forall s (m :: * -> *).
(WithSolver s, MonadIO m) =>
(Solver, Handle) -> StateT s m () -> m ()
interactiveWith (Solver
solver, Handle
handle) StateT s m ()
m = do
  ((), 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 -> Bool -> s
forall a. WithSolver a => Solver -> Bool -> a
withSolver Solver
solver Bool
False
  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 ()
Process.close Handle
handle

-- | Like 'interactiveWith' but it prints all communication with the solver to console.
debugInteractiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()
debugInteractiveWith :: forall s (m :: * -> *).
(WithSolver s, MonadIO m) =>
(Solver, Handle) -> StateT s m () -> m ()
debugInteractiveWith (Solver
solver, Handle
handle) StateT s m ()
m = do
  ((), 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 -> Bool -> s
forall a. WithSolver a => Solver -> Bool -> a
withSolver Solver
solver Bool
True
  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 ()
Process.close Handle
handle

-- | Solves the current problem with respect to a minimal solution for a given numerical expression.
--
--   This is done by incrementally refining the upper bound for a given target.
--   Terminates, when setting the last intermediate result as new upper bound results in 'Unsat'.
--   Then removes that last assertion and returns the previous (now confirmed minimal) result.
--
--   You can also provide a step-size. You do not have to worry about stepping over the optimal result.
--   This implementation takes care of it.
--
--   Access to intermediate results is also possible via an 'IO'-Action.
--
-- ==== __Examples__
--
-- @
-- x <- var \@IntSort
-- assert $ x >? 4
-- solveMinimized x Nothing Nothing
-- @
--
-- The solver will return @x := 5@.
--
-- The first 'Nothing' indicates that each intermediate result will be set as next upper bound.
-- The second 'Nothing' shows that we do not care about intermediate, but only the final (minimal) result.
--
-- @
-- x <- var \@IntSort
-- assert $ x >? 4
-- solveMinimized x (Just (\\r -> r-1)) (Just print)
-- @
--
-- The solver will still return @x := 5@.
--
-- However, here we want the next bound of each refinement to be @lastResult - 1@.
-- Also, every intermediate result is printed.
solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
  => Expr t                             -- ^ Target to minimize
  -> Maybe (Expr t -> Expr t)           -- ^ Step-size: Lambda is given last result as argument, producing the next upper bound
  -> Maybe (Solution -> IO ())          -- ^ Accessor to intermediate results
  -> m (Result, Solution)
solveMinimized :: forall (m :: * -> *) (t :: SMTSort).
(MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t,
 Orderable (Expr t)) =>
Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
solveMinimized = (Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
forall (m :: * -> *) (t :: SMTSort).
(MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t) =>
(Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
solveOptimized Expr t -> Expr t -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<?)

-- | Solves the current problem with respect to a maximal solution for a given numerical expression.
--
--   This is done by incrementally refining the lower bound for a given target.
--   Terminates, when setting the last intermediate result as new lower bound results in 'Unsat'.
--   Then removes that last assertion and returns the previous (now confirmed maximal) result.
--
--   You can also provide a step-size. You do not have to worry about stepping over the optimal result.
--   This implementation takes care of it.
--
--   Access to intermediate results is also possible via an 'IO'-Action.
--
-- ==== __Examples__
--
-- @
-- x <- var \@IntSort
-- assert $ x <? 4
-- solveMaximized x Nothing Nothing
-- @
--
-- The solver will return @x := 3@.
--
-- The first 'Nothing' indicates that each intermediate result will be set as next lower bound.
-- The second 'Nothing' shows that we do not care about intermediate, but only the final (maximal) result.
--
-- @
-- x <- var \@IntSort
-- assert $ x <? 4
-- solveMinimized x (Just (+1)) (Just print)
-- @
--
-- The solver will still return @x := 3@.
--
-- However, here we want the next bound of each refinement to be @lastResult + 1@.
-- Also, every intermediate result is printed.
solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
  => Expr t                             -- ^ Target to maximize
  -> Maybe (Expr t -> Expr t)           -- ^ Step-size: Lambda is given last result as argument, producing the next lower bound
  -> Maybe (Solution -> IO ())          -- ^ Accessor to intermediate results
  -> m (Result, Solution)
solveMaximized :: forall (m :: * -> *) (t :: SMTSort).
(MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t,
 Orderable (Expr t)) =>
Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
solveMaximized = (Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
forall (m :: * -> *) (t :: SMTSort).
(MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t) =>
(Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
solveOptimized Expr t -> Expr t -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>?)

solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)
  => (Expr t -> Expr t -> Expr BoolSort)
  -> Expr t
  -> Maybe (Expr t -> Expr t)
  -> Maybe (Solution -> IO ())
  -> m (Result, Solution)
solveOptimized :: forall (m :: * -> *) (t :: SMTSort).
(MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t) =>
(Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
solveOptimized Expr t -> Expr t -> Expr 'BoolSort
op Expr t
goal Maybe (Expr t -> Expr t)
mStep Maybe (Solution -> IO ())
mDebug = Result -> Solution -> Expr t -> m (Result, Solution)
refine Result
Unknown Solution
forall a. Monoid a => a
mempty Expr t
goal
  where
    refine :: Result -> Solution -> Expr t -> m (Result, Solution)
refine Result
oldRes Solution
oldSol Expr t
target = do
      Result
res <- m Result
forall s (m :: * -> *). MonadIncrSMT s m => m Result
checkSat
      case Result
res of
        Result
Sat   -> do
          Solution
sol <- m Solution
forall s (m :: * -> *). MonadIncrSMT s m => m Solution
getModel
          case Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
sol Expr t
target of
            Maybe (Decoded (Expr t))
Nothing        -> (Result, Solution) -> m (Result, Solution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
Sat, Solution
forall a. Monoid a => a
mempty)
            Just Decoded (Expr t)
targetSol -> do
              case Maybe (Solution -> IO ())
mDebug of
                Maybe (Solution -> IO ())
Nothing    -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                Just Solution -> IO ()
debug -> 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
$ Solution -> IO ()
debug Solution
sol
              m ()
forall s (m :: * -> *). MonadIncrSMT s m => m ()
push
              let step :: Expr t -> Expr t
step = (Expr t -> Expr t) -> Maybe (Expr t -> Expr t) -> Expr t -> Expr t
forall a. a -> Maybe a -> a
fromMaybe Expr t -> Expr t
forall a. a -> a
id Maybe (Expr t -> Expr t)
mStep
              Expr 'BoolSort -> m ()
forall s (m :: * -> *). MonadSMT s m => Expr 'BoolSort -> m ()
assert (Expr 'BoolSort -> m ()) -> Expr 'BoolSort -> m ()
forall a b. (a -> b) -> a -> b
$ Expr t
target Expr t -> Expr t -> Expr 'BoolSort
`op` Expr t -> Expr t
step (Decoded (Expr t) -> Expr t
forall a. Codec a => Decoded a -> a
encode Decoded (Expr t)
targetSol)
              Result -> Solution -> Expr t -> m (Result, Solution)
refine Result
res Solution
sol Expr t
target
        Result
_ -> do
          m ()
forall s (m :: * -> *). MonadIncrSMT s m => m ()
pop
          case Maybe (Expr t -> Expr t)
mStep of
            Maybe (Expr t -> Expr t)
Nothing -> (Result, Solution) -> m (Result, Solution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
oldRes, Solution
oldSol)
            Just Expr t -> Expr t
_  -> (Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
forall (m :: * -> *) (t :: SMTSort).
(MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t) =>
(Expr t -> Expr t -> Expr 'BoolSort)
-> Expr t
-> Maybe (Expr t -> Expr t)
-> Maybe (Solution -> IO ())
-> m (Result, Solution)
solveOptimized Expr t -> Expr t -> Expr 'BoolSort
op Expr t
goal Maybe (Expr t -> Expr t)
forall a. Maybe a
Nothing Maybe (Solution -> IO ())
mDebug -- make sure the very last step did not skip the optimal result