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

module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where

import Copilot.Theorem.IL

import System.IO

class Show a => SmtFormat a where
   push            :: a
   pop             :: a
   checkSat        :: a
   setLogic        :: String -> a
   declFun         :: String -> Type -> [Type] -> a
   assert          :: Expr -> a

data Backend a = Backend
  { Backend a -> String
name            :: String
  , Backend a -> String
cmd             :: String
  , Backend a -> [String]
cmdOpts         :: [String]
  , Backend a -> Handle -> IO ()
inputTerminator :: Handle -> IO ()
  , Backend a -> Bool
incremental     :: Bool
  , Backend a -> String
logic           :: String
  , Backend a -> String -> Maybe SatResult
interpret       :: String -> Maybe SatResult
  }

data SatResult = Sat | Unsat | Unknown