IntroductionNotationJoin Algorithms for Uninterpreted FunctionsAbstract Congruence ClosureJoin of Two Congruence ClosuresSpecial Cases for which the Join Algorithm is CompleteComplexity and OptimizationsRelated WorkLimits of Congruence Closure based ApproachesRelatively Complete Join AlgorithmInteresting Future ExtensionsConclusionJoin Algorithms for the Theory of UninterpretedFunctions?Sumit Gulwani1, Ashish Tiwari2, and George C. Necula11University of California, Berkeley, CA 94720, {gulwani,necula}@cs.berkeley.edu2SRI International, Menlo Park, CA 94025, [email protected]. The join of two sets of facts, E1and E2, is defined as the setof all facts that are implied independently by both E1and E2. Congru-ence closure is a widely used representation for sets of equational factsin the theory of uninterpreted function symbols (UFS). We present anoptimal join algorithm for special classes of the theory of UFS using theabstract congruence closure framework. Several known join algorithms,which work on a strict subclass, can be cast as specific instantiations ofour generic procedure. We demonstrate the limitations of any approachfor computing joins that is based on the use of congruence closure. Wealso mention some interesting open problems in this area.1 IntroductionComputational logic is used extensively in formal modeling and analysis of sys-tems, particularly in areas s uch as verification of hardware and software systems,and program analysis. A wide variety of logical theories are used for this pur-pose. However, even for the simplest of theories, reasoning on formulas in thepresence of the conjunction ∧ and disjunction ∨ connectives is computationallyhard. Unsurprisingly, therefore, almost all practical uses of logical computationhave come in the form of decision procedures that work on facts stored as con-junctions of atomic formulas. What happens when the application requires thecomputation of the logical disjunction of two such facts? Join algorithms providean approximate solution by constructing a conjunction of atomic formulas thatis implied by the original disjunction.Join algorithms were first studied in the context of program analysis. Ab-stract interpretation [5] is a well-known static program analysis technique thatcan be used to automatically generate program invariants, and to verify programassertions, even in the absence of loop invariants. The program is evaluated overa lattice of abstract states, each one representing one or more concrete executionstates. The lattice join ope ration (t) is used to compute the abstract state follow-ing a merge in a control-flow graph, from the abstract states before the merge?Research of the first and third authors was supported in part by NSF grants CCR-0081588, CCR-0085949, and CCR-0326577, and gifts from Microsoft Research. Re-search of the second author was supported in part by NSF grant CCR-0326540 andNASA Contract NAS1-20334.point. The join operation can be viewed as computing the intersection of thefacts (or union of the models) before the merge point. The lack of a suitable joinalgorithm restricts the utility of several interesting theories for abstract inter-pretation. Nevertheless, join algorithms are known for some important theoriessuch as linear arithmetic [10], linear inequalities [6,3], polynomial equations [17],and the initial term algebra [8,18].A join algorithm for a theory Th takes as input two sets of atomic factsand produces the strongest set of facts that is implied independently by boththe input sets of facts in Th. For example, the join of the sets {a = 2, b = 3}and {a = 1, b = 4} in the theory of linear arithmetic c an be represented by{a + b = 5}. The join of {a = x, b = f (x)} and {a = y, b = f(y)} in the theoryof uninterpreted function symbols (UFS) can be represented by {b = f (a)}.It is interesting to point out that though decision procedures for satisfiabilityof a conjunction of atomic formulas are well studied for a wide class of logicaltheories, the same is not true for join algorithms. Join algorithms app e ar to bemuch harder than the dec ision proce dures for the same theory. While there areefficient congruence closure based decision procedures for the theory of UFS, joinalgorithms for this theory have been studied in this paper and independentlyin [19]. In the special case of the theory of initial term algebra, several joinalgorithms have been proposed [1,18,8]. All of these algorithms primarily useEDAG/value graph like data structures [15,12].This paper has two main technical contributions. In Section 3, we present anabstract congruence closure based algorithm that generalizes all the known joinalgorithms for subclasses of UFS and can compute the join for a strictly biggersubclass of the theory of UFS than these algorithms. We show that the existingalgorithms are a special case of our algorithm.In Section 4 we present some results concerning the limitations of any congru-ence closure based approach for obtaining join algorithms for the general theoryof UFS. We show that the join of two finite sets of ground equations cannotbe finitely represented (using ground equations). In special cases when it canbe finitely represented, the presentation can become exponential. This partiallyexplains the lack of any known complete join algorithms for even special classesof the UFS theory.2 NotationA set Σ of function symbols and constants is called a signature. Function sym-bols in Σ are denoted by f, g and constants by a, b. In the context of programanalysis, these constants arise from program variables, and henceforth we referto them as (program) variables. We use T (Σ) to refer to the set of ground termsover Σ, which are constructed using symbols only from Σ. We use the notationft1. . . tkto refer to the term f(t1, . . , tk). We also use the notation fit to denotei applications of the unary function f on term t.Definition 1 (Join). Let Th be some (first-order) theory over a signature Σ.Let E1and E2be two sets of ground equations over Σ. The join of E1and E2in theory Th is denoted by E1tThE2, and is defined to be (any presentationfor) the set {s = t | s, t ∈ T (Σ), Th |= E1⇒ s = t, Th |= E2⇒ s = t}.We ignore the subscript Th from tThwhenever it is clear from the context.In this paper, we mainly concern ourselves with the theory of UFS. If E is aset of equations (interpreted as a binary relation over terms, not necessarilysymmetric), the notation →Edenotes the closure of E under