This course aims at the design, implementation, and optimization of state-of-the-art decision procedures for equality logic and uninterpreted functions in SMT solving. The implementation will be based on the SMT-RAT toolbox and can benefit from its manifold features. We will form at least two teams and compare their solvers within a competition. The resulting solvers will be tested on the official SMT-LIB benchmarks and it will be compared also to state-of-the-art solvers.
Equality logic is an extension of pure propositional logic with equalities between theory atoms. In its 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.
The theory of uninterpreted functions further extends equality logic with function symbols, whose semantics is not interpreted. Thus the considered function symbols do not comprise any semantic meaning other than functional congruence, that is, we only know that if the same function f is applied to two different terms t and t’ with the same semantic value then we get the same function value (t=t’ implies f(t)=f(t’)).