An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements
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:
str.replace_re
, str.replace_re_all
, str.is_digit
,
str.from_code
, re.diff
, and re.comp
str.in_re
instead of str.in.re
),
new escape sequences. The new syntax is enabled by default for smt2 files../examples/api/sygus_*.cpp
.->
) as first-class sorts and handling partially applied
function symbols. Support for higher-order constraints can be enabled by
the option --uf-ho
.comprehension
.Improvements:
global
parameter is set to true, they persist after popping the user context.Changes:
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.edu.stanford.CVC4
instead of edu.nyu.acsys.CVC4
.--lang=sygus1
). A
script is provided to convert version 1.0 files to version 2.0, see
./contrib/sygus-v1-to-v2.sh
.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.
Downloads, documentation, tutorials, and more information are available at the CVC4 web site: http://cvc4.cs.stanford.edu/
-The CVC4 team