Age | Commit message (Expand) | Author |
2011-04-25 | Monday tasks: | Morgan Deters |
2011-04-25 | Weekend work. The main points: | Morgan Deters |
2011-04-23 | * reviewed BooleanSimplification, added documentation & unit test | Morgan Deters |
2011-04-20 | numerous bugfixes | Morgan Deters |
2011-04-20 | Minor mixed-bag commit. Expected performance impact negligible. | Morgan Deters |
2011-04-20 | Tuesday end-of-day commit. | Morgan Deters |
2011-04-18 | more work on CVC language | Morgan Deters |
2011-04-18 | mostly CVC presentation language parsing and printing | Morgan Deters |
2011-04-18 | Partial merge from datatypes-merge branch: | Morgan Deters |
2011-04-15 | partial merge from portfolio branch, adding conversions (library-internal-onl... | Morgan Deters |
2011-04-11 | fix "make dist" issues in makefiles | Morgan Deters |
2011-04-10 | merge from replay branch | Morgan Deters |
2011-04-04 | Add documentation to Node and TNode (closes bug #201). | Morgan Deters |
2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
2011-03-30 | Add Valuation::getSatValue() so that theories can access the current | Morgan Deters |
2011-03-27 | fixes to attribute-internals warnings on 64-bit; also some GCC function attri... | Morgan Deters |
2011-03-26 | fix for bug 253, was propagating an asserted literal | Dejan Jovanović |
2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
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 |