This project provides an intermediate representation (IR) in Rust for SMT-LIB queries along with tools for performing computations over queries and transforming queries in various ways. To demonstrate the benefit to the automated reasoning community, the project includes two sample applications:
-
A tool to perform homomorphic transformations on SMT-LIB queries, with a focus on string theory. String function applications are extracted into variables, and variable names are canonicalized. Most importantly, the string literals themselves are modified. The string properties that have to be maintained when transforming a string literal depend on the context in which this literal is used; this context is determined through a callgraph representation of the SMT query. The string properties themselves and the string functions they depend on are described in the string_fcts module. The tool and its usage is described here.
-
A tool to transform SMT-LIB queries in supported subsets of the language into SAT problems. The tool and its usage is described here. The IR is described/documented here.
-
A tool to translate between an older "dialect" of SMT into the current standard. The tool and its usage are described here.
See CONTRIBUTING for more information.
This project is licensed under the Apache-2.0 License.