notbugAs an Amazon Associate I earn from qualifying purchases.
Want a good read? Try FreeBSD Mastery: Jails (IT Mastery Book 15)

/commits.php is going away

I'm proposing to take /commits.php away - it mainly duplicates the home page. Details in this GitHub issue.
Port details
cvc4 Automatic theorem prover for SMT (Satisfiability Modulo Theories)
1.7_4 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 View this port on Repology. pkg-fallout 1.7_4Version 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: 2021-05-15 07:14:04
Commit Hash: 9671981
Also Listed In: java
License: GPLv3
Description:
SVNWeb : git : Homepage
pkg-plist: as obtained via: make generate-plist
Expand this list (118 items)
Collapse this list.
  1. @ldconfig
  2. /usr/local/share/licenses/cvc4-1.7_4/catalog.mk
  3. /usr/local/share/licenses/cvc4-1.7_4/LICENSE
  4. /usr/local/share/licenses/cvc4-1.7_4/GPLv3
  5. bin/cvc4
  6. bin/pcvc4
  7. include/cvc4/api/cvc4cpp.h
  8. include/cvc4/api/cvc4cppkind.h
  9. include/cvc4/base/configuration.h
  10. include/cvc4/base/exception.h
  11. include/cvc4/base/listener.h
  12. include/cvc4/base/modal_exception.h
  13. include/cvc4/context/cdhashmap_forward.h
  14. include/cvc4/context/cdhashset_forward.h
  15. include/cvc4/context/cdinsert_hashmap_forward.h
  16. include/cvc4/context/cdlist_forward.h
  17. include/cvc4/cvc4.h
  18. include/cvc4/cvc4_public.h
  19. include/cvc4/cvc4parser_public.h
  20. include/cvc4/expr/array.h
  21. include/cvc4/expr/array_store_all.h
  22. include/cvc4/expr/ascription_type.h
  23. include/cvc4/expr/chain.h
  24. include/cvc4/expr/datatype.h
  25. include/cvc4/expr/emptyset.h
  26. include/cvc4/expr/expr.h
  27. include/cvc4/expr/expr_iomanip.h
  28. include/cvc4/expr/expr_manager.h
  29. include/cvc4/expr/expr_stream.h
  30. include/cvc4/expr/kind.h
  31. include/cvc4/expr/pickler.h
  32. include/cvc4/expr/record.h
  33. include/cvc4/expr/symbol_table.h
  34. include/cvc4/expr/type.h
  35. include/cvc4/expr/uninterpreted_constant.h
  36. include/cvc4/expr/variable_type_map.h
  37. include/cvc4/options/argument_extender.h
  38. include/cvc4/options/arith_heuristic_pivot_rule.h
  39. include/cvc4/options/arith_propagation_mode.h
  40. include/cvc4/options/arith_unate_lemma_mode.h
  41. include/cvc4/options/datatypes_modes.h
  42. include/cvc4/options/language.h
  43. include/cvc4/options/option_exception.h
  44. include/cvc4/options/options.h
  45. include/cvc4/options/printer_modes.h
  46. include/cvc4/options/quantifiers_modes.h
  47. include/cvc4/options/set_language.h
  48. include/cvc4/options/smt_modes.h
  49. include/cvc4/options/sygus_out_mode.h
  50. include/cvc4/options/theoryof_mode.h
  51. include/cvc4/parser/input.h
  52. include/cvc4/parser/parser.h
  53. include/cvc4/parser/parser_builder.h
  54. include/cvc4/parser/parser_exception.h
  55. include/cvc4/printer/sygus_print_callback.h
  56. include/cvc4/proof/unsat_core.h
  57. include/cvc4/smt/command.h
  58. include/cvc4/smt/logic_exception.h
  59. include/cvc4/smt/smt_engine.h
  60. include/cvc4/smt_util/lemma_channels.h
  61. include/cvc4/smt_util/lemma_input_channel.h
  62. include/cvc4/smt_util/lemma_output_channel.h
  63. include/cvc4/theory/logic_info.h
  64. include/cvc4/util/abstract_value.h
  65. include/cvc4/util/bitvector.h
  66. include/cvc4/util/bool.h
  67. include/cvc4/util/cardinality.h
  68. include/cvc4/util/channel.h
  69. include/cvc4/util/divisible.h
  70. include/cvc4/util/floatingpoint.h
  71. include/cvc4/util/gmp_util.h
  72. include/cvc4/util/hash.h
  73. include/cvc4/util/integer.h
  74. include/cvc4/util/integer_cln_imp.h
  75. include/cvc4/util/integer_gmp_imp.h
  76. include/cvc4/util/maybe.h
  77. include/cvc4/util/proof.h
  78. include/cvc4/util/rational.h
  79. include/cvc4/util/rational_cln_imp.h
  80. include/cvc4/util/rational_gmp_imp.h
  81. include/cvc4/util/regexp.h
  82. include/cvc4/util/resource_manager.h
  83. include/cvc4/util/result.h
  84. include/cvc4/util/sexpr.h
  85. include/cvc4/util/statistics.h
  86. include/cvc4/util/tuple.h
  87. include/cvc4/util/unsafe_interrupt_exception.h
  88. lib/libcvc4.so
  89. lib/libcvc4.so.6
  90. lib/libcvc4jni.so
  91. lib/libcvc4parser.so
  92. lib/libcvc4parser.so.6
  93. lib/python3.8/site-packages/CVC4.py
  94. lib/python3.8/site-packages/_CVC4.so
  95. share/cvc4/drat.plf
  96. share/cvc4/er.plf
  97. share/cvc4/lrat.plf
  98. share/cvc4/sat.plf
  99. share/cvc4/smt.plf
  100. share/cvc4/th_arrays.plf
  101. share/cvc4/th_base.plf
  102. share/cvc4/th_bv.plf
  103. share/cvc4/th_bv_bitblast.plf
  104. share/cvc4/th_bv_rewrites.plf
  105. share/cvc4/th_int.plf
  106. share/cvc4/th_real.plf
  107. share/java/cvc4/CVC4-1.7.0.jar
  108. share/java/cvc4/CVC4.jar
  109. man/man1/cvc4.1.gz
  110. man/man1/pcvc4.1.gz
  111. man/man3/SmtEngine.3cvc.gz
  112. man/man3/libcvc4.3.gz
  113. man/man3/libcvc4parser.3.gz
  114. man/man3/options.3cvc.gz
  115. man/man5/cvc4.5.gz
  116. @owner
  117. @group
  118. @mode
Collapse this list.
Dependency lines:
  • For RUN/BUILD depends:
    • cvc4>0:math/cvc4
  • For LIB depends:
    • libcvc4.so:math/cvc4
    • libcvc4jni.so:math/cvc4
    • libcvc4parser.so:math/cvc4
To install the port: cd /usr/ports/math/cvc4/ && make install clean
To add the package, run one of these commands:
  • pkg install math/cvc4
  • pkg install cvc4
PKGNAME: cvc4
Flavors: there is no flavor information for this port.
distinfo:
Packages (timestamps in pop-ups are UTC):
cvc4
ABIlatestquarterly
FreeBSD:11:aarch641.6_11.7_3
FreeBSD:11:amd641.7_41.7_4
FreeBSD:11:armv6-1.7_3
FreeBSD:11:i3861.7_41.7_4
FreeBSD:11:mips--
FreeBSD:11:mips64--
FreeBSD:12:aarch641.6_11.7_4
FreeBSD:12:amd641.7_41.7_4
FreeBSD:12:armv61.6_1-
FreeBSD:12:armv71.6_1-
FreeBSD:12:i3861.7_41.7_4
FreeBSD:12:mips--
FreeBSD:12:mips64--
FreeBSD:12:powerpc64-1.7_4
FreeBSD:13:aarch641.7_41.7_4
FreeBSD:13:amd641.7_41.7_4
FreeBSD:13:armv6--
FreeBSD:13:armv7--
FreeBSD:13:i3861.7_41.7_4
FreeBSD:13:mips--
FreeBSD:13:mips64--
FreeBSD:13:powerpc64-1.7_4
FreeBSD:14:aarch641.7_4-
FreeBSD:14:amd641.7_4-
FreeBSD:14:armv6--
FreeBSD:14:armv7--
FreeBSD:14:i3861.7_4-
FreeBSD:14:mips--
FreeBSD:14:mips64--
FreeBSD:14:powerpc641.7_4-
 

