kdrag.solvers.kb.simplify

kdrag.solvers.kb.simplify(t: BoolRef | QuantifierRef, rules: list[RewriteRule]) → BoolRef | QuantifierRef

Simplify an equation using a set of rewrite rules.

>>> x = smt.Real("x")
>>> simplify(smt.ForAll([x], -(-(-(-(-x)))) == -x), [rw.rewrite_of_expr(smt.ForAll([x], -(-x) == x))])
ForAll(X!..., -X!... == -X!...)

Parameters:

• t (BoolRef | QuantifierRef)

• rules (list[RewriteRule])

Return type:

BoolRef | QuantifierRef