mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

detect overlapping signatures #1134

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-07 08:13:14 -07:00
parent 98391883ca
commit d06e48a361
2 changed files with 24 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/cmd_context/cmd_context.cpp
View file

@ -72,14 +72,34 @@ void func_decls::finalize(ast_manager & m) {
m_decls = 0;
}
bool func_decls::signatures_collide(func_decl* f, func_decl* g) const {
if (f == g) {
return true;
}
if (f->get_arity() != g->get_arity() || f->get_range() == g->get_range()) {
return false;
}
for (unsigned i = 0; i < f->get_arity(); ++i) {
if (f->get_domain(i) != g->get_domain(i))
return false;
}
// they have the same type arguments, but different range types.
return true;
}
bool func_decls::contains(func_decl * f) const {
if (GET_TAG(m_decls) == 0) {
return UNTAG(func_decl*, m_decls) == f;
func_decl* g = UNTAG(func_decl*, m_decls);
if (!g) return false;
return signatures_collide(f, g);
}
else {
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
return fs->contains(f);
for (func_decl* g : *fs) {
if (signatures_collide(f, g)) return true;
}
}
return false;
}
bool func_decls::insert(ast_manager & m, func_decl * f) {
@ -661,7 +681,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
msg += f->get_arity() == 0 ? "constant" : "function";
msg += " '";
msg += s.str();
msg += "' (with the given signature) already declared";
msg += "' (with the given signature) already declared with an overlapping signature";
throw cmd_exception(msg.c_str());
}
if (s != f->get_name()) {

1
src/cmd_context/cmd_context.h
View file

@ -42,6 +42,7 @@ Notes:
class func_decls {
func_decl * m_decls;
bool signatures_collide(func_decl* f, func_decl* g) const;
public:
func_decls():m_decls(0) {}
func_decls(ast_manager & m, func_decl * f);