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
  • UTRC

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

-The CVC4 team