Age | Commit message (Expand) | Author |
2016-10-12 | Fix some typos, fix some formatting, minor cleanupfix_typos | Andres Notzli |
2016-10-05 | Added an option that allow empty dependencies when attempting to minimize pre... | guykatzz |
2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli |
2016-08-03 | Fixed an issue where arrays proofs would sometimes have an extra ")" at the end. | Guy |
2016-07-28 | The "aggressive" optimizer for lemma L now returns the conjunction of all lem... | Guy |
2016-07-28 | Bug fix involving negated lemmas | Guy |
2016-07-27 | Proper handling of IFF lemmas in the unsat core. | Guy |
2016-07-27 | Added an option for a more aggressive weakest implicant optimization | Guy |
2016-07-27 | If we can't find a weaker implicant, fail gracefully and return the original ... | Guy |
2016-07-26 | Bug fix: | Guy |
2016-07-26 | Letification of BV constants | Guy |
2016-07-26 | Added functionality to retrieve a lemma's "weakest implicant" in the unsat co... | Guy |
2016-07-24 | Use letification for the aliasing declarations as well (consequently, print t... | Guy |
2016-07-19 | Bug fix | Guy |
2016-07-19 | Allow a caller to query whether an unsat core is available or not | Guy |
2016-07-15 | Moved the assertion to a better spot | Guy |
2016-07-15 | The ProofManager now allows theory solvers to get their lemmas that participa... | Guy |
2016-06-30 | Support for the letification of chained AND and OR operations in LFSC proofs | Guy |
2016-06-20 | Addressed a bug that occurs when proof production is triggered via text flags... | Guy |
2016-06-20 | Fixed a bug where the proofManager's init() call was not getting called, resu... | Guy |
2016-06-08 | Support for printing a global let map in LFSC proofs. | Guy |
2016-06-01 | Merge from proof branch | Guy |
2016-06-01 | Revert "Merging proof branch" | Guy |
2016-06-01 | Merging proof branch | Guy |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-03-23 | squash-merge from proof branch | Guy |
2016-02-24 | Unifying the definitions of ClauseId to a single source of truth. | Tim King |
2016-01-28 | Adding listeners to Options. | Tim King |
2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-06-01 | When proof enabled, disable uf sym break. Add regression. | ajreynol |
2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
2015-03-16 | Fixed proof unitialized memory and minor memory leaks. | Liana Hadarean |
2015-03-10 | CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig... | ajreynol |
2014-08-25 | Fix Win32 builds. | Morgan Deters |
2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters |
2014-07-01 | Update copyrights. | Morgan Deters |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
2013-11-05 | fixed proof regression script and added a new uf test case | lianah |
2013-10-09 | cleaned up proof code | lianah |
2013-10-08 | added currying for uf proofs; still needs debugging | lianah |
2013-10-08 | fixed uf proof with holes bugs | lianah |
2013-10-07 | fixed some bugs | Liana Hadarean |
2013-10-07 | first draft implementation of uf proofs with holes | Liana Hadarean |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-09-28 | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak... | Morgan Deters |
2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g... | Morgan Deters |