kdrag.solvers.sympy.simp
- kdrag.solvers.sympy.simp(e: ExprRef) Proof
Sympy simplification as an axiom schema. Sympy nor the translation to and from z3 are particularly sound. It is very useful though and better than nothing. Your mileage may vary
>>> x = smt.Real("x") >>> simp(sin(x)**2 + cos(x)**2) |= sin(x)**2 + cos(x)**2 == 1
- Parameters:
e (ExprRef)
- Return type: