package psmt2-frontend

  1. Overview
  2. Docs
type token =
  1. | VERSION
  2. | VERBOSITY
  3. | VALUES
  4. | UNDERSCORE
  5. | THEORIES
  6. | SYMBOL of string
  7. | STRINGLIT of string
  8. | STATUTS
  9. | SOURCE
  10. | SORTSDESCRIPTION
  11. | SORTS
  12. | SMTLIBVERSION
  13. | SETOPTION
  14. | SETLOGIC
  15. | SETINFO
  16. | SERIES
  17. | RP
  18. | RESSOURCELIMIT
  19. | RESETASSERTIONS
  20. | RESET
  21. | REGULAROUTPUTCHAN
  22. | REASONUNKNOWN
  23. | RANDOMSEED
  24. | PUSH
  25. | PRODUCEUNSATCORES
  26. | PRODUCEUNSATASSUMPTIONS
  27. | PRODUCEPROOFS
  28. | PRODUCEMODELS
  29. | PRODUCEASSIGNEMENT
  30. | PRODUCEASSERTIONS
  31. | PRINTSUCCESS
  32. | POP
  33. | PATTERN
  34. | PAR
  35. | NUMERAL of string
  36. | NOTES
  37. | NAMED
  38. | NAME
  39. | MATCH
  40. | LP
  41. | LICENSE
  42. | LET
  43. | LANGUAGE
  44. | INTERACTIVE
  45. | INSTANCE
  46. | INCREMENTAL
  47. | HEXADECIMAL of string
  48. | GLOBALDECLARATIONS
  49. | GETVALUE
  50. | GETUNSATCORE
  51. | GETUNSATASSUMPTIONS
  52. | GETPROOF
  53. | GETOPTION
  54. | GETMODEL
  55. | GETINFO
  56. | GETASSIGN
  57. | GETASSERT
  58. | FUNSDESCRIPT
  59. | FUNS
  60. | FORALL
  61. | EXTENSIONS
  62. | EXIT
  63. | EXISTS
  64. | EXCLIMATIONPT
  65. | ERRORBEHAV
  66. | EOF
  67. | ECHO
  68. | DIFFICULTY
  69. | DIAGNOOUTPUTCHAN
  70. | DEFINITIO
  71. | DEFINESORT
  72. | DEFINEFUNSREC
  73. | DEFINEFUNREC
  74. | DEFINEFUN
  75. | DECLARESORT
  76. | DECLAREFUN
  77. | DECLAREDATATYPES
  78. | DECLAREDATATYPE
  79. | DECLARECONST
  80. | DECIMAL of string
  81. | CHECKSATASSUMING
  82. | CHECKSAT
  83. | CHECKENTAILMENT
  84. | CHECKALLSAT
  85. | CATEGORY
  86. | BINARY of string
  87. | AXIOMS
  88. | AUTHORS
  89. | AUTHOR
  90. | ASSERTIONSTACKLVL
  91. | ASSERT
  92. | ASCIIWOR of string
  93. | AS
  94. | ALLSTATS
exception Error
val term_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Smtlib_syntax.term list * bool
val term : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Smtlib_syntax.term
val commands : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Smtlib_syntax.commands