Age | Commit message (Expand) | Author |
2016-04-30 | Reviewed Tim's Asan changes and improved SatProof comments. | Liana Hadarean |
2016-04-26 | Fixing memory leaks for garbage collection of ResChains in the sat proof impl... | Tim King |
2016-04-09 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-04-09 | Made ProofArray's printing functions non-static, and consequently the data me... | Guy |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-04-03 | s_ prefix for static members | Guy |
2016-04-03 | Removed the theory-specific merge reason types. Instead, added a mechanism fo... | Guy |
2016-03-23 | squash-merge from proof branch | Guy |
2016-02-24 | Adding the missing clause_id.h file. | Tim King |
2016-02-24 | Unifying the definitions of ClauseId to a single source of truth. | Tim King |
2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
2016-02-01 | Adding a destructor to ProofOutputChannel. | Tim King |
2016-02-01 | Fixing white spaces in sat_proof.h. | Tim King |
2016-02-01 | Deleting the dead code in proof/sat_proof.cpp. | 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-30 | Shuffling around public vs. private headers | Tim King |
2015-12-24 | Miscellaneous fixes | Tim King |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-10-26 | This commit fixes a bug related to a public header depending on a compiler fl... | Tim King |
2015-06-01 | When proof enabled, disable uf sym break. Add regression. | ajreynol |
2015-05-25 | Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report. | ajreynol |
2015-05-12 | Merge pull request #74 from finnhaedicke/namespace_minisat | barrettcw |
2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
2015-04-17 | moved Minisat namespace into CVC4 | Finn Haedicke |
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 |
2014-06-21 | Fix compiler warnings (mostly unused variables). | Morgan Deters |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-11-13 | Add virtual destructors where missing | Morgan Deters |
2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | 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-09 | fixed uf proof bug: now storing deleted theory lemmas | 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-09-13 | Fix sat_proof "parentheses into the void" after conferring with Liana. | Morgan Deters |
2013-05-10 | now proofs print mapping between atom and propositional variable as a comment... | lianah |
2013-05-10 | fixes to the proof system so it works with theory lemmas and explanations | lianah |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters |
2013-03-14 | fix to build system: #include the proper file when they are in both builds an... | Morgan Deters |