CongruenceClosureRewrite (infer.SemDiffLib.CongruenceClosureRewrite)

module F = Stdlib.Format

module CC = CongruenceClosureSolver

module Var : sig ... end

type subst

val pp_subst : CC.t -> F.formatter -> subst -> unit

val mk_subst : (Var.t * CC.Atom.t) list -> subst

module Pattern : sig ... end

module Rule : sig ... end

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

Match a pattern against a specific atom. Returns all valid substitutions.

val subst_find : subst -> Var.t -> CC.Atom.t option

Look up a variable binding in a substitution.

type parse_error

val pp_parse_error : F.formatter -> parse_error -> unit

val parse_pattern : 
  CC.t ->
  string ->
  (Pattern.t, parse_error) IStdlib.IStd.result

val parse_rule : CC.t -> string -> (Rule.t, parse_error) IStdlib.IStd.result

module TestOnly : sig ... end