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
c - d + a*x - b*y > 0 where
c-d > 0 or
c-d = 0
a>0 if term
x is ordered before term
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
val simplify_term :
(UfSymbol.t * (Var.t list * Term.t)) list -> Term.t -> Term.t
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
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.