module Language.Fixpoint.Smt.Types (
Raw
, symbolBuilder
, Command (..)
, Response (..)
, SMTLIB2 (..)
, runSmt2
, Context (..)
, TheorySymbol (..)
, SMTEnv
) where
import Language.Fixpoint.Types
import qualified Data.Text as T
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.Builder as LT
import Text.PrettyPrint.HughesPJ
import System.IO (Handle)
import System.Process
type Raw = LT.Text
symbolBuilder :: Symbol -> LT.Builder
symbolBuilder = LT.fromText . symbolSafeText
data Command = Push
| Pop
| CheckSat
| Declare !Symbol [Sort] !Sort
| Define !Sort
| Assert !(Maybe Int) !Expr
| AssertAxiom !(Triggered Expr)
| Distinct [Expr]
| GetValue [Symbol]
| CMany [Command]
deriving (Eq, Show)
instance PPrint Command where
pprintTidy _ = ppCmd
ppCmd :: Command -> Doc
ppCmd Push = text "Push"
ppCmd Pop = text "Pop"
ppCmd CheckSat = text "CheckSat"
ppCmd (Declare {}) = text "Declare ..."
ppCmd (Define {}) = text "Define ..."
ppCmd (Assert _ e) = text "Assert" <+> pprint e
ppCmd (AssertAxiom _) = text "AssertAxiom ..."
ppCmd (Distinct {}) = text "Distinct ..."
ppCmd (GetValue {}) = text "GetValue ..."
ppCmd (CMany {}) = text "CMany ..."
data Response = Ok
| Sat
| Unsat
| Unknown
| Values [(Symbol, T.Text)]
| Error !T.Text
deriving (Eq, Show)
data Context = Ctx
{ ctxPid :: !ProcessHandle
, ctxCin :: !Handle
, ctxCout :: !Handle
, ctxLog :: !(Maybe Handle)
, ctxVerbose :: !Bool
, ctxExt :: !Bool
, ctxAeq :: !Bool
, ctxBeq :: !Bool
, ctxNorm :: !Bool
, ctxSmtEnv :: !SMTEnv
}
type SMTEnv = SEnv Sort
data TheorySymbol = Thy
{ tsSym :: !Symbol
, tsRaw :: !Raw
, tsSort :: !Sort
, tsInterp :: !Bool
}
deriving (Eq, Ord, Show)
class SMTLIB2 a where
smt2 :: a -> LT.Builder
runSmt2 :: (SMTLIB2 a) => a -> LT.Builder
runSmt2 = smt2