diff --git a/src/cegis/cegis-util/type_helper.cpp b/src/cegis/cegis-util/type_helper.cpp index 68e4dc8439d..a4ea0e84cf1 100644 --- a/src/cegis/cegis-util/type_helper.cpp +++ b/src/cegis/cegis-util/type_helper.cpp @@ -16,12 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com #include -const typet &replace_struct_by_symbol_type(const symbol_tablet &st, - const typet &type) +const typet &replace_struct_by_symbol_type( + const symbol_tablet &st, + const typet &type) { const irep_idt &type_id=type.id(); - if(ID_struct != type_id && ID_incomplete_struct != type_id - && ID_union != type_id && ID_incomplete_union != type_id) return type; + if(type_id!=ID_struct && type_id!=ID_incomplete_struct && + type_id!=ID_union && type_id!=ID_incomplete_union) + { + return type; + } std::string tag(TAG_PREFIX); tag+=id2string(to_struct_union_type(type).get_tag()); return st.lookup(tag).type; @@ -31,16 +35,20 @@ namespace { bool instanceof(const typet &lhs, const typet &rhs, const namespacet &ns) { - if(type_eq(lhs, rhs, ns)) return true; - assert(ID_class == lhs.id()); - const class_typet &lhs_class=to_class_type(lhs); - const class_typet::basest &bases=lhs_class.bases(); - for(const exprt &base : bases) + if(type_eq(lhs, rhs, ns)) { - const typet &type=base.type(); - if (instanceof(ns.follow(type), rhs, ns)) return true; + return true; } - return false; + assert(ID_class==lhs.id()); + const class_typet &lhs_class=to_class_type(lhs); + const class_typet::basest &bases=lhs_class.bases(); + return std::any_of( + std::begin(bases), + std::end(bases), + [&](const exprt &base) + { + return instanceof(ns.follow(base.type()), rhs, ns); + }); } } @@ -49,22 +57,32 @@ bool instanceof(const symbol_tablet &st, const typet &lhs, const typet &rhs) const namespacet ns(st); const typet &resolved_lhs=ns.follow(lhs); const typet &resolved_rhs=ns.follow(rhs); - if(ID_class != resolved_lhs.id() || ID_class != resolved_rhs.id()) + if(ID_class!=resolved_lhs.id() || ID_class!=resolved_rhs.id()) + { return type_eq(resolved_lhs, resolved_rhs, ns); + } return instanceof(resolved_lhs, resolved_rhs, ns); } -instanceof_anyt::instanceof_anyt(const symbol_tablet &st, - const std::set &types) : - st(st), types(types) +instanceof_anyt::instanceof_anyt( + const symbol_tablet &st, + const std::set &types): + st(st), + types(types) { } -bool instanceof_anyt::operator ()(const typet &type) const +bool instanceof_anyt::operator()(const typet &type) const { - if(types.empty()) return true; - return types.end() - != std::find_if(types.begin(), types.end(), - [this, &type](const typet &rhs) - { return instanceof(st, type, rhs);}); + if(types.empty()) + { + return true; + } + return types.end()!=std::find_if( + types.begin(), + types.end(), + [this, &type](const typet &rhs) + { + return instanceof(st, type, rhs); + }); }