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.