remove '#include <iostream>' from headers and from unneeded places

It's harmful to have iostream everywhere as it injects functions in the compiled files

scripts/update_api.py

@@ -1771,7 +1771,6 @@ def write_log_h_preamble(log_h):
 
 def write_log_c_preamble(log_c):
   log_c.write('// Automatically generated file\n')
-  log_c.write('#include<iostream>\n')
   log_c.write('#include\"api/z3.h\"\n')
   log_c.write('#include\"api/api_log_macros.h\"\n')
   log_c.write('#include\"api/z3_logger.h\"\n')

src/api/api_ast.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
 #include "api/api_util.h"

src/api/api_ast_map.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_ast_vector.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_fpa.cpp

@@ -16,7 +16,6 @@ Module Name:
 Notes:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_goal.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_numeral.cpp

@@ -16,7 +16,6 @@ Revision History:
 
 --*/
 #include<cmath>
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_opt.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
 #include "util/scoped_ctrl_c.h"

src/api/api_params.cpp

@@ -17,7 +17,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_parsers.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_qe.cpp

@@ -17,7 +17,6 @@ Module Name:
 
 --*/
 
-#include <iostream>
 #include "ast/expr_map.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"

src/api/api_rcf.cpp

@@ -19,7 +19,6 @@ Module Name:
 Notes:
     
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_solver.cpp

@@ -16,7 +16,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include<thread>
 #include "util/scoped_ctrl_c.h"
 #include "util/cancel_eh.h"

src/api/api_special_relations.cpp

@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 
-#include <iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_stats.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/api_tactic.cpp

@@ -15,7 +15,6 @@ Module Name:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"

src/api/c++/z3++.h

@@ -21,7 +21,7 @@ Copyright (c) 2012 Microsoft Corporation
 #pragma once
 
 #include<cassert>
-#include<iostream>
+#include<ostream>
 #include<string>
 #include<sstream>
 #include<memory>

src/api/z3_private.h

@@ -18,7 +18,6 @@ Module Name:
 
 --*/
 
-#include<iostream>
 #include "util/rational.h"
 #include "api/z3_macros.h"
 

src/api/z3_replayer.cpp

@@ -22,6 +22,7 @@ Module Name:
 #include "util/stream_buffer.h"
 #include "util/symbol.h"
 #include "util/trace.h"
+#include<iostream>
 #include<sstream>
 #include<vector>
 

src/api/z3_replayer.h

@@ -18,7 +18,6 @@ Module Name:
 --*/
 #pragma once
 
-#include<iostream>
 #include "api/z3.h"
 #include "util/z3_exception.h"
 

src/ast/ast.cpp

@@ -30,6 +30,7 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_translation.h"
 #include "util/z3_version.h"
+#include <iostream>
 
 
 // -----------------------------------

src/ast/ast_ll_pp.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include<iostream>
+#include "ast/ast_ll_pp.h"
 #include "ast/for_each_ast.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"

src/ast/ast_ll_pp.h

@@ -19,7 +19,7 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
-#include<iostream>
+#include<ostream>
 
 void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, bool only_exprs=true, bool compact=true);
 void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs=true, bool compact=true);

src/ast/ast_pp_dot.h

@@ -6,7 +6,7 @@ Abstract: Pretty-printer for proofs in Graphviz format
 
 #pragma once
 
