notbugAs an Amazon Associate I earn from qualifying purchases.
Want a good read? Try FreeBSD Mastery: Jails (IT Mastery Book 15)
Port details
cvc4 Automatic theorem prover for SMT (Satisfiability Modulo Theories)
1.7_2 math 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 1.7Version of this port present on the latest quarterly branch.
Maintainer: greg@unrelenting.technology search for ports maintained by this maintainer
Port Added: 2018-06-21 11:06:27
Last Update: 2019-08-19 16:35:28
SVN Revision: 509290
Also Listed In: java
License: GPLv3
Description:
SVNWeb : Homepage
pkg-plist: as obtained via: make generate-plist
Expand this list (116 items)
  1. /usr/local/share/licenses/cvc4-1.7_2/catalog.mk
  2. /usr/local/share/licenses/cvc4-1.7_2/LICENSE
  3. /usr/local/share/licenses/cvc4-1.7_2/GPLv3
  4. bin/cvc4
  5. bin/pcvc4
  6. include/cvc4/api/cvc4cpp.h
  7. include/cvc4/api/cvc4cppkind.h
  8. include/cvc4/base/configuration.h
  9. include/cvc4/base/exception.h
  10. include/cvc4/base/listener.h
  11. include/cvc4/base/modal_exception.h
  12. include/cvc4/context/cdhashmap_forward.h
  13. include/cvc4/context/cdhashset_forward.h
  14. include/cvc4/context/cdinsert_hashmap_forward.h
  15. include/cvc4/context/cdlist_forward.h
  16. include/cvc4/cvc4.h
  17. include/cvc4/cvc4_public.h
  18. include/cvc4/cvc4parser_public.h
  19. include/cvc4/expr/array.h
  20. include/cvc4/expr/array_store_all.h
  21. include/cvc4/expr/ascription_type.h
  22. include/cvc4/expr/chain.h
  23. include/cvc4/expr/datatype.h
  24. include/cvc4/expr/emptyset.h
  25. include/cvc4/expr/expr.h
  26. include/cvc4/expr/expr_iomanip.h
  27. include/cvc4/expr/expr_manager.h
  28. include/cvc4/expr/expr_stream.h
  29. include/cvc4/expr/kind.h
  30. include/cvc4/expr/pickler.h
  31. include/cvc4/expr/record.h
  32. include/cvc4/expr/symbol_table.h
  33. include/cvc4/expr/type.h
  34. include/cvc4/expr/uninterpreted_constant.h
  35. include/cvc4/expr/variable_type_map.h
  36. include/cvc4/options/argument_extender.h
  37. include/cvc4/options/arith_heuristic_pivot_rule.h
  38. include/cvc4/options/arith_propagation_mode.h
  39. include/cvc4/options/arith_unate_lemma_mode.h
  40. include/cvc4/options/datatypes_modes.h
  41. include/cvc4/options/language.h
  42. include/cvc4/options/option_exception.h
  43. include/cvc4/options/options.h
  44. include/cvc4/options/printer_modes.h
  45. include/cvc4/options/quantifiers_modes.h
  46. include/cvc4/options/set_language.h
  47. include/cvc4/options/smt_modes.h
  48. include/cvc4/options/sygus_out_mode.h
  49. include/cvc4/options/theoryof_mode.h
  50. include/cvc4/parser/input.h
  51. include/cvc4/parser/parser.h
  52. include/cvc4/parser/parser_builder.h
  53. include/cvc4/parser/parser_exception.h
  54. include/cvc4/printer/sygus_print_callback.h
  55. include/cvc4/proof/unsat_core.h
  56. include/cvc4/smt/command.h
  57. include/cvc4/smt/logic_exception.h
  58. include/cvc4/smt/smt_engine.h
  59. include/cvc4/smt_util/lemma_channels.h
  60. include/cvc4/smt_util/lemma_input_channel.h
  61. include/cvc4/smt_util/lemma_output_channel.h
  62. include/cvc4/theory/logic_info.h
  63. include/cvc4/util/abstract_value.h
  64. include/cvc4/util/bitvector.h
  65. include/cvc4/util/bool.h
  66. include/cvc4/util/cardinality.h
  67. include/cvc4/util/channel.h
  68. include/cvc4/util/divisible.h
  69. include/cvc4/util/floatingpoint.h
  70. include/cvc4/util/gmp_util.h
  71. include/cvc4/util/hash.h
  72. include/cvc4/util/integer.h
  73. include/cvc4/util/integer_cln_imp.h
  74. include/cvc4/util/integer_gmp_imp.h
  75. include/cvc4/util/maybe.h
  76. include/cvc4/util/proof.h
  77. include/cvc4/util/rational.h
  78. include/cvc4/util/rational_cln_imp.h
  79. include/cvc4/util/rational_gmp_imp.h
  80. include/cvc4/util/regexp.h
  81. include/cvc4/util/resource_manager.h
  82. include/cvc4/util/result.h
  83. include/cvc4/util/sexpr.h
  84. include/cvc4/util/statistics.h
  85. include/cvc4/util/tuple.h
  86. include/cvc4/util/unsafe_interrupt_exception.h
  87. lib/libcvc4.so
  88. lib/libcvc4.so.6
  89. lib/libcvc4jni.so
  90. lib/libcvc4parser.so
  91. lib/libcvc4parser.so.6
  92. lib/python3.6/site-packages/CVC4.py
  93. lib/python3.6/site-packages/_CVC4.so
  94. share/cvc4/drat.plf
  95. share/cvc4/er.plf
  96. share/cvc4/lrat.plf
  97. share/cvc4/sat.plf
  98. share/cvc4/smt.plf
  99. share/cvc4/th_arrays.plf
  100. share/cvc4/th_base.plf
  101. share/cvc4/th_bv.plf
  102. share/cvc4/th_bv_bitblast.plf
  103. share/cvc4/th_bv_rewrites.plf
  104. share/cvc4/th_int.plf
  105. share/cvc4/th_real.plf
  106. share/java/cvc4/CVC4-1.7.0.jar
  107. share/java/cvc4/CVC4.jar
  108. man/man1/cvc4.1.gz
  109. man/man1/pcvc4.1.gz
  110. man/man3/SmtEngine.3cvc.gz
  111. man/man3/libcvc4.3.gz
  112. man/man3/libcvc4parser.3.gz
  113. man/man3/options.3cvc.gz
  114. man/man5/cvc4.5.gz
  115. @postexec /usr/sbin/service ldconfig restart > /dev/null
  116. @postunexec /usr/sbin/service ldconfig restart > /dev/null
