summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-04Adding phase-caching to minisat. Dejan Jovanović
2010-03-03Some SAT stuff, not doing anything special yet, just to keep it in sync.Dejan Jovanović
2010-03-02* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"Morgan Deters
2010-03-01Added some documentation to theory_uf.Tim King
2010-02-28* context.h - Changed cdlist::push_back to use a new copy constructor instead...Dejan Jovanović
2010-02-28TheoryUFWhite is passing. I fixed 2 errors. Unfortunately, I also changed a ...Tim King
2010-02-27A bag of unrelated fixes to bring trunk more in-line with recentMorgan Deters
2010-02-27Adding --mmap option to use memory-mapped file input, which provides a margin...Christopher L. Conway
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-26Fixed a bug in CDList reallocation. (Also corrected a couple whitespace probl...Tim King
2010-02-26Changing the hashing in attributes to what Nodes do, i.e. hash on the id of t...Dejan Jovanović
2010-02-25Adding Node::getOperator()Christopher L. Conway
2010-02-25Updated uf to reflect APPLY structure after conversation with Chris. Also cor...Tim King
2010-02-25* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.Morgan Deters
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-24Cleaned up and documented ecdata and theory_uf.Tim King
2010-02-24Committing small changes to attribute, and theory to avoid future merge probl...Tim King
2010-02-23Minor optimizations to parser (use const string& for ids, keep only one bindi...Christopher L. Conway
2010-02-23cosmetic changes, comments, and renaming of Expr related stuff to Node (lefto...Dejan Jovanović
2010-02-22finally worksDejan Jovanović
2010-02-22Merging from branch branches/Liana r241Dejan Jovanović
2010-02-22Switching to types-as-attributes in parserChristopher L. Conway
2010-02-22* src/expr/attribute.h: fixed an issue with "const pointer"-valuedMorgan Deters
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
2010-02-22Re-committing revision 232 properly:Morgan Deters
2010-02-22undoing improperly-committed revision 232; will re-commit to get "svn blame" ...Morgan Deters
2010-02-22* Add virtual destructors to CnfStream, Theory, OutputChannel, andCesare Tinelli
2010-02-22Small changes to the smt-engine, removed the assertions list.Dejan Jovanović
2010-02-22resolve bug 32; public-facing interface functions in expr package must set cu...Morgan Deters
2010-02-22fix bug 33 (statically link the "cvc4" binary); also main driver cleanupMorgan 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-19Changing minArity of AND/OR to 1 in SMT parserChristopher L. Conway
2010-02-18Adding --no-checking option to disable semantic checks in parserChristopher L. Conway
2010-02-17Initial draft of TheoryUF. Should compile without problems. A decent amount o...Tim King
2010-02-16Moving parser error checking into AntlrParserChristopher L. Conway
2010-02-16Adding --parse-only optionChristopher L. Conway
2010-02-16removing assertion and warning that shouldn't be there. adding initialization...Dejan Jovanović
2010-02-16Converting semantic predicates in parser to AlwaysAssertionsChristopher L. Conway
2010-02-13simplification minisat Dejan Jovanović
2010-02-13Improvements to CNF conversion when already in CNFDejan Jovanović
2010-02-12build fixDejan Jovanović
2010-02-12Fix to compile out Debug(...) << ... statements in optimized mode. Someone pl...Dejan Jovanović
2010-02-12Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25mi...Dejan Jovanović
2010-02-10note on setup(); for discussion at 2010.02.11 meetingMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback