Age | Commit message (Expand) | Author |
2011-03-15 | Merge from cudd branch. This mostly just adds support for linking | Morgan Deters |
2011-03-14 | Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array b... | Morgan Deters |
2011-02-28 | Review of mktheorytraits, mkrewriter, and recent changes to other mk* scripts... | Morgan Deters |
2011-02-28 | minor doxygen build target fixes | Morgan Deters |
2011-02-26 | fix serious regression breakage (segfaults) caused by an off-by-one error in ... | Morgan Deters |
2011-02-26 | adding the variables count to the statistics in the expr manager | Dejan Jovanović |
2011-02-26 | adding statistics about how many different kinds of expressions we have creat... | Dejan Jovanović |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
2010-12-16 | minor fixes for correct doxygen output | Morgan Deters |
2010-12-14 | congruence closure module now supports things other than APPLY_UF; ported fro... | Morgan Deters |
2010-12-14 | permit PARAMETERIZED operators to be zero-ary | Morgan Deters |
2010-11-15 | Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer | Morgan Deters |
2010-11-08 | cleanup, documentation, SMT-LIBv2 compliance | Morgan Deters |
2010-10-31 | enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d... | Morgan Deters |
2010-10-29 | minor fixes as a result of review of Chris's getType() rewrite; also fix some... | Morgan Deters |
2010-10-28 | Changing NodeBuilder::debugCheckType() to maybeCheckType() | Christopher L. Conway |
2010-10-28 | Disabling bottom-up algorithm in NodeManager::getType() when type checking | Christopher L. Conway |
2010-10-27 | Small change to documentation in NodeManager::getType | Christopher L. Conway |
2010-10-27 | Slightly more efficient version of getType | Christopher L. Conway |
2010-10-27 | Modifying getType to use a non-recursive algorithm (Fixes: #228) | Christopher L. Conway |
2010-10-26 | GetValueCommand now gives a TUPLE as output, with the first operand the input... | Morgan Deters |
2010-10-25 | missing case in expr output; resolves bug 226 | Morgan Deters |
2010-10-24 | add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like pri... | Morgan Deters |
2010-10-22 | comment out the "interactive" check in SmtEngine::getValue() for now (resolve... | Morgan Deters |
2010-10-21 | * Option --no-type-checking now disables type checks in SmtEngine | Christopher L. Conway |
2010-10-12 | IDENTITY has been removed. | Tim King |
2010-10-12 | fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), debugPrintTyp... | Morgan Deters |
2010-10-12 | fix some leaks in parser, add debug code to node manager to find more | Morgan Deters |
2010-10-12 | Merge from cc-memout branch. Here are the main points | Morgan Deters |
2010-10-11 | use "forward" headers | Morgan Deters |
2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp... | Morgan Deters |
2010-10-09 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ... | Morgan Deters |
2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
2010-10-08 | * (define-fun...) now has proper type checking in non-debug builds | Morgan Deters |
2010-10-07 | type checking for define-fun in production builds; related to (and might reso... | Morgan Deters |
2010-10-07 | NodeSelfIterator implementation and unit test (resolves bug #204); also fix P... | Morgan Deters |
2010-10-07 | SMT-LIBv2 (define-fun...) command now functional; does eager expansion at pre... | Morgan Deters |
2010-10-06 | declare-sort, define-sort working but not thoroughly tested; define-fun half ... | Morgan Deters |
2010-10-05 | parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti... | Morgan Deters |
2010-10-04 | re-add a dependency to fix compile warnings | Morgan Deters |
2010-10-04 | remove/shuffle some #include dependencies; fix some documentation; apply codi... | Morgan Deters |
2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
2010-10-02 | revert a workaround fix to CDMap that was committed as part of the arith-inde... | Morgan Deters |
2010-09-28 | node iterator work | Morgan Deters |
2010-09-28 | fix TLS support for platforms (e.g. Mac OS X) where __thread storage class do... | Morgan Deters |
2010-09-27 | add workaround for systems (i.e., Mac OS X) that don't support __thread; also... | ACSYS |
2010-09-24 | Fix build system for Mac OS X builds (resolves bug #203) | Morgan Deters |
2010-09-21 | Rm'ing automatic type check in NodeBuilder for vars/constants | Christopher L. Conway |
2010-09-21 | remove assertion in TNode destructor and ensure all TNode methods check rc > ... | Morgan Deters |
2010-09-21 | some code cleanup, documentation, review of "kinded-iterator" code, and addit... | Morgan Deters |