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