From 16ad33bf399d1b9aa1e333bbb89b560ffc868632 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jun 2016 18:15:51 -0700 Subject: [PATCH 1/5] add collection of statistics #652 Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/tactic/core/CMakeLists.txt | 1 + src/tactic/probe.cpp | 16 ++++++++-------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/contrib/cmake/src/tactic/core/CMakeLists.txt index ed3a84edf..fcd26bd84 100644 --- a/contrib/cmake/src/tactic/core/CMakeLists.txt +++ b/contrib/cmake/src/tactic/core/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(core_tactics blast_term_ite_tactic.cpp cofactor_elim_term_ite.cpp cofactor_term_ite_tactic.cpp + collect_statistics_tactic.cpp ctx_simplify_tactic.cpp der_tactic.cpp distribute_forall_tactic.cpp diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index ecc27eccf..677438cdf 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -287,14 +287,14 @@ struct is_non_qfbv_predicate { if (fid == m.get_basic_family_id()) return; if (fid == u.get_family_id()) { - if (n->get_decl_kind() == OP_BSDIV0 || - n->get_decl_kind() == OP_BUDIV0 || - n->get_decl_kind() == OP_BSREM0 || - n->get_decl_kind() == OP_BUREM0 || - n->get_decl_kind() == OP_BSMOD0) - throw found(); - return; - } + if (n->get_decl_kind() == OP_BSDIV0 || + n->get_decl_kind() == OP_BUDIV0 || + n->get_decl_kind() == OP_BSREM0 || + n->get_decl_kind() == OP_BUREM0 || + n->get_decl_kind() == OP_BSMOD0) + throw found(); + return; + } if (is_uninterp_const(n)) return; throw found(); From b11f9050e370376e43bd76f70ce5abb11da3ff6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jun 2016 18:20:25 -0700 Subject: [PATCH 2/5] fix bugs exposed from bad indentation warnings, #650 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_reachable_cache.cpp | 7 ++++++- src/smt/theory_fpa.cpp | 5 ++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/muz/pdr/pdr_reachable_cache.cpp b/src/muz/pdr/pdr_reachable_cache.cpp index 85100c19f..2bedc1393 100644 --- a/src/muz/pdr/pdr_reachable_cache.cpp +++ b/src/muz/pdr/pdr_reachable_cache.cpp @@ -109,7 +109,12 @@ namespace pdr { UNREACHABLE(); break; } - if (found) m_stats.m_hits++; m_stats.m_miss++; + if (found) { + m_stats.m_hits++; + } + else { + m_stats.m_miss++; + } return found; } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 8e96c925d..ee7559500 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -691,7 +691,10 @@ namespace smt { m_rw.reset(); m_th_rw.reset(); m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); - if (m_factory) dealloc(m_factory); m_factory = 0; + if (m_factory) { + dealloc(m_factory); + m_factory = 0; + } ast_manager & m = get_manager(); dec_ref_map_key_values(m, m_conversions); dec_ref_collection_values(m, m_is_added_to_model); From 3ea71b4b25739cae6fa432038c0251e75c2f0fdf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Jun 2016 12:49:48 +0100 Subject: [PATCH 3/5] Fixed SMT2 scanner to allow 0xFF characters. Thanks to Santiago Zanella-Beguelin for reporting this issue. --- src/parsers/smt2/smt2scanner.cpp | 25 +++++++++++++++---------- src/parsers/smt2/smt2scanner.h | 1 + 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 156cc2e5d..911f449dc 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -23,10 +23,12 @@ namespace smt2 { void scanner::next() { if (m_cache_input) - m_cache.push_back(m_curr); - SASSERT(m_curr != EOF); + m_cache.push_back(m_curr); + SASSERT(!m_at_eof); if (m_interactive) { m_curr = m_stream.get(); + if (m_stream.eof()) + m_at_eof = true; } else if (m_bpos < m_bend) { m_curr = m_buffer[m_bpos]; @@ -37,7 +39,7 @@ namespace smt2 { m_bend = static_cast(m_stream.gcount()); m_bpos = 0; if (m_bpos == m_bend) { - m_curr = EOF; + m_at_eof = true; } else { m_curr = m_buffer[m_bpos]; @@ -52,7 +54,7 @@ namespace smt2 { next(); while (true) { char c = curr(); - if (c == EOF) + if (m_at_eof) return; if (c == '\n') { new_line(); @@ -70,7 +72,7 @@ namespace smt2 { next(); while (true) { char c = curr(); - if (c == EOF) { + if (m_at_eof) { throw scanner_exception("unexpected end of quoted symbol", m_line, m_spos); } else if (c == '\n') { @@ -167,7 +169,7 @@ namespace smt2 { m_string.reset(); while (true) { char c = curr(); - if (c == EOF) + if (m_at_eof) throw scanner_exception("unexpected end of string", m_line, m_spos); if (c == '\n') { new_line(); @@ -237,10 +239,11 @@ namespace smt2 { } } - scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive): + scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) : m_interactive(interactive), m_spos(0), m_curr(0), // avoid Valgrind warning + m_at_eof(false), m_line(1), m_pos(0), m_bv_size(UINT_MAX), @@ -289,9 +292,13 @@ namespace smt2 { } scanner::token scanner::scan() { - while (true) { + while (true) { signed char c = curr(); m_pos = m_spos; + + if (m_at_eof) + return EOF_TOKEN; + switch (m_normalized[(unsigned char) c]) { case ' ': next(); @@ -327,8 +334,6 @@ namespace smt2 { return read_symbol(); else return read_signed_number(); - case -1: - return EOF_TOKEN; default: { scanner_exception ex("unexpected character", m_line, m_spos); next(); diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h index 8313c24df..3ad47dfb1 100644 --- a/src/parsers/smt2/smt2scanner.h +++ b/src/parsers/smt2/smt2scanner.h @@ -34,6 +34,7 @@ namespace smt2 { bool m_interactive; int m_spos; // position in the current line of the stream char m_curr; // current char; + bool m_at_eof; int m_line; // line int m_pos; // start position of the token From 9253ca9d863d8bcdac809593739c01348e5644b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jun 2016 08:10:10 -0700 Subject: [PATCH 4/5] make use of warning_msg safe for formatting. Thanks to Scott McPeak for reporting Signed-off-by: Nikolaj Bjorner --- src/api/api_config_params.cpp | 6 +++--- src/ast/ast.cpp | 2 +- src/ast/well_sorted.cpp | 2 +- src/muz/rel/dl_base.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 2 +- src/smt/theory_utvpi_def.h | 2 +- src/util/warning.cpp | 1 - 7 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 5b385a872..a04a9f12c 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -37,7 +37,7 @@ extern "C" { catch (z3_exception & ex) { // The error handler is only available for contexts // Just throw a warning. - warning_msg(ex.msg()); + warning_msg("%s", ex.msg()); } } @@ -62,7 +62,7 @@ extern "C" { catch (z3_exception & ex) { // The error handler is only available for contexts // Just throw a warning. - warning_msg(ex.msg()); + warning_msg("%s", ex.msg()); return Z3_FALSE; } } @@ -88,7 +88,7 @@ extern "C" { catch (z3_exception & ex) { // The error handler is only available for contexts // Just throw a warning. - warning_msg(ex.msg()); + warning_msg("%s", ex.msg()); } } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 507f75482..4e505f977 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1965,7 +1965,7 @@ bool ast_manager::check_sorts(ast const * n) const { return true; } catch (ast_exception & ex) { - warning_msg(ex.msg()); + warning_msg("%s", ex.msg()); return false; } } diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp index f9f04a2df..cb9ee3f61 100644 --- a/src/ast/well_sorted.cpp +++ b/src/ast/well_sorted.cpp @@ -66,7 +66,7 @@ struct well_sorted_proc { strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << "\n"; strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << "\n"; strm << "Function sort: " << mk_pp(decl, m_manager) << "."; - warning_msg(strm.str().c_str()); + warning_msg("%s", strm.str().c_str()); m_error = true; return; } diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index b7f4d6cef..f79f6c8eb 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -391,7 +391,7 @@ namespace datalog { std::ostringstream buffer; buffer << "creating large table of size " << upper_bound; if (p) buffer << " for relation " << p->get_name(); - warning_msg(buffer.str().c_str()); + warning_msg("%s", buffer.str().c_str()); } for(table_element i = 0; i < upper_bound; i++) { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 17a931cc3..00f63afd5 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1034,7 +1034,7 @@ namespace smt2 { else { std::ostringstream str; str << "unknown attribute " << id; - warning_msg(str.str().c_str()); + warning_msg("%s", str.str().c_str()); next(); // just consume the consume_sexpr(); diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index d5ed4e825..ff295d5a3 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -250,7 +250,7 @@ namespace smt { std::stringstream msg; msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n"; TRACE("utvpi", tout << msg.str();); - warning_msg(msg.str().c_str()); + warning_msg("%s", msg.str().c_str()); get_context().push_trail(value_trail(m_non_utvpi_exprs)); m_non_utvpi_exprs = true; } diff --git a/src/util/warning.cpp b/src/util/warning.cpp index 1105a12f7..ed4cd8725 100644 --- a/src/util/warning.cpp +++ b/src/util/warning.cpp @@ -167,4 +167,3 @@ void warning_msg(const char * msg, ...) { va_end(args); } } - From bfe26390f01665c48f1cb2e9a297432bd0e06eba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jun 2016 08:12:32 -0700 Subject: [PATCH 5/5] fix bug introduced when hiding unused variables in 96e157e, reported by Mikolas Janota Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_trailing.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index cf50ab0e2..31e9121ec 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -67,10 +67,8 @@ struct bv_trailing::imp { } expr_ref out1(m); expr_ref out2(m); - DEBUG_CODE( - const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH); - const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH); - SASSERT(rm1 == min && rm2 == min);); + VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH)); + VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH)); const bool are_eq = m.are_equal(out1, out2); result = are_eq ? m.mk_true() : m.mk_eq(out1, out2); return are_eq ? BR_DONE : BR_REWRITE2;