improve efficiency of vcgen of large float exprs
MODIFY
ir/type.cpp
ir/type.cpp
@@ -442,7 +442,7 @@ bool FloatType::isNaNInt(const expr &e) const {
unsigned h, l;
bool ok = sign.isExtract(nan, h, l) && fraction.isExtract(nan2, h, l) &&
nan.eq(nan2);
- auto nan_name = nan.str();
+ auto nan_name = nan.fn_name();
ok &= string_view(nan_name).substr(0, 4) == "NaN!";
return ok && exponent.isAllOnes();

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1564,8 +1564,10 @@ string expr::numeral_string() const {
return Z3_get_numeral_decimal_string(ctx(), ast(), 12);
}
-string expr::str() const {
- return isValid() ? Z3_ast_to_string(ctx(), ast()) : "(null)";
+string expr::fn_name() const {
+ if (isApp())
+ return Z3_get_symbol_string(ctx(), Z3_get_decl_name(ctx(), decl()));
+ return "";
}
ostream& operator<<(ostream &os, const expr &e) {

MODIFY
smt/expr.h
smt/expr.h
@@ -289,7 +289,7 @@ public:
void printSigned(std::ostream &os) const;
void printHexadecimal(std::ostream &os) const;
std::string numeral_string() const;
- std::string str() const;
+ std::string fn_name() const; // empty if not a function
friend std::ostream &operator<<(std::ostream &os, const expr &e);
// for container use only

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -72,7 +72,7 @@ static void print_single_varval(ostream &os, State &st, const Model &m,
// needed, not because it's undef
bool found_undef = false;
for (auto &var : partial.vars()) {
- auto name = var.str();
+ auto name = var.fn_name();
found_undef |= string_view(name).substr(0, 6) == "undef!";
}
if (found_undef)

improve efficiency of vcgen of large float exprs