head 1.7; access; symbols pkgsrc-2026Q3:1.6.0.2 pkgsrc-2026Q3-base:1.6; locks; strict; comment @# @; 1.7 date 2026.11.08.14.00.44; author alnsn; state Exp; branches; next 1.6; commitid pGHs9WKEIrMzbF2H; 1.6 date 2026.09.18.22.07.57; author alnsn; state Exp; branches; next 1.5; commitid uqyZYPEWAPCCv9WG; 1.5 date 2026.07.25.18.58.36; author alnsn; state Exp; branches; next 1.4; commitid ANoo1rAJXNbif4PG; 1.4 date 2026.07.03.22.03.50; author alnsn; state Exp; branches; next 1.3; commitid uhy8aJBs1lwGYfMG; 1.3 date 2026.07.03.20.36.34; author alnsn; state Exp; branches; next 1.2; commitid UCcOTNnplQZJufMG; 1.2 date 2026.07.02.23.52.13; author alnsn; state Exp; branches; next 1.1; commitid vfywKXYOh215y8MG; 1.1 date 2026.07.02.23.20.47; author alnsn; state Exp; branches; next ; commitid LgXNqbK6t0xIq8MG; desc @@ 1.7 log @Revbump after adding pkg-config files to symfpu and cadical. Not strictly necessary because cvc5 doesn't use pkg-config. @ text @# $NetBSD: Makefile,v 1.6 2026/09/18 22:07:57 alnsn Exp $ DISTNAME= cvc5-1.4.0 PKGREVISION= 1 CATEGORIES= math MASTER_SITES= ${MASTER_SITE_GITHUB:=cvc5/} GITHUB_TAG= cvc5-${PKGVERSION_NOREV} MAINTAINER= pkgsrc-users@@NetBSD.org HOMEPAGE= https://cvc5.github.io/ COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories) LICENSE= modified-bsd USE_TOOLS+= git USE_LANGUAGES= c c++ CMAKE_CONFIGURE_ARGS+= -DCMAKE_BUILD_TYPE=Production CMAKE_CONFIGURE_ARGS+= -DCMAKE_PREFIX_PATH=${PREFIX} CMAKE_CONFIGURE_ARGS+= -DBUILD_SHARED_LIBS=ON CMAKE_CONFIGURE_ARGS+= -DUSE_PYTHON_VENV=OFF CMAKE_CONFIGURE_ARGS+= -DUSE_POLY=ON CMAKE_CONFIGURE_ARGS+= -DUSE_MPFR=ON DEPENDS+= ${PYPKGPREFIX}-pyparsing>=3.0.9:../../devel/py-pyparsing BUILDLINK_DEPMETHOD.cadical= build TEST_TARGET= check CVC5_BUILD_SRC= ${WRKSRC}/${CMAKE_BUILD_DIR}/src TEST_ENV+= LD_LIBRARY_PATH=${CVC5_BUILD_SRC}:${CVC5_BUILD_SRC}/parser:${CVC5_BUILD_SRC}/main .include "../../devel/cmake/build.mk" .include "../../lang/python/tool.mk" .include "../../devel/gmp/buildlink3.mk" .include "../../math/cadical/buildlink3.mk" .include "../../math/libpoly/buildlink3.mk" .include "../../math/mpfr/buildlink3.mk" .include "../../math/symfpu/buildlink3.mk" .include "../../mk/bsd.pkg.mk" @ 1.6 log @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 called after an unsat response when uninterpreted sorts are present. - Fixes issues related to theory combination with arrays and non-linear arithmetic. - Added full proof support in CaDiCaL, meaning `--sat-solver=cadical` can now be used in combination with proofs `--produce-proofs`. - Improved proof support for Alethe: full translation for CPC fragment for logics in AUFNIRA. - Minor updates and fixes to the CPC proof signature. The current CPC proofs are checkable by Ethos 0.2.3 (`./contrib/get-ethos-checker`). -- View it on GitHub: https://github.com/cvc5/cvc5/releases/tag/cvc5-1.4.0 @ text @d1 1 a1 1 # $NetBSD: Makefile,v 1.5 2026/07/25 18:58:36 alnsn Exp $ d4 1 @ 1.5 log @math/cadical is build-only dep, bump pkgrev. @ text @d1 1 a1 1 # $NetBSD: Makefile,v 1.4 2026/07/03 22:03:50 alnsn Exp $ d3 1 a3 2 DISTNAME= cvc5-1.3.4 PKGREVISION= 1 d21 1 d36 1 @ 1.4 log @TEST_TARGET=check is better. @ text @d1 1 a1 1 # $NetBSD: Makefile,v 1.3 2026/07/03 20:36:34 alnsn Exp $ d4 1 d25 2 @ 1.3 log @Pass LD_LIBRARY_PATH to TEST_ENV. @ text @d1 1 a1 1 # $NetBSD: Makefile,v 1.2 2026/07/02 23:52:13 alnsn Exp $ d24 1 a24 1 TEST_TARGET= test @ 1.2 log @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 @ text @d1 1 a1 1 # $NetBSD: Makefile,v 1.1 2026/07/02 23:20:47 alnsn Exp $ d24 3 a26 8 # Tests take a long time to finish, you can instead # run them inside a sandboxed shell and pass -j N: # make build-env # cd cmake-pkgsrc-build # export LD_LIBRARY_PATH=$(pwd)/src:$(pwd)/src/parser:$(pwd)/src/main # ctest -j 32 # ^D #TEST_TARGET= test @ 1.1 log @Initial import of math/cvc5 version 1.3.4. 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. @ text @d1 1 a1 1 # $NetBSD$ a25 1 # make install d27 3 a29 1 # cd cmake-pkgsrc-build && ctest -j 32 @