Module Binsec.Smtlib

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;
}