CVC4 1.8 Released

We are delighted to announce version 1.8 of CVC4, the open-source flagship SMT solver. It is a joint project led by Stanford University and the University of Iowa. It is available at http://cvc4.cs.stanford.edu.

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 has been removed.
• Support for certain option aliases has been removed.
• Support for parallel portfolio builds has been removed.

We welcome feedback, feature requests, contributions, and collaborations. It is our hope that CVC4 will become a research platform for a broad and diverse set of users and developers. If you are interested in getting involved with the project, please contact a member of the development team.

The development of CVC4 is supported in part by the organizations listed in the Acknowledgements.

Downloads, documentation, tutorials, and more information are available at the CVC4 web site: http://cvc4.cs.stanford.edu/

-The CVC4 team