{-# LANGUAGE TemplateHaskell #-}

{- |
This module provides functions for having SMT-Problems solved by external solvers.

The base type for every solver is the 'SolverConfig'. It describes where the solver executable is located and how it should behave.
You can provide a time-out using the decorator 'timingout'.
Another decorator - 'debugging' - allows you to debug all the information you want. The actual debuggers can be found in "Language.Hasmtlib.Type.Debugger".
-}
module Language.Hasmtlib.Type.Solver
  (
  -- * Solver configuration

  -- ** Type
  SolverConfig(..)

  -- ** Decoration
  , debugging, timingout

  -- ** Lens
  , processConfig, mTimeout, mDebugger

  -- * Stateful solving
  , Solver, solver, solveWith

  -- * Interactive solving
  , interactiveWith

  -- ** Minimzation
  , solveMinimized

  -- ** Maximization
  , solveMaximized
  )
where

import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Internal.Parser
import Language.Hasmtlib.Type.MonadSMT
import Language.Hasmtlib.Type.Debugger
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 Data.ByteString.Lazy hiding (singleton)
import qualified SMTLIB.Backends as Backend
import qualified SMTLIB.Backends.Process as Process
import Data.Default
import Data.Maybe
import Data.Attoparsec.ByteString (parseOnly)
import Control.Lens hiding (op)
import Control.Monad
import Control.Monad.State
import Control.Monad.Trans.Control
import System.Timeout.Lifted

-- | Function that turns a state into a 'Result' and a 'Solution'.
type Solver s m = s -> m (Result, Solution)

-- | Configuration for solver processes.
data SolverConfig s = SolverConfig
  { forall s. SolverConfig s -> Config
_processConfig  :: Process.Config         -- ^ The underlying config of the process
  , forall s. SolverConfig s -> Maybe Int
_mTimeout       :: Maybe Int              -- ^ Timeout in microseconds
  , forall s. SolverConfig s -> Maybe (Debugger s)
_mDebugger      :: Maybe (Debugger s)     -- ^ Debugger for communication with external solver
  }
$(makeLenses ''SolverConfig)

-- | Creates 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,
--
-- 5. close the process and clean up all resources and
--
-- 6. return the decoded solution.
solver :: (RenderProblem s, MonadIO m) => SolverConfig s -> Solver s m
solver :: forall s (m :: * -> *).
(RenderProblem s, MonadIO m) =>
SolverConfig s -> Solver s m
solver (SolverConfig Config
cfg Maybe Int
mTO 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 os :: Seq Builder
os   = s -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderOptions s
s
        l :: Builder
l    = s -> Builder
forall s. RenderProblem s => s -> Builder
renderLogic s
s
        vs :: Seq Builder
vs   = s -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderDeclareVars s
s
        as :: Seq Builder
as   = s -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderAssertions s
s
        sas :: Seq Builder
sas  = s -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderSoftAssertions s
s
        mins :: Seq Builder
mins = s -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderMinimizations s
s
        maxs :: Seq Builder
maxs = s -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderMaximizations 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 (Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
os ((Builder -> IO ()) -> IO ())
-> (Debugger s -> Builder -> IO ()) -> Debugger s -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugOption) 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
os (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)
    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 -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
`debugLogic` Builder
l) Maybe (Debugger s)
debugger
    Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver Builder
l
    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 (Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
vs ((Builder -> IO ()) -> IO ())
-> (Debugger s -> Builder -> IO ()) -> Debugger s -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugVar) 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
vs (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)
    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 (Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
as ((Builder -> IO ()) -> IO ())
-> (Debugger s -> Builder -> IO ()) -> Debugger s -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugAssert) 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
as (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)
    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 (Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
sas ((Builder -> IO ()) -> IO ())
-> (Debugger s -> Builder -> IO ()) -> Debugger s -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugAssertSoft) 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
sas (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)
    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 (Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
mins ((Builder -> IO ()) -> IO ())
-> (Debugger s -> Builder -> IO ()) -> Debugger s -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMinimize) 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
mins (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)
    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 (Seq Builder -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Seq Builder
maxs ((Builder -> IO ()) -> IO ())
-> (Debugger s -> Builder -> IO ()) -> Debugger s -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Debugger s -> Builder -> IO ()
forall s. Debugger s -> Builder -> IO ()
debugMaximize) 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
maxs (Solver -> Builder -> IO ()
Backend.command_ Solver
pSolver)

    let timingOut :: IO ByteString -> IO ByteString
timingOut IO ByteString
io = case Maybe Int
mTO of
          Maybe Int
Nothing -> IO ByteString
io
          Just Int
t -> ByteString -> Maybe ByteString -> ByteString
forall a. a -> Maybe a -> a
fromMaybe ByteString
"unknown" (Maybe ByteString -> ByteString)
-> IO (Maybe ByteString) -> IO ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO ByteString -> IO (Maybe ByteString)
forall (m :: * -> *) a.
MonadBaseControl IO m =>
Int -> m a -> m (Maybe a)
timeout Int
t IO ByteString
io
    ByteString
resultResponse <- IO ByteString -> IO ByteString
timingOut (IO ByteString -> IO ByteString) -> IO ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ByteString
Backend.command Solver
pSolver Builder
renderCheckSat
    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
renderGetModel
    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 String Result
forall a. Parser a -> ByteString -> Either String a
parseOnly Parser Result
resultParser (ByteString -> ByteString
toStrict ByteString
resultResponse) of
      Left String
e    -> String -> IO (Result, Solution)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
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 String Solution
forall a. Parser a -> ByteString -> Either String a
parseOnly Parser Solution
anyModelParser (ByteString -> ByteString
toStrict ByteString
modelResponse) of
          Left String
e    -> String -> IO (Result, Solution)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
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)

