First public release of CVC4, version 1.0, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu. (sci-mathematics/cvc3 currently in the tree)
CVC4 is the latest in the CVC series of SMT solvers and provides the functionality of its predecessors while dramatically boosting performance. Features include:
support for the native (CVC) language as well as the SMT-LIB standard language;
decision procedures for the following theories and their combination: equality with uninterpreted functions, real and integer linear arithmetic, bit-vectors, arrays, tuples, records, and user-defined inductive data types;
support for quantifiers through heuristic instantiation;
an interactive text-based interface;
a rich API for embedding in other systems (available for C++ and Java);
model generation abilities;
source compatibility with much of the CVC3 API via a “compatibility library”;
essentially no limit on the use of source or binaries for research or commercial purposes (details on the license can be found on the web site).
dev-java/antlr was updated
Already in the tree. Thanks!