Module `Psmt2Frontend.Smtlib_syntax`Source

Sourcetype 'a data = {

p : (Lexing.position * Lexing.position) option;
c : 'a;
ty : Smtlib_ty.ty;
mutable is_quantif : bool;

}

Sourcetype constant =

| Const_Dec of string
| Const_Num of string
| Const_Str of string
| Const_Hex of string
| Const_Bin of string

Sourcetype symbol = string data

Sourcetype keyword_aux =

| Category
| Smtlibversion
| Source
| Statuts of symbol
| License
| Notes
| Axioms
| Definitio
| Extensions
| Funs
| FunsDescript
| Language
| Sorts
| SortsDescr
| Theories
| Values

Sourceand keyword = keyword_aux data

Sourceand key_option_aux =

| Diagnooutputchan
| Globaldeclarations
| Interactive
| Printsucces
| Produceassertions
| Produceassignement
| Producemodels
| Produceproofs
| Produceunsatassumptions
| Produceunsatcores
| Randomseed
| Regularoutputchan
| Verbosity
| Ressourcelimit

Sourceand key_option = key_option_aux data

Sourceand option_aux =

| Option_key of key_option * index
| Option_attribute of attribute

Sourceand option = option_aux data

Sourceand key_info_aux =

| Allstats
| Assertionstacklvl
| Authors
| Difficulty
| Errorbehav
| Incremental
| Instance
| Name
| Reasonunknown
| Series
| Version
| Key_info of keyword

Sourceand key_info = key_info_aux data

Sourceand key_term_aux =

| Pattern of term list
| Named of symbol

Sourceand key_term = key_term_aux data

Sourceand sexpr_aux =

| SexprSpecConst of constant
| SexprSymbol of symbol
| SexprKeyword of keyword
| SexprInParen of sexpr list

Sourceand sexpr = sexpr_aux data

Sourceand attribute_value_aux =

| AttributeValSpecConst of constant
| AttributeValSymbol of symbol
| AttributeValSexpr of sexpr list
| NoAttributeValue

Sourceand attribute_value = attribute_value_aux data

Sourceand attribute_aux =

| AttributeKey of key_info
| AttributeKeyValue of key_info * attribute_value

Sourceand attribute = attribute_aux data

Sourceand index_aux =

| IndexSymbol of symbol
| IndexNumeral of string

Sourceand index = index_aux data

Sourceand identifier_aux =

| IdSymbol of symbol
| IdUnderscoreSymNum of symbol * index list

Sourceand identifier = identifier_aux data

Sourceand prop_literal_aux =

| PropLit of symbol
| PropLitNot of symbol

Sourceand prop_literal = prop_literal_aux data

Sourceand sort_aux =

| SortIdentifier of identifier
| SortIdMulti of identifier * sort list

Sourceand sort = sort_aux data

Sourceand sorted_var = symbol * sort

Sourceand qualidentifier_aux =

| QualIdentifierId of identifier
| QualIdentifierAs of identifier * sort

Sourceand qualidentifier = qualidentifier_aux data

Sourceand varbinding = symbol * term

Sourceand pattern_aux =

| MatchPattern of symbol * symbol list
| MatchUnderscore

Sourceand pattern = pattern_aux data

Sourceand term_aux =

| TermSpecConst of constant
| TermQualIdentifier of qualidentifier
| TermQualIdTerm of qualidentifier * term list
| TermLetTerm of varbinding list * term
| TermForAllTerm of sorted_var list * term
| TermExistsTerm of sorted_var list * term
| TermExclimationPt of term * key_term list
| 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 =

| Cmd_Assert of symbol list * term
| Cmd_CheckSat
| Cmd_CheckAllSat of symbol list
| Cmd_CheckSatAssum of prop_literal list
| Cmd_CheckEntailment of symbol list * term
| Cmd_DeclareConst of symbol * symbol list * sort
| Cmd_DeclareDataType of symbol * symbol list * constructor_dec list
| Cmd_DeclareDataTypes of sort_dec list * (symbol list * constructor_dec list) list
| Cmd_DeclareFun of symbol * symbol list * sort list * sort
| Cmd_DeclareSort of symbol * string
| Cmd_DefineFun of symbol * symbol list * sorted_var list * sort * term
| Cmd_DefineFunRec of symbol * symbol list * sorted_var list * sort * term
| Cmd_DefineFunsRec of (symbol * symbol list * sorted_var list * sort) list * term list
| Cmd_DefineSort of symbol * symbol list * sort
| Cmd_Echo of symbol
| Cmd_GetAssert
| Cmd_GetProof
| Cmd_GetUnsatCore
| Cmd_GetValue of term list
| Cmd_GetAssign
| Cmd_GetOption of keyword
| Cmd_GetInfo of key_info
| Cmd_GetModel
| Cmd_GetUnsatAssumptions
| Cmd_Reset
| Cmd_ResetAssert
| Cmd_SetLogic of symbol
| Cmd_SetOption of option
| Cmd_SetInfo of attribute
| Cmd_Push of string
| Cmd_Pop of string
| Cmd_Exit
| Cmd_Maximize of term
| Cmd_Minimize of term

Sourcetype command = command_aux data

Sourcetype commands = command list

package psmt2-frontend

Module Psmt2Frontend.Smtlib_syntaxSource

Module `Psmt2Frontend.Smtlib_syntax`Source