Module XFD.SMTLib.Types

Exported datatypes:

Type synonym: SMTLib = [Command]

Constructors:

• DeclareConst :: String -> Sort -> Command
• Assert :: Term -> Command
• CheckSat :: Command
• GetModel :: Command
• GetValue :: [Term] -> Command
• Echo :: String -> Command
• Exit :: Command
• Pop :: Int -> Command
• Push :: Int -> Command
• SetLogic :: String -> Command
• SetOption :: Option -> Command

Constructors:

• ProduceModels :: Bool -> Option

Constructors:

• TermSpecConstant :: SpecConstant -> Term
• TermQualIdentifier :: QualIdentifier -> Term
• TermQualIdentifierT :: QualIdentifier -> [Term] -> Term

Constructors:

• QIdentifier :: Identifier -> QualIdentifier

Constructors:

• ISymbol :: String -> Identifier

Constructors:

• SpecConstantNumeral :: Int -> SpecConstant

Constructors:

• SortId :: Identifier -> Sort
• SortIdentifiers :: Identifier -> [Sort] -> Sort

Constructors:

• SV :: String -> Sort -> SortedVar

Constructors:

• FunDef :: String -> [SortedVar] -> Sort -> Term -> FunDef

Constructors:

• CmdGenResponse :: GenResponse -> CmdResponse
• CmdCheckSatResponse :: CheckSatResponse -> CmdResponse
• CmdGetModelResponse :: GetModelResponse -> CmdResponse
• CmdGetValueResponse :: GetValueResponse -> CmdResponse

Constructors:

• Success :: GenResponse
• Unsupported :: GenResponse
• Error :: String -> GenResponse

Constructors:

• Sat :: CheckSatResponse
• Unsat :: CheckSatResponse
• Unknown :: CheckSatResponse

Type synonym: GetModelResponse = [ModelResponse]

Constructors:

• MRDefineFun :: FunDef -> ModelResponse

Type synonym: GetValueResponse = [ValuationPair]

Constructors:

• ValuationPair :: Term -> Term -> ValuationPair

Exported operations: