| 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-12-02 | Update copyright headers. | Aina Niemetz | |
| 2020-10-29 | Add mkInteger to the API (#5274) | mudathirmahgoub | |
| This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort. The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals. This means subtyping is effectively eliminated from all theories except arithmetic. Other changes: Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR. Benchmarks are updated to match the changes in the parsers Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu | |||
| 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-29 | Make ExprManager constructor private (#4669) | Andres Noetzli | |
| This commit makes the ExprManager constructor private and updates the initialization of subsolvers, unit tests, and system tests accordingly. This is a step towards making options part of SmtEngine instead of NodeManager. | |||
| 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 | |
| 2017-07-07 | Update copyright headers. | Mathias Preiner | |
| 2016-04-20 | update from the master | PaulMeng | |
| 2014-07-01 | Update copyrights. | Morgan Deters | |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
| 2013-04-01 | update copyrights | Morgan Deters | |
| 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-10-22 | fix misleading comment in example | Morgan Deters | |
| 2012-10-05 | BoolExpr removed and replaced with Expr | Dejan Jovanović | |
| 2012-07-10 | * fixing the simple_vc_cxx.cpp compile issue (no more Integer constants) | Dejan Jovanović | |
| * adding as examples the programs i used to translate nonlinear smt2 problems to other formats | |||
| 2011-11-15 | Bindings work (ocaml bindings are now sort of working); also minor cleanup | Morgan Deters | |
| 2011-09-30 | interfaces fixes and cleanups...and examples of each interface! | Morgan Deters | |
 |
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