Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz | |
2021-04-05 | New C++ Api: Rename and move headers. (#6292) | Aina Niemetz | |
2021-04-01 | Rename namespace CVC5 to cvc5. (#6258) | Aina Niemetz | |
2021-03-31 | Rename namespace CVC4 to CVC5. (#6249) | Aina Niemetz | |
2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
2020-09-22 | Update copyright header script to support CMake and Python files (#5067) | Mathias Preiner | |
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header. | |||
2020-06-23 | New C++ API: Remove examples for old API. (#4650) | Aina Niemetz | |
This removes obsolete examples for the old API in preparation of making the old API private. Examples for the new API are renamed from *-new.cpp to *.cpp. | |||
2020-06-16 | Update copyright headers. | Aina Niemetz | |
2020-03-31 | Rename checkValid/query to checkEntailed. (#4191) | Aina Niemetz | |
This renames api::Solver::checkValidAssuming to checkEntailed and removes api::Solver::checkValid. Internally, SmtEngine::query is renamed to SmtEngine::checkEntailed, and these changes are further propagated to the Result class. | |||
2019-09-25 | Use separate CMake project for CVC4 examples. (#3196) | Mathias Preiner | |
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-03-21 | Add bit-vector extract example. (#1681) | Aina Niemetz | |
2018-03-05 | Add support for check-sat-assuming. (#1637) | Aina Niemetz | |
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)). | |||
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2016-04-20 | update from the master | PaulMeng | |
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-05-02 | Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue. | Morgan Deters | |
2013-11-27 | Incremental is now on by default when using from API, off for command-line ↵ | Morgan Deters | |
driver except in interactive mode. | |||
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2012-12-01 | updated examples | Morgan Deters | |
2012-12-01 | added a new example for the combination of bit-vectors and arrays (includes ↵ | Liana Hadarean | |
model generation) and set the logic for the bitvector example | |||
2012-11-30 | all API examples now have java versions too; bitvectors gets built; also ↵ | Morgan Deters | |
updated old-style copyrights in the examples | |||
2012-11-30 | added a simple API example example showing how to use the bit-vector theory. | Liana Hadarean | |