Module Nonlinear

module Nonlinear: sig .. end
Operations for manipulating non-linear terms and formulas.

val ensure_symbols : 'a Syntax.context -> unit
Ensure that a context has the following named symbols
val uninterpret_rewriter : 'a Syntax.context ->
('a, Syntax.typ_fo) Syntax.expr -> ('a, Syntax.typ_fo) Syntax.expr
Replace non-linear arithmetic with uninterpreted functions. The uninterpreted function symbols are named symbols: mul, div, and mod. This rewriter is safe to apply top-down or bottom-up.
val interpret_rewriter : 'a Syntax.context ->
('a, Syntax.typ_fo) Syntax.expr -> ('a, Syntax.typ_fo) Syntax.expr
Replace non-linear uninterpreted functions with interpreted ones. This rewriter is safe to apply top-down or bottom-up.
val uninterpret : 'a Syntax.context -> ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr
Replace non-linear arithmetic with uninterpreted functions. The uninterpreted function symbols are named symbols: mul, div, and mod.
val interpret : 'a Syntax.context -> ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr
Replace non-linear uninterpreted functions with interpreted ones.
val linearize : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
Compute a linear approximation of a non-linear formula.