Collapse this list.
Dependency lines:
  • cvc4>0:math/cvc4
To install the port: cd /usr/ports/math/cvc4/ && make install clean
To add the package: pkg install cvc4
PKGNAME: cvc4
Flavors: there is no flavor information for this port.
distinfo:

Dependencies
NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
Build dependencies:
  1. bash : shells/bash
  2. swig3.0 : devel/swig30
  3. swig3.0 : devel/swig30
  4. java : java/openjdk8
  5. cmake : devel/cmake
  6. ninja : devel/ninja
  7. pkgconf>=1.3.0_1 : devel/pkgconf
  8. python3.6 : lang/python36
Library dependencies:
  1. libantlr3c.so : devel/libantlr3c
  2. libboost_system.so : devel/boost-libs
  3. libcryptominisat5.so : math/cryptominisat
  4. libgmp.so : math/gmp
  5. libboost_thread.so : devel/boost-libs
  6. libreadline.so.8 : devel/readline
This port is required by:
for Libraries
  1. lang/maude
  2. lang/solidity

Configuration Options

USES:

Master Sites:
  1. https://codeload.github.com/CVC4/CVC4/tar.gz/1.7?dummy=/

Number of commits found: 14

Commit History - (may be incomplete: see SVNWeb link above for full details)
DateByDescription
19 Aug 2019 15:35:28
Original commit files touched by this commit  1.7_2
Revision:509290
jbeich search for other commits by this committer
devel/boost-*: update to 1.71.0

Changes:	http://www.boost.org/users/history/version_1_71_0.html
PR:		238827
Exp-run by:	antoine
Differential Revision:	https://reviews.freebsd.org/D20774
06 Aug 2019 17:36:37
Original commit files touched by this commit  1.7_1
Revision:508264
fernape search for other commits by this committer
math/cvc4: simplify post-patch

* Bump PORTREVISION
* Unbreak lang/maude and lang/solidity (broken in r508058 and r508059)

Reported by:	jbeich@
Reviewed by:	jbeich@
Differential Revision:	https://reviews.freebsd.org/D21170
05 Aug 2019 16:59:26
Original commit files touched by this commit  1.7
Revision:508195
fernape search for other commits by this committer
math/cvc4: Fix headers

Fix headers so other programs can include them safely.

This unbreaks lang/maude and lang/solidity

PR:	238376
Reported by:	jbeich@
01 Aug 2019 15:20:28
Original commit files touched by this commit  1.7
Revision:507774
fernape search for other commits by this committer
math/cvc4: update to 1.7

ChangeLog:

https://github.com/CVC4/CVC4/releases/tag/1.7

* New Features:
    Proofs:
        Support for bit-vector proofs with eager bitblasting
    Strings:
        Support for str.replaceall operator.
        New option --re-elim
    SyGuS:
        Support for abduction (--sygus-abduct)

* Improvements:
    Strings:
        Significantly better performance

* Changes:
    API change: Expr::iffExpr() is renamed to Expr::eqExpr()
    Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
    The CVC3 compatibility layer has been removed.
    The build system now uses CMake instead of Autotools
