CVC4 1.6 Released

We are delighted to announce version 1.6 of CVC4, the open-source flagship SMT solver developed at Stanford University, New York University and the University of Iowa, available at http://cvc4.cs.stanford.edu.

This version is very close to the version of CVC4 submitted to the SMT-competition 2018.

New Features:

• A new theory of floating points.
• Novel approach for solving quantified bit-vectors (BV).
• Eager bit-blasting: Support for SAT solver CaDiCaL.
• A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
• Support for transcendental functions (sin, cos, exp). In SMT2 input, this can be enabled by adding T to the logic (e.g., QF_NRAT).
• Support for new operators in strings, including string inequality (str.<=) and string code (str.code).
• Support for automated rewrite rule generation from sygus (*.sy) inputs using syntax-guided enumeration (option -–sygus-rr).

Improvements:

• Incremental unsat core support.
• Further development of rewrite rules for the theory of strings and regular expressions.
• Many optimizations for syntax-guided synthesis, including improved symmetry breaking for enumerative search and specialized algorithms for programming-by-examples conjectures.

Changes:

• Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added support for CryptoMinisat 5.
• The LFSC proof checker now resides in its own repository on GitHub. It is not distributed with CVC4 anymore.

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 following organizations:

• The Air Force Office of Scientific Research (award FA9550-09-1-0596)
• The Defense Advanced Research Projects Agency (award FA8750-13-2-0241)
• The European Research Council (grant 306595 “STATOR”)
• GE Global Research
• Google
• Intel Corporation
• The National Science Foundation (grants 0644299, 0914956, 1049495, 1228768, 1320583)
• The Semiconductor Research Corporation (tasks 1850.001, 1850.002)

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

-The CVC4 team