From 001c120169a06da94f04cd4231614f8098a24e3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Mar 2019 15:35:33 -0700 Subject: [PATCH 1/6] x64 Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index d1033ae58..fe31dc16c 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -42,7 +42,8 @@ def download_installs(): os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'), 'ubuntu-16' : ('so', 'ubuntu-x64'), 'x64-win' : ('dll', 'win-x64'), - 'x86-win' : ('dll', 'win-x86'), +# Skip x86 as I can't get dotnet build to produce AnyCPU TargetPlatform +# 'x86-win' : ('dll', 'win-x86'), 'osx' : ('dylib', 'macos'), 'debian' : ('so', 'debian.8-x64') } @@ -82,13 +83,19 @@ def unpack(): shutil.move("tmp/%s/bin/%s" % (package_dir, b), "out/lib/netstandard1.4/%s" % b) def mk_targets(): - shutil.copy("../src/api/dotnet/Microsoft.Z3.targets.in", "out/Microsoft.Z3.targets") + mk_dir("out/build") + shutil.copy("../src/api/dotnet/Microsoft.Z3.targets.in", "out/build/Microsoft.Z3.targets") + +def mk_license(): + mk_dir("out/license") + shutil.copy("../LICENSE.txt", "out/license/LICENSE.txt") def create_nuget_spec(): + mk_license() contents = """ - Microsoft.Z3 + Microsoft.Z3.x64 %s Microsoft @@ -108,7 +115,7 @@ Linux Dependencies: """ - with open("out/Microsoft.Z3.nuspec", 'w') as f: + with open("out/Microsoft.Z3.x64.nuspec", 'w') as f: f.write(contents % version_num) def create_nuget_package(): @@ -128,8 +135,8 @@ nuget_sign_input = """ "SignRequestFiles": [ { "CustomerCorrelationId": "42fc9577-af9e-4ac9-995d-1788d8721d17", - "SourceLocation": "Microsoft.Z3.%s.nupkg", - "DestinationLocation": "Microsoft.Z3.%s.nupkg" + "SourceLocation": "Microsoft.Z3.x64.%s.nupkg", + "DestinationLocation": "Microsoft.Z3.x64.%s.nupkg" } ], "SigningInfo": { @@ -155,7 +162,7 @@ nuget_sign_input = """ }""" def sign_nuget_package(): - package_name = "Microsoft.Z3.%s.nupkg" % version_num + package_name = "Microsoft.Z3.x64.%s.nupkg" % version_num input_file = "out/nuget_sign_input.json" output_path = os.path.abspath("out").replace("\\","\\\\") with open(input_file, 'w') as f: From e19c1194963e896683074dd738df8e3b40893922 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Mar 2019 15:41:52 -0700 Subject: [PATCH 2/6] copyright Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index fe31dc16c..0b6f130b1 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -104,7 +104,7 @@ Z3 is a satisfiability modulo theories solver from Microsoft Research. Linux Dependencies: libgomp.so.1 installed - Copyright Microsoft Corporation. All rights reserved. + © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg https://github.com/Z3Prover/z3 From 0a477a0a93bd6bf5ebac8be9998fbe53ad6ff431 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Thu, 14 Mar 2019 15:46:03 -0700 Subject: [PATCH 3/6] Remove dependency on TargetPlatform macro Unnecessary, since dropping support for x86 --- src/api/dotnet/Microsoft.Z3.targets.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/Microsoft.Z3.targets.in b/src/api/dotnet/Microsoft.Z3.targets.in index a5ff7b8aa..bf2ca2dc7 100644 --- a/src/api/dotnet/Microsoft.Z3.targets.in +++ b/src/api/dotnet/Microsoft.Z3.targets.in @@ -1,10 +1,10 @@ - + false libz3.dll PreserveNewest - \ No newline at end of file + From 7b50fca02c1399efe115e1d1efaa08f8529d71e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Mar 2019 18:22:42 -0700 Subject: [PATCH 4/6] display dimacs Signed-off-by: Nikolaj Bjorner --- src/ast/display_dimacs.cpp | 60 +++++++++++++++++++++++++++++++++----- 1 file changed, 52 insertions(+), 8 deletions(-) diff --git a/src/ast/display_dimacs.cpp b/src/ast/display_dimacs.cpp index da39538d9..a1375dff8 100644 --- a/src/ast/display_dimacs.cpp +++ b/src/ast/display_dimacs.cpp @@ -26,6 +26,7 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) { ptr_vector exprs; unsigned num_vars = 0; unsigned num_cls = fmls.size(); + bool is_from_dimacs = true; for (expr * f : fmls) { unsigned num_lits; expr * const * lits; @@ -41,10 +42,51 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) { expr * l = lits[j]; if (m.is_not(l)) l = to_app(l)->get_arg(0); - if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { - num_vars++; - expr2var.setx(l->get_id(), num_vars, UINT_MAX); - exprs.setx(l->get_id(), l, nullptr); + if (!is_uninterp_const(l)) { + is_from_dimacs = false; + break; + } + symbol const& s = to_app(l)->get_decl()->get_name(); + if (s.is_numerical() && s.get_num() > 0) { + if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { + ++num_vars; + expr2var.setx(l->get_id(), s.get_num(), UINT_MAX); + exprs.setx(l->get_id(), l, nullptr); + } + continue; + } + is_from_dimacs = false; + break; + } + if (!is_from_dimacs) { + num_vars = 0; + expr2var.reset(); + exprs.reset(); + break; + } + } + + if (!is_from_dimacs) { + for (expr * f : fmls) { + unsigned num_lits; + expr * const * lits; + if (m.is_or(f)) { + num_lits = to_app(f)->get_num_args(); + lits = to_app(f)->get_args(); + } + else { + num_lits = 1; + lits = &f; + } + for (unsigned j = 0; j < num_lits; j++) { + expr * l = lits[j]; + if (m.is_not(l)) + l = to_app(l)->get_arg(0); + if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { + num_vars++; + expr2var.setx(l->get_id(), num_vars, UINT_MAX); + exprs.setx(l->get_id(), l, nullptr); + } } } } @@ -71,10 +113,12 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) { } out << "0\n"; } - for (expr* e : exprs) { - if (e && is_app(e)) { - symbol const& n = to_app(e)->get_decl()->get_name(); - out << "c " << expr2var[e->get_id()] << " " << n << "\n"; + if (!is_from_dimacs) { + for (expr* e : exprs) { + if (e && is_app(e)) { + symbol const& n = to_app(e)->get_decl()->get_name(); + out << "c " << expr2var[e->get_id()] << " " << n << "\n"; + } } } return out; From f0aebb1600ac1660c43f155f81b6747891e2e4b4 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Fri, 15 Mar 2019 15:20:32 -0700 Subject: [PATCH 5/6] Fixed nuget package spec generation code --- scripts/mk_nuget_release.py | 40 ++++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 18 deletions(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 0b6f130b1..4a2bfd98e 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -20,19 +20,23 @@ import subprocess import mk_util import mk_project -data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode()) +release_data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode()) +release_tag_name = release_data['tag_name'] +release_tag_ref_data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/git/refs/tags/%s" % release_tag_name).read().decode()) +release_tag_sha = release_tag_ref_data['object']['sha'] +release_tag_data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/git/tags/%s" % release_tag_sha).read().decode()) -version_str = data['tag_name'] -version_num = version_str[3:] +release_version = release_tag_name[3:] +release_commit = release_tag_data['object']['sha'] -print(version_str) +print(release_version) def mk_dir(d): if not os.path.exists(d): os.makedirs(d) def download_installs(): - for asset in data['assets']: + for asset in latest_release_data['assets']: url = asset['browser_download_url'] name = asset['name'] print("Downloading ", url) @@ -85,18 +89,13 @@ def unpack(): def mk_targets(): mk_dir("out/build") shutil.copy("../src/api/dotnet/Microsoft.Z3.targets.in", "out/build/Microsoft.Z3.targets") - -def mk_license(): - mk_dir("out/license") - shutil.copy("../LICENSE.txt", "out/license/LICENSE.txt") def create_nuget_spec(): - mk_license() contents = """ Microsoft.Z3.x64 - %s + {0} Microsoft Z3 is a satisfiability modulo theories solver from Microsoft Research. @@ -106,17 +105,22 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover - https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg + https://raw.githubusercontent.com/Z3Prover/z3/{1}/package/icon.jpg https://github.com/Z3Prover/z3 - https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt - + https://raw.githubusercontent.com/Z3Prover/z3/{1}/LICENSE.txt + true en -""" +""".format(release_version, release_commit) with open("out/Microsoft.Z3.x64.nuspec", 'w') as f: - f.write(contents % version_num) + f.write(contents) def create_nuget_package(): subprocess.call(["nuget", "pack"], cwd="out") @@ -162,11 +166,11 @@ nuget_sign_input = """ }""" def sign_nuget_package(): - package_name = "Microsoft.Z3.x64.%s.nupkg" % version_num + package_name = "Microsoft.Z3.x64.%s.nupkg" % release_version input_file = "out/nuget_sign_input.json" output_path = os.path.abspath("out").replace("\\","\\\\") with open(input_file, 'w') as f: - f.write(nuget_sign_input % (output_path, output_path, version_num, version_num)) + f.write(nuget_sign_input % (output_path, output_path, release_version, release_version)) subprocess.call(["EsrpClient.exe", "sign", "-a", "authorization.json", "-p", "policy.json", "-i", input_file, "-o", "out\\diagnostics.json"]) From a492eb020901a394fc9b13bda30fbd5d7f630995 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Fri, 15 Mar 2019 15:23:33 -0700 Subject: [PATCH 6/6] Fixed missed renamed variable --- scripts/mk_nuget_release.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 4a2bfd98e..0b418f48d 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -36,7 +36,7 @@ def mk_dir(d): os.makedirs(d) def download_installs(): - for asset in latest_release_data['assets']: + for asset in release_data['assets']: url = asset['browser_download_url'] name = asset['name'] print("Downloading ", url)