TestOnly (infer.SemDiffLib.CongruenceClosureRewrite.TestOnly)

val e_match_pattern_at : 
  ?debug:bool ->
  CC.t ->
  Pattern.t ->
  CC.Atom.t ->
  subst list

val e_match_pattern : 
  ?debug:bool ->
  CC.t ->
  Pattern.t ->
  f:(CC.Atom.t -> subst -> unit) ->
  unit

val e_match_ellipsis_at : 
  CC.t ->
  Pattern.ellipsis ->
  CC.Atom.t ->
  CC.Atom.t list

val pattern_to_term : CC.t -> subst -> Pattern.t -> CC.Atom.t

val apply_rule_at : ?debug:bool -> CC.t -> Rule.t -> CC.Atom.t -> int

return the number of compatible substitution used during rewriting

val rewrite_rules_once : ?debug:bool -> CC.t -> Rule.t list -> int