This course aims at the design, implementation, and optimization of state-of-the-art decision procedures for equality logic and uninterpreted functions. The implementation will take place within the SMT-RAT project and can benefit from it’s manifold features. The resulting solver will be tested on the official SMT-LIB benchmarks and be compared to state-of-the-art solvers. Furthermore, we will form at least two teams and compare their solvers within a competition.
Equality Logic
Equality logic is an extension to pure propositional logic that allows for equalities between theory atoms. In it’s most basic form, these theory atoms are only constants or variables. More involved logics like linear arithmetic can be seen as an extension allowing theory atoms to be a linear combination of theory variables and, furthermore, introducing arbitrary inequalities.
Uninterpreted Functions
The theory of uninterpreted functions consists of theory terms and function calls of theory terms. The terms and functions do not comprise any semantic meaning other than functional congruence, that is 