projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9e164f1) | patch
CongruenceClosure module now should support nullary congruence operators (now that...
authorMorgan Deters <mdeters@gmail.com>
Mon, 28 Feb 2011 07:49:56 +0000 (07:49 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 28 Feb 2011 07:49:56 +0000 (07:49 +0000)
commit320fc000e028c1a08b4453255fc80b0105b28bb3
treeaf06d8bdb5d5e59c5a2ddcee46ad46aa54f984fatree
parent9e164f1af5d2bd6f13eb894c8d395c7155590877commit | diff
CongruenceClosure module now should support nullary congruence operators (now that they are allowed for the datatypes theory, as in (APPLY_CONSTRUCTOR nil) or (APPLY_CONSTRUCTOR zero)).  It does this by treating such terms with zero children as non-candidates for congruence, even though they have the congruence kind APPLY_CONSTRUCTOR.
src/util/congruence_closure.h diff | blob | history