From e83e9b02dfd977653491f9c76ab05411335a9511 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Nov 2018 15:17:55 -0800 Subject: [PATCH] increment version number to 4.8.4 Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- scripts/mk_nuget_release.py | 18 ++++++++++-------- scripts/mk_project.py | 2 +- src/sat/sat_parallel.cpp | 11 ----------- src/sat/sat_parallel.h | 2 -- 5 files changed, 12 insertions(+), 23 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index cd9c14435..bc5eecdef 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,7 +34,7 @@ endif() ################################################################################ set(Z3_VERSION_MAJOR 4) set(Z3_VERSION_MINOR 8) -set(Z3_VERSION_PATCH 3) +set(Z3_VERSION_PATCH 4) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 09cfd2b7a..7d2f23998 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -31,8 +31,6 @@ def download_installs(): for asset in data['assets']: url = asset['browser_download_url'] name = asset['name'] - if "x64" not in name: - continue print("Downloading ", url) sys.stdout.flush() urllib.request.urlretrieve(url, "packages/%s" % name) @@ -40,6 +38,8 @@ def download_installs(): os_info = {"ubuntu-14" : ('so', 'ubuntu.14.04-x64'), 'ubuntu-16' : ('so', 'ubuntu.16.04-x64'), 'win' : ('dll', 'win-x64'), + 'win' : ('dll', 'win-x86'), + 'osx' : ('dylib', 'macos'), 'debian' : ('so', 'debian.8-x64') } def classify_package(f): @@ -54,18 +54,20 @@ def unpack(): # out # +- runtimes # +- win-x64 + # +- win-x86 # +- ubuntu.16.04-x64 # +- ubuntu.14.04-x64 # +- debian.8-x64 + # +- macos # + - for f in os.listdir("packages"): - if f.endswith("zip") and "x64" in f and classify_package(f): - print(f) + for f in os.listdir("packages"): + print(f) + if f.endswith("zip") and classify_package(f): os_name, package_dir, ext, dst = classify_package(f) zip_ref = zipfile.ZipFile("packages/%s" % f, 'r') zip_ref.extract("%s/bin/libz3.%s" % (package_dir, ext), "tmp") mk_dir("out/runtimes/%s" % dst) - shutil.move("tmp/%s/bin/libz3.%s" % (package_dir, ext), "out/runtimes/%s/." % dst) + shutil.move("tmp/%s/bin/libz3.%s" % (package_dir, ext), "out/runtimes/%s/." % dst, "/y") if "win" in f: mk_dir("out/lib/netstandard1.4/") for b in ["Microsoft.Z3.dll"]: @@ -77,7 +79,7 @@ def create_nuget_spec(): contents = """ - Microsoft.Z3.x64 + Microsoft.Z3 %s Microsoft Z3 is a satisfiability modulo theories solver from Microsoft Research. @@ -96,7 +98,7 @@ def create_nuget_spec(): """ - with open("out/Microsoft.Z3.x64.nuspec", 'w') as f: + with open("out/Microsoft.Z3.nuspec", 'w') as f: f.write(contents % mk_util.get_version_string(3)) def create_nuget_package(): diff --git a/scripts/mk_project.py b/scripts/mk_project.py index e70a094a0..8cf60ab62 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 8, 3, 0) + set_version(4, 8, 4, 0) # Z3 Project definition def init_project_def(): diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 33cb02a87..ce2080f8c 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -285,17 +285,6 @@ namespace sat { return copied; } - void parallel::set_phase(local_search& s) { - #pragma omp critical (par_solver) - { - m_consumer_ready = true; - m_phase.reserve(s.num_vars(), l_undef); - for (unsigned i = 0; i < s.num_vars(); ++i) { - m_phase[i] = s.get_phase(i) ? l_true : l_false; - } - m_num_clauses = s.num_non_binary_clauses(); - } - } bool parallel::copy_solver(solver& s) { bool copied = false; diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index 256623380..afb148ed4 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -104,8 +104,6 @@ namespace sat { void get_phase(solver& s); - void set_phase(local_search& s); - bool get_phase(local_search& s); bool copy_solver(solver& s);