From 9b4cf1559dd431a716b351b4d14105ea27efb263 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Nov 2018 15:33:46 -0800 Subject: [PATCH 01/27] recover error stream from dimacs Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 6 ++++- src/sat/dimacs.cpp | 47 ++++++++++++++++++++--------------- src/sat/dimacs.h | 2 +- src/shell/dimacs_frontend.cpp | 6 ++--- 4 files changed, 36 insertions(+), 25 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index cb4ae19db..a5ad7b525 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -183,8 +183,12 @@ extern "C" { } else if (ext && std::string("dimacs") == ext) { ast_manager& m = to_solver_ref(s)->get_manager(); + std::stringstream err; sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); - parse_dimacs(is, solver); + if (!parse_dimacs(is, err, solver)) { + SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str()); + return; + } sat2goal s2g; ref mc; atom2bool_var a2b(m); diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp index 463418b23..970e682b3 100644 --- a/src/sat/dimacs.cpp +++ b/src/sat/dimacs.cpp @@ -21,6 +21,8 @@ Revision History: #undef min #include "sat/sat_solver.h" +struct lex_error {}; + class stream_buffer { std::istream & m_stream; int m_val; @@ -67,7 +69,7 @@ void skip_line(Buffer & in) { } template -int parse_int(Buffer & in) { +int parse_int(Buffer & in, std::ostream& err) { int val = 0; bool neg = false; skip_whitespace(in); @@ -81,9 +83,8 @@ int parse_int(Buffer & in) { } if (*in < '0' || *in > '9') { - std::cerr << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n"; - exit(3); - exit(ERR_PARSER); + err << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n"; + throw lex_error(); } while (*in >= '0' && *in <= '9') { @@ -95,14 +96,14 @@ int parse_int(Buffer & in) { } template -void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits) { +void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::literal_vector & lits) { int parsed_lit; int var; lits.reset(); while (true) { - parsed_lit = parse_int(in); + parsed_lit = parse_int(in, err); if (parsed_lit == 0) break; var = abs(parsed_lit); @@ -114,24 +115,30 @@ void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits) } template -void parse_dimacs_core(Buffer & in, sat::solver & solver) { +bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) { sat::literal_vector lits; - while (true) { - skip_whitespace(in); - if (*in == EOF) { - break; - } - else if (*in == 'c' || *in == 'p') { - skip_line(in); - } - else { - read_clause(in, solver, lits); - solver.mk_clause(lits.size(), lits.c_ptr()); + try { + while (true) { + skip_whitespace(in); + if (*in == EOF) { + break; + } + else if (*in == 'c' || *in == 'p') { + skip_line(in); + } + else { + read_clause(in, err, solver, lits); + solver.mk_clause(lits.size(), lits.c_ptr()); + } } } + catch (lex_error) { + return false; + } + return true; } -void parse_dimacs(std::istream & in, sat::solver & solver) { +bool parse_dimacs(std::istream & in, std::ostream& err, sat::solver & solver) { stream_buffer _in(in); - parse_dimacs_core(_in, solver); + return parse_dimacs_core(_in, err, solver); } diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h index 50ebec0c8..4c5d51502 100644 --- a/src/sat/dimacs.h +++ b/src/sat/dimacs.h @@ -21,7 +21,7 @@ Revision History: #include "sat/sat_types.h" -void parse_dimacs(std::istream & s, sat::solver & solver); +bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver); #endif /* DIMACS_PARSER_H_ */ diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 3a2af72cf..738566ce2 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -136,7 +136,7 @@ void verify_solution(char const * file_name) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + parse_dimacs(in, std::cerr, solver); sat::model const & m = g_solver->get_model(); for (unsigned i = 1; i < m.size(); i++) { @@ -178,10 +178,10 @@ unsigned read_dimacs(char const * file_name) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + parse_dimacs(in, std::cerr, solver); } else { - parse_dimacs(std::cin, solver); + parse_dimacs(std::cin, std::cerr, solver); } IF_VERBOSE(20, solver.display_status(verbose_stream());); From 2fbaad15d7324b4b67a968a6c3831416f384393b Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 14 Nov 2018 09:57:47 -0800 Subject: [PATCH 02/27] Build example for dotnetcore. --- scripts/mk_util.py | 36 +++++++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 88d7d7246..cfcf78538 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2391,7 +2391,41 @@ class DotNetExampleComponent(ExampleComponent): out.write('\n') out.write('_ex_%s: %s\n\n' % (self.name, exefile)) if is_dotnet_core_enabled(): - print("TBD: build script for dotnet_example on core") + proj_name = 'dotnet_example.csproj' + out.write('_ex_%s:' % self.name) + for csfile in get_cs_files(self.ex_dir): + out.write(' ') + out.write(os.path.join(self.to_ex_dir, csfile)) + out.write('\n') + out.write('\t@echo "" > %s\n' % proj_name) + out.write('\t@echo " " >> %s\n' % proj_name) + out.write('\t@echo " Exe" >> %s\n' % proj_name) + out.write('\t@echo " netcoreapp2.0" >> %s\n' % proj_name) + out.write('\t@echo " ') + if VS_X64: + out.write('x64') + elif VS_ARM: + out.write('ARM') + else: + out.write('x86') + out.write('" >> %s\n' % proj_name) + out.write('\t@echo " " >> %s\n' % proj_name) + out.write('\t@echo " " >> %s\n' % proj_name) + out.write('\t@echo " " >> %s\n' % (self.to_ex_dir, proj_name)) + out.write('\t@echo " " >> %s\n' % proj_name) + out.write('\t@echo " Microsoft.Z3.dll" >> %s\n' % proj_name) + out.write('\t@echo " " >> %s\n' % proj_name) + out.write('\t@echo " " >> %s\n' % proj_name) + out.write('\t@echo "" >> %s\n' % proj_name) + + dotnetCmdLine = [DOTNET, "build", proj_name] + dotnetCmdLine.extend(['-c']) + if DEBUG_MODE: + dotnetCmdLine.extend(['Debug']) + else: + dotnetCmdLine.extend(['Release']) + MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) + out.write('\n') class JavaExampleComponent(ExampleComponent): def __init__(self, name, path): From d4567a125588160d7bf0517d27000b26788580ad Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 14 Nov 2018 11:11:25 -0800 Subject: [PATCH 03/27] Fix `echo` command for Windows. --- scripts/mk_util.py | 42 +++++++++++++++++++++++++----------------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index cfcf78538..472da8595 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2396,27 +2396,35 @@ class DotNetExampleComponent(ExampleComponent): for csfile in get_cs_files(self.ex_dir): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) + + def mk_echo(msg): + echo_ex_qu = '' if IS_WINDOWS else '"' + echo_in_qu = '"' if IS_WINDOWS else '\\"' + echo_esc = '^' if IS_WINDOWS else '' + + msg = msg.replace('"', echo_in_qu).replace('<', echo_esc + '<').replace('>', echo_esc + '>') + out.write('\t@echo %s%s%s > %s\n' % (echo_ex_qu, msg, echo_ex_qu, proj_name)) + out.write('\n') - out.write('\t@echo "" > %s\n' % proj_name) - out.write('\t@echo " " >> %s\n' % proj_name) - out.write('\t@echo " Exe" >> %s\n' % proj_name) - out.write('\t@echo " netcoreapp2.0" >> %s\n' % proj_name) - out.write('\t@echo " ') + mk_echo('') + mk_echo(' ') + mk_echo(' Exe') + mk_echo(' netcoreapp2.0') if VS_X64: - out.write('x64') + platform = 'x64' elif VS_ARM: - out.write('ARM') + platform = 'ARM' else: - out.write('x86') - out.write('" >> %s\n' % proj_name) - out.write('\t@echo " " >> %s\n' % proj_name) - out.write('\t@echo " " >> %s\n' % proj_name) - out.write('\t@echo " " >> %s\n' % (self.to_ex_dir, proj_name)) - out.write('\t@echo " " >> %s\n' % proj_name) - out.write('\t@echo " Microsoft.Z3.dll" >> %s\n' % proj_name) - out.write('\t@echo " " >> %s\n' % proj_name) - out.write('\t@echo " " >> %s\n' % proj_name) - out.write('\t@echo "" >> %s\n' % proj_name) + platform = 'x86' + mk_echo(' %s' % platform) + mk_echo(' ') + mk_echo(' ') + mk_echo(' ' % self.to_ex_dir) + mk_echo(' ') + mk_echo(' Microsoft.Z3.dll') + mk_echo(' ') + mk_echo('') dotnetCmdLine = [DOTNET, "build", proj_name] dotnetCmdLine.extend(['-c']) From e39907c4810ce51dec97936965d64e8c109915ee Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 14 Nov 2018 11:25:18 -0800 Subject: [PATCH 04/27] Fix some problems in `mk_echo`. --- scripts/mk_util.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 472da8595..b6afaf897 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2397,13 +2397,14 @@ class DotNetExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) - def mk_echo(msg): + def mk_echo(msg, first = False): echo_ex_qu = '' if IS_WINDOWS else '"' echo_in_qu = '"' if IS_WINDOWS else '\\"' echo_esc = '^' if IS_WINDOWS else '' + echo_dir = '>' if first else '>>' msg = msg.replace('"', echo_in_qu).replace('<', echo_esc + '<').replace('>', echo_esc + '>') - out.write('\t@echo %s%s%s > %s\n' % (echo_ex_qu, msg, echo_ex_qu, proj_name)) + out.write('\t@echo %s%s%s %s %s\n' % (echo_ex_qu, msg, echo_ex_qu, echo_dir, proj_name)) out.write('\n') mk_echo('') @@ -2421,7 +2422,7 @@ class DotNetExampleComponent(ExampleComponent): mk_echo(' ') mk_echo(' ' % self.to_ex_dir) mk_echo(' ') - mk_echo(' Microsoft.Z3.dllMicrosoft.Z3.dll') mk_echo(' ') mk_echo(' ') mk_echo('') From 33363aeb58ab641c8e9b3c3a9ffaaf33e8c24f5e Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 14 Nov 2018 11:27:55 -0800 Subject: [PATCH 05/27] Fix problem in `mk_echo`. --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b6afaf897..aaeed1dea 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2407,7 +2407,7 @@ class DotNetExampleComponent(ExampleComponent): out.write('\t@echo %s%s%s %s %s\n' % (echo_ex_qu, msg, echo_ex_qu, echo_dir, proj_name)) out.write('\n') - mk_echo('') + mk_echo('', True) mk_echo(' ') mk_echo(' Exe') mk_echo(' netcoreapp2.0') From 52910fa465e8a839e2a20dfaf682e89e84a899b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 11:31:39 -0800 Subject: [PATCH 06/27] fix #1937 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 12 +++++++++++- src/parsers/smt2/smt2parser.cpp | 11 +++++++---- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dad485d94..82607452f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -561,6 +561,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu zstring s; rational pos, len; + TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";); bool constantBase = m_util.str.is_string(a, s); bool constantPos = m_autil.is_numeral(b, pos); bool constantLen = m_autil.is_numeral(c, len); @@ -599,6 +600,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu SASSERT(_len > 0); expr_ref_vector as(m()), bs(m()); m_util.str.get_concat(a, as); + if (as.empty()) { + result = a; + return BR_DONE; + } for (unsigned i = 0; i < as.size() && _len > 0; ++i) { if (m_util.str.is_unit(as[i].get())) { if (_pos == 0) { @@ -613,7 +618,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu return BR_FAILED; } } - result = m_util.str.mk_concat(bs); + if (bs.empty()) { + result = m_util.str.mk_empty(m().get_sort(a)); + } + else { + result = m_util.str.mk_concat(bs); + } return BR_DONE; } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 106a77c0e..64f9c36fd 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -346,7 +346,8 @@ namespace smt2 { // consume garbage // return true if managed to recover from the error... bool sync_after_error() { - while (true) { + unsigned num_errors = 0; + while (num_errors < 100) { try { while (curr_is_rparen()) next(); @@ -374,8 +375,10 @@ namespace smt2 { catch (scanner_exception & ex) { SASSERT(ex.has_pos()); error(ex.line(), ex.pos(), ex.msg()); + ++num_errors; } } + return false; } void check_next(scanner::token t, char const * msg) { @@ -3117,7 +3120,7 @@ namespace smt2 { bool operator()() { m_num_bindings = 0; - bool found_errors = false; + unsigned found_errors = 0; try { scan_core(); @@ -3126,7 +3129,7 @@ namespace smt2 { error(ex.msg()); if (!sync_after_error()) return false; - found_errors = true; + found_errors++; } while (true) { @@ -3138,7 +3141,7 @@ namespace smt2 { parse_cmd(); break; case scanner::EOF_TOKEN: - return !found_errors; + return found_errors == 0; default: throw parser_exception("invalid command, '(' expected"); break; From 139d8b85f018dc392f85af989af62a920e7c7e48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 11:43:41 -0800 Subject: [PATCH 07/27] core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 88d7d7246..6d3ad3d4b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -456,7 +456,9 @@ def check_dotnet(): raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') def check_dotnet_core(): - # TBD: check DOTNET + r = exec_cmd([DOTNET, '--help']) + if r != 0: + raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities') pass def check_ml(): From 727929c9af003d71eab1f0d90cc8e01761943491 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 12:04:31 -0800 Subject: [PATCH 08/27] fix test build Signed-off-by: Nikolaj Bjorner --- src/test/cnf_backbones.cpp | 4 ++-- src/test/sat_lookahead.cpp | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 50584c90c..10f3e56a7 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -238,10 +238,10 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + if (!parse_dimacs(in, std::cerr, solver)) return; } else { - parse_dimacs(std::cin, solver); + if (!parse_dimacs(std::cin, std::cerr, solver)) return; } IF_VERBOSE(20, solver.display_status(verbose_stream());); diff --git a/src/test/sat_lookahead.cpp b/src/test/sat_lookahead.cpp index fccbe8eed..23c4a4738 100644 --- a/src/test/sat_lookahead.cpp +++ b/src/test/sat_lookahead.cpp @@ -34,7 +34,8 @@ void tst_sat_lookahead(char ** argv, int argc, int& i) { std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; exit(ERR_OPEN_FILE); } - parse_dimacs(in, solver); + if (!parse_dimacs(in, std::cerr, solver)) + return; } sat::lookahead lh(solver); From 2501a875efcaa5d837601b40eafdcdeb7f351505 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 13:44:40 -0800 Subject: [PATCH 09/27] update script to generate file directly instead of from makefile Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 42 +++++++++++++++++++----------------------- 1 file changed, 19 insertions(+), 23 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 12ccc538c..63938caf9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2399,36 +2399,32 @@ class DotNetExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) - def mk_echo(msg, first = False): - echo_ex_qu = '' if IS_WINDOWS else '"' - echo_in_qu = '"' if IS_WINDOWS else '\\"' - echo_esc = '^' if IS_WINDOWS else '' - echo_dir = '>' if first else '>>' - - msg = msg.replace('"', echo_in_qu).replace('<', echo_esc + '<').replace('>', echo_esc + '>') - out.write('\t@echo %s%s%s %s %s\n' % (echo_ex_qu, msg, echo_ex_qu, echo_dir, proj_name)) - - out.write('\n') - mk_echo('', True) - mk_echo(' ') - mk_echo(' Exe') - mk_echo(' netcoreapp2.0') + proj_path = os.path.join(BUILD_DIR, proj_name) if VS_X64: platform = 'x64' elif VS_ARM: platform = 'ARM' else: platform = 'x86' - mk_echo(' %s' % platform) - mk_echo(' ') - mk_echo(' ') - mk_echo(' ' % self.to_ex_dir) - mk_echo(' ') - mk_echo(' Microsoft.Z3.dll') - mk_echo(' ') - mk_echo(' ') - mk_echo('') + dotnet_proj_str = """xemacs + + Exe + netcoreapp2.0 + %s + + + + + Microsoft.Z3.dll + + +""" % (platform, self.to_ex_dir) + + with open(proj_path, 'w') as ous: + ous.write(dotnet_proj_str) + + out.write('\n') dotnetCmdLine = [DOTNET, "build", proj_name] dotnetCmdLine.extend(['-c']) if DEBUG_MODE: From 690bd8502ab66ccae28a3d7538b7933930197e91 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 14 Nov 2018 13:47:46 -0800 Subject: [PATCH 10/27] Choose runtime for .NET core DLL. --- scripts/mk_util.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index aaeed1dea..c84b1c3a4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1888,6 +1888,15 @@ class DotNetCoreDLLComponent(Component): else: dotnetCmdLine.extend(['Release']) + if IS_WINDOWS: + runtime = "win-" + ("x64" if VS_X64 else "x86") + elif IS_LINUX: + runtime = "linux-x64" if LINUX_X64 else "" + elif IS_OSX: + runtime = "osx-x64" if LINUX_X64 else "" + if runtime != "": + dotnetCmdLine.extend(['-r', runtime]) + path = os.path.abspath(BUILD_DIR) dotnetCmdLine.extend(['-o', path]) From 1cc2cc01431e17e46be7b7bd89127dcbdd05e089 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 14:07:14 -0800 Subject: [PATCH 11/27] add TBD marker Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 63938caf9..be7132b75 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1839,6 +1839,7 @@ class DotNetCoreDLLComponent(Component): self.key_file = default_key_file def mk_pkg_config_file(self): + # TBD revise """ Create pkgconfig file for the dot net bindings. These are needed by Monodevelop. From c3725000182ef974e1e120c299adaa0377284dc9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 14:51:58 -0800 Subject: [PATCH 12/27] update for nuget/core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 103 ++++++++++++++++++++++++++------------------- 1 file changed, 60 insertions(+), 43 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4037b3996..bd455b95e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -562,6 +562,11 @@ def set_version(major, minor, build, revision): def get_version(): return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) +def get_version_string(n): + if n == 3: + return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD) + return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_REVISION) + def build_static_lib(): return STATIC_LIB @@ -1639,11 +1644,7 @@ class DotNetDLLComponent(Component): pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) substitutions = { 'PREFIX': PREFIX, 'GAC_PKG_NAME': self.gac_pkg_name(), - 'VERSION': "{}.{}.{}.{}".format( - VER_MAJOR, - VER_MINOR, - VER_BUILD, - VER_REVISION) + 'VERSION': get_version_string(4) } pkg_config_output = os.path.join(BUILD_DIR, self.build_dir, @@ -1838,30 +1839,14 @@ class DotNetCoreDLLComponent(Component): self.assembly_info_dir = assembly_info_dir self.key_file = default_key_file - def mk_pkg_config_file(self): + def mk_nuget_config_file(self): # TBD revise """ - Create pkgconfig file for the dot net bindings. These + Create nuget file for the dot net bindings. These are needed by Monodevelop. """ - pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) - substitutions = { 'PREFIX': PREFIX, - 'GAC_PKG_NAME': self.gac_pkg_name(), - 'VERSION': "{}.{}.{}.{}".format( - VER_MAJOR, - VER_MINOR, - VER_BUILD, - VER_REVISION) - } - pkg_config_output = os.path.join(BUILD_DIR, - self.build_dir, - '{}.pc'.format(self.gac_pkg_name())) - - # FIXME: Why isn't the build directory available? - mk_dir(os.path.dirname(pkg_config_output)) - # Configure file that will be installed by ``make install``. - configure_file(pkg_config_template, pkg_config_output, substitutions) - + return + def mk_makefile(self, out): global DOTNET_KEY_FILE if not is_dotnet_core_enabled(): @@ -1879,26 +1864,55 @@ class DotNetCoreDLLComponent(Component): out.write(cs_file) out.write('\n') - csproj = os.path.join(self.to_src_dir, "core", "core.csproj") + if VS_X64: + platform = 'x64' + elif VS_ARM: + platform = 'ARM' + else: + platform = 'x86' + + version = get_version_string(3) + + core_csproj_str = """ + + + netcoreapp1.0 + %s + $(DefineConstants);DOTNET_CORE + portable + Microsoft.Z3 + Library + Microsoft.Z3 + $(PackageTargetFallback);dnxcore50 + 1.0.4 + %s + true + Microsoft + Microsoft + Z3 is a satisfiability modulo theories solver from Microsoft Research. + © Microsoft Corporation. All rights reserved. + smt constraint solver theorem prover + + + + + + +""" % (platform, version, self.to_src_dir) + + mk_dir(os.path.join(BUILD_DIR, 'dotnet')) + csproj = os.path.join('dotnet', 'z3.csproj') + with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: + ous.write(core_csproj_str) + dotnetCmdLine = [DOTNET, "build", csproj] - # TBD: select build configurations also based on architecture - # Debug|x86, Debug|x64, Debug|arm - # Release|x86, Release|x64, Release|arm dotnetCmdLine.extend(['-c']) if DEBUG_MODE: dotnetCmdLine.extend(['Debug']) else: dotnetCmdLine.extend(['Release']) - if IS_WINDOWS: - runtime = "win-" + ("x64" if VS_X64 else "x86") - elif IS_LINUX: - runtime = "linux-x64" if LINUX_X64 else "" - elif IS_OSX: - runtime = "osx-x64" if LINUX_X64 else "" - if runtime != "": - dotnetCmdLine.extend(['-r', runtime]) path = os.path.abspath(BUILD_DIR) dotnetCmdLine.extend(['-o', path]) @@ -1911,8 +1925,8 @@ class DotNetCoreDLLComponent(Component): out.write('\n') out.write('%s: %s\n\n' % (self.name, dllfile)) - # Create pkg-config file - self.mk_pkg_config_file() + # Create nuget file + self.mk_nuget_config_file() return def main_component(self): @@ -1926,8 +1940,8 @@ class DotNetCoreDLLComponent(Component): mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) - shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), - '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) + shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), + '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) if DEBUG_MODE: shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) @@ -1937,8 +1951,8 @@ class DotNetCoreDLLComponent(Component): mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) - shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), - '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) + shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), + '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) def mk_install_deps(self, out): if not is_dotnet_core_enabled(): @@ -1949,6 +1963,7 @@ class DotNetCoreDLLComponent(Component): return "{}.Sharp".format(self.dll_name) def _install_or_uninstall_to_gac(self, out, install): + # TBD revise for nuget gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()), '/root', '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR) @@ -1967,6 +1982,7 @@ class DotNetCoreDLLComponent(Component): flags=' '.join(gacUtilFlags))) def mk_install(self, out): + # TBD revise for nuget if not is_dotnet_core_enabled(): return self._install_or_uninstall_to_gac(out, install=True) @@ -1978,6 +1994,7 @@ class DotNetCoreDLLComponent(Component): MakeRuleCmd.install_files(out, pkg_config_output, INSTALL_PKGCONFIG_DIR) def mk_uninstall(self, out): + # TBD revise for nuget if not is_dotnet_core_enabled(): return self._install_or_uninstall_to_gac(out, install=False) From 13d1ccfeaf9463f73740a964a9ab0ee042897ee9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 14:59:53 -0800 Subject: [PATCH 13/27] update for nuget/core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bd455b95e..2662d0933 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1890,7 +1890,7 @@ class DotNetCoreDLLComponent(Component): Microsoft Microsoft Z3 is a satisfiability modulo theories solver from Microsoft Research. - © Microsoft Corporation. All rights reserved. + Copyright Microsoft Corporation. All rights reserved. smt constraint solver theorem prover From 4f4463b2b71e58268a57a127a8fb8b0204b4ab2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 15:06:24 -0800 Subject: [PATCH 14/27] update for nuget/core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 2662d0933..1ac9abd0f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -456,6 +456,8 @@ def check_dotnet(): raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') def check_dotnet_core(): + if not IS_WINDOWS: + return r = exec_cmd([DOTNET, '--help']) if r != 0: raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities') From c6c4dc456379aa5c9fdede19226686444e579292 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 16:57:47 -0800 Subject: [PATCH 15/27] start script on assembling platform binaries to wrap with nuget install Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 62 +++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 scripts/mk_nuget_release.py diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py new file mode 100644 index 000000000..98a7c6362 --- /dev/null +++ b/scripts/mk_nuget_release.py @@ -0,0 +1,62 @@ +# +# Copyright (c) 2018 Microsoft Corporation +# + +# 1. download releases from github +# 2. copy over libz3.dll for the different architectures +# 3. copy over Microsoft.Z3.dll from suitable distribution +# 4. copy nuspec file from packages +# 5. call nuget pack + +import json +import os +import urllib.request +import zipfile +import sys +import os.path + +data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode()) + +version_str = data['tag_name'] + +def mk_dir(d): + if not os.path.exists(d): + os.makedirs(d) + +def download_installs(): + for asset in data['assets']: + url = asset['browser_download_url'] + name = asset['name'] + print("Downloading ", url) + sys.stdout.flush() + urllib.request.urlretrieve(url, "packages/%s" % name) + +os_names = ["ubuntu-14", "ubuntu-16", "win", "debian", "osx"] + +def unpack(): + for f in os.listdir("packages"): + if f.endswith("zip") and "x64" in f: + print(f) + # determine os from os_names + # instead of this string manipulation. + + name = os.path.splitext(f)[0] + os_name = name[name.find("x64")+4:] + os_name = os_name[:os_name.find("-")] + print(os_name) + + zip_ref = zipfile.ZipFile("packages/%s" % f, 'r') + path = "out/%s" % os_name + zip_ref.extract("%s/bin/libz3.so" % name) + + # unzip files in packages + pass + +def main(): + mk_dir("packages") +# download_installs() +# create_nuget_dir() + unpack() +# create_nuget_package() + +main() From 6a9c8a8999449439ec589ff9f6ee781151ee9d59 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 19:40:56 -0800 Subject: [PATCH 16/27] remove spurious string Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1ac9abd0f..9c5b0c9a9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2436,7 +2436,7 @@ class DotNetExampleComponent(ExampleComponent): else: platform = 'x86' - dotnet_proj_str = """xemacs + dotnet_proj_str = """ Exe netcoreapp2.0 From 03bb5a085facc26b4503d7dbc7c0efc289cab8a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 09:21:03 -0800 Subject: [PATCH 17/27] fix #1940 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 06f30cbdf..737213477 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -899,7 +899,7 @@ bool seq_decl_plugin::are_distinct(app* a, app* b) const { } if (is_app_of(a, m_family_id, OP_SEQ_UNIT) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) { - return true; + return m_manager->are_distinct(a->get_arg(0), b->get_arg(0)); } if (is_app_of(a, m_family_id, OP_SEQ_EMPTY) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) { From a85a612bae9e09e40981df809c06d97669b16073 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 10:03:43 -0800 Subject: [PATCH 18/27] use old-fashined C for test_capi Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 14e403826..dbcd0e82a 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -379,6 +379,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) Z3_sort t; Z3_symbol f_name, t_name; Z3_ast_vector q; + unsigned i; t = Z3_get_range(ctx, f); @@ -399,7 +400,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) 1, &t_name, &t, 1, &f_name, &f); printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q)); - for (unsigned i = 0; i < Z3_ast_vector_size(ctx, q); ++i) { + for (i = 0; i < Z3_ast_vector_size(ctx, q); ++i) { Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i)); } } @@ -1644,6 +1645,7 @@ void parser_example2() Z3_symbol names[2]; Z3_func_decl decls[2]; Z3_ast_vector f; + unsigned i; printf("\nparser_example2\n"); LOG_MSG("parser_example2"); @@ -1668,7 +1670,7 @@ void parser_example2() 2, names, decls); printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f)); printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f)); - for (unsigned i = 0; i < Z3_ast_vector_size(ctx, f); ++i) { + for (i = 0; i < Z3_ast_vector_size(ctx, f); ++i) { Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i)); } check(ctx, s, Z3_L_TRUE); From 8bfeca063d45a8bcefa9157b28a69bcd66d62b02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 10:36:27 -0800 Subject: [PATCH 19/27] update example build for dotnet core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9c5b0c9a9..ced57ab77 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2428,7 +2428,8 @@ class DotNetExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) - proj_path = os.path.join(BUILD_DIR, proj_name) + mk_dir(os.path.join(BUILD_DIR, 'dotnet_example')) + csproj = os.path.join('dotnet_example', proj_name) if VS_X64: platform = 'x64' elif VS_ARM: @@ -2443,18 +2444,18 @@ class DotNetExampleComponent(ExampleComponent): %s - + - Microsoft.Z3.dll + ..\Microsoft.Z3.dll """ % (platform, self.to_ex_dir) - with open(proj_path, 'w') as ous: + with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: ous.write(dotnet_proj_str) out.write('\n') - dotnetCmdLine = [DOTNET, "build", proj_name] + dotnetCmdLine = [DOTNET, "build", csproj] dotnetCmdLine.extend(['-c']) if DEBUG_MODE: dotnetCmdLine.extend(['Debug']) From bb5837791a21f9f7bd8e85b381e3dc36ec8c03ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 11:02:49 -0800 Subject: [PATCH 20/27] clean up dotnet core component Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 62 +++++----------------------------------------- 1 file changed, 6 insertions(+), 56 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ced57ab77..5bba2420a 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1829,7 +1829,7 @@ class DotNetDLLComponent(Component): MakeRuleCmd.remove_installed_files(out, pkg_config_file) -# TBD: retool the following for 'dotnet build' +# build for dotnet core class DotNetCoreDLLComponent(Component): def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file): Component.__init__(self, name, path, deps) @@ -1841,15 +1841,9 @@ class DotNetCoreDLLComponent(Component): self.assembly_info_dir = assembly_info_dir self.key_file = default_key_file - def mk_nuget_config_file(self): - # TBD revise - """ - Create nuget file for the dot net bindings. These - are needed by Monodevelop. - """ - return def mk_makefile(self, out): + # TBD: handle keyfile global DOTNET_KEY_FILE if not is_dotnet_core_enabled(): return @@ -1915,26 +1909,20 @@ class DotNetCoreDLLComponent(Component): else: dotnetCmdLine.extend(['Release']) - path = os.path.abspath(BUILD_DIR) dotnetCmdLine.extend(['-o', path]) - # Now emit the command line MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) - # State that the high-level "dotnet" target depends on the .NET bindings - # dll we just created the build rule for out.write('\n') out.write('%s: %s\n\n' % (self.name, dllfile)) - # Create nuget file - self.mk_nuget_config_file() - return def main_component(self): return is_dotnet_core_enabled() def has_assembly_info(self): + # TBD: is this required for dotnet core given that version numbers are in z3.csproj file? return True def mk_win_dist(self, build_path, dist_path): @@ -1957,51 +1945,13 @@ class DotNetCoreDLLComponent(Component): '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) def mk_install_deps(self, out): - if not is_dotnet_core_enabled(): - return - out.write('%s' % self.name) - - def gac_pkg_name(self): - return "{}.Sharp".format(self.dll_name) - - def _install_or_uninstall_to_gac(self, out, install): - # TBD revise for nuget - gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()), - '/root', - '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR) - ] - if install: - install_or_uninstall_flag = '-i' - else: - # Note need use ``-us`` here which takes an assembly file name - # rather than ``-u`` which takes an assembly display name (e.g. - # ) - install_or_uninstall_flag = '-us' - MakeRuleCmd.write_cmd(out, '{gacutil} {install_or_uninstall_flag} {assembly_name}.dll -f {flags}'.format( - gacutil=GACUTIL, - install_or_uninstall_flag=install_or_uninstall_flag, - assembly_name=self.dll_name, - flags=' '.join(gacUtilFlags))) + pass def mk_install(self, out): - # TBD revise for nuget - if not is_dotnet_core_enabled(): - return - self._install_or_uninstall_to_gac(out, install=True) - - # Install pkg-config file. Monodevelop needs this to find Z3 - pkg_config_output = os.path.join(self.build_dir, - '{}.pc'.format(self.gac_pkg_name())) - MakeRuleCmd.make_install_directory(out, INSTALL_PKGCONFIG_DIR) - MakeRuleCmd.install_files(out, pkg_config_output, INSTALL_PKGCONFIG_DIR) + pass def mk_uninstall(self, out): - # TBD revise for nuget - if not is_dotnet_core_enabled(): - return - self._install_or_uninstall_to_gac(out, install=False) - pkg_config_file = os.path.join('lib','pkgconfig','{}.pc'.format(self.gac_pkg_name())) - MakeRuleCmd.remove_installed_files(out, pkg_config_file) + pass class JavaDLLComponent(Component): def __init__(self, name, dll_name, package_name, manifest_file, path, deps): From becf5de8720b44c286e504050a018ef6c9b0efe9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 16:16:15 -0800 Subject: [PATCH 21/27] with Mathias on nuget package generation Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 93 ++++++++++++++++++++++++++++--------- scripts/mk_project.py | 5 +- 2 files changed, 76 insertions(+), 22 deletions(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 98a7c6362..1db75cd69 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -14,6 +14,10 @@ import urllib.request import zipfile import sys import os.path +import shutil +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()) @@ -27,36 +31,83 @@ 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) -os_names = ["ubuntu-14", "ubuntu-16", "win", "debian", "osx"] +os_info = {"ubuntu-14" : ('so', 'ubuntu.14.04-x64'), + 'ubuntu-16' : ('so', 'ubuntu.16.04-x64'), + 'win' : ('dll', 'win-x64'), + 'debian' : ('so', 'debian.8-x64') } +def classify_package(f): + for os_name in os_info: + if os_name in f: + ext, dst = os_info[os_name] + return os_name, f[:-4], ext, dst + return None + def unpack(): - for f in os.listdir("packages"): - if f.endswith("zip") and "x64" in f: - print(f) - # determine os from os_names - # instead of this string manipulation. - - name = os.path.splitext(f)[0] - os_name = name[name.find("x64")+4:] - os_name = os_name[:os_name.find("-")] - print(os_name) - - zip_ref = zipfile.ZipFile("packages/%s" % f, 'r') - path = "out/%s" % os_name - zip_ref.extract("%s/bin/libz3.so" % name) - # unzip files in packages - pass + # out + # +- runtimes + # +- win-x64 + # +- ubuntu.16.04-x64 + # +- ubuntu.14.04-x64 + # +- debian.8-x64 + # + + for f in os.listdir("packages"): + if f.endswith("zip") and "x64" in f and classify_package(f): + print(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) + if "win" in f: + mk_dir("out/lib/netstandard1.0/") + for b in ["Microsoft.Z3.dll"]: + zip_ref.extract("%s/bin/%s" % (package_dir, b), "tmp") + shutil.move("tmp/%s/bin/%s" % (package_dir, b), "out/lib/netstandard1.0/%s" % b) + +def create_nuget_spec(): + mk_project.init_version() + contents = """ + + + Microsoft.Z3.x64 + %s + Microsoft + Z3 is a satisfiability modulo theories solver from Microsoft Research. + Copyright 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 + https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt + + true + en + +""" + + with open("out/Microsoft.Z3.x64.nuspec", 'w') as f: + f.write(contents % mk_util.get_version_string(3)) + +def create_nuget_package(): + subprocess.call(["nuget", "pack"], cwd="out") def main(): mk_dir("packages") -# download_installs() -# create_nuget_dir() + #download_installs() unpack() -# create_nuget_package() - + create_nuget_spec() + create_nuget_package() + + main() diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 5bd96c0fc..e70a094a0 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -7,9 +7,12 @@ ############################################ from mk_util import * +def init_version(): + set_version(4, 8, 3, 0) + # Z3 Project definition def init_project_def(): - set_version(4, 8, 3, 0) + init_version() add_lib('util', [], includes2install = ['z3_version.h']) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) From 60d7444c965fa2c2481120dd25c29c1257f96f89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 16:16:38 -0800 Subject: [PATCH 22/27] build generated files outside of src Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 2 +- scripts/mk_util.py | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 98a7c6362..2b7734fe0 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -54,7 +54,7 @@ def unpack(): def main(): mk_dir("packages") -# download_installs() + download_installs() # create_nuget_dir() unpack() # create_nuget_package() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5bba2420a..7e405f42f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1909,7 +1909,7 @@ class DotNetCoreDLLComponent(Component): else: dotnetCmdLine.extend(['Release']) - path = os.path.abspath(BUILD_DIR) + path = os.path.join(os.path.abspath(BUILD_DIR), ".") dotnetCmdLine.extend(['-o', path]) MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine)) @@ -3170,7 +3170,8 @@ def mk_bindings(api_files): if is_dotnet_enabled(): dotnet_output_dir = get_component('dotnet').src_dir elif is_dotnet_core_enabled(): - dotnet_output_dir = get_component('dotnetcore').src_dir + dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet') + mk_dir(dotnet_output_dir) java_output_dir = None java_package_name = None if is_java_enabled(): @@ -3199,10 +3200,10 @@ def mk_bindings(api_files): mk_z3consts_ml(api_files) if is_dotnet_enabled(): check_dotnet() - mk_z3consts_dotnet(api_files) + mk_z3consts_dotnet(api_files, dotnet_output_dir) if is_dotnet_core_enabled(): check_dotnet_core() - mk_z3consts_dotnet(api_files) + mk_z3consts_dotnet(api_files, dotnet_output_dir) # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): @@ -3219,7 +3220,7 @@ def mk_z3consts_py(api_files): print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add .Net definitions -def mk_z3consts_dotnet(api_files): +def mk_z3consts_dotnet(api_files, output_dir): dotnet = get_component(DOTNET_COMPONENT) if not dotnet: dotnet = get_component(DOTNET_CORE_COMPONENT) @@ -3228,7 +3229,7 @@ def mk_z3consts_dotnet(api_files): api_file_c = dotnet.find_file(api_file, dotnet.name) api_file = os.path.join(api_file_c.src_dir, api_file) full_path_api_files.append(api_file) - generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir) + generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, output_dir) if VERBOSE: print("Generated '{}".format(generated_file)) From f4ced3c1647d1288d3dd0df8cf9e95b0d92c5f2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Nov 2018 16:40:35 -0800 Subject: [PATCH 23/27] use netstandard1.4 Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 4 ++-- scripts/mk_util.py | 3 +-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 2847f2884..09cfd2b7a 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -67,10 +67,10 @@ def unpack(): mk_dir("out/runtimes/%s" % dst) shutil.move("tmp/%s/bin/libz3.%s" % (package_dir, ext), "out/runtimes/%s/." % dst) if "win" in f: - mk_dir("out/lib/netstandard1.0/") + mk_dir("out/lib/netstandard1.4/") for b in ["Microsoft.Z3.dll"]: zip_ref.extract("%s/bin/%s" % (package_dir, b), "tmp") - shutil.move("tmp/%s/bin/%s" % (package_dir, b), "out/lib/netstandard1.0/%s" % b) + shutil.move("tmp/%s/bin/%s" % (package_dir, b), "out/lib/netstandard1.4/%s" % b) def create_nuget_spec(): mk_project.init_version() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 7e405f42f..790de530d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1872,14 +1872,13 @@ class DotNetCoreDLLComponent(Component): core_csproj_str = """ - netcoreapp1.0 + netstandard1.4 %s $(DefineConstants);DOTNET_CORE portable Microsoft.Z3 Library Microsoft.Z3 - $(PackageTargetFallback);dnxcore50 1.0.4 %s true From 5ebe342da14995fe8f89c99dd9cbbae008af5591 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Nov 2018 13:27:58 -0800 Subject: [PATCH 24/27] add support for keyfiles Signed-off-by: Nikolaj Bjorner --- scripts/mk_unix_dist.py | 6 +++++- scripts/mk_util.py | 42 +++++++++++++++++++++++++---------------- scripts/mk_win_dist.py | 2 +- 3 files changed, 32 insertions(+), 18 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 00cf3c706..06d87cd63 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -186,7 +186,11 @@ def mk_dist_dir(): build_path = BUILD_DIR dist_path = os.path.join(DIST_DIR, get_z3_name()) mk_dir(dist_path) - mk_util.DOTNET_ENABLED = DOTNET_ENABLED + name = get_z3_name() + if "x64" in name or "mac" in name: + mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED + else: + mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 790de530d..bb91df59b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -668,6 +668,7 @@ def display_help(exit_code): if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") print(" --optimize generate optimized code during linking.") + print(" --dotnetcore generate .NET platform bindings.") print(" --dotnet generate .NET bindings.") print(" --dotnet-key= sign the .NET assembly using the private key in .") print(" --java generate Java bindings.") @@ -1627,6 +1628,23 @@ class PythonInstallComponent(Component): def mk_makefile(self, out): return +def set_key_file(self): + global DOTNET_KEY_FILE + # We need to give the assembly a strong name so that it + # can be installed into the GAC with ``make install`` + if not DOTNET_KEY_FILE is None: + self.key_file = DOTNET_KEY_FILE + + if not self.key_file is None: + if os.path.isfile(self.key_file): + self.key_file = os.path.abspath(self.key_file) + elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): + self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) + else: + print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) + self.key_file = None + + class DotNetDLLComponent(Component): def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file): Component.__init__(self, name, path, deps) @@ -1688,19 +1706,7 @@ class DotNetDLLComponent(Component): ] ) - # We need to give the assembly a strong name so that it - # can be installed into the GAC with ``make install`` - if not DOTNET_KEY_FILE is None: - self.key_file = DOTNET_KEY_FILE - - if not self.key_file is None: - if os.path.isfile(self.key_file): - self.key_file = os.path.abspath(self.key_file) - elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): - self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) - else: - print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) - self.key_file = None + set_key_file(self) if not self.key_file is None: print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file)) @@ -1843,8 +1849,6 @@ class DotNetCoreDLLComponent(Component): def mk_makefile(self, out): - # TBD: handle keyfile - global DOTNET_KEY_FILE if not is_dotnet_core_enabled(): return cs_fp_files = [] @@ -1859,6 +1863,11 @@ class DotNetCoreDLLComponent(Component): out.write(' ') out.write(cs_file) out.write('\n') + + set_key_file(self) + key = "" + if not self.key_file is None: + key = "%s" % self.key_file if VS_X64: platform = 'x64' @@ -1887,13 +1896,14 @@ class DotNetCoreDLLComponent(Component): Z3 is a satisfiability modulo theories solver from Microsoft Research. Copyright Microsoft Corporation. All rights reserved. smt constraint solver theorem prover + %s -""" % (platform, version, self.to_src_dir) +""" % (platform, version, key, self.to_src_dir) mk_dir(os.path.join(BUILD_DIR, 'dotnet')) csproj = os.path.join('dotnet', 'z3.csproj') diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 9e0374192..10865676d 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -208,7 +208,7 @@ def mk_dist_dir(x64): build_path = BUILD_X86_DIR dist_path = os.path.join(DIST_DIR, get_z3_name(x64)) mk_dir(dist_path) - mk_util.DOTNET_ENABLED = DOTNET_ENABLED + mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED From cfb14c879a4cd063a17b06ca0d5ffe6a864bb5d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Nov 2018 13:59:00 -0800 Subject: [PATCH 25/27] make dotnet core dist optional Signed-off-by: Nikolaj Bjorner --- scripts/mk_unix_dist.py | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 06d87cd63..8e5336f67 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -23,6 +23,7 @@ VERBOSE=True DIST_DIR='dist' FORCE_MK=False DOTNET_ENABLED=True +DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False @@ -55,6 +56,7 @@ def display_help(): print(" -b , --build= subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).") print(" -f, --force force script to regenerate Makefiles.") print(" --nodotnet do not include .NET bindings in the binary distribution files.") + print(" --dotnetcore build for dotnet core.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") print(" --nopython do not include Python bindings in the binary distribution files.") @@ -88,6 +90,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--dotnetcore': + DOTNET_CORE_ENABLED = True elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': @@ -108,7 +112,11 @@ def check_build_dir(path): def mk_build_dir(path): if not check_build_dir(path) or FORCE_MK: opts = ["python", os.path.join('scripts', 'mk_make.py'), "-b", path, "--staticlib"] - if DOTNET_ENABLED: + if DOTNET_CORE_ENABLED: + opts.append('--dotnetcore') + if not DOTNET_KEY_FILE is None: + opts.append('--dotnet-key=' + DOTNET_KEY_FILE) + elif DOTNET_ENABLED: opts.append('--dotnet') if not DOTNET_KEY_FILE is None: opts.append('--dotnet-key=' + DOTNET_KEY_FILE) @@ -187,7 +195,7 @@ def mk_dist_dir(): dist_path = os.path.join(DIST_DIR, get_z3_name()) mk_dir(dist_path) name = get_z3_name() - if "x64" in name or "mac" in name: + if DOTNET_CORE_ENABLED: mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED else: mk_util.DOTNET_ENABLED = DOTNET_ENABLED From 1a5be0f25e0c8eb5c11e32eec979376fa03af214 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Nov 2018 15:14:43 -0800 Subject: [PATCH 26/27] make dotnet core dist optional Signed-off-by: Nikolaj Bjorner --- scripts/mk_unix_dist.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 8e5336f67..3e4456676 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -73,6 +73,7 @@ def parse_options(): 'force', 'nojava', 'nodotnet', + 'dotnetcore', 'dotnet-key=', 'githash', 'nopython' @@ -194,9 +195,8 @@ def mk_dist_dir(): build_path = BUILD_DIR dist_path = os.path.join(DIST_DIR, get_z3_name()) mk_dir(dist_path) - name = get_z3_name() if DOTNET_CORE_ENABLED: - mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED + mk_util.DOTNET_CORE_ENABLED = True else: mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE From 69dc74923908206f0a568ee89fd6cc1c8392802c Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 17 Nov 2018 21:02:00 +0700 Subject: [PATCH 27/27] Fix missing word in doc comment. --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e1359949d..be463b1b0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5579,7 +5579,7 @@ extern "C" { \brief Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically - converted to Booleans either, so the caller intends to + converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.