From b2d5c24c1df440b653bd6a31955849545a8bf6ad Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Dec 2023 16:55:09 +0000 Subject: [PATCH 1/5] remove a few string copies --- src/api/api_ast.cpp | 6 ++---- src/api/api_ast_map.cpp | 4 ++-- src/api/api_context.cpp | 6 +++--- src/api/api_fpa.cpp | 4 ++-- src/api/api_goal.cpp | 4 ++-- src/api/api_model.cpp | 4 ++-- src/api/api_numeral.cpp | 10 +++++----- src/api/api_solver.cpp | 16 ++++++++-------- src/ast/ast_pp.h | 4 ++-- src/ast/rewriter/pb_rewriter.cpp | 8 ++------ src/ast/well_sorted.cpp | 3 +-- src/math/lp/numeric_pair.h | 1 - src/model/model_smt2_pp.cpp | 6 ++---- src/sat/sat_cutset.cpp | 2 +- src/sat/sat_solver.cpp | 2 +- src/smt/smt_context_pp.cpp | 4 ++-- src/util/sstream.h | 31 ------------------------------- src/util/zstring.cpp | 4 ++-- 18 files changed, 39 insertions(+), 80 deletions(-) delete mode 100644 src/util/sstream.h diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index dfe47b8b5..424b361f3 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -146,8 +146,7 @@ extern "C" { ast_manager& m = mk_c(c)->m(); recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin(); if (!p.has_def(d)) { - std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl"; - SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str()); + SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl"); return; } expr_ref abs_body(m); @@ -168,8 +167,7 @@ extern "C" { return; } if (!pd.get_def()->get_cases().empty()) { - std::string msg = "function " + mk_pp(d, m) + " has already been given a definition"; - SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str()); + SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " has already been given a definition"); return; } diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp index 5976d0e41..523ba1f59 100644 --- a/src/api/api_ast_map.cpp +++ b/src/api/api_ast_map.cpp @@ -160,8 +160,8 @@ extern "C" { for (; it != end; ++it) { buffer << "\n (" << mk_ismt2_pp(it->m_key, mng, 3) << "\n " << mk_ismt2_pp(it->m_value, mng, 3) << ")"; } - buffer << ")"; - return mk_c(c)->mk_external_string(buffer.str()); + buffer << ')'; + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 66cd715c9..344224dd3 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -338,12 +338,12 @@ namespace api { std::ostringstream buffer; app * a = to_app(n); buffer << mk_pp(a->get_decl(), m()) << " applied to: "; - if (a->get_num_args() > 1) buffer << "\n"; + if (a->get_num_args() > 1) buffer << '\n'; for (unsigned i = 0; i < a->get_num_args(); ++i) { buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort "; - buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << "\n"; + buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << '\n'; } - auto str = buffer.str(); + auto str = std::move(buffer).str(); warning_msg("%s", str.c_str()); break; } diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index aeb075e45..3c350ed18 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1022,7 +1022,7 @@ extern "C" { if (mpfm.is_inf(val)) mpqm.set(q, 0); std::stringstream ss; mpqm.display_decimal(ss, q, sbits); - return mk_c(c)->mk_external_string(ss.str()); + return mk_c(c)->mk_external_string(std::move(ss).str()); Z3_CATCH_RETURN(""); } @@ -1100,7 +1100,7 @@ extern "C" { } std::stringstream ss; ss << exp; - return mk_c(c)->mk_external_string(ss.str()); + return mk_c(c)->mk_external_string(std::move(ss).str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index cfe0974df..cbb67f2a2 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -185,7 +185,7 @@ extern "C" { std::ostringstream buffer; to_goal_ref(g)->display(buffer); // Hack for removing the trailing '\n' - std::string result = buffer.str(); + std::string result = std::move(buffer).str(); SASSERT(result.size() > 0); result.resize(result.size()-1); return mk_c(c)->mk_external_string(std::move(result)); @@ -203,7 +203,7 @@ extern "C" { } to_goal_ref(g)->display_dimacs(buffer, include_names); // Hack for removing the trailing '\n' - std::string result = buffer.str(); + std::string result = std::move(buffer).str(); SASSERT(result.size() > 0); result.resize(result.size()-1); return mk_c(c)->mk_external_string(std::move(result)); diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 3512b4b05..e449cb0ea 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -432,14 +432,14 @@ extern "C" { if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) { model_smt2_pp(buffer, mk_c(c)->m(), *(to_model_ref(m)), 0); // Hack for removing the trailing '\n' - result = buffer.str(); + result = std::move(buffer).str(); if (!result.empty()) result.resize(result.size()-1); } else { model_params p; model_v2_pp(buffer, *(to_model_ref(m)), p.partial()); - result = buffer.str(); + result = std::move(buffer).str(); } return mk_c(c)->mk_external_string(std::move(result)); Z3_CATCH_RETURN(nullptr); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index ebac4de31..98dceffb7 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -189,7 +189,7 @@ extern "C" { if (ok && r.is_int() && !r.is_neg()) { std::stringstream strm; r.display_bin(strm, r.get_num_bits()); - return mk_c(c)->mk_external_string(strm.str()); + return mk_c(c)->mk_external_string(std::move(strm).str()); } else { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); @@ -237,7 +237,7 @@ extern "C" { else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) { std::ostringstream buffer; fu.fm().display_smt2(buffer, tmp, false); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); } else { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); @@ -288,21 +288,21 @@ extern "C" { if (u.is_numeral(e, r) && !r.is_int()) { std::ostringstream buffer; r.display_decimal(buffer, precision); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); } if (u.is_irrational_algebraic_numeral(e)) { algebraic_numbers::anum const & n = u.to_irrational_algebraic_numeral(e); algebraic_numbers::manager & am = u.am(); std::ostringstream buffer; am.display_decimal(buffer, n, precision); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); } else if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) return Z3_get_numeral_string(c, a); else if (mk_c(c)->fpautil().is_numeral(to_expr(a), ftmp)) { std::ostringstream buffer; fu.fm().display_decimal(buffer, ftmp, 12); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); } else if (Z3_get_numeral_rational(c, a, r)) { return mk_c(c)->mk_external_string(r.to_string()); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 953167fe9..ac100ee30 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -170,8 +170,8 @@ extern "C" { if (g_is_threaded || g_thread_id != std::this_thread::get_id()) { g_is_threaded = true; std::ostringstream strm; - strm << smt2log << "-" << std::this_thread::get_id(); - smt2log = symbol(strm.str()); + strm << smt2log << '-' << std::this_thread::get_id(); + smt2log = symbol(std::move(strm).str()); } to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str()); } @@ -208,7 +208,7 @@ extern "C" { if (!smt_logics::supported_logic(to_symbol(logic))) { std::ostringstream strm; strm << "logic '" << to_symbol(logic) << "' is not recognized"; - SET_ERROR_CODE(Z3_INVALID_ARG, strm.str()); + SET_ERROR_CODE(Z3_INVALID_ARG, std::move(strm).str()); RETURN_Z3(nullptr); } else { @@ -306,7 +306,7 @@ extern "C" { if (!parse_smt2_commands(*ctx.get(), is)) { ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(errstrm).str()); return; } @@ -333,7 +333,7 @@ extern "C" { std::stringstream err; sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); if (!parse_dimacs(is, err, solver)) { - SET_ERROR_CODE(Z3_PARSER_ERROR, err.str()); + SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(err).str()); return; } sat2goal s2g; @@ -400,7 +400,7 @@ extern "C" { if (!initialized) to_solver(s)->m_solver = nullptr; descrs.display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -799,7 +799,7 @@ extern "C" { init_solver(c, s); std::ostringstream buffer; to_solver_ref(s)->display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } @@ -810,7 +810,7 @@ extern "C" { init_solver(c, s); std::ostringstream buffer; to_solver_ref(s)->display_dimacs(buffer, include_names); - return mk_c(c)->mk_external_string(buffer.str()); + return mk_c(c)->mk_external_string(std::move(buffer).str()); Z3_CATCH_RETURN(""); } diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h index 7ccb8ec15..1f20ce300 100644 --- a/src/ast/ast_pp.h +++ b/src/ast/ast_pp.h @@ -58,13 +58,13 @@ inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) { inline std::string operator+(char const* s, mk_pp const& pp) { std::ostringstream strm; strm << s << pp; - return strm.str(); + return std::move(strm).str(); } inline std::string operator+(std::string const& s, mk_pp const& pp) { std::ostringstream strm; strm << s << pp; - return strm.str(); + return std::move(strm).str(); } inline std::string& operator+=(std::string& s, mk_pp const& pp) { diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 2f06710ff..4f1fe3fd1 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -157,9 +157,7 @@ expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) { continue; } - std::ostringstream strm; - strm << 'x' << i; - name = symbol(strm.str()); + name = symbol('x' + std::to_string(i)); trail.push_back(m.mk_const(name, a.mk_int())); expr* x = trail.back(); m.is_not(e,e); @@ -188,9 +186,7 @@ void pb_rewriter::validate_rewrite(func_decl* f, unsigned sz, expr*const* args, } void pb_rewriter::dump_pb_rewrite(expr* fml) { - std::ostringstream strm; - strm << "pb_rewrite_" << (s_lemma++) << ".smt2"; - std::ofstream out(strm.str()); + std::ofstream out("pb_rewrite_" + std::to_string(s_lemma++) + ".smt2"); ast_smt_pp pp(m()); pp.display_smt2(out, fml); out.close(); diff --git a/src/ast/well_sorted.cpp b/src/ast/well_sorted.cpp index fa8e2768b..84cdf28ad 100644 --- a/src/ast/well_sorted.cpp +++ b/src/ast/well_sorted.cpp @@ -70,8 +70,7 @@ struct well_sorted_proc { strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << '\n'; strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << '\n'; strm << "Function sort: " << mk_pp(decl, m_manager) << '.'; - auto str = strm.str(); - warning_msg("%s", str.c_str()); + warning_msg("%s", std::move(strm).str().c_str()); m_error = true; return; } diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h index 251274006..93780f7be 100644 --- a/src/math/lp/numeric_pair.h +++ b/src/math/lp/numeric_pair.h @@ -24,7 +24,6 @@ #include #ifdef lp_for_z3 #include "util/rational.h" -#include "util/sstream.h" #include "util/z3_exception.h" #else // include "util/numerics/mpq.h" diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index b5ac3fbad..89ea98075 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -68,7 +68,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod buffer << " "; } buffer << "\n-----------"; - std::string buffer_str = buffer.str(); + std::string buffer_str = std::move(buffer).str(); unsigned len = static_cast(buffer_str.length()); pp_indent(out, indent); out << ";; "; @@ -206,9 +206,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co if (f_i->is_partial()) { body = mk_string(m, "#unspecified"); for (unsigned j = 0; j < f->get_arity(); j++) { - std::stringstream strm; - strm << "x!" << (j+1); - var_names.push_back(symbol(strm.str())); + var_names.push_back(symbol("x!" + std::to_string(j+1))); } } else { diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp index aae9bf1ab..2d31bcf14 100644 --- a/src/sat/sat_cutset.cpp +++ b/src/sat/sat_cutset.cpp @@ -273,7 +273,7 @@ namespace sat { std::string cut::table2string(unsigned num_input, uint64_t table) { std::ostringstream strm; display_table(strm, num_input, table); - return strm.str(); + return std::move(strm).str(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a1b88bed1..2d2962940 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2280,7 +2280,7 @@ namespace sat { << std::setw(4) << m_stats.m_restart << mk_stat(*this) << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n"; - std::string str(strm.str()); + std::string str = std::move(strm).str(); svector nums; for (size_t i = 0; i < str.size(); ++i) { while (i < str.size() && str[i] != ' ') ++i; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 3925a4e21..4842f6e23 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -510,7 +510,7 @@ namespace smt { #else strm << "lemma_" << (++m_lemma_id) << ".smt2"; #endif - return strm.str(); + return std::move(strm).str(); } @@ -722,7 +722,7 @@ namespace smt { << std::setw(4) << m_stats.m_num_del_clauses << " " << std::setw(7) << mem_stat() << ")\n"; - std::string str(strm.str()); + std::string str = std::move(strm).str(); svector offsets; for (size_t i = 0; i < str.size(); ++i) { while (i < str.size() && str[i] != ' ') ++i; diff --git a/src/util/sstream.h b/src/util/sstream.h deleted file mode 100644 index fba13c5d5..000000000 --- a/src/util/sstream.h +++ /dev/null @@ -1,31 +0,0 @@ -/* -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - nat_set.h - -Abstract: - - Wrapper for sstream. - -Author: - - Leonardo de Moura (leonardo) 2013 - -Revision History: - -*/ -#pragma once -#include -#include - -namespace lean { -/** \brief Wrapper for std::ostringstream */ -class sstream { - std::ostringstream m_strm; -public: - std::string str() const { return m_strm.str(); } - template sstream & operator<<(T const & t) { m_strm << t; return *this; } -}; -} diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index eaa5bb5ee..8e08820f6 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -152,7 +152,7 @@ std::string zstring::encode() const { unsigned ch = m_buffer[i]; if (ch < 32 || ch >= 128 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) { _flush(); - strm << "\\u{" << std::hex << ch << std::dec << "}"; + strm << "\\u{" << std::hex << ch << std::dec << '}'; } else { if (offset == 99) @@ -161,7 +161,7 @@ std::string zstring::encode() const { } } _flush(); - return strm.str(); + return std::move(strm).str(); } bool zstring::suffixof(zstring const& other) const { From 4898a156d8fcc2a627e82778fae6b55437f829f7 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Dec 2023 16:58:45 +0000 Subject: [PATCH 2/5] shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0 --- src/ast/ast.cpp | 33 ++++++--------------------------- src/ast/ast.h | 17 +++++++---------- 2 files changed, 13 insertions(+), 37 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 6ea293b57..f3be7d2c6 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -319,26 +319,6 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain, // // ----------------------------------- -static app_flags mk_const_flags() { - app_flags r; - r.m_depth = 1; - r.m_ground = true; - r.m_has_quantifiers = false; - r.m_has_labels = false; - return r; -} - -static app_flags mk_default_app_flags() { - app_flags r; - r.m_depth = 1; - r.m_ground = true; - r.m_has_quantifiers = false; - r.m_has_labels = false; - return r; -} - -app_flags app::g_constant_flags = mk_const_flags(); - app::app(func_decl * decl, unsigned num_args, expr * const * args): expr(AST_APP), m_decl(decl), @@ -1762,8 +1742,7 @@ ast * ast_manager::register_node_core(ast * n) { inc_ref(t->get_decl()); unsigned num_args = t->get_num_args(); if (num_args > 0) { - app_flags * f = t->flags(); - *f = mk_default_app_flags(); + app_flags * f = &t->m_flags; SASSERT(t->is_ground()); SASSERT(!t->has_quantifiers()); SASSERT(!t->has_labels()); @@ -1776,13 +1755,13 @@ ast * ast_manager::register_node_core(ast * n) { unsigned arg_depth = 0; switch (arg->get_kind()) { case AST_APP: { - app_flags * arg_flags = to_app(arg)->flags(); - arg_depth = arg_flags->m_depth; - if (arg_flags->m_has_quantifiers) + app *app = to_app(arg); + arg_depth = app->get_depth(); + if (app->has_quantifiers()) f->m_has_quantifiers = true; - if (arg_flags->m_has_labels) + if (app->has_labels()) f->m_has_labels = true; - if (!arg_flags->m_ground) + if (!app->is_ground()) f->m_ground = false; break; } diff --git a/src/ast/ast.h b/src/ast/ast.h index b4b3b1b2f..9618c7e12 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -704,6 +704,7 @@ struct app_flags { unsigned m_ground:1; // application does not have free variables or nested quantifiers. unsigned m_has_quantifiers:1; // application has nested quantifiers. unsigned m_has_labels:1; // application has nested labels. + app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {} }; class app : public expr { @@ -711,19 +712,15 @@ class app : public expr { func_decl * m_decl; unsigned m_num_args; + app_flags m_flags; expr * m_args[0]; - static app_flags g_constant_flags; - - // remark: store term depth in the end of the app. the depth is only stored if the num_args > 0 static unsigned get_obj_size(unsigned num_args) { - return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags); + return sizeof(app) + num_args * sizeof(expr *); } friend class tmp_app; - app_flags * flags() const { return m_num_args == 0 ? &g_constant_flags : reinterpret_cast(const_cast(m_args + m_num_args)); } - app(func_decl * decl, unsigned num_args, expr * const * args); public: func_decl * get_decl() const { return m_decl; } @@ -744,10 +741,10 @@ public: expr * const * end() const { return m_args + m_num_args; } sort * _get_sort() const { return get_decl()->get_range(); } - unsigned get_depth() const { return flags()->m_depth; } - bool is_ground() const { return flags()->m_ground; } - bool has_quantifiers() const { return flags()->m_has_quantifiers; } - bool has_labels() const { return flags()->m_has_labels; } + unsigned get_depth() const { return m_flags.m_depth; } + bool is_ground() const { return m_flags.m_ground; } + bool has_quantifiers() const { return m_flags.m_has_quantifiers; } + bool has_labels() const { return m_flags.m_has_labels; } }; // ----------------------------------- From c9c53b7c6501c7ccd4657353061fbef05aa411b7 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Dec 2023 18:19:20 +0000 Subject: [PATCH 3/5] tmp_enode: don't heap allocate an app. store it inline instead. Saves heap allocations and double indirections --- src/ast/ast.h | 4 ++++ src/smt/smt_enode.cpp | 18 ++++-------------- src/smt/smt_enode.h | 3 +-- 3 files changed, 9 insertions(+), 16 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 9618c7e12..a42d894ae 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -707,6 +707,8 @@ struct app_flags { app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {} }; +namespace smt { class tmp_enode; } + class app : public expr { friend class ast_manager; @@ -720,8 +722,10 @@ class app : public expr { } friend class tmp_app; + friend class smt::tmp_enode; app(func_decl * decl, unsigned num_args, expr * const * args); + app() : expr(AST_APP) {} public: func_decl * get_decl() const { return m_decl; } family_id get_family_id() const { return get_decl()->get_family_id(); } diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 86b83af4c..4bcb4a41c 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -327,7 +327,6 @@ namespace smt { } tmp_enode::tmp_enode(): - m_app(0), m_capacity(0), m_enode_data(nullptr) { SASSERT(m_app.get_app()->get_decl() == 0); @@ -340,14 +339,13 @@ namespace smt { void tmp_enode::set_capacity(unsigned new_capacity) { SASSERT(new_capacity > m_capacity); - if (m_enode_data) - dealloc_svect(m_enode_data); + dealloc_svect(m_enode_data); m_capacity = new_capacity; unsigned sz = sizeof(enode) + m_capacity * sizeof(enode*); m_enode_data = alloc_svect(char, sz); memset(m_enode_data, 0, sz); enode * n = get_enode(); - n->m_owner = m_app.get_app(); + n->m_owner = &m_app; n->m_root = n; n->m_next = n; n->m_class_size = 1; @@ -359,19 +357,11 @@ namespace smt { if (num_args > m_capacity) set_capacity(num_args * 2); enode * r = get_enode(); - if (m_app.get_app()->get_decl() != f) { - r->m_func_decl_id = UINT_MAX; - } - m_app.set_decl(f); - m_app.set_num_args(num_args); + m_app.m_decl = f; + m_app.m_num_args = num_args; r->m_commutative = num_args == 2 && f->is_commutative(); memcpy(get_enode()->m_args, args, sizeof(enode*)*num_args); return r; } - void tmp_enode::reset() { - get_enode()->m_func_decl_id = UINT_MAX; - } - }; - diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 92902ea0b..7229dab29 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -456,7 +456,7 @@ namespace smt { void unmark_enodes2(unsigned num_enodes, enode * const * enodes); class tmp_enode { - tmp_app m_app; + app m_app; unsigned m_capacity; char * m_enode_data; enode * get_enode() { return reinterpret_cast(m_enode_data); } @@ -465,7 +465,6 @@ namespace smt { tmp_enode(); ~tmp_enode(); enode * set(func_decl * f, unsigned num_args, enode * const * args); - void reset(); }; inline mk_pp pp(enode* n, ast_manager& m) { return mk_pp(n->get_expr(), m); } From 6246c6517d8743185d8e0b73b7e1a799351ba176 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Dec 2023 18:30:53 +0000 Subject: [PATCH 4/5] fix debug build --- src/smt/smt_enode.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 4bcb4a41c..8fbf43d60 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -329,7 +329,6 @@ namespace smt { tmp_enode::tmp_enode(): m_capacity(0), m_enode_data(nullptr) { - SASSERT(m_app.get_app()->get_decl() == 0); set_capacity(5); } From c4fa719751bf867fb9ad61bb60d94eac11e13291 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 20 Dec 2023 19:10:05 +0000 Subject: [PATCH 5/5] revert last two commits; MSVC doesn't like to statically allocate flexible arrays --- src/ast/ast.h | 4 ---- src/smt/smt_enode.cpp | 9 ++++++--- src/smt/smt_enode.h | 2 +- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index a42d894ae..9618c7e12 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -707,8 +707,6 @@ struct app_flags { app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {} }; -namespace smt { class tmp_enode; } - class app : public expr { friend class ast_manager; @@ -722,10 +720,8 @@ class app : public expr { } friend class tmp_app; - friend class smt::tmp_enode; app(func_decl * decl, unsigned num_args, expr * const * args); - app() : expr(AST_APP) {} public: func_decl * get_decl() const { return m_decl; } family_id get_family_id() const { return get_decl()->get_family_id(); } diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 8fbf43d60..e26ac1aa3 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -327,8 +327,10 @@ namespace smt { } tmp_enode::tmp_enode(): + m_app(0), m_capacity(0), m_enode_data(nullptr) { + SASSERT(m_app.get_app()->get_decl() == 0); set_capacity(5); } @@ -344,7 +346,7 @@ namespace smt { m_enode_data = alloc_svect(char, sz); memset(m_enode_data, 0, sz); enode * n = get_enode(); - n->m_owner = &m_app; + n->m_owner = m_app.get_app(); n->m_root = n; n->m_next = n; n->m_class_size = 1; @@ -356,11 +358,12 @@ namespace smt { if (num_args > m_capacity) set_capacity(num_args * 2); enode * r = get_enode(); - m_app.m_decl = f; - m_app.m_num_args = num_args; + m_app.set_decl(f); + m_app.set_num_args(num_args); r->m_commutative = num_args == 2 && f->is_commutative(); memcpy(get_enode()->m_args, args, sizeof(enode*)*num_args); return r; } }; + diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 7229dab29..c07576f38 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -456,7 +456,7 @@ namespace smt { void unmark_enodes2(unsigned num_enodes, enode * const * enodes); class tmp_enode { - app m_app; + tmp_app m_app; unsigned m_capacity; char * m_enode_data; enode * get_enode() { return reinterpret_cast(m_enode_data); }