summaryrefslogtreecommitdiff
path: root/NEWS
AgeCommit message (Collapse)Author
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-30Remove invalid options from run scripts (#6645)Andres Noetzli
This commit removes some of the options in the run scripts that are not supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of those options are effectively enabled by default in cvc5.
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all` were not correctly enforcing that the operations replace the _first_ occurrence of some regular expression in a string. This commit fixes the issue by introducing a new operator `str.indexof_re(s, r, n)`, which, analoguously to `str.indexof`, returns the index of the first match of the regular expression `r` in `s`. The commit adds basic rewrites for evaluating the operator as well as its reduction. Additionally, it converts the reductions of `str.replace_re` and `str.replace_re_all` to use that new operator. This simplifies the reductions of the two operators and ensures that the semantics are consistent between the two.
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs. The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first. ``` status total solved sat unsat best timeout memout error uniq disagr time_cpu memory benchmark config AUFDTLIRA newUnsatCoresAssumps-safe/ ee 35 4 0 4 4 7 0 23 2 0 954.0 1267.5 newUnsatCoresProofs ok 35 31 0 31 25 4 0 0 0 0 894.1 1692.9 oldUnsatCores ok 35 32 0 32 30 3 0 0 1 0 799.2 1428.5 AUFLIA newUnsatCoresAssumps-safe/ ok 11 7 0 7 7 4 0 0 7 0 532.2 7604.4 newUnsatCoresProofs ok 11 4 0 4 1 6 0 0 0 0 829.0 12459.8 oldUnsatCores ok 11 4 0 4 3 6 0 0 0 0 818.2 7764.4 AUFLIRA newUnsatCoresAssumps-safe/ to 2 0 0 0 0 2 0 0 0 0 241.6 125.6 newUnsatCoresProofs ok 2 2 0 2 1 0 0 0 0 0 54.2 45.5 oldUnsatCores ok 2 2 0 2 2 0 0 0 0 0 49.4 79.7 AUFNIRA newUnsatCoresAssumps-safe/ ok 10 5 0 5 5 5 0 0 2 0 748.4 1630.0 newUnsatCoresProofs ok 10 4 0 4 0 6 0 0 0 0 850.7 2978.8 oldUnsatCores ok 10 8 0 8 5 2 0 0 1 0 502.7 2048.5 BV newUnsatCoresAssumps-safe/ ok 7 1 1 0 1 6 0 0 1 0 734.2 2065.0 newUnsatCoresProofs ok 7 6 3 3 4 1 0 0 0 0 246.7 1023.9 oldUnsatCores ok 7 6 3 3 3 1 0 0 0 0 248.6 992.0 LIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.9 47.7 newUnsatCoresProofs ok 1 1 0 1 1 0 0 0 0 0 0.3 6.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 0.3 5.3 LRA newUnsatCoresAssumps-safe/ ok 5 3 0 3 3 2 0 0 3 0 450.7 260.4 newUnsatCoresProofs ok 5 2 0 2 0 3 0 0 0 0 537.8 424.5 oldUnsatCores ok 5 2 0 2 2 3 0 0 0 0 533.8 298.5 NIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.8 22.0 newUnsatCoresProofs ok 1 1 0 1 0 0 0 0 0 0 46.3 48.0 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 43.3 40.3 QF_ABV newUnsatCoresAssumps-safe/ ok 105 70 59 11 70 35 0 0 63 0 8195.5 19363.3 newUnsatCoresProofs ok 105 34 24 10 17 71 0 0 5 0 11099.5 35756.7 oldUnsatCores ok 105 37 23 14 18 69 0 0 1 0 11198.0 26878.1 QF_ANIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1631.8 newUnsatCoresProofs ok 4 4 3 1 2 0 0 0 0 0 175.1 1513.6 oldUnsatCores ok 4 4 3 1 3 0 0 0 0 0 173.8 1495.1 QF_AUFLIA newUnsatCoresAssumps-safe/ ok 35 6 1 5 6 29 0 0 3 0 3718.4 524.1 newUnsatCoresProofs ok 35 24 4 20 1 11 0 0 0 0 2357.2 36556.0 oldUnsatCores ok 35 32 5 27 29 3 0 0 5 0 1857.6 10067.7 QF_AUFNIA newUnsatCoresAssumps-safe/ ok 3 1 0 1 1 2 0 0 0 0 324.7 543.6 newUnsatCoresProofs ok 3 2 2 0 1 1 0 0 1 0 223.1 509.0 oldUnsatCores ok 3 2 1 1 1 1 0 0 0 0 268.5 484.3 QF_AX newUnsatCoresAssumps-safe/ ok 12 1 0 1 1 11 0 0 0 0 1379.2 391.3 newUnsatCoresProofs ok 12 10 0 10 0 2 0 0 0 0 528.7 7433.9 oldUnsatCores ok 12 12 0 12 11 0 0 0 1 0 343.0 2855.2 QF_BV newUnsatCoresAssumps-safe/ ok 96 56 30 26 49 39 2 0 35 0 9248.2 98058.7 newUnsatCoresProofs ok 96 37 26 11 23 52 7 0 7 0 9781.9 135924.7 oldUnsatCores ok 96 50 29 21 24 43 3 0 7 0 9155.6 107216.0 QF_IDL newUnsatCoresAssumps-safe/ ok 109 51 39 12 43 58 0 0 33 0 10427.2 50846.5 newUnsatCoresProofs ok 109 33 32 1 2 76 0 0 0 0 11692.8 108963.1 oldUnsatCores ok 109 75 55 20 64 34 0 0 26 0 10088.1 53105.6 QF_LIA newUnsatCoresAssumps-safe/ ok 306 155 111 44 138 151 0 0 119 0 25346.4 50556.0 newUnsatCoresProofs ok 306 117 95 22 49 189 0 0 0 0 27092.6 122894.9 oldUnsatCores ok 306 187 110 77 152 119 0 0 34 0 24521.0 61261.1 QF_LRA newUnsatCoresAssumps-safe/ ok 72 39 20 19 38 33 0 0 31 0 7475.3 16892.2 newUnsatCoresProofs ok 72 31 16 15 2 41 0 0 0 0 7569.3 35658.7 oldUnsatCores ok 72 41 18 23 32 31 0 0 2 0 7243.2 20593.9 QF_NIA newUnsatCoresAssumps-safe/ ok 4389 2009 1862 147 2002 903 0 0 1931 0 163975.7 280779.3 newUnsatCoresProofs ok 4389 2326 2156 170 752 792 0 0 37 0 151051.9 387779.8 oldUnsatCores ok 4389 2394 2199 195 2174 730 0 0 81 0 146419.3 259669.8 QF_NRA newUnsatCoresAssumps-safe/ ok 135 65 57 8 57 70 0 0 45 0 10195.7 24701.4 newUnsatCoresProofs ok 135 71 49 22 35 64 0 0 5 0 10825.3 32982.8 oldUnsatCores ok 135 75 54 21 51 61 0 0 9 0 10865.3 27260.9 QF_RDL newUnsatCoresAssumps-safe/ ok 7 5 1 4 5 2 0 0 1 0 564.7 958.4 newUnsatCoresProofs ok 7 1 1 0 0 6 0 0 0 0 842.0 11029.6 oldUnsatCores ok 7 6 1 5 2 1 0 0 1 0 665.8 1982.6 QF_S newUnsatCoresAssumps-safe/ ok 5 1 1 0 0 4 0 0 0 0 603.3 191.4 newUnsatCoresProofs ok 5 5 5 0 2 0 0 0 0 0 161.9 285.8 oldUnsatCores ok 5 4 4 0 3 1 0 0 0 0 225.9 219.3 QF_SLIA newUnsatCoresAssumps-safe/ ok 258 74 67 7 70 184 0 0 64 0 27245.9 20290.4 newUnsatCoresProofs ok 258 179 163 16 47 79 0 0 6 0 18996.0 33722.6 oldUnsatCores ok 258 184 162 22 149 74 0 0 9 0 18395.8 23004.3 QF_UF newUnsatCoresAssumps-safe/ ok 29 25 0 25 6 4 0 0 2 0 2362.4 7504.3 newUnsatCoresProofs ok 29 0 0 0 0 28 1 0 0 0 3508.0 124190.7 oldUnsatCores ok 29 27 0 27 23 2 0 0 4 0 1866.3 13635.1 QF_UFBV newUnsatCoresAssumps-safe/ ok 2 2 0 2 1 0 0 0 1 0 189.5 1599.3 newUnsatCoresProofs to 2 0 0 0 0 2 0 0 0 0 241.8 1818.8 oldUnsatCores ok 2 1 0 1 1 1 0 0 0 0 193.7 1500.9 QF_UFIDL newUnsatCoresAssumps-safe/ ok 9 9 0 9 7 0 0 0 4 0 697.0 1133.0 newUnsatCoresProofs to 9 0 0 0 0 9 0 0 0 0 1088.0 14652.6 oldUnsatCores ok 9 5 0 5 2 4 0 0 0 0 848.5 2079.6 QF_UFLIA newUnsatCoresAssumps-safe/ ok 1 1 0 1 0 0 0 0 0 0 117.1 76.4 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.9 208.5 oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 110.6 127.7 QF_UFLRA newUnsatCoresAssumps-safe/ ok 7 4 1 3 0 0 3 0 0 0 266.6 55098.3 newUnsatCoresProofs mo 7 0 0 0 0 0 7 0 0 0 261.7 56000.0 oldUnsatCores ok 7 7 4 3 7 0 0 0 3 0 408.4 20933.4 QF_UFNIA newUnsatCoresAssumps-safe/ ok 48 21 19 2 21 4 0 0 20 0 592.3 880.6 newUnsatCoresProofs ok 48 27 22 5 18 4 0 0 1 0 641.4 1548.8 oldUnsatCores ok 48 26 21 5 26 7 0 0 1 0 887.5 1044.6 QF_UFNRA newUnsatCoresAssumps-safe/ ok 1 1 1 0 1 0 0 0 1 0 108.3 17.9 newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.8 19.0 oldUnsatCores to 1 0 0 0 0 1 0 0 0 0 120.8 14.7 UF newUnsatCoresAssumps-safe/ ok 21 5 0 5 5 16 0 0 5 0 2123.8 3168.7 newUnsatCoresProofs ok 21 13 0 13 6 8 0 0 0 0 1496.3 6617.8 oldUnsatCores ok 21 16 0 16 11 5 0 0 3 0 1443.3 3919.2 UFDT newUnsatCoresAssumps-safe/ ok 35 6 0 6 6 29 0 0 5 0 3777.0 4485.5 newUnsatCoresProofs ok 35 28 0 28 15 7 0 0 0 0 1416.9 4293.6 oldUnsatCores ok 35 30 0 30 26 5 0 0 1 0 1406.9 3188.5 UFDTLIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1640.5 newUnsatCoresProofs ok 4 4 0 4 1 0 0 0 0 0 139.3 942.3 oldUnsatCores ok 4 4 0 4 3 0 0 0 0 0 156.4 851.8 UFDTLIRA newUnsatCoresAssumps-safe/ ok 1 1 0 1 1 0 0 0 1 0 0.0 3.1 newUnsatCoresProofs ok 1 0 0 0 0 0 0 0 0 0 0.0 3.2 oldUnsatCores ok 1 0 0 0 0 0 0 0 0 0 0.0 2.7 UFDTNIRA newUnsatCoresAssumps-safe/ ok 10 3 0 3 3 6 0 0 3 0 754.8 1386.9 newUnsatCoresProofs ok 10 7 0 7 5 3 0 0 0 0 377.0 848.8 oldUnsatCores ok 10 7 0 7 7 3 0 0 0 0 376.5 563.4 UFLIA newUnsatCoresAssumps-safe/ ok 24 8 0 8 8 16 0 0 8 0 2231.6 3179.2 newUnsatCoresProofs ok 24 14 0 14 3 10 0 0 1 0 1915.5 5131.1 oldUnsatCores ok 24 15 0 15 14 9 0 0 2 0 1857.5 3479.7 UFNIA newUnsatCoresAssumps-safe/ ok 354 183 28 155 116 133 0 0 113 0 25941.4 839089.7 newUnsatCoresProofs ok 354 107 17 90 28 107 92 0 2 0 23496.9 1020258.1 oldUnsatCores ok 354 237 19 218 233 72 0 0 66 0 19906.9 914273.0 ```
2021-02-09cmake: Make Python3 default and improve toml error messages. (#5884)Mathias Preiner
./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.
2020-11-12Models standard (#5415)yoni206
This PR relates to #4987 . Our plan is to: delete the model keyword avoid printing extra declarations by default wrap UF values with as expressions. This PR does step 1, and fixes regressions accordingly.
2020-09-25Restrict bvxnor to only allow two operands (was n-ary). (#5138)Aina Niemetz
Bit-vector operator bvxnor was previously mistakenly marked as left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We now restrict bvxnor to only allow two operands in order to avoid confusion about the semantics, since the behavior of n-ary operands to bvxnor is now undefined in SMT-LIB.
2020-09-08Make CVC/API BV div/mod semantics match SMT-LIB (#4997)Andres Noetzli
This commit changes the semantics of the CVC language and with the default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`, and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the commit also adds comments to our API documentation for the different semantics enabled by the `bv-div-zero-const` option.
2020-09-02Use SMT-COMP configuration for competition build (#4995)Andres Noetzli
This commit changes our `competition` build to include the libraries that we have used for SMT-COMP by default. This makes it easier for users to reproduce our SMT-COMP configuration for performance measurements. We are using GPL libraries for this build type, so the commit adds color to highlight the fact that this build type produces a GPL build.
2020-07-17Support for using 'libedit' over 'readline' #4571 (#4579)Andrew V. Jones
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2020-07-10Front end support for integer AND (#4717)Andrew Reynolds
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
With this PR, we now support a preliminary draft of a theory of sequences. This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them. As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term. We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).
2020-07-02Remove SWIG bindings (#4683)Andres Noetzli
This commit removes support for SWIG bindings for the legacy API. The bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da and we are not planning on using SWIG for the Java API for the new API.
2020-06-30Update NEWS post 1.8 release (#4666)Andres Noetzli
2020-06-27Add API for retrieving separation heap/nil term (#4663)Andres Noetzli
This commit extends the API to support the retrieval of heap/nil term when separation logic is used and changes the corresponding system test accordingly. This commit is in preparation of making the constructor of `ExprManager` private.
2020-06-19Update info for 1.8 release (#4633)Andres Noetzli
2020-06-16Updates to NEWS. (#4628)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback