SMT: Equality Logic With Uninterpreted
Functions
Koller, Lukas
June 2020

1

Introduction

Consider the problem of verifying the correctness of a program. One approachis, given pre-conditions, to check if the output of the program satisfies certain
post-conditions. A large formula is constructed from the program and its preand post-conditions. Thus, the problem of verifying the program comes down
to checking the satisfiability of the constructed formula.
Satisfiability modulo theories (SMT) solvers are widely used in program verification. As assigning and comparing values is a common task in programs,
it is convenient to use equalities in the formula. Hence, a SMT solver has tobe able to reason about equality. To reason about equality, any modern-day
SMT solver contains a solver for the theory of equality logic with uninterpretedfunctions (EUF) with an implementation of the congruence closure algorithm.
This paper gives an introduction to SMT and EUF. The essential congruence
closure algorithm is explained and an efficient implementation of the algorithm
is given using Directed-Acylic-Graphs (DAGs) and the Union-Find algorithm.
Ackermann (1954) showed that EUF is decidable. Based on this, Shostak(1978) formulated a decision procedure for formulas in EUF with the congruence
closure algorithm. Soon after efficient implementations using DAGs and theUnion-Find algorithm followed (Nelson and Oppen, 1980; Downey et al., 1980).
Today any modern-day SMT solver contains an efficient implementation of thecongruence closure algorithm as part of a solver for EUF (Moura and Bjørner,2008).

2

Satisfiability Modulo Theories (SMT)

Satisfiability modulo theories (SMT) is the satisfiability problem for formulaswith respect to some first-order theory, or combinations of first-order theories. A
first-order theory extends Boolean logic with specific predicates, functions, andquantifiers (non-logical symbols), thus SMT is a generalization of the Boolean
satisfiability problem (SAT). Compared to SAT, SMT allows a richer and more1

convenient representation of formulas, as SMT can reason about equality, linear
arithmetic, bit-vectors, and other first-order theories.
Example 2.1 (First-Order Theories). Examples for first-order theories are:
• Theory of Equality Logic introduces equality (=).
¬(x1 = x2 ) ∧ x1 = 4• Theory of Linear Arithmetic adds arithmetic functions, such as + and −,and arithmetic predicates, like = or <.
(3y + 2x − 1 = 0) ∧ (0 < x)
• Theory of Bit Vectors allows the use of binary numbers and binary operators, such as bit-shift (), XOR (⊕), or binary negation (∼).
(a  2) = c ∧ c ⊕ d

3

Theory of Equality Logic With Uninterpreted
Functions

The theory of equality logic with uninterpreted functions (EUF) extends Boolean
logic and adds the equality predicate (=). In EUF the equality is a binary predicate, which evaluates to True or False based on the axioms for an equivalence
relation:∀x. x = x

(Reflexivity)∀x. ∀y. x = y =⇒ y = x(Symmetry)∀x. ∀y. ∀z. x = y ∧ y = z =⇒ x = z(Transitivity)

Compared to Boolean logic variables in EUF are non-binary and are definedover an infinite domain, such as N or R. Functions in EUF are uninterpreted
and only maintain the property of functional congruence:
Definition 3.1 (Functional Congruence)
For each n > 0 and n-ary function f∀x̄, ȳ.

n^xi = yi =⇒ f (x̄) = f (ȳ)

i=1

By using uninterpreted functions the details and characteristics of functions
are ignored. This can generalize and simplify theorems and proofs. However,some properties of a function can be lost when replacing the function with anuninterpreted function.

2

Example 3.1 (Uninterpreted Functions & Commutativity). For some fixed
x1 ,x2 ,y1 , and y2 the following formula is valid as + is commutative.
x1 = y1 ∧ x2 = y2 =⇒ x1 + x2 = y2 + y1
When generalizing + with an uninterpreted function symbol f , we obtain:
x1 = y1 ∧ x2 = y2 =⇒ f (x1 , x2 ) = f (y2 , y1 )The formula is no longer valid as the uninterpreted function f is not commutative. A constraint can be added to the formula to keep the commutativity.
x1 = y1 ∧ x2 = y2 =⇒ f (x1 , x2 ) = f (y2 , y1 ) ∨ f (x1 , x2 ) = f (y1 , y2 )3.1

Congruence Closure Algorithm

