mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add line/pos information for pattern warnings. Issue #607
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
69ccc02931
commit
6f5785338a
|
@ -72,7 +72,7 @@ extern "C" {
|
|||
expr * const* no_ps = reinterpret_cast<expr * const*>(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;
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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_ */
|
||||
|
|
Loading…
Reference in a new issue