Module CongruenceClosureRewrite.Rule

type t =
  1. | Regular of {
    1. lhs : Pattern.t;
    2. rhs : Pattern.t;
    3. exclude : CC.Atom.t list;
    4. mutable fire_count : int;
    }
  2. | Ellipsis of {
    1. ellipsis : Pattern.ellipsis;
    2. mutable fire_count : int;
    }
val pp : F.formatter -> t -> unit
val fire_count : t -> int
exception FuelExhausted of {
  1. round_count : int;
}
val full_rewrite : ?debug:bool -> ?fuel:int -> CC.t -> t list -> int

iterate rewriting until saturation.