remove some copies/moves

src/ast/ast.cpp

@@ -234,8 +234,7 @@ std::ostream& operator<<(std::ostream& out, sort_size const & ss) {
 // -----------------------------------
 std::ostream & operator<<(std::ostream & out, sort_info const & info) {
     operator<<(out, static_cast<decl_info const&>(info));
-    out << " :size " << info.get_num_elements();
+    return out << " :size " << info.get_num_elements();
-    return out;
 }
 
 // -----------------------------------
@@ -2237,7 +2236,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
         std::ostringstream buffer;
         buffer << "Wrong number of arguments (" << num_args
                << ") passed to function " << mk_pp(decl, *this);
-        throw ast_exception(buffer.str());
+        throw ast_exception(std::move(buffer).str());
     }
     app * r = nullptr;
     if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {

src/ast/bv_decl_plugin.cpp

@@ -886,8 +886,8 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
 }
 
 sort * bv_util::mk_sort(unsigned bv_size) {
-    parameter p[1] = { parameter(bv_size) };
+    parameter p(bv_size);
-    return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
+    return m_manager.mk_sort(get_fid(), BV_SORT, 1, &p);
 }
 
 unsigned bv_util::get_int2bv_size(parameter const& p) {

src/ast/datatype_decl_plugin.cpp

@@ -69,8 +69,8 @@ namespace datatype {
             domain.push_back(a->instantiate(ps)->get_range());
         }
         sort_ref range = get_def().instantiate(ps);
-        parameter pas[1] = { parameter(name()) };
+        parameter pas(name());
-        return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_CONSTRUCTOR, 1, pas, domain.size(), domain.data(), range), m);        
+        return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_CONSTRUCTOR, 1, &pas, domain.size(), domain.data(), range), m);
     }
 
     func_decl_ref constructor::instantiate(sort* dt) const {
@@ -1052,8 +1052,8 @@ namespace datatype {
     func_decl * util::get_constructor_is(func_decl * con) {
         SASSERT(is_constructor(con));
         sort * datatype = con->get_range();
-        parameter ps[1] = { parameter(con)};
+        parameter ps(con);
-        return m.mk_func_decl(fid(), OP_DT_IS, 1, ps, 1, &datatype);
+        return m.mk_func_decl(fid(), OP_DT_IS, 1, &ps, 1, &datatype);
     }
 
     func_decl * util::get_constructor_recognizer(func_decl * con) {

src/cmd_context/basic_cmds.cpp

@@ -817,9 +817,9 @@ public:
         sort_ref range(ctx.m());
         array_sort_args.push_back(m_f->get_range());
         range = array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data());
-        parameter p[1] = { parameter(m_f) };
+        parameter p(m_f);
         func_decl_ref new_map(ctx.m());
-        new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, p, domain.size(), domain.data(), range.get());
+        new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, &p, domain.size(), domain.data(), range.get());
         if (new_map == 0)
             throw cmd_exception("invalid array map operator");
         ctx.insert(m_name, new_map);

src/model/array_factory.cpp

@@ -45,8 +45,8 @@ expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) {
     func_decl * f    = mk_aux_decl_for_array_sort(m_manager, s);
     fi = alloc(func_interp, m_manager, get_array_arity(s));
     m_model.register_decl(f, fi);
-    parameter p[1] = { parameter(f) };
+    parameter p(f);
-    expr * val = m_manager.mk_app(get_family_id(), OP_AS_ARRAY, 1, p);
+    expr * val = m_manager.mk_app(get_family_id(), OP_AS_ARRAY, 1, &p);
     register_value(val);
     return val;
 }

src/smt/theory_array_base.cpp

@@ -958,8 +958,8 @@ namespace smt {
                 fi->insert_entry(args.data(), result);
             }
 
-            parameter p[1] = { parameter(f) };
+            parameter p(f);
-            return m.mk_app(m_fid, OP_AS_ARRAY, 1, p); 
+            return m.mk_app(m_fid, OP_AS_ARRAY, 1, &p);
         }
     };
 

