sig
  type symbol = int
  type var = int
  type units = (AAC_matcher.symbol * AAC_matcher.symbol) list
  type ext_units = {
    unit_for : AAC_matcher.units;
    is_ac : (AAC_matcher.symbol * bool) list;
  }
  type 'a mset = ('a * int) list
  val linear : 'AAC_matcher.mset -> 'a list
  module Terms :
    sig
      type t =
          Dot of
            (AAC_matcher.symbol * AAC_matcher.Terms.t * AAC_matcher.Terms.t)
        | Plus of
            (AAC_matcher.symbol * AAC_matcher.Terms.t * AAC_matcher.Terms.t)
        | Sym of (AAC_matcher.symbol * AAC_matcher.Terms.t array)
        | Var of AAC_matcher.var
        | Unit of AAC_matcher.symbol
      val equal_aac :
        AAC_matcher.units ->
        AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> bool
      type nf_term
      val nf_term_compare :
        AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.nf_term -> int
      val nf_equal :
        AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.nf_term -> bool
      val sprint_nf_term : AAC_matcher.Terms.nf_term -> string
      val term_of_t :
        AAC_matcher.units -> AAC_matcher.Terms.t -> AAC_matcher.Terms.nf_term
      val t_of_term : AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.t
    end
  module Subst :
    sig
      type t
      val sprint : AAC_matcher.Subst.t -> string
      val instantiate :
        AAC_matcher.Subst.t -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t
      val to_list :
        AAC_matcher.Subst.t -> (AAC_matcher.var * AAC_matcher.Terms.t) list
    end
  val matcher :
    ?strict:bool ->
    AAC_matcher.ext_units ->
    AAC_matcher.Terms.t ->
    AAC_matcher.Terms.t -> AAC_matcher.Subst.t AAC_search_monad.m
  val subterm :
    ?strict:bool ->
    AAC_matcher.ext_units ->
    AAC_matcher.Terms.t ->
    AAC_matcher.Terms.t ->
    (int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m)
    AAC_search_monad.m
end