| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-25 | New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977) | Aina Niemetz | |
| This cleans up naming of API functions to create first-order constants and variables. mkVar -> mkConst mkBoundVar -> mkVar declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed. Note that we want to avoid redundancy in order to reduce code duplication and maintenance overhead (we do not allow nested API calls, since this is problematic when tracing API calls). | |||
| 2019-04-03 | Update copyright headers. | Aina Niemetz | |
| 2019-04-01 | Update includes to use cvc4 top-level directory in examples (#2877) | makaimann | |
| Because the headers are now installed in a `cvc4` directory, the examples need to include from there as well. | |||
| 2019-03-26 | Update copyright headers. | Aina Niemetz | |
| 2019-03-18 | New C++: Remove redundant mkVar function. | Aina Niemetz | |
| s | |||
| 2019-01-29 | New C++ API: Fix checks for mkTerm. (#2820) | Aina Niemetz | |
| This required fixing the OpTerm handling for mkTerm functions in the API. | |||
| 2018-10-04 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
| 2018-06-27 | Header for new C++ API. (#1697) | Aina Niemetz | |
 |
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