Module Language.SMTLIB.Types

Exported datatypes:

Representation of an SMT-LIB script

Constructors:

• SMTLib :: [Command] -> SMTLib

Type synonym: Symbol = String

Type synonym: Ident = String

Type synonym: Numeral = Int

Constructors:

• KW :: Symbol -> Keyword

S-expressions

Constructors:

• Num :: Numeral -> SpecConstant
• Dec :: Float -> SpecConstant
• Str :: String -> SpecConstant

Constructors:

• SEConst :: SpecConstant -> SExpr
• SESym :: Symbol -> SExpr
• SEKW :: Keyword -> SExpr
• SEList :: [SExpr] -> SExpr

Sorts

Constructors:

• SComb :: Ident -> [Sort] -> Sort

Attributes

Constructors:

• AVConst :: SpecConstant -> AttrValue
• AVSym :: Symbol -> AttrValue
• AVSExpr :: [SExpr] -> AttrValue

Constructors:

• AKW :: Keyword -> Attribute
• AVal :: Keyword -> AttrValue -> Attribute

Terms

Constructors:

• Id :: Ident -> QIdent
• As :: Ident -> Sort -> QIdent

Constructors:

• SV :: Symbol -> Sort -> SortedVar

Constructors:

• PComb :: Symbol -> [Symbol] -> Pattern

Constructors:

• TConst :: SpecConstant -> Term
• TComb :: QIdent -> [Term] -> Term
• Let :: [(Symbol,Term)] -> Term -> Term
• Forall :: [SortedVar] -> Term -> Term
• Exists :: [SortedVar] -> Term -> Term
• Match :: Term -> [(Pattern,Term)] -> Term
• Annot :: Term -> [Attribute] -> Term

Theories

Constructors:

• SortSymDecl :: Ident -> Numeral -> [Attribute] -> SortSymDecl

Constructors:

• NUMERAL :: MetaSpecConstant
• DECIMAL :: MetaSpecConstant
• STRING :: MetaSpecConstant

Constructors:

• Spec :: SpecConstant -> Sort -> [Attribute] -> FunSymDecl
• Meta :: MetaSpecConstant -> Sort -> [Attribute] -> FunSymDecl
• Ident :: Ident -> [Sort] -> [Attribute] -> FunSymDecl

Constructors:

• ParFunSymDecl :: FunSymDecl -> [Symbol] -> Ident -> [Sort] -> [Attribute] -> ParFunSymDecl

Constructors:

• TASorts :: [SortSymDecl] -> TheoryAttr
• TAFuns :: [ParFunSymDecl] -> TheoryAttr
• TASortsDesc :: String -> TheoryAttr
• TAFunsDesc :: String -> TheoryAttr
• TADefinition :: String -> TheoryAttr
• TAValues :: String -> TheoryAttr
• TANotes :: String -> TheoryAttr
• TA :: Attribute -> TheoryAttr

Constructors:

• Theory :: Symbol -> [TheoryAttr] -> Theory

Info flags

Constructors:

• AllStatistics :: InfoFlag
• AssertionStackLevels :: InfoFlag
• Authors :: InfoFlag
• ErrorBehavior :: InfoFlag
• Name :: InfoFlag
• ReasonUnknown :: InfoFlag
• Version :: InfoFlag
• IFKW :: Keyword -> InfoFlag

Command options

Constructors:

• DiagnosticOutput :: String -> Option
• GlobalDecls :: Bool -> Option
• Interactive :: Bool -> Option
• PrintSuccess :: Bool -> Option
• ProduceAssertions :: Bool -> Option
• ProduceAssign :: Bool -> Option
• ProduceModels :: Bool -> Option
• ProduceProofs :: Bool -> Option
• ProduceUnsatAssump :: Bool -> Option
• ProduceUnsatCores :: Bool -> Option
• RandomSeed :: Numeral -> Option
• RegularOutput :: String -> Option
• ReproducibleResLimit :: Numeral -> Option
• Verbosity :: Numeral -> Option
• OptAttr :: Attribute -> Option

Commands

Constructors:

• FunDec :: Symbol -> [SortedVar] -> Sort -> FunDec

Constructors:

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

Constructors:

• Sym :: Symbol -> PropLit
• Not :: Symbol -> PropLit

sort declaration for datatypes

Constructors:

• SortDecl :: Symbol -> Numeral -> SortDecl

datatype declaration

Constructors:

• MT :: [ConsDecl] -> DTDecl
• PT :: [Symbol] -> [ConsDecl] -> DTDecl

Constructors:

• Cons :: Symbol -> [SortedVar] -> ConsDecl

Constructors:

