Port details |
- cvc3 Automatic theorem prover for the SMT problem
- 2.4.1_7 math
=0 2.4.1_7Version of this port present on the latest quarterly branch.
- Maintainer: lwhsu@FreeBSD.org
- Port Added: 2007-03-25 04:06:19
- Last Update: 2023-01-05 08:16:03
- Commit Hash: 7a04fc5
- License: not specified in port
- WWW:
- https://www.cs.nyu.edu/acsys/cvc3/
- Description:
- CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in logical
theories and their combination.
CVC3 is the last offspring of a series of popular SMT provers, which originated
at Stanford University with the SVC system. In particular, it builds on the
code base of CVC Lite, its most recent predecessor. Its high level design
follows that of the Sammy prover.
CVC3 works with a version of first-order logic with polymorphic types and has
a wide variety of features including:
* several built-in base theories: rational and integer linear arithmetic,
arrays, tuples, records, inductive data types, bit vectors, and equality
over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* a rich C and C++ API for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial purposes
(see license).
- ¦ ¦ ¦ ¦
- Manual pages:
- FreshPorts has no man page information for this port.
- pkg-plist: as obtained via:
make generate-plist - Dependency lines:
-
- No installation instructions:
- This port has been deleted.
- PKGNAME: cvc3
- Flavors: there is no flavor information for this port.
- distinfo:
- SHA256 (cvc3-2.4.1.tar.gz) = d55b1d6006cfbac3f6d4c086964558902c3ed0efa66ac499cfb2193f3ee4acf7
SIZE (cvc3-2.4.1.tar.gz) = 1196616
Packages (timestamps in pop-ups are UTC):
- Dependencies
- NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
- Build dependencies:
-
- bison : devel/bison
- gmake>=4.3 : devel/gmake
- gcc12 : lang/gcc12
- as : devel/binutils
- perl5>=5.32.r0<5.33 : lang/perl5.32
- Runtime dependencies:
-
- gcc12 : lang/gcc12
- perl5>=5.32.r0<5.33 : lang/perl5.32
- Library dependencies:
-
- libgmp.so : math/gmp
- There are no ports dependent upon this port
Configuration Options:
- No options to configure
- Options name:
- math_cvc3
- USES:
- bison gmake pathfix perl5
- FreshPorts was unable to extract/find any pkg message
- Master Sites:
|
Commit History - (may be incomplete: for full details, see links to repositories near top of page) |
Commit | Credits | Log message |
2.4.1_7 05 Jan 2023 08:16:03 |
Li-Wen Hsu (lwhsu) |
Remove math/cvc3, it was succeeded by CVC4 and CVC5
Reported by: yuri |
07 Sep 2022 21:58:51 |
Stefan Eßer (se) |
Remove WWW entries moved into port Makefiles
Commit b7f05445c00f has added WWW entries to port Makefiles based on
WWW: lines in pkg-descr files.
This commit removes the WWW: lines of moved-over URLs from these
pkg-descr files.
Approved by: portmgr (tcberner) |
2.4.1_7 07 Sep 2022 21:10:59 |
Stefan Eßer (se) |
Add WWW entries to port Makefiles
It has been common practice to have one or more URLs at the end of the
ports' pkg-descr files, one per line and prefixed with "WWW:". These
URLs should point at a project website or other relevant resources.
Access to these URLs required processing of the pkg-descr files, and
they have often become stale over time. If more than one such URL was
present in a pkg-descr file, only the first one was tarnsfered into
the port INDEX, but for many ports only the last line did contain the
port specific URL to further information.
There have been several proposals to make a project URL available as
a macro in the ports' Makefiles, over time.
(Only the first 15 lines of the commit message are shown above ) |
2.4.1_7 20 Jul 2022 14:22:24 |
Tobias C. Berner (tcberner) |
math: remove 'Created by' lines
A big Thank You to the original contributors of these ports:
* Aaron Dalton <aaron@FreeBSD.org>
* Aaron Dalton <aaron@daltons.ca>
* Alessando Sagratini <ale_sagra@hotmail.com>
* Alex Dupre <ale@FreeBSD.org>
* Alexey Dokuchaev <danfe@FreeBSD.org>
* Amarendra Godbole <amarendra.godbole@gmail.com>
* Anders Nordby <anders@FreeBSD.org>
* Andreas Fehlner (fehlner@gmx.de)
* Andrew L. Neporada <andrew@chg.ru>
* Andrey <gugu@zoo.rambler.ru>
* Andrey Zakhvatov (Only the first 15 lines of the commit message are shown above ) |
2.4.1_7 04 Jun 2021 05:53:21 |
Gerald Pfeifer (gerald) |
*/*: Replace USE_GCC=any with USE_GCC=yes
USE_GCC=any has been equivalent to USE_GCC=yes in most cases (such
as i386 and amd64 since 12.x and depending on configuration 11.x,
most newer installations on other platforms, and 13.x across the
board).
Since commit 96c17633d90386b5bcf8 Mk/bsd.gcc.mk is treating them as
different spellings of the same, so continue the deorbiting of the
USE_GCC=any form and simply replace it with USE_GCC=yes.
This should not make any functional difference at all.
Discussed with: mat, linimon, pkubaj |
2.4.1_7 06 Apr 2021 14:31:07 |
Mathieu Arnold (mat) |
Remove # $FreeBSD$ from Makefiles. |
2.4.1_7 26 Jan 2021 13:59:25 |
sunpoet |
Fix build with bison 3.7.4
PR: 248911
Exp-run by: antoine |
2.4.1_7 26 Jul 2019 20:46:57 |
gerald |
Bump PORTREVISION for ports depending on the canonical version of GCC
as defined in Mk/bsd.default-versions.mk which has moved from GCC 8.3
to GCC 9.1 under most circumstances now after revision 507371.
This includes ports
- with USE_GCC=yes or USE_GCC=any,
- with USES=fortran,
- using Mk/bsd.octave.mk which in turn features USES=fortran, and
- with USES=compiler specifying openmp, nestedfct, c11, c++0x, c++11-lang,
c++11-lib, c++14-lang, c++17-lang, or gcc-c++11-lib
plus, everything INDEX-11 shows with a dependency on lang/gcc9 now.
PR: 238330 |
2.4.1_6 12 Dec 2018 01:35:36 |
gerald |
Bump PORTREVISION for ports depending on the canonical version of GCC
defined via Mk/bsd.default-versions.mk which has moved from GCC 7.4 t
GCC 8.2 under most circumstances.
This includes ports
- with USE_GCC=yes or USE_GCC=any,
- with USES=fortran,
- using Mk/bsd.octave.mk which in turn features USES=fortran, and
- with USES=compiler specifying openmp, nestedfct, c11, c++0x, c++11-lang,
c++11-lib, c++14-lang, c++17-lang, or gcc-c++11-lib
plus, as a double check, everything INDEX-11 showed depending on lang/gcc7.
PR: 231590 |
2.4.1_5 29 Jul 2018 22:18:46 |
gerald |
Bump PORTREVISION for ports depending on the canonical version of GCC
in the ports tree (via Mk/bsd.default-versions.mk and lang/gcc) which
has now moved from GCC 6 to GCC 7 by default.
This includes ports
- featuring USE_GCC=yes or USE_GCC=any,
- featuring USES=fortran,
- using Mk/bsd.octave.mk which in turn features USES=fortran, and those
- with USES=compiler specifying one of openmp, nestedfct, c11, c++0x,
c++11-lib, c++11-lang, c++14-lang, c++17-lang, or gcc-c++11-lib.
PR: 222542 |
2.4.1_4 10 Mar 2018 17:46:06 |
gerald |
Bump PORTREVISIONs of all users of math/mpc that we just updated to
version 1.1.0 (via revision 464079). |
2.4.1_3 10 Sep 2017 20:55:39 |
gerald |
Bump PORTREVISION for ports depending on the canonical version of GCC
(via Mk/bsd.default-versions.mk and lang/gcc) which has moved from
GCC 5.4 to GCC 6.4 under most circumstances.
This includes ports
- with USE_GCC=yes or USE_GCC=any,
- with USES=fortran,
- using Mk/bsd.octave.mk which in turn features USES=fortran, and
- with USES=compiler specifying openmp, nestedfct, c++11-lib, c++11-lang,
c++14-lang, c++0x, c11, or gcc-c++11-lib.
PR: 219275 |
2.4.1_2 01 Apr 2017 15:23:32 |
gerald |
Bump PORTREVISIONs for ports depending on the canonical version of GCC and
lang/gcc which have moved from GCC 4.9.4 to GCC 5.4 (at least under some
circumstances such as versions of FreeBSD or platforms).
This includes ports
- with USE_GCC=yes or USE_GCC=any,
- with USES=fortran,
- using using Mk/bsd.octave.mk which in turn has USES=fortran, and
- with USES=compiler specifying openmp, nestedfct, c++11-lib, c++14-lang,
c++11-lang, c++0x, c11, or gcc-c++11-lib.
PR: 216707 |
2.4.1_1 11 Feb 2017 19:54:32 |
jbeich |
math/cvc3: unbreak with gcc6 or later
In file included from src/include/expr_manager.h:445:0,
from src/include/expr.h:803,
from expr.cpp:25:
src/include/expr_value.h: In static member function 'static size_t
CVC3::ExprString::hash(const string&)':
src/include/expr_value.h:667:34: error: no match for call to '(std::hash<char*>)
(const char*)'
return s_charHash(str.c_str());
^
In file included from src/include/hash_map.h:54:0,
from src/include/compat_hash_map.h:34,
from src/include/expr.h:33,
from src/include/assumptions.h:36,
from src/include/theorem_producer.h:75,
from common_theorem_producer.h:34,
from common_theorem_producer.cpp:27:
src/include/hash_table.h: In instantiation of 'Hash::hash_table<_Key, _Value,
_HashFcn, _EqualKey, _ExtractKey>::~hash_table() [with _Key = CVC3::Expr; _Value
= std::pair<const CVC3::Expr, CVC3::CDOmap<CVC3::Expr, CVC3::Theorem,
std::hash<CVC3::Expr> >*>; _HashFcn = std::hash<CVC3::Expr>; _EqualKey =
std::equal_to<CVC3::Expr>; _ExtractKey = Hash::_Select1st<std::pair<const
CVC3::Expr, CVC3::CDOmap<CVC3::Expr, CVC3::Theorem, std::hash<CVC3::Expr> >*>
>]':
src/include/hash_map.h:82:9: required from 'CVC3::CDMap<Key, Data,
HashFcn>::~CDMap() [with Key = CVC3::Expr; Data = CVC3::Theorem; HashFcn =
std::hash<CVC3::Expr>]'
common_theorem_producer.h:60:38: required from here
src/include/hash_table.h:319:5: error: use of deleted function
'std::hash<CVC3::Expr>::~hash()'
}
^ |
2.4.1_1 20 Nov 2016 09:38:09 |
gerald |
Bump PORTREVISIONS for ports depending on the canonical version of GCC and
lang/gcc which have moved from GCC 4.8.5 to GCC 4.9.4 (at least under some
circumstances such as versions of FreeBSD or platforms).
In particular that is ports with USE_GCC=yes, USE_GCC=any, or one of
gcc-c++11-lib, openmp, nestedfct, c++11-lib as well as c++14-lang,
c++11-lang, c++0x, c11 requested via USES=compiler. |
2.4.1 21 Oct 2016 15:21:13 |
mat |
Use USES=pathfix where applicable.
PR: 213195
Submitted by: mat
Exp-run by: antoine
Sponsored by: Absolight
Differential Revision: https://reviews.freebsd.org/D8093 |
2.4.1 23 May 2016 18:36:52 |
amdmi3 |
Convert tab after WWW: in pkg-descrs to single space as per PHB
Approved by: portmgr blanket |
2.4.1 19 May 2016 10:44:12 |
amdmi3 |
- Fix trailing whitespace in pkg-descrs, categories [g-n]*
Approved by: portmgr blanket |
2.4.1 01 Apr 2016 14:16:20 |
mat |
Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p.
With hat: portmgr
Sponsored by: Absolight |
2.4.1 13 Nov 2014 23:24:01 |
antoine |
Cleanup plist |
2.4.1 16 Jul 2014 03:25:08 |
vanilla |
Stagify.
Approved by: lwhsu@ (maintainer) |
2.4.1 13 Jul 2014 23:36:40 |
bapt |
Modernize LIB_DEPENDS
With hat: portmgr |
2.4.1 07 Jul 2014 15:31:02 |
olgeni |
Remove indefinite articles and trailing periods from COMMENT, plus minor
COMMENT typos and surrounding whitespace fixes. A few Makefiles where not
included as they contain Latin-1 characters that break the Phabricator
workflow. Category M.
CR: D306
Approved by: portmgr (bapt) |
2.4.1 13 Nov 2013 15:55:10 |
lwhsu |
- Try to fix build with USE_GCC, anyway, cvc4 is out and would be ported later |
2.4.1 20 Sep 2013 20:55:06 |
bapt |
Add NO_STAGE all over the place in preparation for the staging support (cat:
math) |
2.4.1 16 Sep 2013 16:32:07 |
bapt |
Convert to new perl framework
Convert USE_GMAKE to USES |
2.4.1 08 Mar 2013 11:32:12 |
bapt |
Convert USE_BISON to USES= bison
It brings bison as a build dependency in case it is set the following way:
USES= bison or USES= bison:build
it brings bison as a run dependency in case it is set the following way:
USES= bison:run
it brings bison both as a run and build dependency in case it the set the
following way:
USES= bison:both
While here trim some headers
Convert some USE_GNOME= gnomehack to USES= pathfix |
2.4.1 04 Feb 2012 14:37:52 |
lwhsu |
- Update to 2.4.1 |
1.2.1_3 20 Mar 2011 12:54:45 |
miwi |
- Get Rid MD5 support |
1.2.1_3 19 Apr 2010 10:43:43 |
ale |
Switch to use newer GMP version.
PR: ports/144487
Submitted by: ale
Approved by: portmgr (-exp run by erwin) |
1.2.1_2 13 May 2009 09:46:02 |
ale |
Chase libgmp and bump PORTREVISION. |
1.2.1_1 17 Oct 2007 10:13:01 |
ade |
Migration from bison 1.x to 2.x
PR: 117086
Tested by: -exp runs |
1.2.1 07 Sep 2007 22:54:09 |
lwhsu |
- Update to 1.2.1 |
1.0 04 Apr 2007 08:49:31 |
lwhsu |
- Change to my FreeBSD.org email
Approved by: clsung (mentor) |
1.0 25 Mar 2007 04:04:31 |
clsung |
Add cvc3 1.0, an automatic theorem prover for the SMT problem.
PR: ports/110770
Submitted by: Li-Wen Hsu <lwhsu at lwhsu.org> |