Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-03-09 | better proof support for bools and formulas | guykatzz | |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
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-02-24 | Unifying the definitions of ClauseId to a single source of truth. | Tim King | |
2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean | |
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-03-10 | CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ | ajreynol | |
signature. Add regressions. | |||
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 ↵ | Morgan Deters | |
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
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 | fixed uf proof with holes bugs | lianah | |
2013-10-07 | first draft implementation of uf proofs with holes | Liana Hadarean | |
2013-05-10 | now proofs print mapping between atom and propositional variable as a ↵ | lianah | |
comment in LFSC | |||
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters | |
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2011-11-01 | Improvements to header installation on user machines. Internally, we can | Morgan Deters | |
still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h> | |||
2011-10-28 | * ability to output NodeBuilders without first converting them to ↵ | Morgan Deters | |
Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup | |||
2011-10-28 | merged the proofgen3 branch into trunk: | Liana Hadarean | |
- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof. |