src/util/gparams.cpp

@@ -276,20 +276,20 @@ public:
                 strm << "the parameter '" << param_name
                      << "', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:" << new_name
                      << "' for the full description of the parameter";
-                throw exception(strm.str());
+                throw exception(std::move(strm).str());
             }
             else if (is_old_param_name(param_name)) {
                 std::stringstream strm;
                 strm << "unknown parameter '" << param_name 
                      << "', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list";
-                throw default_exception(strm.str());
+                throw default_exception(std::move(strm).str());
             }
             else {
                 std::stringstream strm;
                 strm << "unknown parameter '" << param_name << "'\n";    
                 strm << "Legal parameters are:\n";
                 d.display(strm, 2, false, false);
-                throw default_exception(strm.str());
+                throw default_exception(std::move(strm).str());
             }
         }
         else {
@@ -298,7 +298,7 @@ public:
             strm << "at module '" << mod_name << "'\n";
             strm << "Legal parameters are:\n";
             d.display(strm, 2, false, false);
-            throw default_exception(strm.str());
+            throw default_exception(std::move(strm).str());
         }
     }
 
@@ -312,7 +312,7 @@ public:
                 if (!('0' <= *value && *value <= '9')) {
                     strm << "Expected values for parameter " << name 
                          << " is an unsigned integer. It was given argument '" << _value << "'";
-                    throw default_exception(strm.str());                    
+                    throw default_exception(std::move(strm).str());
                 }
             }
             break;
@@ -321,7 +321,7 @@ public:
                 if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-' && *value != '/') {
                     strm << "Expected values for parameter " << name 
                          << " is a double. It was given argument '" << _value << "'";
-                    throw default_exception(strm.str());                                        
+                    throw default_exception(std::move(strm).str());
                 }
             }
             break;
@@ -330,7 +330,7 @@ public:
             if (strcmp(value, "true") != 0 && strcmp(value, "false") != 0) {
                 strm << "Expected values for parameter " << name 
                      << " are 'true' or 'false'. It was given argument '" << value << "'";
-                throw default_exception(strm.str());
+                throw default_exception(std::move(strm).str());
             }
             break;
         default:
@@ -368,7 +368,7 @@ public:
                 if (mod_name[0]) {
                     strm << " at module '" << mod_name << "'";
                 }
-                throw default_exception(strm.str());
+                throw default_exception(std::move(strm).str());
             }
         }
         else if (k == CPK_SYMBOL) {
@@ -385,7 +385,7 @@ public:
             if (mod_name[0]) {
                 strm << " at module '" << mod_name << "'";            
             }
-            throw exception(strm.str());
+            throw exception(std::move(strm).str());
         }
     }
 
@@ -406,7 +406,7 @@ public:
             else {
                 std::stringstream strm;
                 strm << "invalid parameter, unknown module '" << m << "'";
-                throw exception(strm.str());
+                throw exception(std::move(strm).str());
             }
         }
     }
@@ -456,7 +456,7 @@ public:
         }
         std::stringstream strm;
         strm << "unknown module '" << m << "'";
-        throw exception(strm.str());
+        throw exception(std::move(strm).str());
     }
 
     // unfortunately, params_ref is not thread safe
@@ -523,7 +523,7 @@ public:
         if (!get_module_param_descr(module_name, d)) {
             std::stringstream strm;
             strm << "unknown module '" << module_name << "'";                    
-            throw exception(strm.str());
+            throw exception(std::move(strm).str());
         }
         out << "[module] " << module_name;
         char const * descr = nullptr;
@@ -548,7 +548,7 @@ public:
             if (!get_module_param_descr(m, d)) {
                 std::stringstream strm;
                 strm << "unknown module '" << m << "'";                    
-                throw exception(strm.str());
+                throw exception(std::move(strm).str());
             }
         }
         if (!d->contains(sp))