Language.Fixpoint.Smt.Types

Contents

• Serialized Representation
• Commands
• Responses
• Typeclass for SMTLIB2 conversion
• SMTLIB2 Process Context
• SMTLIB2 symbol environment
• Theory Symbol
• Strict Formatter

Description

Synopsis

• type Raw = Text
• data Command
  • = Push
  • | Pop
  • | CheckSat
  • | Declare Symbol [Sort] Sort
  • | Define Sort
  • | Assert (Maybe Int) Expr
  • | Distinct [Expr]
  • | GetValue [Symbol]
  • | CMany [Command]
• data Response
  • = Ok
  • | Sat
  • | Unsat
  • | Unknown
  • | Values [(Symbol, Raw)]
  • | Error Raw
• class SMTLIB2 a where
  • defunc :: a -> SMT2 a
  • smt2 :: a -> Text
  • runSmt2 :: SMTEnv -> a -> Text
• data Context = Ctx {
  • pId :: ProcessHandle
  • cIn :: Handle
  • cOut :: Handle
  • cLog :: Maybe Handle
  • verbose :: Bool
  • smtenv :: SMTEnv
  }
• type SMTEnv = SEnv Sort
• emptySMTEnv :: SEnv a
• data SMTSt = SMTSt {
  • fresh :: Int
  • smt2env :: SMTEnv
  }
• withExtendedEnv :: (Foldable t, MonadState SMTSt m) => t (Symbol, Sort) -> m b -> m b
• type SMT2 = State SMTSt
• freshSym :: MonadState SMTSt m => m Symbol
• data TheorySymbol = Thy {
  • tsSym :: Symbol
  • tsRaw :: Raw
  • tsSort :: Sort
  }
• format :: Params ps => Format -> ps -> Text

Serialized Representation

Commands

Responses

Typeclass for SMTLIB2 conversion

SMTLIB2 Process Context

SMTLIB2 symbol environment

Theory Symbol

Strict Formatter