Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-06-10 | Add support for str.replace_re/str.replace_re_all (#4594) | Andres Noetzli | |
This commit adds support for the last remaining string operators from the new SMT-LIB standard for the theory of strings. The commit adds the kinds, type checking, reductions, and evaluation rewrites for `str.replace_re` and `str.replace_re_all`. | |||
2020-06-06 | Keep definitions when global-declarations enabled (#4572) | Andres Noetzli | |
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions are kept when `:global-declarations` are enabled. Until now, CVC4 was keeping track of the symbols of a definition correctly but lost the body of the definition when the user context was popped. This commit fixes the issue by adding a `global` parameter to `SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If that parameter is set, the definitions of functions are added at level 0 to `d_definedFunctions` and the lemmas for recursive function definitions are kept in an additional list and asserted during each `checkSat` call. The commit also updates new API, the commands, and the parsers to reflect this change. | |||
2020-06-05 | Changing default language (#4561) | Haniel Barbosa | |
Useful to avoid issues when a language is not set and it cannot be easily inferred (for example via the API). Since the language that covers most operators in CVC4 is the SMT one we use that as default now. | |||
2020-06-05 | Printing FP values as binary or indexed BVs according to option (#4554) | Haniel Barbosa | |
2020-06-04 | Update Java tests to match changes in API (#4535) | Andres Noetzli | |
Commit cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 renamed `Result::Validity` and `SmtEngine::query()` to `Result::Entailment` and `SmtEngine::checkEntailed()`, respectively. The commit did not update the Java tests which lead to issues in debug builds with Java bindings. The commit also adds a corresponding `NEWS` entry. | |||
2020-02-12 | Rename Java package to edu.stanford.CVC4 (#3752) | Andres Noetzli | |
2019-04-04 | adding sygus news (#2934) | Haniel Barbosa | |
2019-03-21 | Add more NEWS (#2859) | Andres Noetzli | |
2019-01-16 | Update NEWS file (#2804) | Andres Noetzli | |
2018-12-17 | New C++ API: Add tests for term object. (#2755) | Aina Niemetz | |
2018-06-25 | More updates to NEWS for 1.6. | Aina Niemetz | |
2018-06-25 | Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6. | Aina Niemetz | |
2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
2017-07-05 | Update unit test, news. | ajreynol | |
2017-06-30 | Updated NEWS, README, RELEASE-NOTES. | Clark Barrett | |
2016-06-09 | Dummy commit. | Clark Barrett | |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
2014-10-03 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: NEWS | |||
2014-10-03 | Fix output of integer-valued real constants in SMT-LIB models (thanks ↵ | Morgan Deters | |
Christoph Sticksel for reporting). | |||
2014-10-03 | More array constants and parsing: better error messages, extend to CVC ↵ | Morgan Deters | |
presentation language. | |||
2014-10-03 | Note array const support in NEWS | Morgan Deters | |
2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters | |
2014-07-13 | New versioning for development version. | Morgan Deters | |
2014-07-02 | Minor. | Morgan Deters | |
2014-07-01 | reword NEWS | Morgan Deters | |
2014-06-30 | Update NEWS | Kshitij Bansal | |
2014-06-21 | Some minor cleanup and documentation. | Morgan Deters | |
2014-06-19 | Documentation clean-ups. | Morgan Deters | |
2014-06-19 | Versioning preparation. | Morgan Deters | |
2014-06-10 | Some news about API changes. | Morgan Deters | |
2014-01-08 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS config/cvc4.m4 | |||
2014-01-08 | Switch license default back to BSD, and add --best and --enable-gpl options. | Morgan Deters | |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: NEWS | |||
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters | |
2013-12-17 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS | |||
2013-12-17 | some config changes: new --bsd option, readline gives warning, default build ↵ | Morgan Deters | |
is now production. | |||
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
2013-12-10 | Update NEWS. | Morgan Deters | |
2013-12-06 | Initializing 1.3.x branch. | Morgan Deters | |
2013-12-05 | Fix NEWS. | Morgan Deters | |
2013-12-05 | NEWS reorganization. | Morgan Deters | |
2013-12-04 | Don't put define-funs in model output; bug 411 testcase no longer relevant. | Morgan Deters | |
2013-12-03 | change string news | Tianyi Liang | |
2013-12-02 | Update NEWS file. | Morgan Deters | |
2013-11-27 | Some versioning in advance of the 1.3 release. | Morgan Deters | |
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 ↵ | Morgan Deters | |
success, nonzero error | |||
2013-09-11 | Theory of strings. | Tianyi Liang | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-09-09 | Support per-command verbosity settings. | Morgan Deters | |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters | |
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases. |