Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!
Bug 451706 - Ebuild request: sci-mathematics/cvc4-1.0 - SMT solver
Summary: Ebuild request: sci-mathematics/cvc4-1.0 - SMT solver
Alias: None
Product: Gentoo Linux
Classification: Unclassified
Component: New packages (show other bugs)
Hardware: All Linux
: Normal enhancement (vote)
Assignee: Default Assignee for New Packages
Depends on: 293305
  Show dependency tree
Reported: 2013-01-13 13:57 UTC by Anton Kochkov
Modified: 2020-01-10 14:31 UTC (History)
2 users (show)

See Also:
Package list:
Runtime testing required: ---


Note You need to log in before you can comment on or make changes to this bug.
Description Anton Kochkov 2013-01-13 13:57:12 UTC
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 (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).
Comment 1 Mark Wright gentoo-dev 2013-01-30 10:12:27 UTC
Requires dev-java/antlr-3.4
Comment 2 Anton Kochkov 2017-09-30 04:42:42 UTC
dev-java/antlr was updated
Comment 3 Anton Kochkov 2020-01-10 14:31:20 UTC
Already in the tree. Thanks!