Dependencies
NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
Build dependencies:
  1. bash : shells/bash
  2. swig : devel/swig
  3. swig : devel/swig
  4. java : java/openjdk8
  5. cmake : devel/cmake
  6. ninja : devel/ninja
  7. pkgconf>=1.3.0_1 : devel/pkgconf
  8. python3.8 : lang/python38
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:
Options name:

USES:

FreshPorts was unable to extract/find any pkg message
Master Sites:
Expand this list (1 items)
Collapse this list.
  1. https://codeload.github.com/CVC4/CVC4/tar.gz/1.7?dummy=/
Collapse this list.

Number of commits found: 21

Commit History - (may be incomplete: see SVNWeb link above for full details)
DateByDescription
15 May 2021 07:14:04
 files touched by this commit commit hash:9671981826f7ef8b1e7fb0a430ee24d4a1f0acf2  1.7_4
tobik search for other commits by this committer
*: Remove unnecessary 'port' argument from USES=readline

PR:		248459
Exp-run by:	antoine
07 Apr 2021 08:09:01
 files touched by this commit commit hash:cf118ccf875508b9a1c570044c93cfcc82bd455c  1.7_4
mat search for other commits by this committer
One more small cleanup, forgotten yesterday.
Reported by:	lwhsu
06 Apr 2021 14:31:07
 files touched by this commit commit hash:305f148f482daf30dcf728039d03d019f88344eb  1.7_4
mat search for other commits by this committer
Remove # $FreeBSD$ from Makefiles.
09 Jul 2020 15:44:39
Original commit files touched by this commit Revision:541757  1.7_4
arrowd search for other commits by this committer
math/cryptominisat and math/py-cryptominisat: Update to 5.7.1

Bump PORTREVISIONs of consumer ports.
17 Jun 2020 18:17:45
Original commit files touched by this commit Revision:539491  1.7_3
sunpoet search for other commits by this committer
Move devel/swig30 to devel/swig and update to 4.0.1

- Do not silence installation message
- Update dependent ports:
  - Fix build with swig 4.0.1
  - Update *_DEPENDS
  - Remove BINARY_ALIAS

Changes:	http://www.swig.org/news.php
PR:		246613
Exp-run by:	antoine
11 Dec 2019 17:53:49
Original commit files touched by this commit Revision:519824  1.7_3
jbeich search for other commits by this committer
devel/boost-*: update to 1.72.0

Changes:	http://www.boost.org/users/history/version_1_72_0.html
PR:		241449
Exp-run by:	antoine
Differential Revision:	https://reviews.freebsd.org/D22136
26 Nov 2019 21:46:13
Original commit files touched by this commit Revision:518482  1.7_2
jkim search for other commits by this committer
Clean up after java/openjdk6 and java/openjdk6-jre removal

java/openjdk6 support was removed from Mk/bsd.java.mk (r512662) and
java/openjdk6 and java/openjdk6-jre were removed from the ports tree
(r512663).  Now this patch completely removes remaining stuff from the
ports tree.

PR:			241953 (exp-run)
Reviewed by:		glewis
Approved by:		portmgr (antoine)
Differential Revision:	https://reviews.freebsd.org/D22342
19 Aug 2019 15:35:28
Original commit files touched by this commit Revision:509290  1.7_2
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 Revision:508264  1.7_1
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 Revision:508195  1.7
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 Revision:507774  1.7
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 Revision:507372  1.6_5
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 Revision:502779  1.6_4
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 Revision:498698  1.6_4
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 Revision:498476  1.6_3
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 Revision:487266  1.6_2
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 Revision:476723  1.6_1
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 Revision:475198  1.6
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 Revision:475115  1.6
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 Revision:474182  1.5
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 Revision:472970  1.5
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: 21