projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2010-03-31 Christopher... Fix bug in SMT-LIB with let/flet bindings commit | commitdiff | tree
2010-03-31 Christopher... Finishing parser cleanup. Code is now review-ready. commit | commitdiff | tree
2010-03-31 Christopher... More parser cleanup. Should fix problems with last... commit | commitdiff | tree
2010-03-31 Christopher... Code cleanup in parser commit | commitdiff | tree
2010-03-31 Christopher... Adding 'generated/' to .gitignore commit | commitdiff | tree
2010-03-30 Christopher... Removing unnecessary .gitignores commit | commitdiff | tree
2010-03-30 Christopher... Merging from branches/antlr3 (r246:354) commit | commitdiff | tree
2010-03-30 Morgan Detersagain, re-enabling integer/rational tests (though they... commit | commitdiff | tree
2010-03-30 Morgan DetersI think this finishes off the CDMap<>/Attribute leaks commit | commitdiff | tree
2010-03-30 Morgan Detersfixing mistaken commit to unit test Makefile.am which... commit | commitdiff | tree
2010-03-30 Morgan DetersHighlights of this commit are: commit | commitdiff | tree
2010-03-28 Tim KingImproved the documentation and testing for Rational. commit | commitdiff | tree
2010-03-28 Christopher... Rm'ing test file (sorry for spam) commit | commitdiff | tree
2010-03-28 Christopher... Adding test file commit | commitdiff | tree
2010-03-26 Tim KingAdded GMP backed Rational and Integer classes, and... commit | commitdiff | tree
2010-03-25 Christopher... Merging let/flet rules in SMT parser commit | commitdiff | tree
2010-03-25 Christopher... Adding comments to NodeManager commit | commitdiff | tree
2010-03-25 Morgan Detersnew domain-specific language for kinds files: permits... commit | commitdiff | tree
2010-03-23 Clark BarrettDocumented that ContextObj::destroy() only restores... commit | commitdiff | tree
2010-03-23 Tim KingFixed some memory cleanup and destruction issues with... commit | commitdiff | tree
2010-03-16 Morgan Deters* test/unit/Makefile.am, test/unit/expr/attribute_white.h, commit | commitdiff | tree
2010-03-15 Morgan DetersThis checkin resolves bug #57. commit | commitdiff | tree
2010-03-14 Morgan Deters* test/unit/context/context_black.h: added a test for... commit | commitdiff | tree
2010-03-13 Clark BarrettFix for bug 45 commit | commitdiff | tree
2010-03-12 Morgan Deters* src/context/cdmap.h: rename orderedIterator to iterat... commit | commitdiff | tree
2010-03-12 Dejan JovanovićFixing unnecessary construction of NOT nodes when... commit | commitdiff | tree
2010-03-12 Morgan Deters* Added shutdown() functions to SmtEngine, TheoryEngine... commit | commitdiff | tree
2010-03-11 Morgan Detersnaive rewriting to fix minisat invariant; rewrite ... commit | commitdiff | tree
2010-03-11 Dejan JovanovićChanging const TNode& to TNode in the CNF conversion... commit | commitdiff | tree
2010-03-11 Tim KingAdded some hand generated UF tests. Unfortunartely... commit | commitdiff | tree
2010-03-11 Dejan JovanovićBoolean variables were marked as theory literals by... commit | commitdiff | tree
2010-03-11 Dejan JovanovićFix for the main bug that was bugging me -- Bug 49... commit | commitdiff | tree
2010-03-10 Morgan Detersfix production-build unit testing errors (they assumed... commit | commitdiff | tree
2010-03-10 Christopher... Lexical scoping for let-bound variables (Bug #53) commit | commitdiff | tree
2010-03-10 Christopher... Adding preliminary let/flet support to SMT parser ... commit | commitdiff | tree
2010-03-09 Christopher... Adding support for "distinct" builtin in SMT parser commit | commitdiff | tree
2010-03-09 Christopher... Adding support for sort U in QF_UF. commit | commitdiff | tree
2010-03-09 Dejan JovanovićAdding the smallest of test cases from the smtlib. commit | commitdiff | tree
2010-03-09 Dejan Jovanovićremoving makefile.in commit | commitdiff | tree
2010-03-09 Tim KingFixed non-debug build problems commit | commitdiff | tree
2010-03-09 Dejan Jovanovićone more simple test for uf commit | commitdiff | tree
2010-03-09 Dejan Jovanović(no commit message) commit | commitdiff | tree
2010-03-08 Morgan DetersThis fixes regressions at levels >= 1 which were failing commit | commitdiff | tree
2010-03-08 Dejan Jovanovićadding simple-uf to the regressions, and the code that... commit | commitdiff | tree
2010-03-08 Dejan JovanovićFixing Debug("prop") => Debug("node") typo commit | commitdiff | tree
2010-03-08 Tim KingImproved output for theory uf commit | commitdiff | tree
2010-03-08 Dejan Jovanovićsome more sat stuff for tim: assertions now go to theory_uf commit | commitdiff | tree
2010-03-08 Dejan JovanovićAdding quiet output of make by default. There are two... commit | commitdiff | tree
2010-03-05 Morgan Deters* public/private code untangled (smt/smt_engine.h no... commit | commitdiff | tree
2010-03-04 Tim KingCommitting a bug fix from Dejan. This resolves an issue... commit | commitdiff | tree
2010-03-04 Dejan JovanovićAdding phase-caching to minisat. commit | commitdiff | tree
2010-03-03 Dejan JovanovićSome SAT stuff, not doing anything special yet, just... commit | commitdiff | tree
2010-03-02 Morgan Deters* NodeBuilder work: specifically, convenience builders... commit | commitdiff | tree
2010-03-01 Tim KingAdded theory black box test. commit | commitdiff | tree
2010-03-01 Tim KingNode builder tests that targetted properly detecting... commit | commitdiff | tree
2010-03-01 Tim KingAdded some documentation to theory_uf. commit | commitdiff | tree
2010-02-28 Dejan Jovanović* context.h - Changed cdlist::push_back to use a new... commit | commitdiff | tree
2010-02-28 Tim KingTheoryUFWhite is passing. I fixed 2 errors. Unfortunat... commit | commitdiff | tree
2010-02-27 Morgan Detersfix compile error in black parser unit test after today... commit | commitdiff | tree
2010-02-27 Morgan DetersA bag of unrelated fixes to bring trunk more in-line... commit | commitdiff | tree
2010-02-27 Christopher... Adding --mmap option to use memory-mapped file input... commit | commitdiff | tree
2010-02-26 Morgan Deters* test/unit/context/context_black.h: Test CDList<>... commit | commitdiff | tree
2010-02-26 Tim KingTheoryUFWhite tests are added. There are also accompany... commit | commitdiff | tree
2010-02-26 Tim KingFixed a bug in CDList reallocation. (Also corrected... commit | commitdiff | tree
2010-02-26 Dejan JovanovićChanging the hashing in attributes to what Nodes do... commit | commitdiff | tree
2010-02-25 Christopher... Adding Node::getOperator() commit | commitdiff | tree
2010-02-25 Tim KingUpdated uf to reflect APPLY structure after conversatio... commit | commitdiff | tree
2010-02-25 Morgan Deters* src/expr/node_builder.h: fixed some overly-aggressive... commit | commitdiff | tree
2010-02-25 Morgan Deters* src/expr/node.h: add a copy constructor. Apparently... commit | commitdiff | tree
2010-02-25 Tim KingCreated basic node builder and kind tests. Also fixed... commit | commitdiff | tree
2010-02-24 Tim KingCleaned up and documented ecdata and theory_uf. commit | commitdiff | tree
2010-02-24 Tim KingCommitting small changes to attribute, and theory to... commit | commitdiff | tree
2010-02-23 Christopher... Minor optimizations to parser (use const string& for... commit | commitdiff | tree
2010-02-23 Dejan Jovanovićcosmetic changes, comments, and renaming of Expr relate... commit | commitdiff | tree
2010-02-22 Dejan Jovanovićfinally works commit | commitdiff | tree
2010-02-22 Dejan JovanovićMerging from branch branches/Liana r241 commit | commitdiff | tree
2010-02-22 Christopher... Switching to types-as-attributes in parser commit | commitdiff | tree
2010-02-22 Morgan Deters* src/expr/attribute.h: fixed an issue with "const... commit | commitdiff | tree
2010-02-22 Morgan Deters* configure.ac: Remove doc/ from search path for Makefi... commit | commitdiff | tree
2010-02-22 Morgan DetersRe-committing revision 232 properly: commit | commitdiff | tree
2010-02-22 Morgan Detersundoing improperly-committed revision 232; will re... commit | commitdiff | tree
2010-02-22 Cesare Tinelli* Add virtual destructors to CnfStream, Theory, OutputC... commit | commitdiff | tree
2010-02-22 Dejan JovanovićSmall changes to the smt-engine, removed the assertions... commit | commitdiff | tree
2010-02-22 Morgan Detersresolve bug 32; public-facing interface functions in... commit | commitdiff | tree
2010-02-22 Morgan Detersfix bug 33 (statically link the "cvc4" binary); also... commit | commitdiff | tree
2010-02-22 Morgan Detersfix bug 22 (remove tracing from non-trace builds; remov... commit | commitdiff | tree
2010-02-19 Morgan Detersspecialized implementation for boolean node attributes... commit | commitdiff | tree
2010-02-19 Morgan Deters* Attribute infrastructure -- static design. Documenta... commit | commitdiff | tree
2010-02-19 Christopher... Changing minArity of AND/OR to 1 in SMT parser commit | commitdiff | tree
2010-02-18 Christopher... Adding --no-checking option to disable semantic checks... commit | commitdiff | tree
2010-02-18 Christopher... Rm'ing doc from SUBDIRS commit | commitdiff | tree
2010-02-18 Christopher... Adding doxygen configuration parameters and doxygen... commit | commitdiff | tree
2010-02-17 Tim KingInitial draft of TheoryUF. Should compile without probl... commit | commitdiff | tree
2010-02-17 Morgan Detersfix bug 27: --with-cxxtest-dir=(relative-path) now... commit | commitdiff | tree
2010-02-16 Christopher... Moving parser error checking into AntlrParser commit | commitdiff | tree
2010-02-16 Christopher... Adding --parse-only option commit | commitdiff | tree
2010-02-16 Dejan Jovanovićremoving assertion and warning that shouldn't be there... commit | commitdiff | tree
2010-02-16 Christopher... Removing spurious commit of configure commit | commitdiff | tree
2010-02-16 Christopher... Converting semantic predicates in parser to AlwaysAsser... commit | commitdiff | tree
2010-02-13 Dejan Jovanovićsimplification minisat commit | commitdiff | tree
next