    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE Safe       #-}

    -- | Backend to  SMT solvers and theorem provers.
    --
    -- This module provides three definitions:
    --
    -- - A class ('SmtFormat') abstracting over the language used to communicate the
    -- desired commands to an SMT solver or theorem prover.
    --
    -- - A class ('Backend') abstracting over the backend, which includes the name of
    -- the executable, any options and flags necessary, and functions to parse the
    -- results and close the communication.
    --
    -- - A type ('SatResult') representing a satisfiability result communicated by
    -- the SMT solver or theorem prover.
    module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where

    import Copilot.Theorem.IL

    import System.IO

    -- | Format of SMT-Lib commands.
    class Show a => SmtFormat a where
       push            :: a
       pop             :: a
       checkSat        :: a
       setLogic        :: String -> a
       declFun         :: String -> Type -> [Type] -> a
       assert          :: Expr -> a

    -- | Backend to an SMT solver or theorem prover.
    data Backend a = Backend
      { forall a. Backend a -> String
    name            :: String
      , forall a. Backend a -> String
    cmd             :: String
      , forall a. Backend a -> [String]
    cmdOpts         :: [String]
      , forall a. Backend a -> Handle -> IO ()
    inputTerminator :: Handle -> IO ()
      , forall a. Backend a -> Bool
    incremental     :: Bool
      , forall a. Backend a -> String
    logic           :: String
      , forall a. Backend a -> String -> Maybe SatResult
    interpret       :: String -> Maybe SatResult
      }

    -- | Satisfiability result communicated by the SMT solver or theorem prover.
    data SatResult = Sat | Unsat | Unknown