module Simplify:`sig`

..`end`

Term simplifier

Simplify a term by evaluating operations with constants.

Integer and real terms are converted to polynomials, terms in that cannot be reduced to addition or linear multiplication become new variables in the polynomials.

Boolean terms are converted to negation normal form, such that only the operators conjunction, disjunction and negation occur.

Relations between polynomials such as `c + a*x > d + b*y`

are
converted to `c - d + a*x - b*y > 0`

where `c-d > 0`

or `c-d = 0`

and `a>0`

if term `x`

is ordered before term `y`

m otherwise `b>0`

.

Let bindings are unfolded. In order to evaluate a term with a
partial model for its variables, bind each variable in the model
to its value or use the convenience function
`Simplify.simplify_term_model`

. To make a model total, give a function in
the optional argument `~default_of_var`

that returns the value to
assign to the variable given as parameter.

**Author(s):** Christoph Sticksel, Adrien Champion, Alain Mebsout

`val has_division_by_zero_happened : ``unit -> bool`

Returns true iff a division by zero happened in a simplification since
this function was last called.

`val simplify_term : ``(UfSymbol.t * (Var.t list * Term.t)) list -> Term.t -> Term.t`

Simplify a term

`val simplify_term_model : ``?default_of_var:(Var.t -> Term.t) ->`

(UfSymbol.t * (Var.t list * Term.t)) list -> Model.t -> Term.t -> Term.t

Simplify a term given an assignment to variables

The optional parameter `default_of_var`

may be a function that
assigns a default value per variable, for example, to smooth a
partially defined model. The defaults for variables must not be
circular, otherwise the simplification will cycle.