electrod 0.1.4 · OCaml Package

constraint 'c = (Var.t, Tuple.t) CCList.Assoc.t

method private allocate_sbs_to_tuples : (Var.t
                                         * (Elo.var, Elo.ident)
                                             Elo_to_LTL1.G.exp)
                                          Containers.List.t ->
  Atom.t Containers.List.t ->
  Tuple.t list

method build_Add : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_All : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method build_And : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Block : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t list ->
  SMV_LTL.t

method build_BoxJoin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Elo.var, Elo.ident) Elo.G.exp list ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) list ->
  Tuple.t ->
  SMV_LTL.t

method build_Card : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.term

method build_Compr : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  (GenGoal.disj * Elo.var list * (Tuple.t -> SMV_LTL.t)) list ->
  SMV_LTL.t list ->
  Tuple.t ->
  SMV_LTL.t

method build_Diff : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_F : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_FIte : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_False : (Var.t * Tuple.t) list -> SMV_LTL.t

method build_G : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Gt : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_Gte : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_H : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_IBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  GenGoal.ibinop ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.term ->
  (SMV_LTL.term -> SMV_LTL.term -> SMV_LTL.term) ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_IComp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  GenGoal.icomp_op ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.term ->
  (SMV_LTL.term -> SMV_LTL.term -> SMV_LTL.t) ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_IEq : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_INEq : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_IUn : (Var.t * Tuple.t) list ->
  GenGoal.iunop ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  (SMV_LTL.term -> SMV_LTL.term) ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_Iden : (Var.t * Tuple.t) list -> Tuple.t -> SMV_LTL.t

method build_Ident : (Var.t * Tuple.t) list ->
  Elo.ident ->
  Elo.ident ->
  Tuple.t ->
  SMV_LTL.t

method build_Iff : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Imp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_In : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method build_Inter : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_Join : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_LBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  GenGoal.lbinop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  ((Elo.var, Elo.ident) GenGoal.fml ->
    (Elo.var, Elo.ident) GenGoal.fml ->
    SMV_LTL.t ->
    SMV_LTL.t ->
    SMV_LTL.t) ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_LProj : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_LUn : (Var.t * Tuple.t) list ->
  GenGoal.lunop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  ((Elo.var, Elo.ident) GenGoal.fml -> SMV_LTL.t -> SMV_LTL.t) ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Let : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  (Elo.var * (Tuple.t -> SMV_LTL.t)) list ->
  SMV_LTL.t list ->
  SMV_LTL.t

method build_Lone : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method build_Lt : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_Lte : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method build_Neg : (Var.t * Tuple.t) list -> SMV_LTL.term -> SMV_LTL.term

method build_No : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method build_None_ : (Var.t * Tuple.t) list -> Tuple.t -> SMV_LTL.t

method build_Not : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_NotIn : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method build_Num : (Var.t * Tuple.t) list -> int -> int -> SMV_LTL.term

method build_O : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_One : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method build_Or : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Over : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_P : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Prime : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_Prod : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_Qual : (Var.t * Tuple.t) list ->
  GenGoal.rqualify ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  Elo_to_LTL1.G.rqualify ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method build_Quant : (Var.t * Tuple.t) list ->
  GenGoal.quant ->
  (Elo.var, Elo.ident) GenGoal.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  Elo_to_LTL1.G.quant ->
  (GenGoal.disj * Elo.var list * (Tuple.t -> SMV_LTL.t)) list ->
  SMV_LTL.t list ->
  SMV_LTL.t

