BSD Ports

math/cvc5 1.4.0 NetBSD

Automatic theorem prover for SMT (Satisfiability Modulo Theories)

System
NetBSD
Repository
pkgsrc
Maintainer
[email protected]
Port added
Last update
Commit
fe10662b9d
License
modified-bsd
Categories
math
Package size
7355.4 KiB, 30372.3 KiB installed

Description

An efficient open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the satisfiability (or, dually, the validity) of first-order formulas with respect to (combinations of) a variety of useful background theories.

In the other systems

SystemPortVersion
NetBSDmath/cvc51.4.0
FreeBSDmath/cvc51.4.2
DragonFlymath/cvc51.2.1

Install

Binary package:

pkgin install cvc5

From pkgsrc:

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

Dependencies

Run dependencies 5

No port depends on this one.

Commit history 6

DateCommitCreditsLog message
fe10662b9d alnsn Update math/cvc5 to version 1.4.0.
## Changes - We now require GCC >= 10 and Clang >= 12. - Update SymFPU. Issue with divider encoding now fixed in SymFPU (related issues: #9505, #11139, #12335). - Fixes parsing issues related to unchecked overflowing of indexed bit-vector operators. This impacts bit-vector operators having width that is greater than or equal to `2^32`. - Fixes a bug where the character code point `\u{30000}` was incorrectly treated as a valid code point. - Fixes a parsing bug with option `--parse-skolem-definitions`. - Fixes a soundness bug in the `--learned-rewrite` preprocessing pass. - We now allow using option `--solve-bv-as-int` with quantifiers, even if the quantified variables occur under UFs. - Fixes an issue where the parser would abort prematurely when `get-value` was …
d4b45077d2 alnsn math/cadical is build-only dep, bump pkgrev.
a24ae002b7 alnsn TEST_TARGET=check is better.
67ebdac846 alnsn Pass LD_LIBRARY_PATH to TEST_ENV.
cac7e33f76 alnsn Add LD_LIBRARY_PATH to testing instruction.
This improves success rate to 99%. $ export LD_LIBRARY_PATH=$(pwd)/src:$(pwd)/src/parser:$(pwd)/src/main $ ctest -j32 ... 99% tests passed, 1 tests failed out of 4291 Label Time Summary: api capi = 0.18 sec*proc (7 tests) api cppapi = 4.69 sec*proc (70 tests) regress0 = 815.38 sec*proc (2540 tests) regress1 = 709.94 sec*proc (1468 tests) regress2 = 211.87 sec*proc (145 tests) regress3 = 1082.17 sec*proc (51 tests) regress4 = 663.37 sec*proc (10 tests) Total Test time (real) = 347.30 sec The following tests did not run: ... 52 skipped regress0 tests ... The following tests FAILED: 4157 - regress3/bags/reduce_constants_dup.smt2 (Failed) regress3

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