search

deividrvale / CRIT

A tool for automating Rewriting Induction (RI) for Logically Constrained Term Rewriting Systems (LCTRSs)
MIT License
0 stars 0 forks source link

Check out Z3.simplify #5

Closed WBrozius closed 2 years ago

WBrozius commented 2 years ago

Possibly Z3 has a simplify method that allows us to easily apply calculation steps to equations that make the terms simpler. For example, this could potentially rewrite term f(x - 1 - 1 - 1 - 1 - 1 - 1) to f(x - 6).

WBrozius commented 2 years ago

The answer is possibly in an "SMT-LIB Standard", like Version 2.6: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

WBrozius commented 2 years ago

Useful links: https://stackoverflow.com/questions/62711306/is-there-a-kind-of-reference-manual-for-z3

WBrozius commented 2 years ago

This page was useful: https://www.philipzucker.com/z3-rise4fun/guide.html