package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type
type numeral = string

Concrete parse tree for SMT-LIB Formulas.

type constant =
  1. | CstNumeral of numeral
  2. | CstDecimal of string
  3. | CstDecimalSize of string * string
  4. | CstHexadecimal of string
  5. | CstBinary of string
  6. | CstString of string
  7. | CstBool of bool
type symbol_desc =
  1. | SimpleSymbol of string
  2. | QuotedSymbol of string
type symbol = {
  1. symbol_desc : symbol_desc;
  2. symbol_loc : Location.t;
}
type symbols = symbol list
type keyword = string
type sexpr_desc =
  1. | SexprConstant of constant
  2. | SexprSymbol of symbol
  3. | SexprKeyword of keyword
  4. | SexprParens of sexprs
and sexpr = {
  1. sexpr_desc : sexpr_desc;
  2. sexpr_loc : Location.t;
}
and sexprs = sexpr list
type index =
  1. | IdxNum of numeral
  2. | IdxSymbol of symbol
type indexes = index list
type info_flag_desc =
  1. | InfoFlagKeyword of keyword
type info_flag = {
  1. info_flag_desc : info_flag_desc;
  2. info_flag_loc : Location.t;
}
type id_desc =
  1. | IdSymbol of symbol
  2. | IdUnderscore of symbol * indexes
type identifier = {
  1. id_desc : id_desc;
  2. id_loc : Location.t;
}
type attr_value_desc =
  1. | AttrValSpecConstant of constant
  2. | AttrValSymbol of symbol
  3. | AttrValSexpr of sexprs
type attr_value = {
  1. attr_value_desc : attr_value_desc;
  2. attr_value_loc : Location.t;
}
type attribute_desc =
  1. | AttrKeyword of keyword
  2. | AttrKeywordValue of keyword * attr_value
type attribute = {
  1. attribute_desc : attribute_desc;
  2. attribute_loc : Location.t;
}
type attributes = attribute list
type smt_option_desc =
  1. | OptionAttribute of attribute
type smt_option = {
  1. smt_option_desc : smt_option_desc;
  2. smt_option_loc : Location.t;
}
type sort = {
  1. sort_desc : sort_desc;
  2. sort_loc : Location.t;
}
and sorts = sort list
and sort_desc =
  1. | SortIdentifier of identifier
  2. | SortFun of identifier * sorts
type qual_identifier_desc =
  1. | QualIdentifierIdentifier of identifier
  2. | QualIdentifierAs of identifier * sort
type qual_identifier = {
  1. qual_identifier_desc : qual_identifier_desc;
  2. qual_identifier_loc : Location.t;
}
type sorted_var_desc =
  1. | SortedVar of symbol * sort
type sorted_var = {
  1. sorted_var_desc : sorted_var_desc;
  2. sorted_var_loc : Location.t;
}
type sorted_vars = sorted_var list
type var_binding_desc =
  1. | VarBinding of symbol * term
and var_binding = {
  1. var_binding_desc : var_binding_desc;
  2. var_binding_loc : Location.t;
}
and var_bindings = var_binding list
and term_desc =
  1. | TermSpecConstant of constant
  2. | TermQualIdentifier of qual_identifier
  3. | TermQualIdentifierTerms of qual_identifier * terms
  4. | TermLetTerm of var_bindings * term
  5. | TermForallTerm of sorted_vars * term
  6. | TermExistsTerm of sorted_vars * term
  7. | TermLambdaTerm of sorted_vars * term
  8. | TermAnnotatedTerm of term * attributes
and terms = term list
and term = {
  1. term_desc : term_desc;
  2. term_loc : Location.t;
}
type fun_def_desc =
  1. | FunDef of symbol * sorts option * sorted_vars * sort * term
type fun_def = {
  1. fun_def_desc : fun_def_desc;
  2. fun_def_loc : Location.t;
}
type fun_rec_def_desc =
  1. | FunRecDef of symbol * sorts option * sorted_vars * sort * term
type fun_rec_def = {
  1. fun_rec_def_desc : fun_rec_def_desc;
  2. fun_rec_def_loc : Location.t;
}
type fun_rec_defs = fun_rec_def list
type command_desc =
  1. | CmdAssert of term
  2. | CmdCheckSat
  3. | CmdCheckSatAssuming of symbols
  4. | CmdComment of string
  5. | CmdDeclareConst of symbol * sort
  6. | CmdDeclareFun of symbol * sorts option * sorts * sort
  7. | CmdDeclareSort of symbol * numeral
  8. | CmdDefineFun of fun_def
  9. | CmdDefineFunRec of fun_rec_defs
  10. | CmdDefineSort of symbol * symbols * sort
  11. | CmdEcho of string
  12. | CmdExit
  13. | CmdGetAssertions
  14. | CmdGetAssignment
  15. | CmdGetInfo of info_flag
  16. | CmdGetModel
  17. | CmdGetOption of keyword
  18. | CmdGetProof
  19. | CmdGetUnsatAssumptions
  20. | CmdGetUnsatCore
  21. | CmdGetValue of terms
  22. | CmdMetaInfo of attribute
  23. | CmdPop of numeral option
  24. | CmdPush of numeral option
  25. | CmdReset
  26. | CmdResetAssertions
  27. | CmdSetInfo of attribute
  28. | CmdSetLogic of symbol
  29. | CmdSetOption of smt_option
type command = {
  1. command_desc : command_desc;
  2. command_loc : Location.t;
}
type commands = command list
type script = {
  1. script_commands : commands;
  2. script_loc : Location.t;
}
type model = {
  1. model_commands : commands;
  2. model_loc : Location.t;
}
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct