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
mul (rational multiplication)imul (integer multiplication)mod (rational modulo)imod (integer modulo)inv (rational inverse).
If the symbols are not present in the context ensure_symbols registers
them.
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.