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.
- Support for bit-vector proofs with eager bitblasting (older versions only supported proofs with lazy bitblasting).
- 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).
- 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.
- Significantly better performance on string benchmarks over the core theory and those with extended string functions like substring, contains, and replace.
- 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
- 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
Downloads, documentation, tutorials, and more information are available at the CVC4 web site: http://cvc4.cs.stanford.edu
-The CVC4 team