mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
revert update to #1134
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d06e48a361
commit
ea331ebfbe
|
@ -73,25 +73,13 @@ void func_decls::finalize(ast_manager & m) {
|
|||
}
|
||||
|
||||
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;
|
||||
return f == g;
|
||||
}
|
||||
|
||||
bool func_decls::contains(func_decl * f) const {
|
||||
if (GET_TAG(m_decls) == 0) {
|
||||
func_decl* g = UNTAG(func_decl*, m_decls);
|
||||
if (!g) return false;
|
||||
return signatures_collide(f, g);
|
||||
return g && signatures_collide(f, g);
|
||||
}
|
||||
else {
|
||||
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
|
||||
|
@ -681,7 +669,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 with an overlapping signature";
|
||||
msg += "' (with the given signature) already declared";
|
||||
throw cmd_exception(msg.c_str());
|
||||
}
|
||||
if (s != f->get_name()) {
|
||||
|
|
Loading…
Reference in a new issue