module Language.Fixpoint.Smt.Types (
Raw
, Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, SMTEnv, emptySMTEnv, SMTSt(..), withExtendedEnv, SMT2, freshSym
, TheorySymbol (..)
, format
) where
import Language.Fixpoint.Types
import qualified Data.Text.Format as DTF
import Data.Text.Format.Params (Params)
import qualified Data.Text as T
import qualified Data.Text.Lazy as LT
import System.IO (Handle)
import System.Process
import Control.Monad.State
type Raw = T.Text
data Command = Push
| Pop
| CheckSat
| Declare Symbol [Sort] Sort
| Define Sort
| Assert (Maybe Int) Expr
| Distinct [Expr]
| GetValue [Symbol]
| CMany [Command]
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
, smtenv :: SMTEnv
}
data TheorySymbol = Thy { tsSym :: Symbol
, tsRaw :: Raw
, tsSort :: Sort
}
deriving (Eq, Ord, Show)
format :: Params ps => DTF.Format -> ps -> T.Text
format f x = LT.toStrict $ DTF.format f x
type SMTEnv = SEnv Sort
data SMTSt = SMTSt {fresh :: Int , smt2env :: SMTEnv}
type SMT2 = State SMTSt
emptySMTEnv = emptySEnv
withExtendedEnv bs act = do
env <- smt2env <$> get
let env' = foldl (\env (x, t) -> insertSEnv x t env) env bs
modify $ \s -> s{smt2env = env'}
r <- act
modify $ \s -> s{smt2env = env}
return r
freshSym = do
n <- fresh <$> get
modify $ \s -> s{fresh = n + 1}
return $ intSymbol "lambda_fun_" n
class SMTLIB2 a where
defunc :: a -> SMT2 a
defunc = return
smt2 :: a -> T.Text
runSmt2 :: SMTEnv -> a -> T.Text
runSmt2 env a = smt2 $ evalState (defunc a) (SMTSt 0 env)