summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t...Dejan Jovanović
2010-03-10fix production-build unit testing errors (they assumed that assertions were on)Morgan Deters
2010-03-10Lexical scoping for let-bound variables (Bug #53)Christopher L. Conway
2010-03-10Adding preliminary let/flet support to SMT parser (Bug #51)Christopher L. Conway
2010-03-09Adding support for "distinct" builtin in SMT parserChristopher L. Conway
2010-03-09Adding support for sort U in QF_UF.Christopher L. Conway
2010-03-09Adding the smallest of test cases from the smtlib.Dejan Jovanović
2010-03-09removing makefile.inDejan Jovanović
2010-03-09Fixed non-debug build problemsTim King
2010-03-09one more simple test for ufDejan Jovanović
2010-03-09(no commit message)Dejan Jovanović
2010-03-08This fixes regressions at levels >= 1 which were failingMorgan Deters
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
2010-03-08Fixing Debug("prop") => Debug("node") typoDejan Jovanović
2010-03-08Improved output for theory ufTim King
2010-03-08some more sat stuff for tim: assertions now go to theory_uf Dejan Jovanović
2010-03-08Adding quiet output of make by default. There are two additional options to c...Dejan Jovanović
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 theory black box test.Tim King
2010-03-01Node builder tests that targetted properly detecting and handling expections ...Tim King
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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback