sig
  module TermPolynomial :
    sig
      type 'a polynomial_context
      type 'a t
      val mk_context :
        'a Syntax.context -> 'a SrkSimplify.TermPolynomial.polynomial_context
      val of_term :
        'a SrkSimplify.TermPolynomial.polynomial_context ->
        'a Syntax.term -> 'a SrkSimplify.TermPolynomial.t
      val term_of :
        'a SrkSimplify.TermPolynomial.polynomial_context ->
        'a SrkSimplify.TermPolynomial.t -> 'a Syntax.term
    end
  val simplify_terms_rewriter : 'a Syntax.context -> 'a Syntax.rewriter
  val simplify_terms :
    'a Syntax.context -> ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr
  val purify :
    'a Syntax.context ->
    'a Syntax.formula ->
    'a Syntax.formula * ('a, Syntax.typ_fo) Syntax.expr Syntax.Symbol.Map.t
  val partition_implicant :
    'a Syntax.formula list -> 'a Syntax.formula list list
end