summaryrefslogtreecommitdiff
path: root/test/unit
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-10fix production-build unit testing errors (they assumed that assertions were on)Morgan Deters
2010-03-08This fixes regressions at levels >= 1 which were failingMorgan Deters
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-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-08Disabling the failing test case for the context.Dejan Jovanović
2010-02-06Preliminary support for types in parserChristopher L. Conway
2010-02-04build system for multi-level regressionsMorgan Deters
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
2010-02-04test infrastructure updated for multiple-level regressionsMorgan Deters
2010-02-04src/expr/kind.h is now automatically generated.Morgan Deters
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re...Morgan Deters
2010-02-03Adding extra test to parserChristopher L. Conway
2010-02-03context_mm testingDejan Jovanović
2010-02-03some more tests for the context.Dejan Jovanović
2010-02-02beginings of test for CDO. one failDejan Jovanović
2010-02-02Minor changes to parserChristopher L. Conway
2010-02-01Fixing the CVC grammar for parsing Boolean expressions. All the associativity...Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback