diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 73215580e..ddcd90cca 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -72,7 +72,7 @@ extern "C" { expr * const* no_ps = reinterpret_cast(no_patterns); pattern_validator v(mk_c(c)->m()); for (unsigned i = 0; i < num_patterns; i++) { - if (!v(num_decls, ps[i])) { + if (!v(num_decls, ps[i], 0, 0)) { SET_ERROR_CODE(Z3_INVALID_PATTERN); return 0; } diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp index d26190541..f50e8b339 100644 --- a/src/parsers/smt/smtparser.cpp +++ b/src/parsers/smt/smtparser.cpp @@ -1574,7 +1574,7 @@ private: } } expr * p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr())); - if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p))) { + if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) { set_error("invalid pattern", children[0]); return false; } @@ -1583,7 +1583,7 @@ private: else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) { app * sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr()); expr * p = m_manager.mk_pattern(1, &sk_hack); - if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p))) { + if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) { set_error("invalid pattern", children[0]); return false; } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 2e98a4072..a995c5917 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1605,7 +1605,7 @@ namespace smt2 { unsigned j = begin_pats; for (unsigned i = begin_pats; i < end_pats; i++) { expr * pat = pattern_stack().get(i); - if (!pat_validator()(num_decls, pat)) { + if (!pat_validator()(num_decls, pat, m_scanner.get_line(), m_scanner.get_pos())) { if (!ignore_bad_patterns()) throw parser_exception("invalid pattern"); continue; diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp index 3d59c2213..0e90e8126 100644 --- a/src/parsers/util/pattern_validation.cpp +++ b/src/parsers/util/pattern_validation.cpp @@ -31,16 +31,19 @@ struct pattern_validation_functor { bool m_found_a_var; family_id m_bfid; family_id m_lfid; + unsigned m_line, m_pos; pattern_validation_functor(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, - family_id bfid, family_id lfid): + family_id bfid, family_id lfid, unsigned line, unsigned pos): m_found_vars(found_vars), m_num_bindings(num_bindings), m_num_new_bindings(num_new_bindings), m_result(true), m_found_a_var(false), m_bfid(bfid), - m_lfid(lfid) { + m_lfid(lfid), + m_line(line), + m_pos(pos) { } bool is_forbidden(func_decl const * decl) { @@ -55,7 +58,7 @@ struct pattern_validation_functor { void operator()(app * n) { func_decl * decl = to_app(n)->get_decl(); if (is_forbidden(decl)) { - warning_msg("'%s' cannot be used in patterns.", decl->get_name().str().c_str()); + warning_msg("(%d,%d): '%s' cannot be used in patterns.", m_line, m_pos, decl->get_name().str().c_str()); m_result = false; } } @@ -63,7 +66,7 @@ struct pattern_validation_functor { void operator()(var * v) { unsigned idx = to_var(v)->get_idx(); if (idx >= m_num_bindings) { - warning_msg("free variables cannot be used in patterns."); + warning_msg("(%d,%d): free variables cannot be used in patterns.", m_line, m_pos); m_result = false; return; } @@ -76,30 +79,30 @@ struct pattern_validation_functor { void operator()(quantifier * q) { m_result = false; } }; -bool pattern_validator::process(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, expr * n) { +bool pattern_validator::process(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, expr * n, unsigned line, unsigned pos) { // I'm traversing the DAG as a tree, this is not a problem since pattern are supposed to be small ASTs. if (n->get_kind() == AST_VAR) { - warning_msg("invalid pattern: variable."); + warning_msg("(%d,%d): invalid pattern: variable.", line, pos); return false; } - pattern_validation_functor f(found_vars, num_bindings, num_new_bindings, m_bfid, m_lfid); + pattern_validation_functor f(found_vars, num_bindings, num_new_bindings, m_bfid, m_lfid, line, pos); for_each_expr(f, n); if (!f.m_result) return false; if (!f.m_found_a_var) { - warning_msg("pattern does not contain any variable."); + warning_msg("(%d,%d): pattern does not contain any variable.", line, pos); return false; } return true; } -bool pattern_validator::operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n) { +bool pattern_validator::operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n, unsigned line, unsigned pos) { uint_set found_vars; - if (!process(found_vars, num_bindings, num_new_bindings, n)) + if (!process(found_vars, num_bindings, num_new_bindings, n, line, pos)) return false; bool r = found_vars.num_elems() == num_new_bindings; if (!r) - warning_msg("pattern does not contain all quantified variables."); + warning_msg("(%d,%d): pattern does not contain all quantified variables.", line, pos); return r; } diff --git a/src/parsers/util/pattern_validation.h b/src/parsers/util/pattern_validation.h index 6c2ad73b7..939781936 100644 --- a/src/parsers/util/pattern_validation.h +++ b/src/parsers/util/pattern_validation.h @@ -27,7 +27,7 @@ class pattern_validator { family_id m_bfid; family_id m_lfid; - bool process(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, expr * n); + bool process(uint_set & found_vars, unsigned num_bindings, unsigned num_new_bindings, expr * n, unsigned line, unsigned pos); public: pattern_validator(ast_manager const & m): @@ -35,8 +35,8 @@ public: m_lfid(m.get_label_family_id()) { } - bool operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n); - bool operator()(unsigned num_new_bindings, expr * n) { return operator()(UINT_MAX, num_new_bindings, n); } + bool operator()(unsigned num_bindings, unsigned num_new_bindings, expr * n, unsigned line, unsigned pos); + bool operator()(unsigned num_new_bindings, expr * n, unsigned line, unsigned pos) { return operator()(UINT_MAX, num_new_bindings, n, line, pos); } }; #endif /* PATTERN_VALIDATION_H_ */