package psmt2-frontend

  1. Overview
  2. Docs

Module Psmt2Frontend.Smtlib_syntaxSource

Sourcetype 'a data = {
  1. p : (Lexing.position * Lexing.position) option;
  2. c : 'a;
  3. ty : Smtlib_ty.ty;
  4. mutable is_quantif : bool;
}
Sourcetype constant =
  1. | Const_Dec of string
  2. | Const_Num of string
  3. | Const_Str of string
  4. | Const_Hex of string
  5. | Const_Bin of string
Sourcetype symbol = string data
Sourcetype keyword_aux =
  1. | Category
  2. | Smtlibversion
  3. | Source
  4. | Statuts of symbol
  5. | License
  6. | Notes
  7. | Axioms
  8. | Definitio
  9. | Extensions
  10. | Funs
  11. | FunsDescript
  12. | Language
  13. | Sorts
  14. | SortsDescr
  15. | Theories
  16. | Values
Sourceand keyword = keyword_aux data
Sourceand key_option_aux =
  1. | Diagnooutputchan
  2. | Globaldeclarations
  3. | Interactive
  4. | Printsucces
  5. | Produceassertions
  6. | Produceassignement
  7. | Producemodels
  8. | Produceproofs
  9. | Produceunsatassumptions
  10. | Produceunsatcores
  11. | Randomseed
  12. | Regularoutputchan
  13. | Verbosity
  14. | Ressourcelimit
Sourceand key_option = key_option_aux data
Sourceand option_aux =
  1. | Option_key of key_option * index
  2. | Option_attribute of attribute
Sourceand option = option_aux data
Sourceand key_info_aux =
  1. | Allstats
  2. | Assertionstacklvl
  3. | Authors
  4. | Difficulty
  5. | Errorbehav
  6. | Incremental
  7. | Instance
  8. | Name
  9. | Reasonunknown
  10. | Series
  11. | Version
  12. | Key_info of keyword
Sourceand key_info = key_info_aux data
Sourceand key_term_aux =
  1. | Pattern of term list
  2. | Named of symbol
Sourceand key_term = key_term_aux data
Sourceand sexpr_aux =
  1. | SexprSpecConst of constant
  2. | SexprSymbol of symbol
  3. | SexprKeyword of keyword
  4. | SexprInParen of sexpr list
Sourceand sexpr = sexpr_aux data
Sourceand attribute_value_aux =
  1. | AttributeValSpecConst of constant
  2. | AttributeValSymbol of symbol
  3. | AttributeValSexpr of sexpr list
  4. | NoAttributeValue
Sourceand attribute_value = attribute_value_aux data
Sourceand attribute_aux =
  1. | AttributeKey of key_info
  2. | AttributeKeyValue of key_info * attribute_value
Sourceand attribute = attribute_aux data
Sourceand index_aux =
  1. | IndexSymbol of symbol
  2. | IndexNumeral of string
Sourceand index = index_aux data
Sourceand identifier_aux =
  1. | IdSymbol of symbol
  2. | IdUnderscoreSymNum of symbol * index list
Sourceand identifier = identifier_aux data
Sourceand prop_literal_aux =
  1. | PropLit of symbol
  2. | PropLitNot of symbol
Sourceand prop_literal = prop_literal_aux data
Sourceand sort_aux =
  1. | SortIdentifier of identifier
  2. | SortIdMulti of identifier * sort list
Sourceand sort = sort_aux data
Sourceand sorted_var = symbol * sort
Sourceand qualidentifier_aux =
  1. | QualIdentifierId of identifier
  2. | QualIdentifierAs of identifier * sort
Sourceand qualidentifier = qualidentifier_aux data
Sourceand varbinding = symbol * term
Sourceand pattern_aux =
  1. | MatchPattern of symbol * symbol list
  2. | MatchUnderscore
Sourceand pattern = pattern_aux data
Sourceand term_aux =
  1. | TermSpecConst of constant
  2. | TermQualIdentifier of qualidentifier
  3. | TermQualIdTerm of qualidentifier * term list
  4. | TermLetTerm of varbinding list * term
  5. | TermForAllTerm of sorted_var list * term
  6. | TermExistsTerm of sorted_var list * term
  7. | TermExclimationPt of term * key_term list
  8. | TermMatch of term * (pattern * term) list
Sourceand term = term_aux data
Sourceand sort_dec = symbol * string
Sourceand selector_dec = symbol * sort
Sourceand constructor_dec = symbol * selector_dec list
Sourcetype command_aux =
  1. | Cmd_Assert of symbol list * term
  2. | Cmd_CheckSat
  3. | Cmd_CheckAllSat of symbol list
  4. | Cmd_CheckSatAssum of prop_literal list
  5. | Cmd_CheckEntailment of symbol list * term
  6. | Cmd_DeclareConst of symbol * symbol list * sort
  7. | Cmd_DeclareDataType of symbol * symbol list * constructor_dec list
  8. | Cmd_DeclareDataTypes of sort_dec list * (symbol list * constructor_dec list) list
  9. | Cmd_DeclareFun of symbol * symbol list * sort list * sort
  10. | Cmd_DeclareSort of symbol * string
  11. | Cmd_DefineFun of symbol * symbol list * sorted_var list * sort * term
  12. | Cmd_DefineFunRec of symbol * symbol list * sorted_var list * sort * term
  13. | Cmd_DefineFunsRec of (symbol * symbol list * sorted_var list * sort) list * term list
  14. | Cmd_DefineSort of symbol * symbol list * sort
  15. | Cmd_Echo of symbol
  16. | Cmd_GetAssert
  17. | Cmd_GetProof
  18. | Cmd_GetUnsatCore
  19. | Cmd_GetValue of term list
  20. | Cmd_GetAssign
  21. | Cmd_GetOption of keyword
  22. | Cmd_GetInfo of key_info
  23. | Cmd_GetModel
  24. | Cmd_GetUnsatAssumptions
  25. | Cmd_Reset
  26. | Cmd_ResetAssert
  27. | Cmd_SetLogic of symbol
  28. | Cmd_SetOption of option
  29. | Cmd_SetInfo of attribute
  30. | Cmd_Push of string
  31. | Cmd_Pop of string
  32. | Cmd_Exit
  33. | Cmd_Maximize of term
  34. | Cmd_Minimize of term
Sourcetype command = command_aux data
Sourcetype commands = command list