summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2010-04-01PARSER STUFF:Morgan Deters
2010-03-31Finishing parser cleanup. Code is now review-ready.Christopher L. Conway
2010-03-30Removing unnecessary .gitignoresChristopher L. Conway
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-03-30again, re-enabling integer/rational tests (though they still fail to compile ...Morgan Deters
2010-03-30I think this finishes off the CDMap<>/Attribute leaksMorgan Deters
2010-03-30fixing mistaken commit to unit test Makefile.am which removed testsMorgan Deters
2010-03-30Highlights of this commit are:Morgan Deters
2010-03-28Improved the documentation and testing for Rational.Tim King
2010-03-26Added GMP backed Rational and Integer classes, and white box tests for them. ...Tim King
2010-03-25Adding comments to NodeManagerChristopher L. Conway
2010-03-16* test/unit/Makefile.am, test/unit/expr/attribute_white.h,Morgan Deters
2010-03-14* test/unit/context/context_black.h: added a test for Clark's fix to bug #45.Morgan Deters
2010-03-12* src/context/cdmap.h: rename orderedIterator to iterator, do awayMorgan Deters
2010-03-12Fixing unnecessary construction of NOT nodes when generating conflict clause...Dejan Jovanović
2010-03-11Changing const TNode& to TNode in the CNF conversion + a new small benchmark ...Dejan Jovanović
2010-03-11Added some hand generated UF tests. Unfortunartely all of them work. Also fix...Tim King
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t...Dejan Jovanović
2010-03-10fix production-build unit testing errors (they assumed that assertions were on)Morgan Deters
2010-03-10Adding preliminary let/flet support to SMT parser (Bug #51)Christopher L. Conway
2010-03-09Adding support for "distinct" builtin in SMT parserChristopher L. Conway
2010-03-09Adding the smallest of test cases from the smtlib.Dejan Jovanović
2010-03-09removing makefile.inDejan Jovanović
2010-03-09one more simple test for ufDejan Jovanović
2010-03-09(no commit message)Dejan Jovanović
2010-03-08This fixes regressions at levels >= 1 which were failingMorgan Deters
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
2010-03-08Improved output for theory ufTim King
2010-03-05* public/private code untangled (smt/smt_engine.h no longer #includesMorgan Deters
2010-03-04Committing a bug fix from Dejan. This resolves an issue with restoring ECData.Tim King
2010-03-02* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"Morgan Deters
2010-03-01Added theory black box test.Tim King
2010-03-01Node builder tests that targetted properly detecting and handling expections ...Tim King
2010-02-27fix compile error in black parser unit test after today's change to parser codeMorgan Deters
2010-02-27A bag of unrelated fixes to bring trunk more in-line with recentMorgan Deters
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
2010-02-26TheoryUFWhite tests are added. There are also accompanying bug fixes. These c...Tim King
2010-02-25Adding Node::getOperator()Christopher L. Conway
2010-02-25* src/expr/node.h: add a copy constructor. Apparently GCC doesn'tMorgan Deters
2010-02-25Created basic node builder and kind tests. Also fixed a couple of node builde...Tim King
2010-02-23cosmetic changes, comments, and renaming of Expr related stuff to Node (lefto...Dejan Jovanović
2010-02-22Switching to types-as-attributes in parserChristopher L. Conway
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
2010-02-22resolve bug 32; public-facing interface functions in expr package must set cu...Morgan Deters
2010-02-22fix bug 22 (remove tracing from non-trace builds; remove all outputMorgan Deters
2010-02-19specialized implementation for boolean node attributes ("flags"): they now sh...Morgan Deters
2010-02-19* Attribute infrastructure -- static design. Documentation is coming.Morgan Deters
2010-02-16Converting semantic predicates in parser to AlwaysAssertionsChristopher L. Conway
2010-02-11Adding precedence regressionsChristopher L. Conway
2010-02-09Changes to the CNF conversion and the SAT solver. All regression pass now, an...Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback