cvc5.git
2010-04-05 Christopher... Removing unused functions that were causing compiler...
2010-04-05 Christopher... Simplifying ANTLR3 overrides
2010-04-05 Morgan Detersupdating COPYING file to reflect that antlr_input_impor...
2010-04-05 Christopher... Updating copyright exclusion
2010-04-05 Christopher... Moving sources copied from libantlr3c to separate file
2010-04-05 Christopher... Ignoring gcov files
2010-04-05 Christopher... Moving code imported from libantlr3c to separate file...
2010-04-05 Morgan Detersfix most of the warnings in the parser by (1) quieting...
2010-04-05 Christopher... Adding match override to AntlrInput, in attempt to...
2010-04-05 Christopher... Minor refactorings, in response to code review (Bug...
2010-04-05 Christopher... Typos and renames for code review
2010-04-05 Morgan Detersminor formatting and code guidelines, related to parser...
2010-04-04 Morgan Deters* Addressed issues brought up in Chris's review of...
2010-04-04 Morgan Deters* Node::isAtomic() now looks at an "atomic" attribute...
2010-04-04 Morgan DetersRecommit revision 365 (undoing revision 375, which...
2010-04-03 Christopher... Reverting r365
2010-04-02 Christopher... Overriding ANTLR3 error recovery routine
2010-04-02 Christopher... Fixing double delete bug in main.cpp
2010-04-02 Tim KingFixed the 32 bit vs. 64 bit problem in the rational...
2010-04-01 Christopher... Changing min/maxArity to use metakind info.
2010-04-01 Christopher... Parser tweaks to address review
2010-04-01 Christopher... Adding newly generated files
2010-04-01 Christopher... Removing Expr::operator=(uintptr_t n), as it's no longe...
2010-04-01 Morgan Deterscvc4 --show-config now gives library version
2010-04-01 Morgan Detersreran update-copyright.pl to get new contributors and...
2010-04-01 Morgan Deters* Minor code formatting stuff in src/expr/type.{h,cpp...
2010-04-01 Morgan Detersminor forgotten things in last commit
2010-04-01 Morgan DetersPARSER STUFF:
2010-04-01 Christopher... Adding check for --disable-shared on --enable-coverage
2010-03-31 Christopher... Fix bug in SMT-LIB with let/flet bindings
2010-03-31 Christopher... Finishing parser cleanup. Code is now review-ready.
2010-03-31 Christopher... More parser cleanup. Should fix problems with last...
2010-03-31 Christopher... Code cleanup in parser
2010-03-31 Christopher... Adding 'generated/' to .gitignore
2010-03-30 Christopher... Removing unnecessary .gitignores
2010-03-30 Christopher... Merging from branches/antlr3 (r246:354)
2010-03-30 Morgan Detersagain, re-enabling integer/rational tests (though they...
2010-03-30 Morgan DetersI think this finishes off the CDMap<>/Attribute leaks
2010-03-30 Morgan Detersfixing mistaken commit to unit test Makefile.am which...
2010-03-30 Morgan DetersHighlights of this commit are:
2010-03-28 Tim KingImproved the documentation and testing for Rational.
2010-03-28 Christopher... Rm'ing test file (sorry for spam)
2010-03-28 Christopher... Adding test file
2010-03-26 Tim KingAdded GMP backed Rational and Integer classes, and...
2010-03-25 Christopher... Merging let/flet rules in SMT parser
2010-03-25 Christopher... Adding comments to NodeManager
2010-03-25 Morgan Detersnew domain-specific language for kinds files: permits...
2010-03-23 Clark BarrettDocumented that ContextObj::destroy() only restores...
2010-03-23 Tim KingFixed some memory cleanup and destruction issues with...
2010-03-16 Morgan Deters* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
2010-03-15 Morgan DetersThis checkin resolves bug #57.
2010-03-14 Morgan Deters* test/unit/context/context_black.h: added a test for...
2010-03-13 Clark BarrettFix for bug 45
2010-03-12 Morgan Deters* src/context/cdmap.h: rename orderedIterator to iterat...
2010-03-12 Dejan JovanovićFixing unnecessary construction of NOT nodes when...
2010-03-12 Morgan Deters* Added shutdown() functions to SmtEngine, TheoryEngine...
2010-03-11 Morgan Detersnaive rewriting to fix minisat invariant; rewrite ...
2010-03-11 Dejan JovanovićChanging const TNode& to TNode in the CNF conversion...
2010-03-11 Tim KingAdded some hand generated UF tests. Unfortunartely...
2010-03-11 Dejan JovanovićBoolean variables were marked as theory literals by...
2010-03-11 Dejan JovanovićFix for the main bug that was bugging me -- Bug 49...
2010-03-10 Morgan Detersfix production-build unit testing errors (they assumed...
2010-03-10 Christopher... Lexical scoping for let-bound variables (Bug #53)
2010-03-10 Christopher... Adding preliminary let/flet support to SMT parser ...
2010-03-09 Christopher... Adding support for "distinct" builtin in SMT parser
2010-03-09 Christopher... Adding support for sort U in QF_UF.
2010-03-09 Dejan JovanovićAdding the smallest of test cases from the smtlib.
2010-03-09 Dejan Jovanovićremoving makefile.in
2010-03-09 Tim KingFixed non-debug build problems
2010-03-09 Dejan Jovanovićone more simple test for uf
2010-03-09 Dejan Jovanović(no commit message)
2010-03-08 Morgan DetersThis fixes regressions at levels >= 1 which were failing
2010-03-08 Dejan Jovanovićadding simple-uf to the regressions, and the code that...
2010-03-08 Dejan JovanovićFixing Debug("prop") => Debug("node") typo
2010-03-08 Tim KingImproved output for theory uf
2010-03-08 Dejan Jovanovićsome more sat stuff for tim: assertions now go to theory_uf
2010-03-08 Dejan JovanovićAdding quiet output of make by default. There are two...
2010-03-05 Morgan Deters* public/private code untangled (smt/smt_engine.h no...
2010-03-04 Tim KingCommitting a bug fix from Dejan. This resolves an issue...
2010-03-04 Dejan JovanovićAdding phase-caching to minisat.
2010-03-03 Dejan JovanovićSome SAT stuff, not doing anything special yet, just...
2010-03-02 Morgan Deters* NodeBuilder work: specifically, convenience builders...
2010-03-01 Tim KingAdded theory black box test.
2010-03-01 Tim KingNode builder tests that targetted properly detecting...
2010-03-01 Tim KingAdded some documentation to theory_uf.
2010-02-28 Dejan Jovanović* context.h - Changed cdlist::push_back to use a new...
2010-02-28 Tim KingTheoryUFWhite is passing. I fixed 2 errors. Unfortunat...
2010-02-27 Morgan Detersfix compile error in black parser unit test after today...
2010-02-27 Morgan DetersA bag of unrelated fixes to bring trunk more in-line...
2010-02-27 Christopher... Adding --mmap option to use memory-mapped file input...
2010-02-26 Morgan Deters* test/unit/context/context_black.h: Test CDList<>...
2010-02-26 Tim KingTheoryUFWhite tests are added. There are also accompany...
2010-02-26 Tim KingFixed a bug in CDList reallocation. (Also corrected...
2010-02-26 Dejan JovanovićChanging the hashing in attributes to what Nodes do...
2010-02-25 Christopher... Adding Node::getOperator()
2010-02-25 Tim KingUpdated uf to reflect APPLY structure after conversatio...
2010-02-25 Morgan Deters* src/expr/node_builder.h: fixed some overly-aggressive...
2010-02-25 Morgan Deters* src/expr/node.h: add a copy constructor. Apparently...
2010-02-25 Tim KingCreated basic node builder and kind tests. Also fixed...
2010-02-24 Tim KingCleaned up and documented ecdata and theory_uf.
next