-- | Decorates a 'SolverConfig' with a timeout. The timeout is given as an 'Int' which specifies
--   after how many __microseconds__ the external solver process shall time out on @(check-sat)@.
--
--   When timing out, the 'Result' will always be 'Unknown'.
--
--   This uses 'timeout' internally.
timingout :: Int -> SolverConfig s -> SolverConfig s
timingout :: forall s. Int -> SolverConfig s -> SolverConfig s
timingout Int
t SolverConfig s
cfg = SolverConfig s
cfg SolverConfig s
-> (SolverConfig s -> SolverConfig s) -> SolverConfig s
forall a b. a -> (a -> b) -> b
& (Maybe Int -> Identity (Maybe Int))
-> SolverConfig s -> Identity (SolverConfig s)
forall s (f :: * -> *).
Functor f =>
(Maybe Int -> f (Maybe Int))
-> SolverConfig s -> f (SolverConfig s)
mTimeout ((Maybe Int -> Identity (Maybe Int))
 -> SolverConfig s -> Identity (SolverConfig s))
-> Int -> SolverConfig s -> SolverConfig s
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ Int
t

-- | Decorates a 'SolverConfig' with a 'Debugger'.
debugging :: Debugger s -> SolverConfig s -> SolverConfig s
debugging :: forall s. Debugger s -> SolverConfig s -> SolverConfig s
debugging Debugger s
debugger SolverConfig s
cfg = SolverConfig s
cfg SolverConfig s
-> (SolverConfig s -> SolverConfig s) -> SolverConfig s
forall a b. a -> (a -> b) -> b
& (Maybe (Debugger s) -> Identity (Maybe (Debugger s)))
-> SolverConfig s -> Identity (SolverConfig s)
forall s s (f :: * -> *).
Functor f =>
(Maybe (Debugger s) -> f (Maybe (Debugger s)))
-> SolverConfig s -> f (SolverConfig s)
mDebugger ((Maybe (Debugger s) -> Identity (Maybe (Debugger s)))
 -> SolverConfig s -> Identity (SolverConfig s))
-> Debugger s -> SolverConfig s -> SolverConfig s
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ Debugger s
debugger

