summaryrefslogtreecommitdiff
path: root/NEWS
AgeCommit message (Collapse)Author
2020-06-10Add 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-06Keep 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-05Changing 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-05Printing FP values as binary or indexed BVs according to option (#4554)Haniel Barbosa
2020-06-04Update 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-12Rename Java package to edu.stanford.CVC4 (#3752)Andres Noetzli
2019-04-04adding sygus news (#2934)Haniel Barbosa
2019-03-21Add more NEWS (#2859)Andres Noetzli
2019-01-16Update NEWS file (#2804)Andres Noetzli
2018-12-17New C++ API: Add tests for term object. (#2755)Aina Niemetz
2018-06-25More updates to NEWS for 1.6.Aina Niemetz
2018-06-25Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.Aina Niemetz
2018-04-02Remove references to nyu (#1721)Clark Barrett
2017-07-05Update unit test, news.ajreynol
2017-06-30Updated NEWS, README, RELEASE-NOTES.Clark Barrett
2016-06-09Dummy commit.Clark Barrett
2014-10-23Parsing 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-03Merge branch '1.4.x'Morgan Deters
Conflicts: NEWS
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks ↵Morgan Deters
Christoph Sticksel for reporting).
2014-10-03More array constants and parsing: better error messages, extend to CVC ↵Morgan Deters
presentation language.
2014-10-03Note array const support in NEWSMorgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-13New versioning for development version.Morgan Deters
2014-07-02Minor.Morgan Deters
2014-07-01reword NEWSMorgan Deters
2014-06-30Update NEWSKshitij Bansal
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-19Documentation clean-ups.Morgan Deters
2014-06-19Versioning preparation.Morgan Deters
2014-06-10Some news about API changes.Morgan Deters
2014-01-08Merge branch '1.3.x'Morgan Deters
Conflicts: COPYING NEWS config/cvc4.m4
2014-01-08Switch license default back to BSD, and add --best and --enable-gpl options.Morgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-17Merge branch '1.3.x'Morgan Deters
Conflicts: COPYING NEWS
2013-12-17some config changes: new --bsd option, readline gives warning, default build ↵Morgan Deters
is now production.
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-12-10Update NEWS.Morgan Deters
2013-12-06Initializing 1.3.x branch.Morgan Deters
2013-12-05Fix NEWS.Morgan Deters
2013-12-05NEWS reorganization.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-03change string newsTianyi Liang
2013-12-02Update NEWS file.Morgan Deters
2013-11-27Some versioning in advance of the 1.3 release.Morgan Deters
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-09-11Theory of strings.Tianyi Liang
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-07-11Support 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback