./math/yices2, Yices 2 SMT solver

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 2.6.1, Package name: yices2-2.6.1, Maintainer: pkgsrc-users

Yices 2 is an SMT solver that decides the satisfiability of formulas
containing uninterpreted function symbols with equality, real and
integer arithmetic, bitvectors, scalar types, and tuples. Yices 2
supports both linear and nonlinear arithmetic.

Yices 2 can process input written in the SMT-LIB notation (both
versions 2.0 and 1.2 are supported). Alternatively, you can write
specifications using Yices 2's own specification language, which
includes tuples and scalar types. You can also use Yices 2 as a
library in your software.


Required to run:
[devel/gmp]

Required to build:
[devel/gperf] [pkgtools/cwrappers]

Master sites:

Filesize: 8695.067 KB

Version history: (Expand)

CVS history: (Expand)


   2023-06-06 14:42:56 by Taylor R Campbell | Files touched by this commit (1319) 
Log message:
Mass-change BUILD_DEPENDS to TOOL_DEPENDS outside mk/.

Almost all uses, if not all of them, are wrong, according to the
semantics of BUILD_DEPENDS (packages built for target available for
use _by_ tools at build-time) and TOOL_DEPEPNDS (packages built for
host available for use _as_ tools at build-time).

No change to BUILD_DEPENDS as used correctly inside buildlink3.

As proposed on tech-pkg:
https://mail-index.netbsd.org/tech-pkg/2023/06/03/msg027632.html
   2021-10-26 12:56:13 by Nia Alarie | Files touched by this commit (458) 
Log message:
math: Replace RMD160 checksums with BLAKE2s checksums

All checksums have been double-checked against existing RMD160 and
SHA512 hashes
   2021-10-07 16:28:36 by Nia Alarie | Files touched by this commit (458) 
Log message:
math: Remove SHA1 hashes for distfiles
   2020-07-13 21:45:45 by Alexander Nasonov | Files touched by this commit (8) 
Log message:
Reset maintainership for all (no longer) mine packages
   2019-11-02 17:16:23 by Roland Illig | Files touched by this commit (47) 
Log message:
math: align variable assignments

pkglint -Wall -F --only aligned -r

Manual correction in R/Makefile.extension for the MASTER_SITES
continuation line.
   2019-08-26 23:11:28 by Alexander Nasonov | Files touched by this commit (1) 
Log message:
Add TEST_TARGET.

Current score on -current amd64: Pass: 861, Fail: 171.
   2019-08-25 00:14:13 by Alexander Nasonov | Files touched by this commit (1) 
Log message:
Make pkglint happy.
   2019-08-25 00:09:16 by Alexander Nasonov | Files touched by this commit (10) | Imported package
Log message:
Initial import of Yices 2, version 2.6.1.

Yices 2 is an SMT solver that decides the satisfiability of formulas
containing uninterpreted function symbols with equality, real and
integer arithmetic, bitvectors, scalar types, and tuples. Yices 2
supports both linear and nonlinear arithmetic.
                                                                                 \ 
                                       Yices 2 can process input written in the \ 
SMT-LIB notation (both
versions 2.0 and 1.2 are supported). Alternatively, you can write
specifications using Yices 2's own specification language, which
includes tuples and scalar types. You can also use Yices 2 as a
library in your software.