Module Ast

module Ast: sig .. end

type cmd =

`\|`	`CheckSynth`
`\|`	`Constraint of term`
`\|`	`DeclareVar of symbol * sort`
`\|`	`InvConstraint of symbol * symbol * symbol * symbol`
`\|`	`SetFeature of feature * boolconst`
`\|`	`SynthFun of symbol * sorted_var list * sort * grammar_def option`
`\|`	`SynthInv of symbol * sorted_var list * grammar_def option`
`\|`	`SmtCmd of smt_cmd`

type smt_cmd =

`\|`	`DeclareDatatype of symbol * dt_dec`
`\|`	`DeclareDatatypes of (sort_decl * dt_dec) list`
`\|`	`DeclareSort of symbol * numeral`
`\|`	`DefineFun of symbol * sorted_var list * sort * term`
`\|`	`DefineSort of symbol * sort`
`\|`	`SetLogic of symbol`
`\|`	`SetOption of symbol * literal`

type term =

`\|`	`Identifier of identifier`
`\|`	`Literal of literal`
`\|`	`IdentifierTerms of identifier * term list`
`\|`	`Exists of sorted_var list * term`
`\|`	`Forall of sorted_var list * term`
`\|`	`Let of var_binding list * term`

type bf_term =

`\|`	`BfIdentifier of identifier`
`\|`	`BfLiteral of literal`
`\|`	`BfIdentifierTerms of identifier * bf_term list`

type sorted_var =

`\|`	`SortedVar of symbol * sort`

type var_binding =

`\|`	`VarBinding of symbol * term`

type identifier =

`\|`	`SymbolIdentifier of symbol`
`\|`	`UnderbarIdentifier of symbol * index list`

type symbol =

`\|`	`Symbol of string`

type index =

`\|`	`NumeralIndex of numeral`
`\|`	`SymbolIndex of symbol`

type sort =

`\|`	`Sort of identifier`
`\|`	`SortWithSorts of identifier * sort list`

type feature =

type sort_decl =

`\|`	`SortDeclaration of symbol * numeral`

type dt_dec =

`\|`	`DTDec of dt_cond_dec list`

type dt_cond_dec =

`\|`	`DTConsDec of symbol * sorted_var list`

type grammar_def =

`\|`	`GrammarDef of (sorted_var * grouped_rule_list) list`

type grouped_rule_list =

`\|`	`GroupedRuleList of symbol * sort * gterm list`

type gterm =

type literal =

type numeral = string

type boolconst = string