summaryrefslogtreecommitdiff
path: root/src/util/congruence_closure.h
AgeCommit message (Expand)Author
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-04-05Memory fix for congruence closure; affects many UF benchmarks, probably AX too.Morgan Deters
2011-02-28CongruenceClosure module now should support nullary congruence operators (now...Morgan Deters
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-12-14make some CC module methods private that should not have been publicMorgan Deters
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-17add some stats to UF/CCMorgan Deters
2010-11-17The "UF engineering issues" release, after much profiling.Morgan Deters
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply codi...Morgan Deters
2010-09-14ensure uf/congruence closure debugging stuff isn't called in production buildsMorgan Deters
2010-08-19UF theory bug fixes, code cleanup, and extra debugging output.Morgan Deters
2010-08-17Merge from "cc" branch:Morgan Deters
2010-06-30add documentation for additional clarity, re-add addTerm()Morgan Deters
2010-06-30checking in CC module interface for reference.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback