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 be part of the SMT solver SMT-RAT 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 
Combining Equality Logic and Uninterpreted Functions with the Existing Theories in SMT-RAT
One task of this practical course is to design and implement a sophisticated approach to combine the aforementioned theories with the logics of (non)linear real/integer arithmetics which are already well supported by SMT-RAT.