# Module `Simplify`

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_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
- Christoph Sticksel, Adrien Champion, Alain Mebsout, Arjun Viswanathan

`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.