FreeBSD Ports

math/cvc5 1.4.2

Automatic theorem prover for SMT (Satisfiability Modulo Theories)

Repository
FreeBSD ports
Maintainer
[email protected]
Last update
Commit
7068c01f29
License
BSD3CLAUSE
Categories
math, java
Package size
6763.6 KiB, 24521.1 KiB installed

Description

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.

Install

As a binary package — by origin, or by package name:

pkg install math/cvc5
pkg install cvc5

From the ports tree:

cd /usr/ports/math/cvc5/ && make install clean

To depend on this port in another port's Makefile:

RUN_DEPENDS=	cvc5>0:math/cvc5
LIB_DEPENDS=	libcvc5.so:math/cvc5

Packages

The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.

Repositoryaarch64amd64armv6armv7i386
FreeBSD:14:latest1.4.11.4.2-1.3.01.4.2
FreeBSD:14:quarterly1.4.11.4.1n/a1.3.01.4.1
FreeBSD:15:latest1.4.21.4.2n/a1.3.01.3.0
FreeBSD:15:quarterly1.4.11.4.1n/an/an/a
FreeBSD:16:latest1.4.11.4.2n/an/an/a
FreeBSD:16:quarterlyn/an/an/an/an/a

Dependencies

As this port's Makefile names them.

Build 4

Library 1

Test 1

The full lists below include those, and their dependencies in turn.

All build dependencies 77
All run dependencies 62
Required by 1

Configuration

Options name: math_cvc5

OptionDefaultDescription
CLNoffUse CLN numeric library
COCOALIBoffUse CoCoALib for further polynomial operations
CRYPTOMINISATonUse CryptoMiniSat as the SAT solver
EDITLINEonUse Editline for better interactive support
GLPKoffUse GLPK simplex solver
GMPonUse GMP numeric library
JAVAonJava platform support
KISSATonUse Kissat solver
POLYonUse LibPoly for polynomial arithmetic
USES
cmake:testing ncurses compiler:c++17-lang localbase:ldflags pkgconfig python:build
Service scripts
none

Files

pkg-plist 24
  • bin/cvc5
  • include/cvc5/c/cvc5.h
  • include/cvc5/c/cvc5_parser.h
  • include/cvc5/cvc5.h
  • include/cvc5/cvc5_export.h
  • include/cvc5/cvc5_kind.h
  • include/cvc5/cvc5_parser.h
  • include/cvc5/cvc5_proof_rule.h
  • include/cvc5/cvc5_skolem_id.h
  • include/cvc5/cvc5_types.h
  • lib/cmake/cvc5/cvc5Config.cmake
  • lib/cmake/cvc5/cvc5ConfigVersion.cmake
  • lib/cmake/cvc5/cvc5JavaTargets.cmake
  • lib/cmake/cvc5/cvc5Targets-.cmake
  • lib/cmake/cvc5/cvc5Targets.cmake
  • lib/libcvc5.so
  • lib/libcvc5.so.1
  • lib/libcvc5.so.
  • lib/libcvc5jni.so
  • lib/libcvc5parser.so
  • lib/libcvc5parser.so.1
  • lib/libcvc5parser.so.
  • %%JAVASHAREDIR%%/cvc5-.jar
  • %%JAVASHAREDIR%%/cvc5.jar
distinfo 1
FileSizeSHA256
cvc5-cvc5-cvc5-1.4.2_GH0.tar.gz8.992756e+06795099b277bfa79a3c9a11c8d3fec780452031dc89ddcc170003963aa3521343

Commit history 6

DateCommitCreditsLog message
7068c01f29 Yuri Victorovich math/cvc5: update 1.4.1 → 1.4.2
ChangeLog: https://github.com/cvc5/cvc5/releases/tag/cvc5-1.4.2
1f901efbd2 Yuri Victorovich math/cvc5: update 1.4.0 → 1.4.1
7f0bbeb5ed Yuri Victorovich math/cvc5: Fix plist when JAVA=OFF
PR: 280044 Reported by: [email protected]
2855ba8e2b Yuri Victorovich math/cvc5: update test results
All tests pass after the latest update of math/symfpu. The older version caused test failures.
1b17991da3 Yuri Victorovich math/cvc5: update 1.3.4 → 1.4.0

The latest 5 of 6 in the history this site was built from.