# CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

19 June 2020

# CVC4 1.8 Released

by Andres Noetzli

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.