by Haniel Barbosa
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.
--re-elimto reduce regular expressions to extended string operators, resulting in better performance on regular expression benchmarks (enabled by default).
--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.
--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-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.
--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.
Expr::iffExpr()is renamed to
Expr::eqExpr()to reflect its actual behavior.
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:
Downloads, documentation, tutorials, and more information are available at the CVC4 web site: http://cvc4.cs.stanford.edu/
-The CVC4 team