Rusty Razor is a tool for constructing finite models for first-order theories with equality.
The model-finding algorithm is inspired by the Chase in database systems. Given an input first-order theory, Razor constructs a set of homomorphically minimal models that satisfy theory.
To learn more about the theoretical foundation of Razor, check out my PhD dissertation.
Provides a framework and interfaces to various components that are used for implementing the Chase. It also implements entrypoints for running the Chase.