Module MoxiAst

type symbol_hs = HString.t
type symbol = Lib.span * symbol_hs
type numeral = Lib.span * Numeral.t
type decimal = Lib.span * Decimal.t
type bitvector = Lib.span * Bitvector.t
type index =
  1. | NumericIndex of numeral
  2. | SymbolicIndex of symbol
type identifier = Lib.span * symbol * index list
type sort = {
  1. id : identifier;
  2. parameters : sort list;
}
type sorted_var = Lib.span * symbol * sort
type constant =
  1. | True
  2. | False
  3. | Numeral of numeral
  4. | Decimal of decimal
  5. | Bitvector of bitvector
type qual_identifier = identifier * bool * sort option
type term =
  1. | Constant of constant
  2. | QualId of qual_identifier
  3. | App of Lib.span * qual_identifier * term list
  4. | Let of Lib.span * var_binding list * term
and var_binding = Lib.span * symbol * term
type formula_type =
  1. | Assumption
  2. | Reachable
  3. | Fairness
  4. | Current
type formula_attr = formula_type * (symbol * term)
type query_attr = symbol * symbol list
type check_system_attr =
  1. | FormulaAttr of formula_attr
  2. | QueryAttr of query_attr
type system_variables = (Lib.span * sorted_var list) option
type check_system_cmd = {
  1. loc : Lib.span;
  2. system_id : symbol;
  3. input : system_variables;
  4. output : system_variables;
  5. local : system_variables;
  6. attrs : check_system_attr list;
}
type subsystem = {
  1. loc : Lib.span;
  2. instance_name : symbol;
  3. system_name : symbol;
  4. variables : symbol list;
}
type define_system_cmd = {
  1. loc : Lib.span;
  2. name : symbol;
  3. input : system_variables;
  4. output : system_variables;
  5. local : system_variables;
  6. subsys : subsystem list;
  7. init : term;
  8. trans : term;
  9. inv : term;
}
type define_fun_cmd = {
  1. loc : Lib.span;
  2. name : symbol;
  3. params : sorted_var list;
  4. sort : sort;
  5. body : term;
}
type declare_const_cmd = {
  1. loc : Lib.span;
  2. name : symbol;
  3. sort : sort;
}
type declare_enum_sort_cmd = {
  1. loc : Lib.span;
  2. name : symbol;
  3. values : symbol list;
}
type command =
  1. | CheckSystemCmd of check_system_cmd
  2. | DefineSystemCmd of define_system_cmd
  3. | DefineFunCmd of define_fun_cmd
  4. | DeclareConstCmd of declare_const_cmd
  5. | DeclareEnumSortCmd of declare_enum_sort_cmd
  6. | SetLogicCmd of symbol
type script = command list
type t = script
val is_query_attr : check_system_attr -> bool