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