Building a Rewrite Rule Database: An Ambitious Project

This post proposes the creation of a database of rewrite rules encompassing various domains, including integer properties, differentiation, set theory, bitvectors, functional programs, and more. The author lists numerous existing projects and libraries containing rewrite rules and discusses the feasibility and challenges of unifying these rules into a common format. While some rules can be directly proven by existing SMT solvers, the author argues that a well-defined rewrite rule database is crucial for precise rewriting and manipulations in specific application contexts and will be a valuable resource for future research.