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: 2019-07-26 21:46:57

SVN Revision: 507372

License: not specified in port

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). WWW: http://www.cs.nyu.edu/acsys/cvc3/

SVNWeb : Homepage

pkg-plist: as obtained via: make generate-plist

Expand this list (95 items)

Collapse this list.

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

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

Dependencies

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. gcc9 : lang/gcc9
4. as : devel/binutils
5. perl5>=5.28.r1<5.29 : lang/perl5.28

Runtime dependencies:

1. gcc9 : lang/gcc9
2. perl5>=5.28.r1<5.29 : lang/perl5.28

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:

Expand this list (1 items)

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

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

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>

12 vulnerabilities affecting 113 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities

Last updated:
2021-01-14 20:39:03