sig
  val ensure_symbols : 'a Syntax.context -> unit
  val uninterpret_rewriter :
    'a Syntax.context ->
    ('a, Syntax.typ_fo) Syntax.expr -> ('a, Syntax.typ_fo) Syntax.expr
  val interpret_rewriter :
    'a Syntax.context ->
    ('a, Syntax.typ_fo) Syntax.expr -> ('a, Syntax.typ_fo) Syntax.expr
  val uninterpret :
    'a Syntax.context -> ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr
  val interpret :
    'a Syntax.context -> ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr
  val linearize : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
end