-- | @'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
solving 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
solving 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
--   interactiveWith z3 $ do
--     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 :: (MonadIO m, MonadBaseControl IO m) => SolverConfig Pipe -> StateT Pipe m a -> m (Maybe a)
interactiveWith :: forall (m :: * -> *) a.
(MonadIO m, MonadBaseControl IO m) =>
SolverConfig Pipe -> StateT Pipe m a -> m (Maybe a)
interactiveWith SolverConfig Pipe
cfg StateT Pipe m a
m = do
  Handle
handle <- IO Handle -> m Handle
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Handle -> m Handle) -> IO Handle -> m Handle
forall a b. (a -> b) -> a -> b
$ Config -> IO Handle
Process.new (Config -> IO Handle) -> Config -> IO Handle
forall a b. (a -> b) -> a -> b
$ SolverConfig Pipe
cfgSolverConfig Pipe
-> Getting Config (SolverConfig Pipe) Config -> Config
forall s a. s -> Getting a s a -> a
^.Getting Config (SolverConfig Pipe) Config
forall s (f :: * -> *).
Functor f =>
(Config -> f Config) -> SolverConfig s -> f (SolverConfig s)
processConfig
  Solver
processSolver <- IO Solver -> m Solver
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Solver -> m Solver) -> IO Solver -> m Solver
forall a b. (a -> b) -> a -> b
$ 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 timingOut :: m (a, Pipe) -> m (Maybe (a, Pipe))
timingOut m (a, Pipe)
io = case SolverConfig Pipe
cfgSolverConfig Pipe
-> Getting (Maybe Int) (SolverConfig Pipe) (Maybe Int) -> Maybe Int
forall s a. s -> Getting a s a -> a
^.Getting (Maybe Int) (SolverConfig Pipe) (Maybe Int)
forall s (f :: * -> *).
Functor f =>
(Maybe Int -> f (Maybe Int))
-> SolverConfig s -> f (SolverConfig s)
mTimeout of
        Maybe Int
Nothing -> (a, Pipe) -> Maybe (a, Pipe)
forall a. a -> Maybe a
Just ((a, Pipe) -> Maybe (a, Pipe))
-> m (a, Pipe) -> m (Maybe (a, Pipe))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a, Pipe)
io
        Just Int
t -> Int -> m (a, Pipe) -> m (Maybe (a, Pipe))
forall (m :: * -> *) a.
MonadBaseControl IO m =>
Int -> m a -> m (Maybe a)
timeout Int
t m (a, Pipe)
io
  Maybe (a, Pipe)
ma <- m (a, Pipe) -> m (Maybe (a, Pipe))
timingOut (m (a, Pipe) -> m (Maybe (a, Pipe)))
-> m (a, Pipe) -> m (Maybe (a, Pipe))
forall a b. (a -> b) -> a -> b
$ StateT Pipe m a -> Pipe -> m (a, Pipe)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT Pipe m a
m (Pipe -> m (a, Pipe)) -> Pipe -> m (a, Pipe)
forall a b. (a -> b) -> a -> b
$ Int
-> Maybe String
-> SharingMode
-> HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> Seq (Seq (StableName ()))
-> Solver
-> Maybe (Debugger Pipe)
-> 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 Solver
processSolver (SolverConfig Pipe
cfgSolverConfig Pipe
-> Getting
     (Maybe (Debugger Pipe)) (SolverConfig Pipe) (Maybe (Debugger Pipe))
-> Maybe (Debugger Pipe)
forall s a. s -> Getting a s a -> a
^.Getting
  (Maybe (Debugger Pipe)) (SolverConfig Pipe) (Maybe (Debugger Pipe))
forall s s (f :: * -> *).
Functor f =>
(Maybe (Debugger s) -> f (Maybe (Debugger s)))
-> SolverConfig s -> f (SolverConfig s)
mDebugger)
  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
  Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ ((a, Pipe) -> a) -> Maybe (a, Pipe) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Pipe) -> a
forall a b. (a, b) -> a
fst Maybe (a, Pipe)
ma

-- | 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