Compare commits
6 Commits
3ea0fe040c
...
042e9c8a1d
| Author | SHA1 | Date |
|---|---|---|
 David Abdurachmanov
|
042e9c8a1d
|
|
|
David Abdurachmanov
|
6ba09b736c
|
|
Jerry James
|
7e13c11207 | |
Richard W.M. Jones
|
4b6c6d8a09 | |
|
Richard W.M. Jones
|
28838627de | |
|
Jerry James
|
69a9e69b24 |
2
sources
2
sources
|
|
@ -1 +1 @@
|
|||
SHA512 (z3-4.12.2.tar.gz) = 375477cbbc9837b44e752c89916409d07bf6a73830b52878aab4f376f08b37dd5ab485da225744d394ab15f2a7e1014edc3be5eb9962934c440a8d55259317e2
|
||||
SHA512 (z3-4.12.4.tar.gz) = fcb778d2e3e0d13fc68afcd8724548279f9edbbb4aac1bbb93e00959c33330ab2fd84f2c2e4b0b78f767819725a90b845fc606a9adc931ae1f0a11f4deae433b
|
||||
|
|
|
|||
205
z3-escapes.patch
205
z3-escapes.patch
|
|
@ -1,205 +0,0 @@
|
|||
Fixes warnings such as these:
|
||||
|
||||
/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:142: SyntaxWarning: invalid escape sequence '\-'
|
||||
words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:577: SyntaxWarning: invalid escape sequence '\W'
|
||||
words = re.split('\W+', line)
|
||||
|
||||
--- z3-z3-4.12.2/scripts/mk_genfile_common.py.orig 2023-05-12 13:59:04.000000000 -0600
|
||||
+++ z3-z3-4.12.2/scripts/mk_genfile_common.py 2023-07-06 10:52:08.477210179 -0600
|
||||
@@ -139,7 +139,7 @@ def mk_z3consts_py_internal(api_files, o
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
- words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
+ words = re.split('[^-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
@@ -227,7 +227,7 @@ def mk_z3consts_dotnet_internal(api_file
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
- words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
+ words = re.split('[^-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
@@ -315,7 +315,7 @@ def mk_z3consts_java_internal(api_files,
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
- words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
+ words = re.split('[^-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
@@ -441,7 +441,7 @@ def mk_z3consts_ml_internal(api_files, o
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
- words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
+ words = re.split('[^-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
@@ -574,7 +574,7 @@ def mk_def_file_internal(defname, dll_na
|
||||
for line in api:
|
||||
m = pat1.match(line)
|
||||
if m:
|
||||
- words = re.split('\W+', line)
|
||||
+ words = re.split(r'\W+', line)
|
||||
i = 0
|
||||
for w in words:
|
||||
if w == 'Z3_API':
|
||||
@@ -618,9 +618,9 @@ def mk_gparams_register_modules_internal
|
||||
fout = open(fullname, 'w')
|
||||
fout.write('// Automatically generated file.\n')
|
||||
fout.write('#include "util/gparams.h"\n')
|
||||
- reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
|
||||
- reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
- reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
+ reg_pat = re.compile(r'[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
|
||||
+ reg_mod_pat = re.compile(r'[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
+ reg_mod_descr_pat = re.compile(r'[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
for h_file in sorted_headers_by_component(h_files_full_path):
|
||||
added_include = False
|
||||
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
||||
@@ -698,9 +698,9 @@ def mk_install_tactic_cpp_internal(h_fil
|
||||
fout.write('#include "cmd_context/tactic_cmds.h"\n')
|
||||
fout.write('#include "cmd_context/simplifier_cmds.h"\n')
|
||||
fout.write('#include "cmd_context/cmd_context.h"\n')
|
||||
- tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
|
||||
- probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)')
|
||||
- simplifier_pat = re.compile('[ \t]*ADD_SIMPLIFIER\(.*\)')
|
||||
+ tactic_pat = re.compile(r'[ \t]*ADD_TACTIC\(.*\)')
|
||||
+ probe_pat = re.compile(r'[ \t]*ADD_PROBE\(.*\)')
|
||||
+ simplifier_pat = re.compile(r'[ \t]*ADD_SIMPLIFIER\(.*\)')
|
||||
for h_file in sorted_headers_by_component(h_files_full_path):
|
||||
added_include = False
|
||||
try:
|
||||
@@ -780,10 +780,10 @@ def mk_mem_initializer_cpp_internal(h_fi
|
||||
fullname = os.path.join(path, 'mem_initializer.cpp')
|
||||
fout = open(fullname, 'w')
|
||||
fout.write('// Automatically generated file.\n')
|
||||
- initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
|
||||
+ initializer_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
|
||||
# ADD_INITIALIZER with priority
|
||||
- initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
|
||||
- finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
|
||||
+ initializer_prio_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
|
||||
+ finalizer_pat = re.compile(r'[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
|
||||
for h_file in sorted_headers_by_component(h_files_full_path):
|
||||
added_include = False
|
||||
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
||||
--- z3-z3-4.12.2/scripts/mk_util.py.orig 2023-07-06 11:53:06.045350565 -0600
|
||||
+++ z3-z3-4.12.2/scripts/mk_util.py 2023-07-06 12:02:59.686951602 -0600
|
||||
@@ -395,7 +395,7 @@ def check_java():
|
||||
else:
|
||||
# Search for jni.h in the library directories...
|
||||
t = open('errout', 'r')
|
||||
- open_pat = re.compile("\[search path for class files: (.*)\]")
|
||||
+ open_pat = re.compile(r"\[search path for class files: (.*)\]")
|
||||
cdirs = []
|
||||
for line in t:
|
||||
m = open_pat.match(line)
|
||||
@@ -808,8 +808,8 @@ def parse_options():
|
||||
def extract_c_includes(fname):
|
||||
result = {}
|
||||
# We look for well behaved #include directives
|
||||
- std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
|
||||
- system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
|
||||
+ std_inc_pat = re.compile(r"[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
|
||||
+ system_inc_pat = re.compile(r"[ \t]*#include[ \t]*\<.*\>[ \t]*")
|
||||
# We should generate and error for any occurrence of #include that does not match the previous pattern.
|
||||
non_std_inc_pat = re.compile(".*#include.*")
|
||||
|
||||
@@ -1716,7 +1716,7 @@ class DotNetDLLComponent(Component):
|
||||
|
||||
print("Version output to csproj:", version)
|
||||
|
||||
- core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk">
|
||||
+ core_csproj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
|
||||
|
||||
<PropertyGroup>
|
||||
<TargetFramework>netstandard1.4</TargetFramework>
|
||||
@@ -2237,7 +2237,7 @@ class DotNetExampleComponent(ExampleComp
|
||||
else:
|
||||
platform = 'x86'
|
||||
|
||||
- dotnet_proj_str = """<Project Sdk="Microsoft.NET.Sdk">
|
||||
+ dotnet_proj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
|
||||
<PropertyGroup>
|
||||
<OutputType>Exe</OutputType>
|
||||
<TargetFramework>netcoreapp2.0</TargetFramework>
|
||||
@@ -3153,7 +3153,7 @@ def mk_vs_proj_property_groups(f, name,
|
||||
f.write(' <Keyword>Win32Proj</Keyword>\n')
|
||||
f.write(' <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str())
|
||||
f.write(' </PropertyGroup>\n')
|
||||
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
|
||||
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.Default.props" />\n')
|
||||
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n')
|
||||
f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type)
|
||||
f.write(' <CharacterSet>Unicode</CharacterSet>\n')
|
||||
@@ -3164,24 +3164,24 @@ def mk_vs_proj_property_groups(f, name,
|
||||
f.write(' <CharacterSet>Unicode</CharacterSet>\n')
|
||||
f.write(' <UseOfMfc>false</UseOfMfc>\n')
|
||||
f.write(' </PropertyGroup>\n')
|
||||
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
|
||||
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.props" />\n')
|
||||
f.write(' <ImportGroup Label="ExtensionSettings" />\n')
|
||||
f.write(' <ImportGroup Label="PropertySheets">\n')
|
||||
- f.write(' <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n')
|
||||
+ f.write(' <Import Project="$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n')
|
||||
f.write(' <PropertyGroup Label="UserMacros" />\n')
|
||||
f.write(' <PropertyGroup>\n')
|
||||
- f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
|
||||
+ f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
|
||||
f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name)
|
||||
f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext)
|
||||
- f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
|
||||
+ f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
|
||||
f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name)
|
||||
f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext)
|
||||
f.write(' </PropertyGroup>\n')
|
||||
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
|
||||
- f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
|
||||
+ f.write(' <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
|
||||
f.write(' </PropertyGroup>\n')
|
||||
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
|
||||
- f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
|
||||
+ f.write(' <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
|
||||
f.write(' </PropertyGroup>\n')
|
||||
|
||||
|
||||
@@ -3258,7 +3258,7 @@ def mk_vs_proj(name, components):
|
||||
mk_vs_proj_link_exe(f, name, debug=False)
|
||||
f.write(' </ItemDefinitionGroup>\n')
|
||||
mk_vs_proj_dep_groups(f, name, components)
|
||||
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
|
||||
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
|
||||
f.write(' <ImportGroup Label="ExtensionTargets">\n')
|
||||
f.write(' </ImportGroup>\n')
|
||||
f.write('</Project>\n')
|
||||
@@ -3299,7 +3299,7 @@ def mk_vs_proj_dll(name, components):
|
||||
mk_vs_proj_link_dll(f, name, debug=False)
|
||||
f.write(' </ItemDefinitionGroup>\n')
|
||||
mk_vs_proj_dep_groups(f, name, components)
|
||||
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
|
||||
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
|
||||
f.write(' <ImportGroup Label="ExtensionTargets">\n')
|
||||
f.write(' </ImportGroup>\n')
|
||||
f.write('</Project>\n')
|
||||
--- z3-z3-4.12.2/scripts/update_api.py.orig 2023-07-06 12:02:07.510504547 -0600
|
||||
+++ z3-z3-4.12.2/scripts/update_api.py 2023-07-06 12:02:19.399378554 -0600
|
||||
@@ -116,8 +116,8 @@ class APITypes:
|
||||
|
||||
def def_Types(self, api_files):
|
||||
global Closures
|
||||
- pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
|
||||
- pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)")
|
||||
+ pat1 = re.compile(r" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
|
||||
+ pat2 = re.compile(r"Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)")
|
||||
for api_file in api_files:
|
||||
with open(api_file, 'r') as api:
|
||||
for line in api:
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
--- a/scripts/update_api.py 2020-09-10 12:51:28.000000000 -0600
|
||||
+++ b/scripts/update_api.py 2020-12-25 17:03:00.196777823 -0700
|
||||
@@ -1755,15 +1755,15 @@ def write_core_py_preamble(core_py):
|
||||
# Automatically generated file
|
||||
import sys, os
|
||||
import ctypes
|
||||
-import pkg_resources
|
||||
+import sysconfig
|
||||
from .z3types import *
|
||||
from .z3consts import *
|
||||
|
||||
-_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
|
||||
+_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so.@MAJVER@'
|
||||
_lib = None
|
||||
_default_dirs = ['.',
|
||||
os.path.dirname(os.path.abspath(__file__)),
|
||||
- pkg_resources.resource_filename('z3', 'lib'),
|
||||
+ sysconfig.get_config_var('LIBDIR'),
|
||||
os.path.join(sys.prefix, 'lib'),
|
||||
None]
|
||||
_all_dirs = []
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
Fixes errors such as these:
|
||||
|
||||
In file included from /builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:53:
|
||||
/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp: In member function ‘void* region::allocate(size_t)’:
|
||||
/builddir/build/BUILD/z3-z3-4.12.2/src/util/tptr.h:29:62: error: ‘uintptr_t’ does not name a type
|
||||
29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
|
||||
| ^~~~~~~~~
|
||||
/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:82:22: note: in expansion of macro ‘ALIGN’
|
||||
82 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
|
||||
| ^~~~~
|
||||
/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:57:1: note: ‘uintptr_t’ is defined in header ‘<cstdint>’; did you forget to ‘#include <cstdint>’?
|
||||
56 | #include "util/page.h"
|
||||
+++ |+#include <cstdint>
|
||||
57 |
|
||||
|
||||
--- z3-z3-4.12.2/src/util/tptr.h.orig 2023-05-12 13:59:04.000000000 -0600
|
||||
+++ z3-z3-4.12.2/src/util/tptr.h 2023-05-13 07:04:48.389716628 -0600
|
||||
@@ -19,6 +19,7 @@ Revision History:
|
||||
|
||||
#pragma once
|
||||
|
||||
+#include <cstdint>
|
||||
#include "util/machine.h"
|
||||
|
||||
#define TAG_SHIFT PTR_ALIGNMENT
|
||||
29
z3.spec
29
z3.spec
|
|
@ -12,8 +12,8 @@
|
|||
%bcond_with test
|
||||
|
||||
Name: z3
|
||||
Version: 4.12.2
|
||||
Release: 7.rvre0%{?dist}
|
||||
Version: 4.12.4
|
||||
Release: 4.rvre0%{?dist}
|
||||
Summary: Satisfiability Modulo Theories (SMT) solver
|
||||
|
||||
License: MIT
|
||||
|
|
@ -21,14 +21,6 @@ URL: https://github.com/Z3Prover/z3
|
|||
Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz
|
||||
# Do not try to build or install native OCaml artifacts on bytecode-only arches
|
||||
Patch0: %{name}-ocaml.patch
|
||||
# Change the way python finds the shared object; see bz 1910923
|
||||
Patch1: %{name}-python.patch
|
||||
# Add a missing include of cstdint
|
||||
# https://github.com/Z3Prover/z3/pull/6720
|
||||
Patch2: %{name}-stdint.patch
|
||||
# Fix malformed python escape sequences
|
||||
# https://github.com/Z3Prover/z3/pull/6797
|
||||
Patch3: %{name}-escapes.patch
|
||||
|
||||
BuildRequires: cmake
|
||||
BuildRequires: doxygen
|
||||
|
|
@ -178,7 +170,7 @@ sed \
|
|||
# Comply with the Java packaging guidelines and fill in the version for python
|
||||
majver=$(cut -d. -f-2 <<< %{version})
|
||||
sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
|
||||
-e "s/@MAJVER@/$majver/" \
|
||||
-e "s/'so'/'so.$majver'/" \
|
||||
-i scripts/update_api.py
|
||||
|
||||
# Turn off HTML timestamps for reproducible builds
|
||||
|
|
@ -317,9 +309,22 @@ cd -
|
|||
%{python3_sitelib}/z3/
|
||||
|
||||
%changelog
|
||||
* Mon Nov 13 2023 David Abdurachmanov <davidlt@rivosinc.com> - 4.12.2-7.rvre0
|
||||
* Sun Dec 31 2023 David Abdurachmanov <davidlt@rivosinc.com> - 4.12.4-4.rvre0
|
||||
- Rebuilt for Fedora/RISCV (riscv64)
|
||||
|
||||
* Thu Dec 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.4-4
|
||||
- Fix python package library load name (bz 2255464)
|
||||
|
||||
* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.4-3
|
||||
- OCaml 5.1.1 + s390x code gen fix for Fedora 40
|
||||
|
||||
* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.4-2
|
||||
- OCaml 5.1.1 rebuild for Fedora 40
|
||||
|
||||
* Sat Dec 9 2023 Jerry James <loganjerry@gmail.com> - 4.12.4-1
|
||||
- Version 4.12.4
|
||||
- Drop upstreamed patches: python, stdint, escapes
|
||||
|
||||
* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.2-7
|
||||
- OCaml 5.1 rebuild for Fedora 40
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue