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