method build_R : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_RBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  GenGoal.rbinop ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  ((Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
    (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
    (Tuple.t -> SMV_LTL.t) ->
    (Tuple.t -> SMV_LTL.t) ->
    Tuple.t ->
    SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_RComp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  GenGoal.comp_op ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  ((Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
    (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
    (Tuple.t -> SMV_LTL.t) ->
    (Tuple.t -> SMV_LTL.t) ->
    SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method build_REq : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method build_RIte : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  SMV_LTL.t ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_RLone : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method build_RNEq : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method build_RNo : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method build_ROne : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method build_RProj : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_RSome : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method build_RTClos : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_RUn : (Var.t * Tuple.t) list ->
  Elo_to_LTL1.G.runop ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  ((Elo.var, Elo.ident) Elo.G.exp ->
    (Tuple.t -> SMV_LTL.t) ->
    Tuple.t ->
    SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_Run : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t list ->
  SMV_LTL.t list

method build_S : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Some_ : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method build_Sub : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_TClos : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_Transpose : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_True : (Var.t * Tuple.t) list -> SMV_LTL.t

method build_U : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_Union : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method build_Univ : (Var.t * Tuple.t) list -> Tuple.t -> SMV_LTL.t

method build_X : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method build_exp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Location.t ->
  int option ->
  Tuple.t ->
  SMV_LTL.t

method build_fml : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  Location.t ->
  SMV_LTL.t

method build_iexp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.term ->
  Location.t ->
  SMV_LTL.term

method visit_'i : (Var.t * Tuple.t) list -> Elo.ident -> Elo.ident

method visit_'v : (Var.t * Tuple.t) list -> Elo.var -> Elo.var

method visit_Add : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_All : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method visit_And : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Block : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t

method visit_BoxJoin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Elo.var, Elo.ident) Elo.G.exp list ->
  Tuple.t ->
  SMV_LTL.t

method visit_Card : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  SMV_LTL.term

method visit_Compr : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  Tuple.t ->
  SMV_LTL.t

method visit_Diff : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_F : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_FIte : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t

method visit_False : (Var.t * Tuple.t) list -> SMV_LTL.t

method visit_G : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Gt : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_Gte : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_H : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_IBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  GenGoal.ibinop ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.term

method visit_IComp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  GenGoal.icomp_op ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.t

method visit_IEq : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_INEq : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_IUn : (Var.t * Tuple.t) list ->
  GenGoal.iunop ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.term

method visit_Iden : (Var.t * Tuple.t) list -> Tuple.t -> SMV_LTL.t

method visit_Ident : (Var.t * Tuple.t) list ->
  Elo.ident ->
  Tuple.t ->
  SMV_LTL.t

method visit_Iff : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Imp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_In : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method visit_Inter : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_Join : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_LBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  GenGoal.lbinop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t

method visit_LProj : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_LUn : (Var.t * Tuple.t) list ->
  GenGoal.lunop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t

method visit_Let : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t

method visit_Lone : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method visit_Lt : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_Lte : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_Neg : (Var.t * Tuple.t) list -> SMV_LTL.term -> SMV_LTL.term

method visit_No : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method visit_None_ : (Var.t * Tuple.t) list -> Tuple.t -> SMV_LTL.t

method visit_Not : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_NotIn : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method visit_Num : (Var.t * Tuple.t) list -> int -> SMV_LTL.term

method visit_O : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_One : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method visit_Or : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Over : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_P : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Prime : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  Tuple.t ->
  SMV_LTL.t

method visit_Prod : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_Qual : (Var.t * Tuple.t) list ->
  GenGoal.rqualify ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  SMV_LTL.t

method visit_Quant : (Var.t * Tuple.t) list ->
  GenGoal.quant ->
  (Elo.var, Elo.ident) GenGoal.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t

method visit_R : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_RBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  GenGoal.rbinop ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  Tuple.t ->
  SMV_LTL.t

method visit_RComp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  GenGoal.comp_op ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  SMV_LTL.t

method visit_REq : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method visit_RIte : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  Tuple.t ->
  SMV_LTL.t

method visit_RLone : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method visit_RNEq : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method visit_RNo : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method visit_ROne : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method visit_RProj : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_RSome : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.rqualify

method visit_RTClos : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_RUn : (Var.t * Tuple.t) list ->
  Elo_to_LTL1.G.runop ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  Tuple.t ->
  SMV_LTL.t

method visit_Run : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t list

method visit_S : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Some_ : (Var.t * Tuple.t) list -> Elo_to_LTL1.G.quant

method visit_Sub : (Var.t * Tuple.t) list ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_TClos : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_Transpose : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_True : (Var.t * Tuple.t) list -> SMV_LTL.t

method visit_U : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method visit_Union : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_Univ : (Var.t * Tuple.t) list -> Tuple.t -> SMV_LTL.t

method visit_X : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method private visit_array : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a array ->
  'b array

method visit_binding : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.binding ->
  Elo.var * (Tuple.t -> SMV_LTL.t)

method visit_block : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  SMV_LTL.t list

method private visit_bool : 'env. 'env -> bool -> bool

method private visit_bytes : 'env. 'env -> bytes -> bytes

method private visit_char : 'env. 'env -> char -> char

method visit_comp_op : (Var.t * Tuple.t) list ->
  GenGoal.comp_op ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  SMV_LTL.t

method visit_disj : (Var.t * Tuple.t) list -> GenGoal.disj -> GenGoal.disj

method visit_exp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  Tuple.t ->
  SMV_LTL.t

method private visit_float : 'env. 'env -> float -> float

method visit_fml : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t

method visit_ibinop : (Var.t * Tuple.t) list ->
  GenGoal.ibinop ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_icomp_op : (Var.t * Tuple.t) list ->
  GenGoal.icomp_op ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.t

method visit_iexp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  SMV_LTL.term

method private visit_int : 'env. 'env -> int -> int

method private visit_int32 : 'env. 'env -> int32 -> int32

method private visit_int64 : 'env. 'env -> int64 -> int64

method visit_iunop : (Var.t * Tuple.t) list ->
  GenGoal.iunop ->
  SMV_LTL.term ->
  SMV_LTL.term

method private visit_lazy_t : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a Lazy.t ->
  'b Lazy.t

method visit_lbinop : (Var.t * Tuple.t) list ->
  GenGoal.lbinop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t ->
  SMV_LTL.t

method private visit_list : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a list ->
  'b list

method visit_lunop : (Var.t * Tuple.t) list ->
  GenGoal.lunop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  SMV_LTL.t ->
  SMV_LTL.t

method private visit_nativeint : 'env. 'env -> nativeint -> nativeint

method private visit_option : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a option ->
  'b option

method visit_prim_exp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.prim_exp ->
  Tuple.t ->
  SMV_LTL.t

method visit_prim_fml : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.prim_fml ->
  SMV_LTL.t

method visit_prim_iexp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.prim_iexp ->
  SMV_LTL.term

method visit_quant : (Var.t * Tuple.t) list ->
  GenGoal.quant ->
  Elo_to_LTL1.G.quant

method visit_rbinop : (Var.t * Tuple.t) list ->
  GenGoal.rbinop ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Elo.var, Elo.ident) Elo_to_LTL1.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method private visit_ref : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a ref ->
  'b ref

method private visit_result : 'env 'a 'b 'e 'f. ('env -> 'a -> 'b) ->
  ('env -> 'e -> 'f) ->
  'env ->
  ('a, 'e) Result.result ->
  ('b, 'f) Result.result

method visit_rqualify : (Var.t * Tuple.t) list ->
  GenGoal.rqualify ->
  Elo_to_LTL1.G.rqualify

method visit_runop : (Var.t * Tuple.t) list ->
  Elo_to_LTL1.G.runop ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> SMV_LTL.t) ->
  Tuple.t ->
  SMV_LTL.t

method visit_sim_binding : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.sim_binding ->
  GenGoal.disj * Elo.var list * (Tuple.t -> SMV_LTL.t)

method private visit_string : 'env. 'env -> string -> string

method visit_t : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.t ->
  SMV_LTL.t list

method private visit_unit : 'env. 'env -> unit -> unit

package electrod