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