cvc3 Automatic theorem prover for the SMT problem
2.4.1_6 math =0

Maintainer: lwhsu@FreeBSD.org
Port Added: 2007-03-25 04:06:19
Last Update: 2018-12-12 01:35:36
SVN Revision: 487272
License: not specified in port

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

WWW: http://www.cs.nyu.edu/acsys/cvc3/

SVNWeb : Homepage

Pseudo-pkg-plist information, but much better, from make generate-plist
Expand this list (95 items)

1. bin/cvc3
2. include/cvc3/assumptions.h
3. include/cvc3/c_interface.h
4. include/cvc3/c_interface_defs.h
5. include/cvc3/cdflags.h
6. include/cvc3/cdlist.h
7. include/cvc3/cdmap.h
8. include/cvc3/cdmap_ordered.h
9. include/cvc3/cdo.h
10. include/cvc3/circuit.h
11. include/cvc3/clause.h
12. include/cvc3/cnf.h
13. include/cvc3/cnf_manager.h
14. include/cvc3/command_line_exception.h
15. include/cvc3/command_line_flags.h
16. include/cvc3/common_proof_rules.h
17. include/cvc3/compat_hash_map.h
18. include/cvc3/compat_hash_set.h
19. include/cvc3/context.h
20. include/cvc3/cvc_util.h
21. include/cvc3/debug.h
22. include/cvc3/dpllt.h
23. include/cvc3/dpllt_basic.h
24. include/cvc3/dpllt_minisat.h
25. include/cvc3/eval_exception.h
26. include/cvc3/exception.h
27. include/cvc3/expr.h
28. include/cvc3/expr_hash.h
29. include/cvc3/expr_manager.h
30. include/cvc3/expr_map.h
31. include/cvc3/expr_op.h
32. include/cvc3/expr_stream.h
33. include/cvc3/expr_transform.h
34. include/cvc3/expr_value.h
35. include/cvc3/fdstream.h
36. include/cvc3/formula_value.h
37. include/cvc3/hash_fun.h
38. include/cvc3/hash_map.h
39. include/cvc3/hash_set.h
40. include/cvc3/hash_table.h
41. include/cvc3/kinds.h
42. include/cvc3/lang.h
43. include/cvc3/memory_manager.h
44. include/cvc3/memory_manager_chunks.h
45. include/cvc3/memory_manager_context.h
46. include/cvc3/memory_manager_malloc.h
47. include/cvc3/notifylist.h
48. include/cvc3/os.h
49. include/cvc3/parser.h
50. include/cvc3/parser_exception.h
51. include/cvc3/pretty_printer.h
52. include/cvc3/proof.h
53. include/cvc3/queryresult.h
54. include/cvc3/rational.h
55. include/cvc3/sat_api.h
56. include/cvc3/search.h
57. include/cvc3/search_fast.h
58. include/cvc3/search_impl_base.h
59. include/cvc3/search_sat.h
60. include/cvc3/search_simple.h
61. include/cvc3/smartcdo.h
62. include/cvc3/smtlib_exception.h
63. include/cvc3/sound_exception.h
64. include/cvc3/statistics.h
65. include/cvc3/theorem.h
66. include/cvc3/theorem_manager.h
67. include/cvc3/theorem_producer.h
68. include/cvc3/theory.h
69. include/cvc3/theory_arith.h
70. include/cvc3/theory_arith3.h
71. include/cvc3/theory_arith_new.h
72. include/cvc3/theory_arith_old.h
73. include/cvc3/theory_array.h
74. include/cvc3/theory_bitvector.h
75. include/cvc3/theory_core.h
76. include/cvc3/theory_datatype.h
77. include/cvc3/theory_datatype_lazy.h
78. include/cvc3/theory_quant.h
79. include/cvc3/theory_records.h
80. include/cvc3/theory_simulate.h
81. include/cvc3/theory_uf.h
82. include/cvc3/translator.h
83. include/cvc3/type.h
84. include/cvc3/typecheck_exception.h
85. include/cvc3/variable.h
86. include/cvc3/vc.h
87. include/cvc3/vc_cmd.h
88. include/cvc3/vcl.h
89. lib/libcvc3.so
90. lib/libcvc3.so.5
91. lib/libcvc3.so.5.0
92. lib/libcvc3.so.5.0.0
93. libdata/pkgconfig/cvc3.pc
94. @postexec /usr/sbin/service ldconfig restart > /dev/null
95. @postunexec /usr/sbin/service ldconfig restart > /dev/null
Collapse this list.

Dependency lines:

• cvc3>0:math/cvc3

---

To install the port: cd /usr/ports/math/cvc3/ && make install clean
To add the package: pkg install cvc3

PKGNAME: cvc3

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

---

NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.

Build dependencies:

1. bison : devel/bison
2. gmake : devel/gmake
3. gcc8 : lang/gcc8
4. as : devel/binutils
5. perl5>=5.26<5.27 : lang/perl5.26

Runtime dependencies:

1. gcc8 : lang/gcc8
2. perl5>=5.26<5.27 : lang/perl5.26

Library dependencies:

1. libgmp.so : math/gmp

There are no ports dependent upon this port

---

Configuration Options

     No options to configure

---

USES:

bison gmake pathfix perl5

---

Master Sites:

1. http://www.cs.nyu.edu/acsys/cvc3/download/2.4.1/

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

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

Bump PORTREVISIONs of all users of math/mpc that we just updated to
version 1.1.0 (via revision 464079).

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

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

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()'
     }
     ^

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.

Use USES=pathfix where applicable.

PR:		213195
Submitted by:	mat
Exp-run by:	antoine
Sponsored by:	Absolight
Differential Revision:	https://reviews.freebsd.org/D8093

Convert tab after WWW: in pkg-descrs to single space as per PHB

Approved by:	portmgr blanket

- Fix trailing whitespace in pkg-descrs, categories [g-n]*

Approved by:	portmgr blanket

Remove ${PORTSDIR}/ from dependencies, categories m, n, o, and p.

With hat:	portmgr
Sponsored by:	Absolight

Cleanup plist

Stagify.

Approved by:	lwhsu@ (maintainer)

Modernize LIB_DEPENDS

With hat:	portmgr

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)

- Try to fix build with USE_GCC, anyway, cvc4 is out and would be ported later

Add NO_STAGE all over the place in preparation for the staging support (cat:
math)

Convert to new perl framework
Convert USE_GMAKE to USES

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

- Update to 2.4.1

- Get Rid MD5 support

Switch to use newer GMP version.

PR:             ports/144487
Submitted by:   ale
Approved by:    portmgr (-exp run by erwin)

Chase libgmp and bump PORTREVISION.

Migration from bison 1.x to 2.x

PR:             117086
Tested by:      -exp runs

- Update to 1.2.1

- Change to my FreeBSD.org email

Approved by:     clsung (mentor)

Add cvc3 1.0, an automatic theorem prover for the SMT problem.

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

16 vulnerabilities affecting 137 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities

Last updated:
2019-04-23 04:07:39