From 9b4cf1559dd431a716b351b4d14105ea27efb263 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Nov 2018 15:33:46 -0800 Subject: [PATCH 1/6] 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 2/6] 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 3/6] 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 4/6] 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 5/6] 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 6/6] 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;