CC(X): Semantic Combination of Congruence Closure with Solvable Theories

Electr. Notes Theor. Comput. Sci., pp. 51-69, 2008.

Cited by: 44|Bibtex|Views2|Links
EI
Keywords:
arbitrary built-in solvable theoryshostak combinationsolvable theoriescanonized termsemantic combinationMore(12+)

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments