summaryrefslogtreecommitdiff
path: root/test/unit/theory
AgeCommit message (Expand)Author
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-12minor unit test fix-upsMorgan Deters
2010-10-12hooked up "we are incomplete" flag after conversation with Tim (a theory noti...Morgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-10-09fix to unit testsMorgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-09-28fix pre-registration of operator, previously committed; clean up theory engin...Morgan Deters
2010-09-13* New normal form for arithmetic is in place.Tim King
2010-08-17Merge from "cc" branch:Morgan Deters
2010-07-29fix TheoryEngineWhite, add documentation; related to bug #188Morgan Deters
2010-07-28Forcing a type check on Node construction in debug mode (Fixes: #188)Christopher L. Conway
2010-07-28fixed theory engine white test for new (old) theoryOf() behavior (re: bug 188)Morgan Deters
2010-07-22incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool);...Morgan Deters
2010-07-07Shared term manager tested and workingClark Barrett
2010-07-07Added shared term manager. Basic mechanism for identifying shared terms isClark Barrett
2010-07-06Moved registration to theory engineClark Barrett
2010-07-04With "-d extra-checking", rewrites are now checked (afterMorgan 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-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-27Preregistration has been turned on. Highly experimental eager splitting suppo...Tim King
2010-04-26Adding the intermediary TypeNode to represent (and separate) the Types at the...Dejan Jovanović
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-09added experimental "make lcov" target (it runs only unit tests); better cover...Morgan Deters
2010-04-08A handful of build system fixes:Morgan Deters
2010-04-05Minor refactorings, in response to code review (Bug #73)Christopher L. Conway
2010-04-04* Addressed issues brought up in Chris's review of Morgan'sMorgan 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-04-01PARSER STUFF:Morgan Deters
2010-03-30Highlights of this commit are:Morgan 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-02-26TheoryUFWhite tests are added. There are also accompanying bug fixes. These c...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback