gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

z3: remove all but 4.14

Browse Source 
Clean up this package set, since nothing depends on it now, and
deal-solver now appears to work fine.
This commit is contained in:
Morgan Jones
2025-04-23 00:26:16 -07:00
committed by Morgan Jones
parent fd15f0eb3c
commit 93bcaf1311
9 changed files with 138 additions and 285 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/applications/science/logic/z3/4-8-5-typos.diff
-26
View File
@@ -1,26 +0,0 @@
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 4c17df2..4c3c311 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -600,8 +600,6 @@ public:
out << " \n";
}
- bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }
-
bool column_has_upper_bound(unsigned j) const {
switch(m_column_types[j]) {
case column_type::free_column:
diff --git a/src/util/lp/static_matrix_def.h b/src/util/lp/static_matrix_def.h
index 7949573..2f1cb42 100644
--- a/src/util/lp/static_matrix_def.h
+++ b/src/util/lp/static_matrix_def.h
@@ -86,7 +86,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * /* basis *
init_row_columns(m, m);
while (m--) {
for (auto & col : A.m_columns[m]){
- set(col.var(), m, A.get_value_of_column_cell(col));
+ set(col.var(), m, A.get_column_cell(col));
}
}
}
pkgs/applications/science/logic/z3/default.nix
-216
View File
@@ -1,216 +0,0 @@
{
lib,
stdenv,
fetchFromGitHub,
fetchpatch,
python,
fixDarwinDylibNames,
javaBindings ? false,
ocamlBindings ? false,
pythonBindings ? true,
jdk ? null,
ocaml ? null,
findlib ? null,
zarith ? null,
writeScript,
replaceVars,
}:
assert javaBindings -> jdk != null;
assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
let
common =
{
version,
sha256,
patches ? [ ],
tag ? "z3",
doCheck ? true,
}:
stdenv.mkDerivation rec {
pname = "z3";
inherit version sha256 patches;
src = fetchFromGitHub {
owner = "Z3Prover";
repo = "z3";
rev = "${tag}-${version}";
sha256 = sha256;
};
strictDeps = true;
nativeBuildInputs =
[ python ]
++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames
++ lib.optional javaBindings jdk
++ lib.optionals ocamlBindings [
ocaml
findlib
];
propagatedBuildInputs = [ python.pkgs.setuptools ] ++ lib.optionals ocamlBindings [ zarith ];
enableParallelBuilding = true;
postPatch =
lib.optionalString ocamlBindings ''
export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
mkdir -p $OCAMLFIND_DESTDIR/stublibs
''
+
lib.optionalString
((lib.versionAtLeast python.version "3.12") && (lib.versionOlder version "4.8.14"))
''
# See https://github.com/Z3Prover/z3/pull/5729. This is a specialization of this patch for 4.8.5.
for file in scripts/mk_util.py src/api/python/CMakeLists.txt; do
substituteInPlace "$file" \
--replace-fail "distutils.sysconfig.get_python_lib()" "sysconfig.get_path('purelib')" \
--replace-fail "distutils.sysconfig" "sysconfig"
done
'';
configurePhase =
lib.concatStringsSep " " (
[ "${python.pythonOnBuildForHost.interpreter} scripts/mk_make.py --prefix=$out" ]
++ lib.optional javaBindings "--java"
++ lib.optional ocamlBindings "--ml"
++ lib.optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}"
)
+ "\n"
+ "cd build";
inherit doCheck;
checkPhase = ''
make -j $NIX_BUILD_CORES test
./test-z3 -a
'';
postInstall =
''
mkdir -p $dev $lib
mv $out/lib $lib/lib
mv $out/include $dev/include
''
+ lib.optionalString pythonBindings ''
mkdir -p $python/lib
mv $lib/lib/python* $python/lib/
ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
''
+ lib.optionalString javaBindings ''
mkdir -p $java/share/java
mv com.microsoft.z3.jar $java/share/java
moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
'';
doInstallCheck = true;
installCheckPhase = ''
$out/bin/z3 -version 2>&1 | grep -F "Z3 version $version"
'';
outputs =
[
"out"
"lib"
"dev"
"python"
]
++ lib.optional javaBindings "java"
++ lib.optional ocamlBindings "ocaml";
meta = with lib; {
description = "High-performance theorem prover and SMT solver";
mainProgram = "z3";
homepage = "https://github.com/Z3Prover/z3";
changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${version}";
license = licenses.mit;
platforms = platforms.unix;
maintainers = with maintainers; [
thoughtpolice
ttuegel
numinit
];
};
};
static-matrix-def-patch = fetchpatch {
# clang / gcc fixes. fixes typos in some member names
name = "gcc-15-fixes.patch";
url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch";
includes = [ "src/math/lp/static_matrix_def.h" ];
hash = "sha256-rEH+UzylzyhBdtx65uf8QYj5xwuXOyG6bV/4jgKkXGo=";
};
static-matrix-patch = fetchpatch {
# clang / gcc fixes. fixes typos in some member names
name = "gcc-15-fixes.patch";
url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch";
includes = [ "src/@dir@/lp/static_matrix.h" ];
stripLen = 3;
extraPrefix = "src/@dir@/";
hash = "sha256-+H1/VJPyI0yq4M/61ay8SRCa6OaoJ/5i+I3zVTAPUVo=";
};
# replace @dir@ in the path of the given list of patches
fixupPatches = dir: map (patch: replaceVars patch { inherit dir; });
in
{
z3_4_14 = common {
version = "4.14.1";
sha256 = "sha256-pTsDzf6Frk4mYAgF81wlR5Kb1x56joFggO5Fa3G2s70=";
};
z3_4_13 = common {
version = "4.13.4";
sha256 = "sha256-8hWXCr6IuNVKkOegEmWooo5jkdmln9nU7wI8T882BSE=";
};
z3_4_12 = common {
version = "4.12.6";
sha256 = "sha256-X4wfPWVSswENV0zXJp/5u9SQwGJWocLKJ/CNv57Bt+E=";
patches =
fixupPatches "math" [
./lower-bound-typo.diff
static-matrix-patch
]
++ [
static-matrix-def-patch
];
};
z3_4_11 = common {
version = "4.11.2";
sha256 = "sha256-OO0wtCvSKwGxnKvu+AfXe4mEzv4nofa7A00BjX+KVjc=";
patches =
fixupPatches "math" [
./lower-bound-typo.diff
static-matrix-patch
./tail-matrix.diff
]
++ [
static-matrix-def-patch
];
};
z3_4_8 = common {
version = "4.8.17";
sha256 = "sha256-BSwjgOU9EgCcm18Zx0P9mnoPc9ZeYsJwEu0ffnACa+8=";
patches =
fixupPatches "math" [
./lower-bound-typo.diff
static-matrix-patch
./tail-matrix.diff
]
++ [
static-matrix-def-patch
];
};
z3_4_8_5 = common {
tag = "Z3";
version = "4.8.5";
sha256 = "sha256-ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
patches =
fixupPatches "util" [
./lower-bound-typo.diff
static-matrix-patch
./tail-matrix.diff
]
++ [
./4-8-5-typos.diff
];
};
}
pkgs/applications/science/logic/z3/lower-bound-typo.diff
-13
View File
@@ -1,13 +0,0 @@
diff --git a/src/@dir@/lp/column_info.h b/src/@dir@/lp/column_info.h
index 1dc0c60..9cbeea6 100644
--- a/src/@dir@/lp/column_info.h
+++ b/src/@dir@/lp/column_info.h
@@ -47,7 +47,7 @@ public:
m_lower_bound_is_strict == c.m_lower_bound_is_strict &&
m_upper_bound_is_set == c.m_upper_bound_is_set&&
m_upper_bound_is_strict == c.m_upper_bound_is_strict&&
- (!m_lower_bound_is_set || m_lower_bound == c.m_low_bound) &&
+ (!m_lower_bound_is_set || m_lower_bound == c.m_lower_bound) &&
(!m_upper_bound_is_set || m_upper_bound == c.m_upper_bound) &&
m_cost == c.m_cost &&
m_is_fixed == c.m_is_fixed &&
pkgs/applications/science/logic/z3/tail-matrix.diff
-12
View File
@@ -1,12 +0,0 @@
diff --git a/src/@dir@/lp/tail_matrix.h b/src/@dir@/lp/tail_matrix.h
index 2047e8c..c84340e 100644
--- a/src/@dir@/lp/tail_matrix.h
+++ b/src/@dir@/lp/tail_matrix.h
@@ -43,7 +43,6 @@ public:
const tail_matrix & m_A;
unsigned m_row;
ref_row(const tail_matrix& m, unsigned row): m_A(m), m_row(row) {}
- T operator[](unsigned j) const { return m_A.get_elem(m_row, j);}
};
ref_row operator[](unsigned i) const { return ref_row(*this, i);}
};
pkgs/applications/science/logic/z3/tptp.nix → pkgs/by-name/z3/z3-tptp/package.nix
+1 -1
View File
@@ -30,6 +30,6 @@ stdenv.mkDerivation rec {
meta = {
inherit (z3.meta) license homepage platforms;
description = "TPTP wrapper for Z3 prover";
maintainers = [ lib.maintainers.raskin ];
maintainers = z3.meta.maintainers ++ [ lib.maintainers.raskin ];
};
}
pkgs/by-name/z3/z3/package.nix
+6
View File
@@ -0,0 +1,6 @@
{
z3_4_14,
...
}@args:
z3_4_14.override args
pkgs/by-name/z3/z3_4_14/package.nix
+130
View File
@@ -0,0 +1,130 @@
{
lib,
stdenv,
fetchFromGitHub,
python3,
fixDarwinDylibNames,
nix-update-script,
javaBindings ? false,
ocamlBindings ? false,
pythonBindings ? true,
jdk ? null,
ocaml ? null,
findlib ? null,
zarith ? null,
versionInfo ? {
regex = "^v(4\\.14\\.[0-9]+)$";
version = "4.14.1";
hash = "sha256-pTsDzf6Frk4mYAgF81wlR5Kb1x56joFggO5Fa3G2s70=";
},
...
}:
assert javaBindings -> jdk != null;
assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
stdenv.mkDerivation (finalAttrs: {
pname = "z3";
inherit (versionInfo) version;
src = fetchFromGitHub {
owner = "Z3Prover";
repo = "z3";
rev = "z3-${finalAttrs.version}";
inherit (versionInfo) hash;
};
strictDeps = true;
nativeBuildInputs =
[ python3 ]
++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames
++ lib.optional javaBindings jdk
++ lib.optionals ocamlBindings [
ocaml
findlib
];
propagatedBuildInputs = [ python3.pkgs.setuptools ] ++ lib.optionals ocamlBindings [ zarith ];
enableParallelBuilding = true;
postPatch = lib.optionalString ocamlBindings ''
export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
mkdir -p $OCAMLFIND_DESTDIR/stublibs
'';
configurePhase =
lib.concatStringsSep " " (
[ "${python3.pythonOnBuildForHost.interpreter} scripts/mk_make.py --prefix=$out" ]
++ lib.optional javaBindings "--java"
++ lib.optional ocamlBindings "--ml"
++ lib.optional pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}"
)
+ "\n"
+ "cd build";
doCheck = true;
checkPhase = ''
make -j $NIX_BUILD_CORES test
./test-z3 -a
'';
postInstall =
''
mkdir -p $dev $lib
mv $out/lib $lib/lib
mv $out/include $dev/include
''
+ lib.optionalString pythonBindings ''
mkdir -p $python/lib
mv $lib/lib/python* $python/lib/
ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python3.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
''
+ lib.optionalString javaBindings ''
mkdir -p $java/share/java
mv com.microsoft.z3.jar $java/share/java
moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
'';
doInstallCheck = true;
installCheckPhase = ''
$out/bin/z3 -version 2>&1 | grep -F "Z3 version $version"
'';
outputs =
[
"out"
"lib"
"dev"
"python"
]
++ lib.optional javaBindings "java"
++ lib.optional ocamlBindings "ocaml";
passthru = {
updateScript = nix-update-script {
extraArgs =
[
"--version-regex"
versionInfo.regex
]
++ lib.optionals (versionInfo.autoUpdate or null != null) [
"--override-filename"
versionInfo.autoUpdate
];
};
};
meta = {
description = "High-performance theorem prover and SMT solver";
mainProgram = "z3";
homepage = "https://github.com/Z3Prover/z3";
changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${finalAttrs.version}";
license = lib.licenses.mit;
platforms = lib.platforms.unix;
maintainers = with lib.maintainers; [
thoughtpolice
ttuegel
numinit
];
};
})
pkgs/top-level/all-packages.nix
-11
View File
@@ -18133,17 +18133,6 @@ with pkgs;
gmp-static = gmp.override { withStatic = true; };
};
inherit (callPackages ../applications/science/logic/z3 { python = python3; })
z3_4_14
z3_4_13
z3_4_12
z3_4_11
z3_4_8
z3_4_8_5
;
z3 = z3_4_13;
z3-tptp = callPackage ../applications/science/logic/z3/tptp.nix { };
tlaplus = callPackage ../applications/science/logic/tlaplus {
jre = jre8; # TODO: remove override https://github.com/NixOS/nixpkgs/pull/89731
};
pkgs/top-level/python-packages.nix
+1 -6
View File
@@ -19224,12 +19224,7 @@ self: super: with self; {
yubico-client = callPackage ../development/python-modules/yubico-client { };
z3-solver =
(toPythonModule (
(pkgs.z3.override { inherit python; }).overrideAttrs (_: {
pname = "z3-solver";
})
)).python;
z3-solver = (toPythonModule (pkgs.z3.override { python3 = python; })).python;
z3c-checkversions = callPackage ../development/python-modules/z3c-checkversions { };