| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
| 2010-12-14 |
Morgan Deters | congruence closure module now supports things other... |
blob | commitdiff | raw | diff to current |
| 2010-10-28 |
Christopher L. Conway | Changing NodeBuilder::debugCheckType() to maybeCheckType() |
blob | commitdiff | raw | diff to current |
| 2010-10-27 |
Christopher L. Conway | Modifying getType to use a non-recursive algorithm... |
blob | commitdiff | raw | diff to current |
| 2010-10-24 |
Morgan Deters | add a CVC4_UNDEFINED keyword, for intentionally undefin... |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Morgan Deters | comment out the "interactive" check in SmtEngine::getVa... |
blob | commitdiff | raw | diff to current |
| 2010-10-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | type checking for define-fun in production builds;... |
blob | commitdiff | raw | diff to current |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
blob | commitdiff | raw | diff to current |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
blob | commitdiff | raw | diff to current |
| 2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
blob | commitdiff | raw | diff to current |
| 2010-09-28 |
Morgan Deters | fix TLS support for platforms (e.g. Mac OS X) where... |
blob | commitdiff | raw | diff to current |
| 2010-09-27 |
ACSYS | add workaround for systems (i.e., Mac OS X) that don... |
blob | commitdiff | raw | diff to current |
| 2010-09-21 |
Morgan Deters | remove assertion in TNode destructor and ensure all... |
blob | commitdiff | raw | diff to current |
| 2010-09-21 |
Christopher L. Conway | Moving automatic type check to NodeBuilder (Fixes:... |
blob | commitdiff | raw | diff to current |
| 2010-09-20 |
Dejan Jovanović | bitvector rewriting for the core theory and testcases |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
| 2010-07-29 |
Christopher L. Conway | Adding configuration_private.h to allow inlining of... |
blob | commitdiff | raw | diff to current |
| 2010-07-28 |
Christopher L. Conway | Forcing a type check on Node construction in debug... |
blob | commitdiff | raw | diff to current |
| 2010-07-27 |
Christopher L. Conway | Adding optional 'check' parameter to getType() methods |
blob | commitdiff | raw | diff to current |
| 2010-07-06 |
Morgan Deters | Don't eagerly collect zombies. This should speed up... |
blob | commitdiff | raw | diff to current |
| 2010-07-02 |
Morgan Deters | * Added white-box TheoryEngine test that tests the... |
blob | commitdiff | raw | diff to current |
| 2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
blob | commitdiff | raw | diff to current |
| 2010-06-16 |
Tim King | This commit just contains miscellaneous arithmetic... |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
| 2010-05-31 |
Christopher L. Conway | First draft implementation of mkAssociative |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Morgan Deters | fix bug #134: infinite deallocation loop |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Morgan Deters | Remove isAtomic() as per 4/27/2010 meeting. Add commen... |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Christopher L. Conway | Adding NodeManager::prepareToBeDestroyed() (Fixes:... |
blob | commitdiff | raw | diff to current |
| 2010-05-13 |
Christopher L. Conway | Minor refactorings and corrections to comments |
blob | commitdiff | raw | diff to current |
| 2010-05-04 |
Dejan Jovanović | Type-checking classes and hooks (not tested yet). |
blob | commitdiff | raw | diff to current |
| 2010-05-02 |
Dejan Jovanović | smt parser for bit-vectors |
blob | commitdiff | raw | diff to current |
| 2010-05-01 |
Dejan Jovanović | Fix for the last night's build errors (type that broke... |
blob | commitdiff | raw | diff to current |
| 2010-04-30 |
Dejan Jovanović | Fix for bug 115, mapping was going in the wrong direction. |
blob | commitdiff | raw | diff to current |
| 2010-04-29 |
Dejan Jovanović | Added the capability to construct expressions by passin... |
blob | commitdiff | raw | diff to current |
| 2010-04-26 |
Dejan Jovanović | Some cleanup. Also added the integer and real types. |
blob | commitdiff | raw | diff to current |
| 2010-04-26 |
Dejan Jovanović | Adding the intermediary TypeNode to represent (and... |
blob | commitdiff | raw | diff to current |
| 2010-04-15 |
Christopher L. Conway | Enhancements to NodeManager tests, taking advantage... |
blob | commitdiff | raw | diff to current |
| 2010-04-14 |
Dejan Jovanović | Marging from types 404:415, changes: Massive |
blob | commitdiff | raw | diff to current |
| 2010-04-13 |
Christopher L. Conway | Doxygen fixes |
blob | commitdiff | raw | diff to current |
| 2010-04-06 |
Morgan Deters | * Add some protected ContextObj accessors for ContextOb... |
blob | commitdiff | raw | diff to current |
| 2010-04-05 |
Christopher L. Conway | Adding black-box tests for NodeManager (Closes bug... |
blob | commitdiff | raw | diff to current |
| 2010-04-05 |
Christopher L. Conway | Minor refactorings, in response to code review (Bug... |
blob | commitdiff | raw | diff to current |
| 2010-04-05 |
Christopher L. Conway | Typos and renames for code review |
blob | commitdiff | raw | diff to current |
| 2010-04-04 |
Morgan Deters | * Addressed issues brought up in Chris's review of... |
blob | commitdiff | raw | diff to current |
| 2010-04-04 |
Morgan Deters | * Node::isAtomic() now looks at an "atomic" attribute... |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | reran update-copyright.pl to get new contributors and... |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | PARSER STUFF: |
blob | commitdiff | raw | diff to current |
| 2010-03-31 |
Christopher L. Conway | Finishing parser cleanup. Code is now review-ready. |
blob | commitdiff | raw | diff to current |
| 2010-03-30 |
Morgan Deters | I think this finishes off the CDMap<>/Attribute leaks |
blob | commitdiff | raw | diff to current |
| 2010-03-30 |
Morgan Deters | Highlights of this commit are: |
blob | commitdiff | raw | diff to current |
| 2010-03-25 |
Christopher L. Conway | Adding comments to NodeManager |
blob | commitdiff | raw | diff to current |
| 2010-03-23 |
Tim King | Fixed some memory cleanup and destruction issues with... |
blob | commitdiff | raw | diff to current |
| 2010-03-16 |
Morgan Deters | * test/unit/Makefile.am, test/unit/expr/attribute_white.h, |
blob | commitdiff | raw | diff to current |
| 2010-03-12 |
Morgan Deters | * src/context/cdmap.h: rename orderedIterator to iterat... |
blob | commitdiff | raw | diff to current |
| 2010-03-08 |
Morgan Deters | This fixes regressions at levels >= 1 which were failing |
blob | commitdiff | raw | diff to current |
| 2010-03-05 |
Morgan Deters | * public/private code untangled (smt/smt_engine.h no... |
blob | commitdiff | raw | diff to current |
| 2010-03-02 |
Morgan Deters | * NodeBuilder work: specifically, convenience builders... |
blob | commitdiff | raw | diff to current |
| 2010-02-26 |
Morgan Deters | * test/unit/context/context_black.h: Test CDList<>... |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Christopher L. Conway | Adding Node::getOperator() |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Morgan Deters | * src/expr/node_builder.h: fixed some overly-aggressive... |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Morgan Deters | * src/expr/node.h: add a copy constructor. Apparently... |
blob | commitdiff | raw | diff to current |
| 2010-02-23 |
Christopher L. Conway | Minor optimizations to parser (use const string& for... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Christopher L. Conway | Switching to types-as-attributes in parser |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Morgan Deters | * src/expr/attribute.h: fixed an issue with "const... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Morgan Deters | * configure.ac: Remove doc/ from search path for Makefi... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Morgan Deters | resolve bug 32; public-facing interface functions in... |
blob | commitdiff | raw | diff to current |
| 2010-02-19 |
Morgan Deters | * Attribute infrastructure -- static design. Documenta... |
blob | commitdiff | raw | diff to current |
| 2010-02-12 |
Dejan Jovanović | Changes to hashing that solve the xinetd boolean benchm... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | remove -*- c++ -*- emacs tag from source files (it... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | minor fix for update-copyright.pl; ran update-copyright... |
blob | commitdiff | raw | diff to current |
| 2010-01-25 |
Morgan Deters | minor fixes to scoped-context node manager |
blob | commitdiff | raw | diff to current |
| 2010-01-25 |
Morgan Deters | scoped node managers |
blob | commitdiff | raw | diff to current |
| 2009-12-17 |
Morgan Deters | update-copyright.pl now retrieves and incorporates... |
blob | commitdiff | raw | diff to current |
| 2009-12-17 |
Morgan Deters | + test infrastructure fixes |
blob | commitdiff | raw | diff to current |
| 2009-12-16 |
Morgan Deters | + refactoring fixes for expr package based on code... |
blob | commitdiff | raw | diff to current |
| 2009-12-16 |
Tim King | Small refactoring changes for the expr package. |
blob | commitdiff | raw | diff to current |
| 2009-12-16 |
Morgan Deters | Fixes to the build system: |
blob | commitdiff | raw | diff to current |
| 2009-12-11 |
Dejan Jovanović | Extracted the public Expr and ExprManager interface... |
blob | commitdiff | raw | diff to current |
| 2009-12-10 |
Dejan Jovanović | killing expr into node... |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history