• Assert :: Term -> Command
• CheckSat :: Command
• CheckSatAssuming :: [PropLit] -> Command
• DeclareConst :: Symbol -> Sort -> Command
• DeclareDatatype :: Symbol -> DTDecl -> Command
• DeclareDatatypes :: [(SortDecl,DTDecl)] -> Command
• DeclareFun :: Symbol -> [Sort] -> Sort -> Command
• DeclareSort :: Symbol -> Numeral -> Command
• DefineFun :: FunDef -> Command
• DefineFunRec :: FunDef -> Command
• DefineFunsRec :: [(FunDec,Term)] -> Command
• DefineSort :: Symbol -> [Symbol] -> Sort -> Command
• Echo :: String -> Command
• Exit :: Command
• GetAssertions :: Command
• GetAssignment :: Command
• GetInfo :: InfoFlag -> Command
• GetModel :: Command
• GetOption :: Option -> Command
• GetProof :: Command
• GetUnsatAssumptions :: Command
• GetUnsatCore :: Command
• GetValue :: [Term] -> Command
• Pop :: Numeral -> Command
• Push :: Numeral -> Command
• Reset :: Command
• ResetAssertions :: Command
• SetInfo :: Attribute -> Command
• SetLogic :: Logic -> Command
• SetOption :: Option -> Command
• Comment :: String -> Command

Logics provided by the SMT-LIB Standard

Explanation of the naming conventions:

• QF: restriction to quantifier free formulas
• A or AX: theory of ArraysEx
• BV: theory FixedSizeBitVectors
• FP: theory FloatingPoint
• IA: theory Ints (Integer Arithmetic)
• RA: theory Reals (Real Arithmetic)
• IRA: theory Reals_Ints (mixed Integer Real Arithmetic)
• IDL: Integer Difference Logic
• RDL: Rational Difference Logic
• L before IA, RA or IRA: linear fragment of those arithmetics
• N before IA, RA or IRA: non-linear fragment of those arithmetics
• UF extension allowing free sort and function symbols

see http://smtlib.cs.uiowa.edu/logics.shtml for more details

Constructors:

• ALL :: Logic
• AUFLIA :: Logic
• AUFLIRA :: Logic
• AUFNIRA :: Logic
• LIA :: Logic
• LRA :: Logic
• QFABV :: Logic
• QFAUFBV :: Logic
• QFAUFLIA :: Logic
• QFAX :: Logic
• QFBV :: Logic
• QFIDL :: Logic
• QFLIA :: Logic
• QFLRA :: Logic
• QFNIA :: Logic
• QFNRA :: Logic
• QFRDL :: Logic
• QFUF :: Logic
• QFUFBV :: Logic
• QFUFIDL :: Logic
• QFUFLIA :: Logic
• QFUFLRA :: Logic
• QFUFNRA :: Logic
• UFLRA :: Logic
• UFNIA :: Logic

Command responses

Constructors:

• ImmediateExit :: ErrorBehavior
• ContinuedExecution :: ErrorBehavior

Constructors:

• Memout :: ReasonUnknown
• Incomplete :: ReasonUnknown
• SEReason :: SExpr -> ReasonUnknown

Constructors:

• MRFun :: FunDef -> ModelRsp
• MRFunRec :: FunDef -> ModelRsp
• MRFunsRec :: [(FunDec,Term)] -> ModelRsp

Constructors:

• AssertionStackLevelsRsp :: Numeral -> InfoRsp
• AuthorsRsp :: String -> InfoRsp
• ErrorBehaviorRsp :: ErrorBehavior -> InfoRsp
• NameRsp :: String -> InfoRsp
• ReasonUnknownRsp :: ReasonUnknown -> InfoRsp
• VersionRsp :: String -> InfoRsp
• AttrRsp :: Attribute -> InfoRsp

Type synonym: ValuationPair = (Term,Term)

Type synonym: TValuationPair = (Symbol,Bool)

Constructors:

• SuccessRsp :: CmdResponse
• UnsupportedRsp :: CmdResponse
• ErrorRsp :: String -> CmdResponse
• CheckSatRsp :: CheckSat -> CmdResponse
• EchoRsp :: String -> CmdResponse
• GetAssertionsRsp :: [Term] -> CmdResponse
• GetAssignmentRsp :: [TValuationPair] -> CmdResponse
• GetInfoRsp :: [InfoRsp] -> CmdResponse
• GetModelRsp :: [ModelRsp] -> CmdResponse
• GetOptionRsp :: AttrValue -> CmdResponse
• GetProofRsp :: SExpr -> CmdResponse
• GetUnsatAssumptionsRsp :: [Symbol] -> CmdResponse
• GetUnsatCoreRsp :: [Symbol] -> CmdResponse
• GetValueRsp :: [ValuationPair] -> CmdResponse

Constructors:

• Sat :: CheckSat
• Unsat :: CheckSat
• Unknown :: CheckSat

Exported operations: