notbugAs an Amazon Associate I earn from qualifying purchases.
Want a good read? Try FreeBSD Mastery: Jails (IT Mastery Book 15)
Want a good monitor light? See my photosAll times are UTC
Ukraine
Port details
cvc3 Automatic theorem prover for the SMT problem
2.4.1_7 math Deleted on this many watch lists=0 search for ports that depend on this port Find issues related to this port Report an issue related to this port View this port on Repology. pkg-fallout 2.4.1_7Version of this port present on the latest quarterly branch.
Maintainer: lwhsu@FreeBSD.org search for ports maintained by this maintainer
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).
Homepage    cgit ¦ Codeberg ¦ GitHub ¦ GitLab ¦ SVNWeb - no subversion history for this port

Manual pages:
FreshPorts has no man page information for this port.
pkg-plist: as obtained via: make generate-plist
Expand this list (97 items)
Collapse this list.
  1. @ldconfig
  2. bin/cvc3
  3. include/cvc3/assumptions.h
  4. include/cvc3/c_interface.h
  5. include/cvc3/c_interface_defs.h
  6. include/cvc3/cdflags.h
  7. include/cvc3/cdlist.h
  8. include/cvc3/cdmap.h
  9. include/cvc3/cdmap_ordered.h
  10. include/cvc3/cdo.h
  11. include/cvc3/circuit.h
  12. include/cvc3/clause.h
  13. include/cvc3/cnf.h
  14. include/cvc3/cnf_manager.h
  15. include/cvc3/command_line_exception.h
  16. include/cvc3/command_line_flags.h
  17. include/cvc3/common_proof_rules.h
  18. include/cvc3/compat_hash_map.h
  19. include/cvc3/compat_hash_set.h
  20. include/cvc3/context.h
  21. include/cvc3/cvc_util.h
  22. include/cvc3/debug.h
  23. include/cvc3/dpllt.h
  24. include/cvc3/dpllt_basic.h
  25. include/cvc3/dpllt_minisat.h
  26. include/cvc3/eval_exception.h
  27. include/cvc3/exception.h
  28. include/cvc3/expr.h
  29. include/cvc3/expr_hash.h
  30. include/cvc3/expr_manager.h
  31. include/cvc3/expr_map.h
  32. include/cvc3/expr_op.h
  33. include/cvc3/expr_stream.h
  34. include/cvc3/expr_transform.h
  35. include/cvc3/expr_value.h
  36. include/cvc3/fdstream.h
  37. include/cvc3/formula_value.h
  38. include/cvc3/hash_fun.h
  39. include/cvc3/hash_map.h
  40. include/cvc3/hash_set.h
  41. include/cvc3/hash_table.h
  42. include/cvc3/kinds.h
  43. include/cvc3/lang.h
  44. include/cvc3/memory_manager.h
  45. include/cvc3/memory_manager_chunks.h
  46. include/cvc3/memory_manager_context.h
  47. include/cvc3/memory_manager_malloc.h
  48. include/cvc3/notifylist.h
  49. include/cvc3/os.h
  50. include/cvc3/parser.h
  51. include/cvc3/parser_exception.h
  52. include/cvc3/pretty_printer.h
  53. include/cvc3/proof.h
  54. include/cvc3/queryresult.h
  55. include/cvc3/rational.h
  56. include/cvc3/sat_api.h
  57. include/cvc3/search.h
  58. include/cvc3/search_fast.h
  59. include/cvc3/search_impl_base.h
  60. include/cvc3/search_sat.h
  61. include/cvc3/search_simple.h
  62. include/cvc3/smartcdo.h
  63. include/cvc3/smtlib_exception.h
  64. include/cvc3/sound_exception.h
  65. include/cvc3/statistics.h
  66. include/cvc3/theorem.h
  67. include/cvc3/theorem_manager.h
  68. include/cvc3/theorem_producer.h
  69. include/cvc3/theory.h
  70. include/cvc3/theory_arith.h
  71. include/cvc3/theory_arith3.h
  72. include/cvc3/theory_arith_new.h
  73. include/cvc3/theory_arith_old.h
  74. include/cvc3/theory_array.h
  75. include/cvc3/theory_bitvector.h
  76. include/cvc3/theory_core.h
  77. include/cvc3/theory_datatype.h
  78. include/cvc3/theory_datatype_lazy.h
  79. include/cvc3/theory_quant.h
  80. include/cvc3/theory_records.h
  81. include/cvc3/theory_simulate.h
  82. include/cvc3/theory_uf.h
  83. include/cvc3/translator.h
  84. include/cvc3/type.h
  85. include/cvc3/typecheck_exception.h
  86. include/cvc3/variable.h
  87. include/cvc3/vc.h
  88. include/cvc3/vc_cmd.h
  89. include/cvc3/vcl.h
  90. lib/libcvc3.so
  91. lib/libcvc3.so.5
  92. lib/libcvc3.so.5.0
  93. lib/libcvc3.so.5.0.0
  94. libdata/pkgconfig/cvc3.pc
  95. @owner
  96. @group
  97. @mode
Collapse this list.
Dependency lines:
  • cvc3>0:math/cvc3
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):
cvc3
ABIaarch64amd64armv6armv7i386powerpcpowerpc64powerpc64le
FreeBSD:13:latest--2.4.1_7---2.4.1_7-
FreeBSD:13:quarterly--------
FreeBSD:14:latest--------
FreeBSD:14:quarterly--------
FreeBSD:15:latest--n/a-n/a---
Dependencies
NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
Build dependencies:
  1. bison : devel/bison
  2. gmake>=4.3 : devel/gmake
  3. gcc12 : lang/gcc12
  4. as : devel/binutils
  5. perl5>=5.32.r0<5.33 : lang/perl5.32
Runtime dependencies:
  1. gcc12 : lang/gcc12
  2. perl5>=5.32.r0<5.33 : lang/perl5.32
Library dependencies:
  1. 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:
Expand this list (1 items)
Collapse this list.
  1. http://www.cs.nyu.edu/acsys/cvc3/download/2.4.1/
Collapse this list.
Port Moves
  • port moved to math/cvc5 on 2023-01-04
    REASON: CVC3 was succeeded by CVC4 and CVC5

Number of commits found: 35

Commit History - (may be incomplete: for full details, see links to repositories near top of page)
CommitCreditsLog message
2.4.1_7
05 Jan 2023 08:16:03
commit hash: 7a04fc56833848131e198bfaed4c7d5b468cb87dcommit hash: 7a04fc56833848131e198bfaed4c7d5b468cb87dcommit hash: 7a04fc56833848131e198bfaed4c7d5b468cb87dcommit hash: 7a04fc56833848131e198bfaed4c7d5b468cb87d files touched by this commit
Li-Wen Hsu (lwhsu) search for other commits by this committer
Remove math/cvc3, it was succeeded by CVC4 and CVC5