The congruence closure algorithm was originally described by Shostak (1978).
With this algorithm, the satisfiability of a conjunction (∧) of equalities andinequalities with uninterpreted functions can be determined.
Algorithm(Congruence Closure)

Let F be a conjunction of equalities and inequalities with uninterpreted functions.
F :(

m
^

si = ti ) ∧ (n^

sj 6= tj )

j=m+1

i=1

Let S be the set of all equalities and inequalities in F , and let T
denote the set of all terms and subterms in F .
A partition of T is constructed as follows:(1) initially put all terms and subterms in their own congruence
class{{t} | t ∈ T }(2) for all 1 ≤ i ≤ ma. with si = ti merge the congruence classes of si and ti
b. propagate the new congruence with symmetry, transitivity,and functional congruence

The constructed partition on T induces a congruence relation ∼ on T . ∼ isa congruence relation, because it satisfies the axioms for an equivalence relation(reflexive, symmetric, and transitive), and also respects functional congruence.
A congruence closure is the smallest congruence relation that contains another relation R. ∼ is the congruence closure that contains all equalities in F
(Shostak, 1978), hence the algorithm is called congruence closure algorithm.
3

The satisfiability of the formula F can be determined with the following theorem (Shostak, 1978).
Theorem 1
F is satisfiable ⇐⇒ @si , ti ∈ T such that si ∼ ti and (si 6= ti ) ∈ S.
Proof Idea.
=⇒ (Soundness). Assume F is satisfiable. There has to exists a model for F .
All si , ti ∈ T with si ∼ ti must have the same value in the model, because themodel satisfies reflexivity, symmetry, transitivity, and functional congruence.
Hence there cannot be an inequality (si 6= ti ) ∈ S.
⇐= (Completeness). Assume there are no si , ti ∈ T such that si ∼ ti and(si 6= ti ) ∈ S. The goal is to construct a model for F . This is done byconstructing a Herbrand model for F . A
Herbrand model assigns a value toS∞each term in the term universe T∞ = i=0 Ti . Ti is inductively defined asfollows:
T0 = T, and Ti+1 = {f (t1 , . . . , tr ) | ti ∈ Ti } ∪ Ti
where f ranges over all function symbols that appear in F . The term universe
contains all possible terms that can be constructed by using all constants andfunction symbols that appear in F . The height of the term universe is infinite
because functions can be arbitrarily nested.
For all terms t ∈ T , the model can directly assign values based on ∼. For
all remaining terms in the term universe, values are assigned with an inductive
construction based on functional congruence.
If for a term t = f (x1 , . . . , xr ) ∈ Tj+1 −Tj there exists a functional congruent
term in Tj , then the model can assign the value from the functional congruent
term to t. Otherwise the model assigns a new value to t. The new value isobtained by evaluating f (x1 , . . . , xr ) with the values of its arguments. For allarguments xi , values already have been assigned as they are all contained in Tj .
The correctness of this construction is then proven by induction over theheight of the term universe (Shostak, 1978).

Example 3.2 (Congruence Closure Algorithm: unsatisfiable formula).
f (a, b) = a ∧ f (f (a, b), b) 6= a
• initial partition:{{a}, {b}, {f (a, b)}, {f (f (a, b), b)}}• impose f (a, b) = a:{{a, f (a, b)}, {b}, {f (f (a, b), b)}}4• a ∼ f (a, b), with functional congruence f (a, b) ∼ f (f (a, b), b):{{a, f (a, b), f (f (a, b), b)}, {b}}The partition yields f (f (a, b), b) ∼ a, but the formula contains the inequalityf (f (a, b), b) 6= a. With Theorem 1 the formula is unsatisfiable.
Example 3.3 (Congruence Closure Algorithm: satisfiable formula).
a = b ∧ b = c ∧ g(f (a), b) = g(f (c), a) ∧ f (a) 6= b
• initial partition:{{a}, {b}, {c}, {f (a)}, {f (c)}, {g(f (a), b)}, {g(f (c), a)}}• impose a = b:{{a, b}, {c}, {f (a)}, {f (c)}, {g(f (a), b)}, {g(f (c), a)}}• impose b = c:{{a, b, c}, {f (a)}, {f (c)}, {g(f (a), b)}, {g(f (c), a)}}• a ∼ c, with functional congruence f (a) ∼ (c):{{a, b, c}, {f (a), f (c)}, {g(f (a), b)}, {g(f (c), a)}}• f (a) ∼ f (c) and b ∼ a, with functional congruence g(f (a), b) ∼ g(f (c), a):{{a, b, c}, {f (a), f (c)}, {g(f (a), b), g(f (c), a)}}There are no inequalities that contradict ∼. From Theorem 1 follows that theformula is satisfiable.
Satisfiability of Arbitrary EUF-Formulas
The congruence closure algorithm can only decide the satisfiability for conjunctions of equalities and inequalities. The satisfiability for an arbitrary formula in
EUF is determined by determining the unsatisfiability of the disjunctive normal
form (DNF) of the negated formula. A DNF is unsatisfiable if all disjuncts areunsatisfiable. As each disjunct in a DNF is a conjunction, the unsatisfiabilityof each disjunct is determined with the congruence closure algorithm.
The disadvantage of this approach is that the DNF of a formula can be
exponentially larger than the original formula. This results in the decision procedure for an arbitrary formula in EUF having exponential worst-case runtime.
That is expected because the decision problem for arbitrary formulas in EUF is
NP-complete (Shostak, 1978).
53.2