-#include <iostream>
+#include <ostream>
 #include "ast/ast_pp.h"
 
 class ast_pp_dot {

src/ast/ast_printer.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "ast/ast_printer.h"
 #include "ast/pp.h"
+#include <iostream>
 
 class simple_ast_printer_context : public ast_printer_context {
     ast_manager & m_manager;
@@ -51,3 +52,6 @@ class simple_ast_printer_context : public ast_printer_context {
 ast_printer_context * mk_simple_ast_printer_context(ast_manager & m) {
     return alloc(simple_ast_printer_context, m);
 }
+
+std::ostream & ast_printer_context::regular_stream() { return std::cout; }
+std::ostream & ast_printer_context::diagnostic_stream() { return std::cerr; }

src/ast/ast_printer.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "ast/ast_smt2_pp.h"
+#include <ostream>
 
 class ast_printer {
 public:
@@ -46,8 +47,8 @@ class ast_printer_context : public ast_printer {
 public:
     ~ast_printer_context() override {}
     virtual ast_manager & get_ast_manager() = 0;
-    virtual std::ostream & regular_stream() { return std::cout; }
-    virtual std::ostream & diagnostic_stream() { return std::cerr; }
+    virtual std::ostream & regular_stream();
+    virtual std::ostream & diagnostic_stream();
 };
 
 

src/ast/ast_smt_pp.cpp

@@ -20,7 +20,7 @@ Revision History:
 --*/
 
 #include<sstream>
-#include<iostream>
+#include<ostream>
 #include "util/vector.h"
 #include "util/smt2_util.h"
 #include "ast/ast_smt_pp.h"

src/ast/fpa/bv2fpa_converter.cpp

@@ -162,7 +162,7 @@ expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) {
         }
     }
     else {
-        std::cout << expr_ref(bv_rm, m) << " not converted\n";
+        //std::cout << expr_ref(bv_rm, m) << " not converted\n";
     }
 
     return res;

src/ast/fpa/fpa2bv_converter.cpp

@@ -124,7 +124,7 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
         result = m_util.mk_bv2rm(result);
     }
     else {
-        std::cout << mk_pp(t, m) << " " << mk_pp(f, m) << "\n";
+        //std::cout << mk_pp(t, m) << " " << mk_pp(f, m) << "\n";
         UNREACHABLE();
 
     }

src/cmd_context/cmd_context.cpp

@@ -51,6 +51,7 @@ Module Name:
 #include "solver/smt_logics.h"
 #include "cmd_context/basic_cmds.h"
 #include "cmd_context/cmd_context.h"
+#include <iostream>
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {

src/math/lp/lp_settings.h

@@ -24,6 +24,7 @@ Revision History:
 #include <algorithm>
 #include <limits>
 #include <iomanip>
+#include <iostream>
 #include <cstring>
 #include "util/stopwatch.h"
 #include "util/statistics.h"

src/math/lp/lu.h

@@ -33,7 +33,7 @@ Revision History:
 #include "math/lp/static_matrix.h"
 #include <string>
 #include "math/lp/numeric_pair.h"
-#include <iostream>
+#include <ostream>
 #include <fstream>
 #include "math/lp/row_eta_matrix.h"
 #include "math/lp/square_dense_submatrix.h"

src/math/lp/mps_reader.h

@@ -26,7 +26,7 @@ Revision History:
 #include <string>
 #include "util/vector.h"
 #include <unordered_map>
-#include <iostream>
+#include <ostream>
 #include <fstream>
 #include <locale>
 #include "math/lp/lp_primal_simplex.h"

src/math/realclosure/realclosure.cpp

@@ -29,6 +29,7 @@ Module Name:
 #include "util/ref_vector.h"
 #include "util/ref_buffer.h"
 #include "util/common_msgs.h"
+#include <iostream>
 
 #ifndef REALCLOSURE_INI_BUFFER_SIZE
 #define REALCLOSURE_INI_BUFFER_SIZE 32

src/math/simplex/sparse_matrix.h

@@ -281,7 +281,7 @@ namespace simplex {
             vector<_row> const& m_rows;
             void move_to_next() {
                 while (m_curr < m_rows.size() && m_rows[m_curr].size() == 0) {
-                    std::cout << "size is 0 for " << m_curr << "\n";
+                    //std::cout << "size is 0 for " << m_curr << "\n";
                     ++m_curr;
                 }
             }

src/math/subpaving/subpaving_t.h

@@ -18,7 +18,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 #include "util/tptr.h"
 #include "util/small_object_allocator.h"
 #include "util/chashtable.h"

src/math/subpaving/tactic/subpaving_tactic.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include "util/mpff.h"
 #include "util/mpfx.h"
 #include "util/f2n.h"
+#include <iostream>
 
 class subpaving_tactic : public tactic {
 

src/model/model_pp.h

@@ -19,7 +19,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 class model_core;
 
 void model_pp(std::ostream & out, model_core const & m);

src/model/model_v2_pp.cpp

@@ -18,6 +18,7 @@ Revision History:
 #include "model/model_v2_pp.h"
 #include "model/model_core.h"
 #include "ast/ast_pp.h"
+#include <iostream>
 
 static void display_function(std::ostream & out, model_core const & md, func_decl * f, bool partial) {
     ast_manager & m = md.get_manager();

src/model/model_v2_pp.h

@@ -17,7 +17,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<iostream>
+#include<ostream>
 class model_core;
 
 void model_v2_pp(std::ostream & out, model_core const & m, bool partial = false);

src/muz/base/dl_boogie_proof.cpp

@@ -121,11 +121,11 @@ namespace datalog {
     }
 
     void boogie_proof::set_proof(proof* p) {
-        std::cout << "set proof\n";
+        //std::cout << "set proof\n";
         m_proof = p;
         proof_utils::push_instantiations_up(m_proof);
         mk_input_resolution(m_proof);
-        std::cout << "proof set\n";
+        //std::cout << "proof set\n";
     }
 
     void boogie_proof::set_model(model* m) {
@@ -201,7 +201,7 @@ namespace datalog {
         ptr_vector<proof> todo;
         todo.push_back(p);
         ast_mark visited;
-        std::cout << "get_subst\n" << mk_pp(p, m) << "\n";
+        //std::cout << "get_subst\n" << mk_pp(p, m) << "\n";
         while (!todo.empty()) {
             proof* p = todo.back();
             todo.pop_back();

src/muz/base/dl_context.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 
+#include<iostream>
 #include<sstream>
 #include<limits>
 #include "ast/arith_decl_plugin.h"

src/muz/base/dl_util.h

@@ -257,12 +257,14 @@ namespace datalog {
             }
             container[i-ofs] = container[i];
         }
+#if 0
         if (r_i != removed_col_cnt) {
             for (unsigned i = 0; i < removed_col_cnt; ++i) {
                 std::cout << removed_cols[i] << " ";
             }
             std::cout << " container size: " << n << "\n";
         }
+#endif
         SASSERT(r_i==removed_col_cnt);
         container.resize(n-removed_col_cnt);
     }