summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-12-14fix to static learning application in UF, resolves bug# 239Morgan 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-11-16Added Theory::presolve().Tim King
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-09bug fixes to model genMorgan Deters
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti...Morgan Deters
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply codi...Morgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-09-28fix predicate bug in UF; code cleanup in theory.cppMorgan 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-07-27Adding optional 'check' parameter to getType() methodsChristopher L. Conway
2010-07-07Added shared term manager. Basic mechanism for identifying shared terms isClark Barrett
2010-07-06Fixes for doubled-statistics (bug 171), a fix to muzzled builds and some mino...Morgan Deters
2010-07-04With "-d extra-checking", rewrites are now checked (afterMorgan Deters
2010-07-03With this commit come a number of changes to build system to supportMorgan Deters
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-07-02* Added white-box TheoryEngine test that tests the rewriterMorgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-29Merging the unate-propagator branch into the trunk. This is a big update so ...Tim King
2010-06-15fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)Morgan Deters
2010-06-15remove warnings about unknown #pragma GCC diagnostic on older compilersMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ...Tim King
2010-05-05bug fixes for types, old unit tests for types work nowDejan Jovanović
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-04-29Added the capability to construct expressions by passing the operator instead...Dejan Jovanović
2010-04-06* Add some protected ContextObj accessors for ContextObj-derived classes:Morgan Deters
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-04-01reran update-copyright.pl to get new contributors and add new header comments...Morgan Deters
2010-03-30Removing unnecessary .gitignoresChristopher L. Conway
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-03-30I think this finishes off the CDMap<>/Attribute leaksMorgan Deters
2010-03-30Highlights of this commit are:Morgan Deters
2010-03-25Adding comments to NodeManagerChristopher L. Conway
2010-03-25new domain-specific language for kinds files: permits characterization of dif...Morgan Deters
2010-03-23Fixed some memory cleanup and destruction issues with ContextObj, ECData, CDL...Tim King
2010-03-16* test/unit/Makefile.am, test/unit/expr/attribute_white.h,Morgan Deters
2010-03-15This checkin resolves bug #57.Morgan Deters
2010-03-12* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,Morgan Deters
2010-03-11naive rewriting to fix minisat invariant; rewrite x == x ==> TRUEMorgan Deters
2010-03-11Added some hand generated UF tests. Unfortunartely all of them work. Also fix...Tim King
2010-03-09Fixed non-debug build problemsTim King
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback