| 2010-03-15 |
Morgan Deters | This 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 Barrett | Fix 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 Deters | naive 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 King | Added 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 Deters | fix 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 King | Fixed 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 Deters | This 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 King | Improved 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 King | Committing 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 King | Added theory black box test. |
commit | commitdiff | tree |
| 2010-03-01 |
Tim King | Node builder tests that targetted properly detecting... |
commit | commitdiff | tree |
| 2010-03-01 |
Tim King | Added 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 King | TheoryUFWhite is passing. I fixed 2 errors. Unfortunat... |
commit | commitdiff | tree |
| 2010-02-27 |
Morgan Deters | fix compile error in black parser unit test after today... |
commit | commitdiff | tree |
| 2010-02-27 |
Morgan Deters | A 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 King | TheoryUFWhite tests are added. There are also accompany... |
commit | commitdiff | tree |
| 2010-02-26 |
Tim King | Fixed 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 King | Updated 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 King | Created basic node builder and kind tests. Also fixed... |
commit | commitdiff | tree |
| 2010-02-24 |
Tim King | Cleaned up and documented ecdata and theory_uf. |
commit | commitdiff | tree |
| 2010-02-24 |
Tim King | Committing 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 Deters | Re-committing revision 232 properly: |
commit | commitdiff | tree |
| 2010-02-22 |
Morgan Deters | undoing 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 Deters | resolve bug 32; public-facing interface functions in... |
commit | commitdiff | tree |
| 2010-02-22 |
Morgan Deters | fix bug 33 (statically link the "cvc4" binary); also... |
commit | commitdiff | tree |
| 2010-02-22 |
Morgan Deters | fix bug 22 (remove tracing from non-trace builds; remov... |
commit | commitdiff | tree |
| 2010-02-19 |
Morgan Deters | specialized 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 King | Initial draft of TheoryUF. Should compile without probl... |
commit | commitdiff | tree |
| 2010-02-17 |
Morgan Deters | fix 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 |
| 2010-02-13 |
Dejan Jovanović | Improvements to CNF conversion when already in CNF |
commit | commitdiff | tree |
| 2010-02-12 |
Dejan Jovanović | build fix |
commit | commitdiff | tree |
| 2010-02-12 |
Dejan Jovanović | Fix to compile out Debug(...) << ... statements in... |
commit | commitdiff | tree |
| 2010-02-12 |
Dejan Jovanović | Changes to hashing that solve the xinetd boolean benchm... |
commit | commitdiff | tree |
| 2010-02-11 |
Dejan Jovanović | svn ignore |
commit | commitdiff | tree |
| 2010-02-11 |
Christopher... | Adding precedence regressions |
commit | commitdiff | tree |
| 2010-02-10 |
Morgan Deters | note on setup(); for discussion at 2010.02.11 meeting |
commit | commitdiff | tree |
| 2010-02-10 |
Morgan Deters | svn:ignore for build stuff; add Liana to AUTHORS |
commit | commitdiff | tree |
| 2010-02-10 |
Dejan Jovanović | fixing annoying eclipse build settings, no more broken... |
commit | commitdiff | tree |
| 2010-02-10 |
Clark Barrett | Added calls to destructor in CDList plus optional flag... |
commit | commitdiff | tree |
| 2010-02-09 |
Dejan Jovanović | Changes to the CNF conversion and the SAT solver. All... |
commit | commitdiff | tree |
| 2010-02-09 |
Morgan Deters | removing other pieces of autotools stuff to fix bug #24 |
commit | commitdiff | tree |
| 2010-02-09 |
Morgan Deters | moving built-in kinds out of the kind.h prologue/middle... |
commit | commitdiff | tree |
| 2010-02-09 |
Dejan Jovanović | empty stubs for push and pop to fix the build fail |
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Disabling the failing test case for the context. |
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Fixing the test case, it had a unary or. The cnf conver... |
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Push/Pop parsing and commands |
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Moving the template stuff back into the header in order... |
commit | commitdiff | tree |
| 2010-02-07 |
Christopher... | Documenting type.h/cpp |
commit | commitdiff | tree |
| 2010-02-06 |
Morgan Deters | force sorting of AC_CONFIG_FILES, otherwise different... |
commit | commitdiff | tree |
| 2010-02-06 |
Christopher... | Preliminary support for types in parser |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog