module Language.Fixpoint.Smt.Types (
Raw
, Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, TheorySymbol (..)
) where
import Language.Fixpoint.Config (SMTSolver (..))
import Language.Fixpoint.Errors
import Language.Fixpoint.Files
import Language.Fixpoint.Types
import Control.Applicative ((*>), (<$>), (<*), (<|>))
import Control.Monad
import Data.Char
import qualified Data.HashMap.Strict as M
import qualified Data.List as L
import Data.Monoid
import qualified Data.Text as T
import Data.Text.Format
import qualified Data.Text.IO as TIO
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.IO as LTIO
import System.Directory
import System.Exit hiding (die)
import System.FilePath
import System.IO (Handle, IOMode (..), hClose, hFlush,
openFile)
import System.Process
import qualified Data.Attoparsec.Text as A
type Raw = T.Text
data Command = Push
| Pop
| CheckSat
| Declare Symbol [Sort] Sort
| Define Sort
| Assert (Maybe Int) Pred
| Distinct [Expr]
| GetValue [Symbol]
deriving (Eq, Show)
data Response = Ok
| Sat
| Unsat
| Unknown
| Values [(Symbol, Raw)]
| Error Raw
deriving (Eq, Show)
data Context = Ctx { pId :: ProcessHandle
, cIn :: Handle
, cOut :: Handle
, cLog :: Maybe Handle
, verbose :: Bool
}
data TheorySymbol = Thy { tsSym :: Symbol
, tsRaw :: Raw
, tsSort :: Sort
}
deriving (Eq, Ord, Show)
class SMTLIB2 a where
smt2 :: a -> LT.Text