content: {-# 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
    { name            :: String
    , cmd             :: String
    , cmdOpts         :: [String]
    , inputTerminator :: Handle -> IO ()
    , incremental     :: Bool
    , logic           :: String
    , interpret       :: String -> Maybe SatResult
    }
  
  -- | Satisfiability result communicated by the SMT solver or theorem prover.
  data SatResult = Sat | Unsat | Unknown
  