26 Jul 2019 20:46:57
Original commit files touched by this commit  1.6_5
Revision:507372
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
27 May 2019 10:10:15
Original commit files touched by this commit  1.6_4
Revision:502779
tobik search for other commits by this committer
math/cvc4: Remove llvm60 build dependency

It was added for FreeBSD 10.x/i386 and is no longer needed.

PR:		238162
Approved by:	greg@unrelenting.technology (maintainer)
12 Apr 2019 06:36:31
Original commit files touched by this commit  1.6_4
Revision:498698
jbeich search for other commits by this committer
devel/boost-*: update to 1.70.0

Changes:	http://www.boost.org/users/history/version_1_70_0.html
PR:		235956
Exp-run by:	antoine
Differential Revision:	https://reviews.freebsd.org/D19303
09 Apr 2019 14:04:50
Original commit files touched by this commit  1.6_3
Revision:498476
sunpoet search for other commits by this committer
Update devel/readline to 8.0

- Bump PORTREVISION of dependent ports for shlib change

Changes:	https://tiswww.case.edu/php/chet/readline/CHANGES
PR:		236156
Exp-run by:	antoine
12 Dec 2018 00:15:50
Original commit files touched by this commit  1.6_2
Revision:487266
jbeich search for other commits by this committer
devel/boost-*: update to 1.69.0

Changes:	http://www.boost.org/users/history/version_1_69_0.html
PR:		232525
Exp-run by:	antoine
Differential Revision:	https://reviews.freebsd.org/D17645
09 Aug 2018 06:58:31
Original commit files touched by this commit  1.6_1
Revision:476723
jbeich search for other commits by this committer
devel/boost-*: update to 1.68.0

- Switch to C++14 for libboost_system to support C++14 consumers

Changes:	http://www.boost.org/users/history/version_1_68_0.html
PR:		229569
Exp-run by:	antoine
Differential Revision:	https://reviews.freebsd.org/D16165
23 Jul 2018 18:51:55
Original commit files touched by this commit  1.6
Revision:475198
yuri search for other commits by this committer
math/cvc4: Fix the warning in 'make describe'

Remove USES=compiler as it conflicts with the explicit compiler setting.

PR:		229987
Reported by:	Yasuhiro KIMURA <yasu@utahime.org>
22 Jul 2018 18:30:29
Original commit files touched by this commit  1.6
Revision:475115
yuri search for other commits by this committer
math/cvc4: Update 1.5 -> 1.6

Port changes:
* Add dependency on cryptominisat, and the corresponding port option
* Add USES=autoreconf, the suplied configure fails, see
https://github.com/CVC4/CVC4/issues/2192
* Now build depends on python
* Force clang-60 to prevent build failures on 10

PR:		229780
Submitted by:	Greg V <greg@unrelenting.technology>
08 Jul 2018 15:29:19
Original commit files touched by this commit  1.5
Revision:474182
swills search for other commits by this committer
math/cvc4: switch to GMP by default

This unbreaks aarch64 and enables parallel mode

PR:		229585
Submitted by:	Greg V <greg@unrelenting.technology> (maintainer)
21 Jun 2018 11:06:10
Original commit files touched by this commit  1.5
Revision:472970
pi search for other commits by this committer
New port: math/cvc4

An efficient open-source 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.

WWW: https://cvc4.cs.stanford.edu/web/

PR:		227702
Submitted by:	Greg V <greg@unrelenting.technology>

Number of commits found: 14

Login
User Login
Create account

Servers and bandwidth provided by
New York Internet, iXsystems, and RootBSD

This site
What is FreshPorts?
About the authors
Issues
FAQ
How big is it?
The latest upgrade!
Privacy
Forums
Blog
Contact

Search
Enter Keywords:
 
more...

Latest Vulnerabilities
mod_perl2Oct 09
xpdfOct 06
xpdf3Oct 06
xpdf4Oct 06
unboundOct 03
cactiOct 02
gitlab-ceOct 02
gitlab-ceOct 02
ruby24Oct 02
ruby25Oct 02
mongodb34Sep 30
mongodb34Sep 30
mongodb36Sep 30
mongodb36Sep 30
mongodb40Sep 30

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

* - modified, not new

All vulnerabilities

Last updated:
2019-10-11 18:37:07


Ports
Home
Categories
Deleted ports
Sanity Test Failures
Newsfeeds

Statistics
Graphs
NEW Graphs (Javascript)
Traffic

Calculated hourly:
Port count 37991
Broken 399
Deprecated 443
Ignore 665
Forbidden 3
Restricted 160
No CDROM 74
Vulnerable 29
Expired 6
Set to expire 414
Interactive 0
new 24 hours 3
new 48 hours9
new 7 days27
new fortnight89
new month229

Servers and bandwidth provided by
New York Internet, iXsystems, and RootBSD
Valid HTML, CSS, and RSS.
Copyright © 2000-2019 Dan Langille. All rights reserved.