| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-03-26 | Update copyright headers. | Aina Niemetz | |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz | |
| 2018-05-03 | Fix warnings in proof code (#1850) | Andres Noetzli | |
| 2018-04-25 | Refactor array-proofs and uf-proofs (#1655) | yoni206 | |
| This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp. | |||
| 2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
| Adds missing override keywords. | |||
| 2017-11-15 | Adding garbage collection for Proof objects. (#1294) | Tim King | |
| 2017-10-25 | Switching EqProof to use shared_ptr everywhere. (#1217) | Tim King | |
| This clarifies the memory ownership of EqProofs. | |||
| 2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King | |
| * Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes. | |||
| 2017-07-07 | Update copyright headers. | Mathias Preiner | |
| 2017-03-17 | better support for proof production when encountering bool terms: handle the ↵ | guykatzz | |
| new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes | |||
| 2017-03-09 | better proof support for bools and formulas | guykatzz | |
| 2016-07-24 | Use letification for the aliasing declarations as well (consequently, print ↵ | Guy | |
| the global let map before the aliasing part) | |||
| 2016-06-08 | Support for printing a global let map in LFSC proofs. | Guy | |
| Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules. | |||
| 2016-06-01 | Merge from proof branch | Guy | |
| 2016-06-01 | Revert "Merging proof branch" | Guy | |
| This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8. | |||
| 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-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback