    {-# LANGUAGE NamedFieldPuns #-}
    {-# LANGUAGE RankNTypes     #-}
    {-# LANGUAGE Safe           #-}
    {-# LANGUAGE ViewPatterns   #-}

    -- | Communication with SMT solvers or theorem provers.
    --
    -- A solver is a running process defined by a 'Backend'.
    module Copilot.Theorem.Prover.SMTIO
      ( Solver
      , startNewSolver, stop
      , assume, entailed, declVars
      ) where

    import Copilot.Theorem.IL
    import Copilot.Theorem.Prover.Backend

    import System.IO
    import System.Process
    import Control.Monad
    import Control.Monad.Trans
    import Control.Monad.Trans.Maybe
    import Data.Maybe
    import Data.Set ((\\), fromList, Set, union, empty, elems)

    -- | A connection with a running SMT solver or theorem prover.
    data Solver a = Solver
      { forall a. Solver a -> String
    solverName :: String
      , forall a. Solver a -> Handle
    inh        :: Handle
      , forall a. Solver a -> Handle
    outh       :: Handle
      , forall a. Solver a -> ProcessHandle
    process    :: ProcessHandle
      , forall a. Solver a -> Bool
    debugMode  :: Bool
      , forall a. Solver a -> Set VarDescr
    vars       :: Set VarDescr
      , forall a. Solver a -> Set Expr
    model      :: Set Expr
      , forall a. Solver a -> Backend a
    backend    :: Backend a
      }

    -- | Output a debugging message if debugging is enabled for the solver.
    debug :: Bool -> Solver a -> String -> IO ()
    debug :: forall a. Bool -> Solver a -> String -> IO ()
    debug Bool
    printName Solver a
    s String
    str = Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Solver a -> Bool
    forall a. Solver a -> Bool
    debugMode Solver a
    s) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
      String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ (if Bool
    printName then String
    "<" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Solver a -> String
    forall a. Solver a -> String
    solverName Solver a
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ">  " else String
    "") String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    str

    send :: Show a => Solver a -> a -> IO ()
    send :: forall a. Show a => Solver a -> a -> IO ()
    send Solver a
    _ (a -> String
    forall a. Show a => a -> String
    show -> String
    "") = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    send Solver a
    s (a -> String
    forall a. Show a => a -> String
    show -> String
    a) = do
        Handle -> String -> IO ()
    hPutStr (Solver a -> Handle
    forall a. Solver a -> Handle
    inh Solver a
    s) (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n"
        Bool -> Solver a -> String -> IO ()
    forall a. Bool -> Solver a -> String -> IO ()
    debug Bool
    True Solver a
    s String
    a
        Handle -> IO ()
    hFlush (Handle -> IO ()) -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Handle
    forall a. Solver a -> Handle
    inh Solver a
    s

    receive :: Solver a -> IO SatResult
    receive :: forall a. Solver a -> IO SatResult
    receive Solver a
    s = Maybe SatResult -> SatResult
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe SatResult -> SatResult)
    -> IO (Maybe SatResult) -> IO SatResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT IO SatResult -> IO (Maybe SatResult)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT ([MaybeT IO SatResult] -> MaybeT IO SatResult
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ([MaybeT IO SatResult] -> MaybeT IO SatResult)
    -> [MaybeT IO SatResult] -> MaybeT IO SatResult
    forall a b. (a -> b) -> a -> b
    $ MaybeT IO SatResult -> [MaybeT IO SatResult]
    forall a. a -> [a]
    repeat MaybeT IO SatResult
    line)
      where
        line :: MaybeT IO SatResult
        line :: MaybeT IO SatResult
    line = do
          eof <- IO Bool -> MaybeT IO Bool
    forall a. IO a -> MaybeT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> MaybeT IO Bool) -> IO Bool -> MaybeT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Handle -> IO Bool
    hIsEOF (Handle -> IO Bool) -> Handle -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Handle
    forall a. Solver a -> Handle
    outh Solver a
    s
          if eof
            then liftIO (debug True s "[received: EOF]") >> return Unknown
            else do
              ln <- liftIO $ hGetLine $ outh s
              liftIO $ debug True s $ "[received: " ++ ln ++ "]"
              MaybeT $ return $ (interpret $ backend s) ln

    -- | Create a new solver implemented by the backend specified.
    --
    -- The error handle from the backend handle is immediately closed/discarded,
    -- and the logic initialized as specifiied by the backend options.
    startNewSolver :: SmtFormat a => String -> Bool -> Backend a -> IO (Solver a)
    startNewSolver :: forall a.
    SmtFormat a =>
    String -> Bool -> Backend a -> IO (Solver a)
    startNewSolver String
    name Bool
    dbgMode Backend a
    b = do
      (i, o, e, p) <- String
    -> [String]
    -> Maybe String
    -> Maybe [(String, String)]
    -> IO (Handle, Handle, Handle, ProcessHandle)
    runInteractiveProcess (Backend a -> String
    forall a. Backend a -> String
    cmd Backend a
    b) (Backend a -> [String]
    forall a. Backend a -> [String]
    cmdOpts Backend a
    b) Maybe String
    forall a. Maybe a
    Nothing Maybe [(String, String)]
    forall a. Maybe a
    Nothing
      hClose e
      let s = String
    -> Handle
    -> Handle
    -> ProcessHandle
    -> Bool
    -> Set VarDescr
    -> Set Expr
    -> Backend a
    -> Solver a
    forall a.
    String
    -> Handle
    -> Handle
    -> ProcessHandle
    -> Bool
    -> Set VarDescr
    -> Set Expr
    -> Backend a
    -> Solver a
    Solver String
    name Handle
    i Handle
    o ProcessHandle
    p Bool
    dbgMode Set VarDescr
    forall a. Set a
    empty Set Expr
    forall a. Set a
    empty Backend a
    b
      send s $ setLogic $ logic b
      return s

    -- | Stop a solver, closing all communication handles and terminating the
    -- process.
    stop :: Solver a -> IO ()
    stop :: forall a. Solver a -> IO ()
    stop Solver a
    s = do
      Handle -> IO ()
    hClose (Handle -> IO ()) -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Handle
    forall a. Solver a -> Handle
    inh Solver a
    s
      Handle -> IO ()
    hClose (Handle -> IO ()) -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Handle
    forall a. Solver a -> Handle
    outh Solver a
    s
      ProcessHandle -> IO ()
    terminateProcess (ProcessHandle -> IO ()) -> ProcessHandle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> ProcessHandle
    forall a. Solver a -> ProcessHandle
    process Solver a
    s

    -- | Register the given expressions as assumptions or axioms with the solver.
    assume :: SmtFormat a => Solver a -> [Expr] -> IO (Solver a)
    assume :: forall a. SmtFormat a => Solver a -> [Expr] -> IO (Solver a)
    assume s :: Solver a
    s@(Solver { Set Expr
    model :: forall a. Solver a -> Set Expr
    model :: Set Expr
    model }) [Expr]
    cs = do
      let newAxioms :: [Expr]
    newAxioms = Set Expr -> [Expr]
    forall a. Set a -> [a]
    elems (Set Expr -> [Expr]) -> Set Expr -> [Expr]
    forall a b. (a -> b) -> a -> b
    $ [Expr] -> Set Expr
    forall a. Ord a => [a] -> Set a
    fromList [Expr]
    cs Set Expr -> Set Expr -> Set Expr
    forall a. Ord a => Set a -> Set a -> Set a
    \\ Set Expr
    model
      Solver a -> [Expr] -> IO ()
    forall a. SmtFormat a => Solver a -> [Expr] -> IO ()
    assume' Solver a
    s [Expr]
    newAxioms
      Solver a -> IO (Solver a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solver a
    s { model = model `union` fromList newAxioms }

    assume' :: SmtFormat a => Solver a -> [Expr] -> IO ()
    assume' :: forall a. SmtFormat a => Solver a -> [Expr] -> IO ()
    assume' Solver a
    s [Expr]
    cs = [Expr] -> (Expr -> IO ()) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Expr]
    cs (Solver a -> a -> IO ()
    forall a. Show a => Solver a -> a -> IO ()
    send Solver a
    s (a -> IO ()) -> (Expr -> a) -> Expr -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> a
    forall a. SmtFormat a => Expr -> a
    assert (Expr -> a) -> (Expr -> Expr) -> Expr -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Expr
    bsimpl)

    -- | Check if a series of expressions are entailed by the axioms or assumptions
    -- already registered with the solver.
    entailed :: SmtFormat a => Solver a -> [Expr] -> IO SatResult
    entailed :: forall a. SmtFormat a => Solver a -> [Expr] -> IO SatResult
    entailed Solver a
    s [Expr]
    cs = do
      Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Backend a -> Bool
    forall a. Backend a -> Bool
    incremental (Backend a -> Bool) -> Backend a -> Bool
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Backend a
    forall a. Solver a -> Backend a
    backend Solver a
    s) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> a -> IO ()
    forall a. Show a => Solver a -> a -> IO ()
    send Solver a
    s a
    forall a. SmtFormat a => a
    push
      case [Expr]
    cs of
          []  -> String -> IO ()
    putStrLn String
    "Warning: no proposition to prove." IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Solver a -> [Expr] -> IO ()
    forall a. SmtFormat a => Solver a -> [Expr] -> IO ()
    assume' Solver a
    s [Bool -> Expr
    ConstB Bool
    True]
          [Expr]
    _   -> Solver a -> [Expr] -> IO ()
    forall a. SmtFormat a => Solver a -> [Expr] -> IO ()
    assume' Solver a
    s [(Expr -> Expr -> Expr) -> [Expr] -> Expr
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 (Type -> Op2 -> Expr -> Expr -> Expr
    Op2 Type
    Bool Op2
    Or) ((Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type -> Op1 -> Expr -> Expr
    Op1 Type
    Bool Op1
    Not) [Expr]
    cs)]
      Solver a -> a -> IO ()
    forall a. Show a => Solver a -> a -> IO ()
    send Solver a
    s a
    forall a. SmtFormat a => a
    checkSat
      (Backend a -> Handle -> IO ()
    forall a. Backend a -> Handle -> IO ()
    inputTerminator (Backend a -> Handle -> IO ()) -> Backend a -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Backend a
    forall a. Solver a -> Backend a
    backend Solver a
    s) (Solver a -> Handle
    forall a. Solver a -> Handle
    inh Solver a
    s)

      Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Backend a -> Bool
    forall a. Backend a -> Bool
    incremental (Backend a -> Bool) -> Backend a -> Bool
    forall a b. (a -> b) -> a -> b
    $ Solver a -> Backend a
    forall a. Solver a -> Backend a
    backend Solver a
    s) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Solver a -> a -> IO ()
    forall a. Show a => Solver a -> a -> IO ()
    send Solver a
    s a
    forall a. SmtFormat a => a
    pop
      Solver a -> IO SatResult
    forall a. Solver a -> IO SatResult
    receive Solver a
    s

    -- | Register the given variables with the solver.
    declVars :: SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a)
    declVars :: forall a. SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a)
    declVars s :: Solver a
    s@(Solver { Set VarDescr
    vars :: forall a. Solver a -> Set VarDescr
    vars :: Set VarDescr
    vars }) [VarDescr]
    decls = do
      let newVars :: [VarDescr]
    newVars = Set VarDescr -> [VarDescr]
    forall a. Set a -> [a]
    elems (Set VarDescr -> [VarDescr]) -> Set VarDescr -> [VarDescr]
    forall a b. (a -> b) -> a -> b
    $ [VarDescr] -> Set VarDescr
    forall a. Ord a => [a] -> Set a
    fromList [VarDescr]
    decls Set VarDescr -> Set VarDescr -> Set VarDescr
    forall a. Ord a => Set a -> Set a -> Set a
    \\ Set VarDescr
    vars
      [VarDescr] -> (VarDescr -> IO ()) -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [VarDescr]
    newVars ((VarDescr -> IO ()) -> IO ()) -> (VarDescr -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ \(VarDescr {String
    varName :: String
    varName :: VarDescr -> String
    varName, Type
    varType :: Type
    varType :: VarDescr -> Type
    varType, [Type]
    args :: [Type]
    args :: VarDescr -> [Type]
    args}) ->
        Solver a -> a -> IO ()
    forall a. Show a => Solver a -> a -> IO ()
    send Solver a
    s (a -> IO ()) -> a -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> Type -> [Type] -> a
    forall a. SmtFormat a => String -> Type -> [Type] -> a
    declFun String
    varName Type
    varType [Type]
    args
      Solver a -> IO (Solver a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solver a
    s { vars = vars `union` fromList newVars }