Bug 451706

Summary:	Ebuild request: sci-mathematics/cvc4-1.0 - SMT solver
Product:	Gentoo Linux	Reporter:	Anton Kochkov <anton.kochkov>
Component:	New packages	Assignee:	Default Assignee for New Packages <maintainer-wanted>
Status:	RESOLVED FIXED
Severity:	enhancement	CC:	gienah, tomwij
Priority:	Normal
Version:	unspecified
Hardware:	All
OS:	Linux
Whiteboard:
Package list:		Runtime testing required:	---
Bug Depends on:	293305
Bug Blocks:

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 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).

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!