Efficient Implementation of the Congruence Closure
Algorithm With Union-Find

One efficient implementation of the congruence closure algorithm uses the UnionFind algorithm and represents a formula as a Directed-Acyclic-Graph (DAG).
The implementation given here is based on an implementation given by Nelson
and Oppen (1980).
3.2.1

Union-Find Algorithm

Union-Find is an algorithm to efficiently maintain a partition on a set of elements. Every partition induces an equivalence relation with equivalence classes.
In Union-Find the membership of an element to an equivalence class is only
maintained by a reference to a single representative element of the equivalenceclass. This allows Union-Find to have a near-constant (inverse Ackermann’sfunction) worst-case time complexity (Tarjan, 1975).
Figure 1 shows a graphical representation of a partition (result from example
3.2) in Union-Find.
Two operations are defined to manipulate the partition:• Find(v): returns the representative element of the equivalence class, whichcontains the element v.
• Union(u,v): combines the two equivalence classes that contain the element u and the element v to one single equivalence class.

abf (a, b)f (f (a, b), b)

Figure1:
The
graphical
representationofthepartition{{a, f (a, b), f (f (a, b), b)}, {b}} in Union-Find is shown here. A dashededge represents the reference to the representative element of an equivalenceclass.

3.2.2

Directed-Acyclic-Graph (DAG)

A Directed-Acyclic-Graph (DAG) is a directed graph with no directed cycle. A
DAG G = (V, E) consists of a set of nodes V , and a set of edges E. Every nodev ∈ V has a label λ(v). The number of outgoing edges from v is denoted by
δ(v). The i-th successor of v is denoted by v[i] = u ∈ V , for 1 ≤ i ≤ δ(v).
Every term and subterm in a formula F is represented by a node in the DAG.
The label for each node corresponds to the root constant or function symbol of6the associated term or subterm. An edge is inserted from every function symbol
to all its arguments.
The construction of a DAG for a formula only considers the relationshipbetween function symbols and arguments. Equalities and inequalities in theformula are not considered for the construction of the DAG. Figure 2 shows two
DAGs that each represent a formula.
λ(v1 ) = fv1
λ(v2 ) = fv2

λ(u1 ) = fu1

λ(v3 ) = fv3

λ(u2 ) = fu2

λ(v4 ) = f

λ(u3 ) = av4

λ(u4 ) = bu3u4

λ(v5 ) = fv5(a)λ(v6 ) = av6(b)Figure 2: (a) DAG representing the formula f (a, b) = a ∧ f (f (a, b), b) 6= a,where e.g. u2 represents the subtrem f (a, b). (b) DAG representing the formulaf 5 (a) = a ∧ f 3 (a) = a ∧ f (a) 6= a.

3.2.3

Implementation

The Union-Find algorithm is sufficient to maintain and propagate an equivalence relation, but the partition constructed by the congruence closure algorithm
induces a congruence relation. The induced congruence relation also respects
functional congruence. To also maintain and propagate functional congruence,
the Union operation is extended by Merge.
An auxiliary function Congruent is defined to determine if two nodes represent congruent subterms.
1: function Congruent(u,v)
2:
3:
4:
5:

