NEWS.md

   1 This file contains a summary of important user-visible changes.
   2
   3 cvc5 1.0.1
   4 ==========
   5
   6 **New Features**
   7
   8 - Support for cross-compiling an ARM binary of cvc5 on x86 macOS.
   9
  10 **Changes**
  11
  12 - Removed support for non-standard `declare-funs`, `declare-consts`, and
  13   `declare-sorts` commands.
  14 - The kind for integer constants is now `CONST_INTEGER`, while real constants
  15   continue to have kind `CONST_RATIONAL`.
  16 - Type rules for (dis)equality and if-then-else no longer allow mixing
  17   integers and reals. Type rules for other operators like `APPLY_UF` now
  18   require their arguments to match the type of the function being applied, and
  19   do not assume integer/real subtyping.
  20 - The API method `mkTuple` no longer supports casting integers to reals when
  21   constructing tuples.
  22
  23 **New Features**
  24
  25 - Support for declaring oracle functions in the API via the method
  26   `declareOracleFun`. This allows users to declare functions whose semantics
  27   are associated with a provided executable implementation.
  28
  29 cvc5 1.0
  30 =========
  31
  32 **Website**: https://cvc5.github.io
  33
  34 **Documentation**: https://cvc5.github.io/docs
  35
  36 **System Description**
  37   * *cvc5: A Versatile and Industrial-Strength SMT Solver.*
  38     Barbosa H., Barrett C., Brain M., Kremer G., Lachnitt H.,
  39     Mann M., Mohamed A., Mohamed M., Niemetz A., Nötzli A.,
  40     Ozdemir A., Preiner M., Reynolds A., Sheng Y., Tinelli C., and Zohar Y.,
  41     TACAS 2022.
  42
  43 **New Features**
  44
  45 * *Streamlined C++ API*
  46   - Documentation: https://cvc5.github.io/docs/latest/api/cpp/cpp.html
  47
  48 * *Two new Python language bindings*
  49   - Base module: Feature complete with C++ API
  50   - Pythonic module: A pythonic wrapper around the base module
  51   - Documentation: https://cvc5.github.io/docs/latest/api/python/python.html
  52
  53 * *New Java language bindings*
  54   - Documentation: https://cvc5.github.io/docs/latest/api/java/java.html
  55
  56 * *Theory of Bags (Multisets)*
  57   - A new theory of bags, which are collections that allow duplicates. It
  58     supports basic operators like union disjoint, union max, intersection,
  59     difference subtract, difference remove, duplicate removal, and multiplicity
  60     of an element in a bag.
  61
  62 * *Theory of Sequences*
  63   - A new parametric theory of sequences whose syntax is compatible with the
  64     syntax for sequences used by Z3.
  65   - A new array-inspired procedure (option `--seq-array`).
  66
  67 * *Arithmetic*
  68   - Nonlinear real arithmetic is now solved using a new solver based on
  69     cylindrical algebraic coverings. Includes full support for non-rational
  70     models and a number of options `--nl-cov-*` for, e.g., different projection
  71     operators, Lazard's lifting or variable elimination.
  72     The new solver requires the libpoly library, and Lazard's lifting
  73     additionally requires CoCoALib.
  74
  75 * *Arrays*
  76   - Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
  77     if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
  78
  79 * *Bit-vectors*
  80   - New bit-vector solver with CaDiCaL as default SAT back-end.
  81   - New approach for solving bit-vectors as integers (option `--solve-bv-as-int`).
  82
  83 * *Datatypes*
  84   - Support for generic datatype updaters `((_ update s) t u)` which replaces
  85     the field specified by selector `s` of `t` by the value `u`.
  86
  87 * *Integers*
  88   - Support for an integer operator `(_ iand n)` that returns the bitwise `and`
  89     of two integers, seen as integers modulo n.
  90   - Support for an integer operator `int.pow2`, used as `(int.pow2 x)` which
  91     represents 2 to the power of x.
  92
  93 * *Quantifiers*
  94   - Improved support for enumerative instantiation (option `--enum-inst`).
  95   - SyGuS-based quantifier instantiation (option `--sygus-inst`).
  96
  97 * *Strings*
  98   - Improved performance using new techniques, including model-based
  99     reductions, eager context-dependent simplification, and equality-based
 100     conflict finding.
 101   - Support for `str.indexof_re(s, r, n)`, which returns the index of the first
 102     occurrence of a regular expression `r` in a string `s` after index `n` or
 103     -1 if `r` does not match a substring after `n`.
 104
 105 * *Proofs*
 106   * Documentation available at:
 107     https://cvc5.github.io/docs/latest/proofs/proofs.html
 108   * When used after an unsatisfiable response to `checkSat`, `getProof`
 109     returns a representation of the refutation proof for the current set of
 110     assertions (get-proof in SMT-LIB).
 111   * Preliminary support for translations to external proof formats LFSC and Alethe.
 112
 113 * *Difficulty Estimation*
 114   - The API method `getDifficulty` returns a map from asserted formulas to
 115     integers which estimates how much that formula contributed to the
 116     difficulty of the overall problem (get-difficulty in SMT-LIB).
 117
 118 * *Learned Literals*
 119   - The API method `getLearnedLiterals` gets a list of literals that are
 120     entailed by the current set of assertions that were learned during solving
 121     (get-learned-literals in SMT-LIB).
 122
 123 * *Abduction and Interpolation*
 124   * The API method `getAbduct` can be used to find an abduct for the current set
 125     of assertions and provided goal (get-abduct in SMT-LIB). Optionally, a
 126     SyGuS grammar can be provided to restrict the shape of possible abducts.
 127     If using the text inferace, the grammar may be provided using the same
 128     syntax for grammars as in SyGuS IF format.
 129   * The API method `getInterpolant` can be used to find an interpolant for the
 130     current set of assertions and provided goal (get-interpolant in SMT-LIB).
 131     Like abduction, grammars may be provided to restrict the shape of
 132     interpolants.
 133
 134 * *Support for Incremental Synthesis Queries*
 135   - The core SyGuS solver now supports getting multiple solutions for a
 136     synthesis conjecture via the API. The method `checkSynthNext` finds the
 137     next SyGuS solution to the current set of SyGuS constraints
 138     (check-synth-next in SyGuS IF).
 139   - `getAbductNext` finds the next abduct for the current set of
 140     assertions and provided goal (get-abduct-next in SMT-LIB).
 141   - `getInterpolantNext` finds the next interpolant for the current set of
 142     assertions and provided goal (get-interpolant-next in SMT-LIB).
 143
 144 * *Pool-based Quantifier Instantiation*
 145   - The API method `declarePool` declares symbol sets of terms called pools
 146     (`declare-pool` in SMT-LIB).
 147   - Pools can be used in annotations of quantified formulas for fine grained
 148     control over quantifier instantiations (:inst-pool, :inst-add-to-pool,
 149     :skolem-add-to-pool in SMT-LIB).
 150
 151 * Diagnostic Outputs
 152   - The option `-o TAG` can be used to enable a class of useful diagnostic
 153     information, such as the state of the input formula before and after
 154     pre-preprocessing, quantifier instantiations, literals learned
 155     during solving, among others. For SyGuS problems, it can be used to
 156     show candidate solutions and grammars that the solver has generated.
 157
 158 * *Unsat cores*
 159   - Production modes based on the new proof infrastructure
 160     (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption
 161     feature of Minisat (`--unsat-cores-mode=assumptions`). The mode based on
 162     SAT assumptions + preprocessing proofs is the new default.
 163   - Computing minimal unsat cores (option `--minimal-unsat-cores`).
 164
 165 * *Blocking Models*
 166   - The API method `blockModels` can be used to block the current model using
 167     various policies for how to exclude the values of terms (`block-model` in
 168     SMT-LIB).
 169   - The API method `blockModelValues` can be used to block the current model
 170     for a provided set of terms (`block-model-values` in SMT-LIB).
 171
 172 * *Model Cores*
 173   - The API method `isModelCoreSymbol` can be used to query whether the value
 174     for a symbol was critical to whether the model satisfies the current set of
 175     assertions.
 176   - Models can be limited to show only model core symbols (option `--model-cores`).
 177
 178 **Changes**
 179
 180 * CaDiCaL and SymFPU are now required dependencies. CaDiCaL 1.4.1 is now the
 181   version used by default.
 182 * Options have been extensively refactored, please refer to the cvc5
 183   documentation for further information.
 184 * Removed support for the CVC language.
 185 * SyGuS: Removed support for SyGuS-IF 1.0.
 186 * Removed support for the (non-standard) `define` command.
 187 * Removed the legacy API along with the Java and Python bindings for it.
 188 * Interactive shell: the GPL-licensed Readline library has been replaced the
 189   BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
 190   of Readline. Without selecting optional GPL components, Editline-enabled CVC4
 191   builds will be BSD licensed.
 192 * The `competition` build type includes the dependencies used for SMT-COMP by
 193   default. Note that this makes this build type produce GPL-licensed binaries.
 194 * Bit-vector operator `bvxnor` was previously mistakenly marked as
 195   left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We
 196   now restrict `bvxnor` to only allow two operands in order to avoid confusion
 197   about the semantics, since the behavior of n-ary operands to `bvxnor` is now
 198   undefined in SMT-LIB.
 199 * SMT-LIB output for `get-model` command now conforms with the standard,
 200   and does *not* begin with the keyword `model`. The output
 201   is the same as before, only with this word removed from the beginning.
 202 * Building with Python 2 is now deprecated.
 203 * The SMT-LIB syntax for some extensions has been changed. Notably, set
 204   operators are now prefixed by `set.`, and relations by `rel.`. For example,
 205   `union` is now written `set.union`.
 206 * Removed support for redundant logics `ALL_SUPPORTED` and `QF_ALL_SUPPORTED`,
 207   use `ALL` and `QF_ALL` instead.