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).
Requires dev-java/antlr-3.4
dev-java/antlr was updated
Already in the tree. Thanks!
