sci-mathematics / vampire

The Vampire Prover, theorem prover for first-order logic

Official package sites : https://github.com/vprover/vampire/ · https://vprover.github.io/ ·

Vampire is a theorem prover, that is, a system able to prove theorems — although now it can do much more! Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of theories, such as arithmetic, arrays, and datatypes, and with higher-order logic. The development of Vampire began in 1994 and has survived a number of rewritings.

v4.8 :: 0/4.8 :: gentoo

Modified
License
BSD
Keywords
~amd64 ~x86
USE flags
debug z3

General

debug
Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces
z3
Enable support for sci-mathematics/z3

dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers

sci-mathematics / z3 : An efficient theorem prover

dev-libs / gmp : Library for arbitrary-precision arithmetic on different type of numbers

sci-mathematics / z3 : An efficient theorem prover

928097
sci-mathematics/vampire-4.8 fails to compile: Portability.hpp:23:20: error: static assertion failed: Vampire assumes that the size of a pointer is 8 bytes for efficiency reasons This may be relaxed in future, but for the moment expect problems if running
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: drop old 4.7-r1
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: bump to 4.8
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Maciej Barć · gentoo
sci-mathematics/vampire: drop old 4.6.1-r2
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: fix build on musl
Bug: https://github.com/vprover/vampire/pull/432 Closes: https://bugs.gentoo.org/832834 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: depend on z3 version >=4.11.2
both vampire 4.6.1 and 4.7 build correctly with >=sci-mathematics/z3-4.11.2 Closes: https://bugs.gentoo.org/872512 Bug: https://bugs.gentoo.org/860237 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: filter LTO (strict-aliasing)
Closes: https://bugs.gentoo.org/863269 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: bump to 4.7
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Maciej Barć · gentoo
sci-mathematics/vampire: restrict z3 dep version
Closes: https://bugs.gentoo.org/860237 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/vampire: new package; add version 4.6.1
Package-Manager: Portage-3.0.28, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org>