Merge branch 'master' of https://github.com/z3prover/z3

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;            
         }
 

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);
     }
 

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;
             }

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("");
     }
 

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));

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);

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());

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("");
     }
 

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;
                 }

src/ast/ast.h

@@ -704,26 +704,23 @@ 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 {
     friend class ast_manager;
 
     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<app_flags*>(const_cast<expr**>(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 @@ class app : public expr {
     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; }
 };
 
 // -----------------------------------

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) {

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();

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;
             }

src/math/lp/numeric_pair.h

@@ -24,7 +24,6 @@
 #include <algorithm>
 #ifdef lp_for_z3
 #include "util/rational.h"
-#include "util/sstream.h"
 #include "util/z3_exception.h"
 #else
 // include "util/numerics/mpq.h"

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<unsigned>(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 {

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();
     }