Reported by:	yuri
07 Sep 2022 21:58:51
commit hash: fb16dfecae4a6efac9f3a78e0b759fb7a3c53de4commit hash: fb16dfecae4a6efac9f3a78e0b759fb7a3c53de4commit hash: fb16dfecae4a6efac9f3a78e0b759fb7a3c53de4commit hash: fb16dfecae4a6efac9f3a78e0b759fb7a3c53de4 files touched by this commit
Stefan Eßer (se) search for other commits by this committer
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
commit hash: b7f05445c00f2625aa19b4154ebcbce5ed2daa52commit hash: b7f05445c00f2625aa19b4154ebcbce5ed2daa52commit hash: b7f05445c00f2625aa19b4154ebcbce5ed2daa52commit hash: b7f05445c00f2625aa19b4154ebcbce5ed2daa52 files touched by this commit
Stefan Eßer (se) search for other commits by this committer
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 View all of this commit message)
2.4.1_7
20 Jul 2022 14:22:24
commit hash: f53eb28489aa8f30712cd8772d1a0e05c394a5dacommit hash: f53eb28489aa8f30712cd8772d1a0e05c394a5dacommit hash: f53eb28489aa8f30712cd8772d1a0e05c394a5dacommit hash: f53eb28489aa8f30712cd8772d1a0e05c394a5da files touched by this commit
Tobias C. Berner (tcberner) search for other commits by this committer
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 View all of this commit message)
2.4.1_7
04 Jun 2021 05:53:21
commit hash: d09ed096c44ca516f3e4922e292b4afabd03ff11commit hash: d09ed096c44ca516f3e4922e292b4afabd03ff11commit hash: d09ed096c44ca516f3e4922e292b4afabd03ff11commit hash: d09ed096c44ca516f3e4922e292b4afabd03ff11 files touched by this commit
Gerald Pfeifer (gerald) search for other commits by this committer
*/*: 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
commit hash: 305f148f482daf30dcf728039d03d019f88344ebcommit hash: 305f148f482daf30dcf728039d03d019f88344ebcommit hash: 305f148f482daf30dcf728039d03d019f88344ebcommit hash: 305f148f482daf30dcf728039d03d019f88344eb files touched by this commit
Mathieu Arnold (mat) search for other commits by this committer
Remove # $FreeBSD$ from Makefiles.
2.4.1_7
26 Jan 2021 13:59:25
Revision:562665Original commit files touched by this commit
sunpoet search for other commits by this committer
Fix build with bison 3.7.4

PR:		248911
Exp-run by:	antoine
2.4.1_7
26 Jul 2019 20:46:57
Revision:507372Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:487272Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:475857Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:464084Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:449591Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:437439Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:433908Original commit files touched by this commit
jbeich search for other commits by this committer
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
Revision:426566Original commit files touched by this commit
gerald search for other commits by this committer
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
Revision:424427Original commit files touched by this commit
mat search for other commits by this committer
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
Revision:415738Original commit files touched by this commit
amdmi3 search for other commits by this committer
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
Revision:415499Original commit files touched by this commit
amdmi3 search for other commits by this committer
- Fix trailing whitespace in pkg-descrs, categories [g-n]*

Approved by:	portmgr blanket
2.4.1
01 Apr 2016 14:16:20
Revision:412348Original commit files touched by this commit
mat search for other commits by this committer
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
Revision:372546Original commit files touched by this commit
antoine search for other commits by this committer
Cleanup plist
2.4.1
16 Jul 2014 03:25:08
Revision:362025Original commit files touched by this commit
vanilla search for other commits by this committer
Stagify.

Approved by:	lwhsu@ (maintainer)
2.4.1
13 Jul 2014 23:36:40
Revision:361728Original commit files touched by this commit
bapt search for other commits by this committer
Modernize LIB_DEPENDS

With hat:	portmgr
2.4.1
07 Jul 2014 15:31:02
Revision:361099Original commit files touched by this commit
olgeni search for other commits by this committer
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
Revision:333703Original commit files touched by this commit
lwhsu search for other commits by this committer
- 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
Revision:327746Original commit files touched by this commit
bapt search for other commits by this committer
Add NO_STAGE all over the place in preparation for the staging support (cat:
math)
2.4.1
16 Sep 2013 16:32:07
Revision:327411Original commit files touched by this commit
bapt search for other commits by this committer
Convert to new perl framework
Convert USE_GMAKE to USES
2.4.1
08 Mar 2013 11:32:12
Revision:313635Original commit files touched by this commit
bapt search for other commits by this committer
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
Original commit files touched by this commit
lwhsu search for other commits by this committer
- Update to 2.4.1
1.2.1_3
20 Mar 2011 12:54:45
Original commit files touched by this commit
miwi search for other commits by this committer
- Get Rid MD5 support
1.2.1_3
19 Apr 2010 10:43:43
Original commit files touched by this commit
ale search for other commits by this committer
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
Original commit files touched by this commit
ale search for other commits by this committer
Chase libgmp and bump PORTREVISION.
1.2.1_1
17 Oct 2007 10:13:01
Original commit files touched by this commit
ade search for other commits by this committer
Migration from bison 1.x to 2.x

PR:             117086
Tested by:      -exp runs
1.2.1
07 Sep 2007 22:54:09
Original commit files touched by this commit
lwhsu search for other commits by this committer
- Update to 1.2.1
1.0
04 Apr 2007 08:49:31
Original commit files touched by this commit
lwhsu search for other commits by this committer
- Change to my FreeBSD.org email

Approved by:     clsung (mentor)
1.0
25 Mar 2007 04:04:31
Original commit files touched by this commit
clsung search for other commits by this committer
Add cvc3 1.0, an automatic theorem prover for the SMT problem.

PR:             ports/110770
Submitted by:   Li-Wen Hsu <lwhsu at lwhsu.org>

Number of commits found: 35