CVC4 1.7 Released

We are delighted to announce version 1.7 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.

New Features:

• Proofs:
  • Support for bit-vector proofs with eager bitblasting (older versions only supported proofs with lazy bitblasting).
• Strings:
  • Support for str.replaceall operator.
  • New option --re-elim to reduce regular expressions to extended string operators, resulting in better performance on regular expression benchmarks (enabled by default).
• SyGuS:
  • Support for abduction (--sygus-abduct). Given a formula, this option uses CVC4’s SyGuS solver to find a sufficient condition such that the conjunction of the condition and the formula is unsatisfiable.
  • Support for two new term enumerator strategies: variable agnostic (--sygus-active-gen=var-agnostic) and fast (--sygus-active-gen=enum). By default, CVC4 tries to choose the best term enumerator strategy automatically based on the input (--sygus-active-gen=auto).
  • Support for streaming solutions of increasingly smaller size when using the PBE solver (--sygus-stream --sygus-pbe). After the first solution is found and printed, the solver will continue to look for new solutions and print those, if any, that are smaller than previously printed solutions.
  • Support for unification-based techniques in non-separable specifications (--sygus-unif). For solving invariant problems a dedicate mode (--sygus-unif-boolean-heuristic-dt) is available that builds candidate solutions using heuristic decision tree learning.

Improvements:

• Strings:
  • Significantly better performance on string benchmarks over the core theory and those with extended string functions like substring, contains, and replace.

Changes:

• API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its actual behavior.
• Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
• The CVC3 compatibility layer has been removed.
• The build system now uses CMake instead of Autotools. Please refer to INSTALL.md for up-to-date instructions on how to build CVC4.

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)
• Amazon AWS Automated Reasoning Group
• The Defense Advanced Research Projects Agency (awards FA8750-13-2-0241, FA8750-15-C-0113, N66001-18-C-4012, FA8650-18-2-7854, FA8650-18-2-7861)
• The European Research Council (grant 306595 “STATOR”)
• GE Global Research
• Google
• Intel Corporation
• NASA (contract #NNL14AA06C)
• The National Science Foundation (grants 0644299, 0914956, 1049495, 1228765, 1228768, 1320583, 1656926)
• The Office of Naval Research (award N68335-17-C-0558)
• The Semiconductor Research Corporation (tasks 1850.001, 1850.002)
• The Stanford Agile Hardware Center
• The Stanford SystemX Alliance
• United Technologies Research Center

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

-The CVC4 team