if λ(u) 6= λ(v) ∨ δ(u) 6= δ(v) then return FALSE
for 1 ≤ i ≤ δ(u) do
if Find(u[i]) 6= Find(v[i]) then return FALSE
return TRUE

7

1: function Merge(u,v)
2:
if Find(u) 6= Find(v) then3:
let Pu and Pv be sets of all congruent predecessors for u and v
4:Union(u, v)
5:
6:
7:

for (x, y) ∈ Pu × Pv do
if Find(x) 6= Find(y) ∧ Congruent(x, y) thenMerge(x, y)Merge uses the Union operation and additionally propagates functional
congruence. Representing a formula as a DAG allows an efficient propagationof functional congruence in Merge. Functional congruence is propagated fromfunction arguments to function symbols. As function arguments are successorsof function symbols in the DAG, functional congruence is propagated to congruent predecessors. Every congruence class has an associated set that contains all
nodes that are predecessors to any node in the congruence class. Let Pu denote
this set for the congruence class that contains the node u. With every Union
operation the corresponding predecessor sets are merged.

u1

u2

λ(u1 ) = fu1
λ(u2 ) = fu3

u4

λ(u3 ) = au2

λ(u1 ) = f

λ(u2 ) = fu3
λ(u4 ) = bu4

λ(u3 ) = a(a)λ(u4 ) = b(b)

Figure 3: A simple example to demonstrate the propagation of functional
congruence. A dashed edge again represents the reference to the representative element of an equivalence class. In (a) a DAG representing the formulaa = b ∧ f (a) = f (b) is shown. The equation a = b was just imposed. (b)shows the same DAG, but the new congruence was propagated via functional
congruence, resulting in the partition {{a, b}, {f (a), f (b)}}.
In Figure 3 the propagation of a new congruence via functional congruenceis shown in a simple example. The equality a = b is imposed in Figure 3 (a), by
merging the congruence classes of a and b. This is done by changing the referenceof u3 from itself to u4 , hence u3 and u4 are now in the same congruence class.
The predecessor set for u3 is Pu3 = {u1 }, and for u4 it is Pu4 = {u2 }. In thiscase the only pair of predecessors from both sets is (u2 , u1 ). Because u2 andu1 are functionally congruent, the congruence is propagated to u2 and u1 by
merging their congruence classes in Figure 3 (b).
With Congruent and Merge the decision procedure based on the congruence closure algorithm is implemented as follows:8Let F be a conjunction of equalities and inequalities with uninterpreted functions.
F :(

m
^

si = ti ) ∧ (

i=1

n
^

sj 6= tj )j=m+1

Let τ (t) be the node in the DAG for F , that corresponds to the termor substerm t in F .
1: for 1 ≤ i ≤ m do

Merge(τ (si ), τ (ti ))3: for m + 1 ≤ j ≤ n do
4:
if Find(τ (sj )) = Find(τ (tj )) then return UNSATISFIABLE
5: return SATISFIABLE
2:

Nelson and Oppen (1980) have shown that the congruence relation constructed in this implementation is the congruence closure that contains all equalities in F . From this follows that for any subterms s and t in F
Find(τ (s)) = Find(τ (t)) ⇐⇒ s ∼ tholds. Where ∼ is the congruence closure, that contains all equalities in F .
With this, the correctness of the implementation can be verified.
If the procedure returns UNSATISFIABLE then for some m + 1 ≤ j ≤ nthere exists sj and tj , with Find(τ (sj )) = Find(τ (tj )). sj and tj are in thesame congruence class. As F contains the inequality sj 6= tj , from Theorem 1
follows that F is unsatisfiable.
When the procedure returns SATISFIABLE then there is no m+1 ≤ j ≤ nsuch that sj and tj are in the same congruence class. From Theorem 1 follows
that F is satisfiable.
3.2.4

Complexity

