CC(X): Semantic Combination of Congruence Closure with Solvable Theories
Electr. Notes Theor. Comput. Sci., pp. 51-69, 2008.
arbitrary built-in solvable theoryshostak combinationsolvable theoriescanonized termsemantic combinationMore(12+)
We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information abou...More
Full Text (Upload PDF)
PPT (Upload PPT)