mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

Relaxed BV type checking, follow up to issue #116

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 12:46:30 +01:00
parent c7fd74e8ad
commit 17c06199a8
1 changed files with 22 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/bv_decl_plugin.cpp
View file

@ -501,9 +501,13 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
func_decl * r = mk_func_decl(k, bv_size); func_decl * r = mk_func_decl(k, bv_size);
if (r != 0) { if (r != 0) {
if (arity != r->get_arity()) { if (arity != r->get_arity()) {
if (r->get_info()->is_associative())
arity = r->get_arity();
else {
m_manager->raise_exception("declared arity mismatches supplied arity"); m_manager->raise_exception("declared arity mismatches supplied arity");
return 0; return 0;
} }
}
for (unsigned i = 0; i < arity; ++i) { for (unsigned i = 0; i < arity; ++i) {
if (domain[i] != r->get_domain(i)) { if (domain[i] != r->get_domain(i)) {
m_manager->raise_exception("declared sorts do not match supplied sorts"); m_manager->raise_exception("declared sorts do not match supplied sorts");
@ -596,9 +600,21 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
func_decl * r = mk_func_decl(k, bv_size); func_decl * r = mk_func_decl(k, bv_size);
if (r != 0) { if (r != 0) {
if (num_args != r->get_arity()) { if (num_args != r->get_arity()) {
if (r->get_info()->is_associative()) {
sort * fs = r->get_domain(0);
for (unsigned i = 0; i < num_args; ++i) {
if (m.get_sort(args[i]) != fs) {
m_manager->raise_exception("declared sorts do not match supplied sorts");
return 0;
}
}
return r;
}
else {
m.raise_exception("declared arity mismatches supplied arity"); m.raise_exception("declared arity mismatches supplied arity");
return 0; return 0;
} }
}
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
if (m.get_sort(args[i]) != r->get_domain(i)) { if (m.get_sort(args[i]) != r->get_domain(i)) {
std::ostringstream buffer; std::ostringstream buffer;