Age | Commit message (Expand) | Author |
2011-04-15 | partial merge from portfolio branch, adding conversions (library-internal-onl... | Morgan Deters |
2011-04-14 | reverting back the minisat code and adding a simpler one that shouldn't chang... | Dejan Jovanović |
2011-04-14 | Three things: | Morgan Deters |
2011-04-14 | fixing an uninitialized literal variable | Dejan Jovanović |
2011-04-13 | adding support for unit conflicts in minisat... | Dejan Jovanović |
2011-04-13 | fix compiler warning in non-replay builds | Morgan Deters |
2011-04-13 | cache the LET rewriting (and defined-function expansion too)---it wasn't befo... | Morgan Deters |
2011-04-13 | add disequality token ("/=") and rules to CVC parser | Morgan Deters |
2011-04-12 | another small fix to "make dist" that can lead to a misconfigured tarball | Morgan Deters |
2011-04-11 | Transitive closure module is working | Clark Barrett |
2011-04-11 | fix "make dist" issues in makefiles | Morgan Deters |
2011-04-10 | merge from replay branch | Morgan Deters |
2011-04-10 | Add -lprofiler when --with-google-perftools is offered; also fix some newswir... | Morgan Deters |
2011-04-09 | changing the sat solver to assert propagated literals back to the theories | Dejan Jovanović |
2011-04-08 | Added util class | Clark Barrett |
2011-04-07 | Made Valuation::getValue() and Valuation::getSatValue() const. | Tim King |
2011-04-05 | Memory fix for congruence closure; affects many UF benchmarks, probably AX too. | Morgan Deters |
2011-04-05 | Added options for setting the random decision frequency and random seed for t... | Tim King |
2011-04-05 | Minor adjustments to the Registrar commit in 1644, documentation. | Morgan Deters |
2011-04-04 | Merging the satliteral-before-prereg branch into trunk. Theory preregistratio... | Tim King |
2011-04-04 | Reverts previous commit r1636. | Tim King |
2011-04-04 | Add documentation to Node and TNode (closes bug #201). | Morgan Deters |
2011-04-02 | Delayed the addition of unate propagation lemmas until propagation is called.... | Tim King |
2011-04-02 | with --with-google-perftools, don't just take it on blind faith, require a su... | Morgan Deters |
2011-04-02 | minor fixes | Morgan Deters |
2011-04-01 | minor bugfixes (fixes broken dynamic-library build from last night) | Morgan Deters |
2011-04-01 | documentation fix | Morgan Deters |
2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
2011-03-31 | Fixes to Valuation. | Tim King |
2011-03-30 | improve recent low-coverage complaints | Morgan Deters |
2011-03-30 | adding CVC4:: qualifier to the #define for debugging so that it can be used o... | Dejan Jovanović |
2011-03-30 | Moved the constructor for Options out of the header and into the cpp. For peo... | Tim King |
2011-03-30 | Added the command line flag --rewrite-arithmetic-equalities. This sets a sta... | Tim King |
2011-03-30 | Add Valuation::getSatValue() so that theories can access the current | Morgan Deters |
2011-03-30 | Merged the branch sparse-tableau into trunk. | Tim King |
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-26 | fix typo | Morgan Deters |
2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
2011-03-25 | Fix for a bug Andrew Reynolds found for iterators that affects empty CDList<>... | Morgan Deters |
2011-03-22 | Merges the small changes on the queue-period branch into trunk. This branch ... | Tim King |
2011-03-22 | updating debug output usage to eliviate impact of bug 252 | Dejan Jovanović |
2011-03-21 | more bugfixes, some basic propagation, and testcases to cover them | Dejan Jovanović |
2011-03-21 | fixing a bug in the BV rewrite, off by one error when merging constants | Dejan Jovanović |
2011-03-20 | again a typo | Dejan Jovanović |
2011-03-20 | more bugfixes for bitvectors | Dejan Jovanović |
2011-03-20 | fixing the failure from last nigth, due to using a reference to an element in... | Dejan Jovanović |
2011-03-20 | missed one case | Dejan Jovanović |
2011-03-20 | commit for the version of bitvectors that passes all the unit tests | Dejan Jovanović |
2011-03-19 | Merges the pqueue-set branch into trunk. During VarOrder mode and Collection... | Tim King |