sig
  type term = TVar of Variable.t | TTerm of Types.Term.t
  type atom =
      AVar of Variable.t
    | AAtom of Types.Atom.t
    | AEq of Ptree.term * Ptree.term
    | ANeq of Ptree.term * Ptree.term
    | ALe of Ptree.term * Ptree.term
    | ALt of Ptree.term * Ptree.term
  type formula =
      PAtom of Ptree.atom
    | PNot of Ptree.formula
    | PAnd of Ptree.formula list
    | POr of Ptree.formula list
    | PImp of Ptree.formula * Ptree.formula
    | PEquiv of Ptree.formula * Ptree.formula
    | PIte of Ptree.formula * Ptree.formula * Ptree.formula
    | PForall of Variable.t list * Ptree.formula
    | PExists of Variable.t list * Ptree.formula
    | PForall_other of Variable.t list * Ptree.formula
    | PExists_other of Variable.t list * Ptree.formula
  type term_or_formula = PF of Ptree.formula | PT of Ptree.term
  type cformula = Ptree.formula
  type pswts = (Ptree.cformula * Ptree.term) list
  type pglob_update = PUTerm of Ptree.term | PUCase of Ptree.pswts
  type pupdate = {
    pup_loc : Util.loc;
    pup_arr : Hstring.t;
    pup_arg : Variable.t list;
    pup_swts : Ptree.pswts;
  }
  type ptransition = {
    ptr_lets : (Hstring.t * Ptree.term) list;
    ptr_name : Hstring.t;
    ptr_args : Variable.t list;
    ptr_reqs : Ptree.cformula;
    ptr_assigns : (Hstring.t * Ptree.pglob_update) list;
    ptr_upds : Ptree.pupdate list;
    ptr_nondets : Hstring.t list;
    ptr_loc : Util.loc;
  }
  type psystem = {
    pglobals : (Util.loc * Hstring.t * Smt.Type.t) list;
    pconsts : (Util.loc * Hstring.t * Smt.Type.t) list;
    parrays : (Util.loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list;
    ptype_defs : (Util.loc * Ast.type_constructors) list;
    pinit : Util.loc * Variable.t list * Ptree.cformula;
    pinvs : (Util.loc * Variable.t list * Ptree.cformula) list;
    punsafe : (Util.loc * Variable.t list * Ptree.cformula) list;
    ptrans : Ptree.ptransition list;
  }
  type pdecl =
      PInit of (Util.loc * Variable.t list * Ptree.cformula)
    | PInv of (Util.loc * Variable.t list * Ptree.cformula)
    | PUnsafe of (Util.loc * Variable.t list * Ptree.cformula)
    | PTrans of Ptree.ptransition
    | PFun
  val add_fun_def : Hstring.t -> Variable.t list -> Ptree.formula -> unit
  val app_fun : Hstring.t -> Ptree.term_or_formula list -> Ptree.formula
  val encode_psystem : Ptree.psystem -> Ast.system
  val psystem_of_decls :
    pglobals:(Util.loc * Hstring.t * Smt.Type.t) list ->
    pconsts:(Util.loc * Hstring.t * Smt.Type.t) list ->
    parrays:(Util.loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list ->
    ptype_defs:(Util.loc * Ast.type_constructors) list ->
    Ptree.pdecl list -> Ptree.psystem
  val print_system : Format.formatter -> Ast.system -> unit
end