Let G = (V, E) be the DAG, which represents the formula F . Let n = |V | bethe number of nodes in G, and let m = |E| be the number of edges in G.
With n nodes in G there can be at most n − 1 Merge operations until
all nodes are in the same congruence class. Hence there can be at most ben − 1 = O(n) recursive Merge operations in total. From this it can be proventhat for any sequence of Merge operations the number of Congruent calls isbounded by O(mn), and the number of Find calls from Congruent (line 4)
is bounded by O(m2 ) (Nelson and Oppen, 1980).
For O(n) Merge operations there are O(n) Find calls from line 2, plus
O(mn) Find calls from line 6, and O(m2 ) Find calls from Congruent. In total
there are O(m2 ) Find calls, which take O(m2 ) time. Each Union operation
9

takes constant time (Tarjan, 1975), resulting in O(n) time for O(n) Merge
operations. The time cost for maintaining the predecessor sets is O(n2 ) (Nelson
and Oppen, 1980).
All in all, this results in the worst-case time complexity of O(m2 ) for this
implementation.

4

Conclusion

This paper gave an introduction to SMT and EUF. The presented implementation of the congruence closure algorithm has a worst-case time complexity ofO(m2 ). Downey et al. (1980) have implemented a faster version (O(m log2 m))of the congruence closure algorithm, by using hash tables instead of DAGs.
An efficient solver for EUF with an implementation of the congruence closurealgorithm is part of any modern SMT solver, such as Z3 (Moura and Bjørner,2008) or CVC4 (Barrett et al., 2011).
With SMT solvers, tools for program verification, such as OpenJML (Cok,2011), have been created. OpenJML can verify a program by simply annotatingcode with pre- and post-conditions.
Besides tools for program verification, SMT solvers have numerous otherapplications, such as testcase generation, static analysis, and hardware verification. SMT solvers have also been integrated into interactive theorem provers
for higher-order logic, such as Isabelle/HOL (Nipkow et al., 2002).
In almost all of the applications, SMT solver must be able to efficiently
reason about equality.

References
Ackermann, W. (1954). Solvable cases of the decision problem. Studies in logic
and the foundations of mathematics. North-Holland Pub. Co.
Barrett, Clark, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan
Jovanovi’c, Tim King, Andrew Reynolds, and Cesare Tinelli (July 2011).
“CVC4”. In: Proceedings of the 23rd International Conference on Computer
Aided Verification (CAV ’11). Ed. by Ganesh Gopalakrishnan and Shaz
Qadeer. Vol. 6806. Lecture Notes in Computer Science. Snowbird, Utah.
Springer, pp. 171–177. url: http://www.cs.stanford.edu/ ~barrett/pubs/BCD+11.pdf.
Cok, David R. (2011). “OpenJML: JML for Java 7 by Extending OpenJDK”. In:
Proceedings of the Third International Conference on NASA Formal Methods. NFM’11. Pasadena, CA: Springer-Verlag, pp. 472–479. isbn: 9783642203978.
Downey, Peter J., Ravi Sethi, and Robert Endre Tarjan (Oct. 1980). “Variations
on the Common Subexpression Problem”. In: J. ACM 27.4, pp. 758–771.
issn: 0004-5411. doi: 10.1145/322217.322228. url: https://doi.org/
10.1145/322217.322228.

10

Moura, Leonardo De and Nikolaj Bjørner (2008). “Z3: an efficient SMT solver”.
In: TACAS’08/ETAPS’08 Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, pp. 337–340.
Nelson, Greg and Derek C. Oppen (Apr. 1980). “Fast Decision Procedures Basedon Congruence Closure”. In: J. ACM 27.2, pp. 356–364. issn: 0004-5411.
doi: 10.1145/322186.322198. url: https://doi.org/10.1145/322186.
322198.
Nipkow, Tobias, Markus Wenzel, and Lawrence C. Paulson (2002). Isabelle/HOL:
A Proof Assistant for Higher-Order Logic. Berlin, Heidelberg: Springer-Verlag.
isbn: 3540433767.
Shostak, Robert E. (July 1978). “An Algorithm for Reasoning about Equality”. In: Commun. ACM 21.7, pp. 583–585. issn: 0001-0782. doi: 10.1145/
359545.359570. url: https://doi.org/10.1145/359545.359570.
Tarjan, Robert Endre (Apr. 1975). “Efficiency of a Good But Not Linear Set
Union Algorithm”. In: J. ACM 22.2, pp. 215–225. issn: 0004-5411. doi: 10.
1145/321879.321884. url: https://doi.org/10.1145/321879.321884.

11