Module XFD.SMTLib.Types

This module defines data types to represent SMT programs and formulas in Curry.

Summary of exported operations:

Exported datatypes:


SMTLib

Type synonym: SMTLib = [Command]


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

Option

Constructors:

  • ProduceModels :: Bool -> Option

Term

Constructors:


QualIdentifier

Constructors:


Identifier

Constructors:

  • ISymbol :: String -> Identifier

SpecConstant

Constructors:

  • SpecConstantNumeral :: Int -> SpecConstant

Sort

Constructors:


SortedVar

Constructors:

  • SV :: String -> Sort -> SortedVar

FunDef

Constructors:


CmdResponse

Constructors:


GenResponse

Constructors:

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

CheckSatResponse

Constructors:

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

GetModelResponse

Type synonym: GetModelResponse = [ModelResponse]


ModelResponse

Constructors:

  • MRDefineFun :: FunDef -> ModelResponse

GetValueResponse

Type synonym: GetValueResponse = [ValuationPair]


ValuationPair

Constructors:

  • ValuationPair :: Term -> Term -> ValuationPair

Exported operations: