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