Changes since 1.7

New Features:

• New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
  make CVC4 1.8 the last version that ships with the legacy API.
• Strings: Full support of the new SMT-LIB standard for the theory of strings,
  including:
  • Support for str.replace_re, str.replace_re_all, str.is_digit,
    str.from_code, re.diff, and re.comp
  • Support for new operator names (e.g. str.in_re instead of str.in.re),
    new escape sequences. The new syntax is enabled by default for smt2 files.
• Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
  examples of the SyGuS API can be found in ./examples/api/sygus_*.cpp.
• Support for higher-order constraints. This includes treating function sorts
  (constructible by ->) as first-class sorts and handling partially applied
  function symbols. Support for higher-order constraints can be enabled by
  the option --uf-ho.
• Support for set comprehension binders comprehension.
• Eager bit-blasting: Support for SAT solver Kissat.

Improvements:

• API: Function definitions can now be requested to be global. If the global
  parameter is set to true, they persist after popping the user context.
• Java/Python bindings: The bindings now allow users to catch exceptions
• Arithmetic: Performance improvements
  • Linear solver: New lemmas inspired by unit-cube tests
  • Non-linear solver: Expanded set of axioms
• Ackermannization: The Ackermannization preprocessing pass now supports
  uninterpreted sorts and as a result all QF_UFBV problems are supported in
  combination with eager bit blasting.

Changes:

• CVC language: Models printed in the CVC language now include an explicit end
  marker to facilitate the communication over pipes with CVC4.
• API change: SmtEngine::query() has been renamed to
  SmtEngine::checkEntailed() and Result::Validity has been renamed to
  Result::Entailment along with corresponding changes to the enum values.
• Java API change: The name of CVC4's package is now edu.stanford.CVC4
  instead of edu.nyu.acsys.CVC4.
• The default output language is changed from CVC to SMT-LIB 2.6. The
  default output language is used when the problem language cannot be
  easily inferred (for example when CVC4 is used from the API).
• Printing of BV constants: previously CVC4 would print BV constant
  values as indexed symbols by default and in binary notation with the
  option --bv-print-consts-in-binary. To be SMT-LIB compliant the
  default behavior is now to print BV constant values in binary
  notation and as indexed symbols with the new option
  --bv-print-consts-as-indexed-symbols. The option
  --bv-print-consts-in-binary has been removed.
• Updated to SyGuS language version 2.0 by default. This is the last release
  that will support the SyGuS language version 1.0 (--lang=sygus1). A
  script is provided to convert version 1.0 files to version 2.0, see
  ./contrib/sygus-v1-to-v2.sh.
• Support for user-provided rewrite rule quantifiers have been removed.
• Support for certain option aliases have been removed.
• Support for parallel portfolio builds has been removed.