SMTLib1

Synopsis

• newtype Name = N String
• data Ident = I Name [Integer]
• data Quant
  • = Exists
  • | Forall
• data Conn
  • = Not
  • | Implies
  • | And
  • | Or
  • | Xor
  • | Iff
  • | IfThenElse
• data Formula
  • = FTrue
  • | FFalse
  • | FPred Ident [Term]
  • | FVar Name
  • | Conn Conn [Formula]
  • | Quant Quant [Binder] Formula
  • | Let Name Term Formula
  • | FLet Name Formula Formula
  • | FAnnot Formula [Annot]
• type Sort = Ident
• data Binder = Bind {
  • bindVar :: Name
  • bindSort :: Sort
  }
• data Term
  • = Var Name
  • | App Ident [Term]
  • | Lit Literal
  • | ITE Formula Term Term
  • | TAnnot Term [Annot]
• data Literal
  • = LitNum Integer
  • | LitFrac Rational
  • | LitStr String
• data Annot = Attr {
  • attrName :: Name
  • attrVal :: Maybe String
  }
• data FunDecl = FunDecl {
  • funName :: Ident
  • funArgs :: [Sort]
  • funRes :: Sort
  • funAnnots :: [Annot]
  }
• data PredDecl = PredDecl {
  • predName :: Ident
  • predArgs :: [Sort]
  • predAnnots :: [Annot]
  }
• data Status
  • = Sat
  • | Unsat
  • | Unknown
• data Command
  • = CmdLogic Ident
  • | CmdAssumption Formula
  • | CmdFormula Formula
  • | CmdStatus Status
  • | CmdExtraSorts [Sort]
  • | CmdExtraFuns [FunDecl]
  • | CmdExtraPreds [PredDecl]
  • | CmdNotes String
  • | CmdAnnot Annot
• data Script = Script {
  • scrName :: Ident
  • scrCommands :: [Command]
  }
• (===) :: Term -> Term -> Formula
• (=/=) :: Term -> Term -> Formula
• (.<.) :: Term -> Term -> Formula
• (.>.) :: Term -> Term -> Formula
• tInt :: Sort
• funDef :: Ident -> [Sort] -> Sort -> Command
• constDef :: Ident -> Sort -> Command
• logic :: Ident -> Command
• assume :: Formula -> Command
• goal :: Formula -> Command
• class PP t where
  • pp :: t -> Doc

Documentation