Restoring ostream format. Resolves a few CIDs 1362780. (#1543)

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 7c8ee7827d6bf944d5a9ff62299e47acfd0f41e6..a7666dfcfc26ffa4f2871b97643ed5d49503c844 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -193,7 +193,10 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
   return !cmd->fail();
 }
 
-void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString) {
+void printStatsIncremental(std::ostream& out,
+                           const std::string& prvsStatsString,
+                           const std::string& curStatsString)
+{
   if(prvsStatsString == "") {
     out << curStatsString;
     return;
@@ -229,9 +232,11 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
         (std::istringstream(curStatValue) >> curFloat);
 
       if(isFloat) {
+        const std::streamsize old_precision = out.precision();
         out << curStatName << ", " << curStatValue << " "
             << "(" << std::setprecision(8) << (curFloat-prvsFloat) << ")"
             << std::endl;
+        out.precision(old_precision);
       } else {
         out << curStatName << ", " << curStatValue << std::endl;
       }

diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index ad04cfe2218da77a55860e46bf73fb0799e9bb9a..08fe0bc1ebe41809cbb57167daf7db0fb1dbe1d4 100644 (file)
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.cpp
@@ -26,6 +26,7 @@
 #include "theory/arith/constraint.h"
 #include "theory/arith/cut_log.h"
 #include "theory/arith/normal_form.h"
+#include "util/ostream_util.h"
 
 using namespace std;
 
@@ -84,8 +85,9 @@ void PrimitiveVec::setup(int l){
 }
 void PrimitiveVec::print(std::ostream& out) const{
   Assert(initialized());
-  out << len << " ";
-  out.precision(15);
+  StreamFormatScope scope(out);
+
+  out << len << " " << std::setprecision(15);
   for(int i = 1; i <= len; ++i){
     out << "["<< inds[i] <<", " << coeffs[i]<<"]";
   }

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 33218dbe9f41985b5675a58e9ed43bd4c2519fff..ddee2e72b567b1a1f107d11a7edfac7d567e735f 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -38,6 +38,8 @@ libutil_la_SOURCES = \
        index.h \
        maybe.h \
        ntuple.h \
+       ostream_util.cpp \
+       ostream_util.h \
        proof.h \
        regexp.cpp \
        regexp.h \

diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp
new file mode 100644 (file)
index 0000000..3d6eeea
--- /dev/null
+++ b/src/util/ostream_util.cpp
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file result.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for using ostreams.
+ **
+ ** Utilities for using ostreams.
+ **/
+#include "util/ostream_util.h"
+
+namespace CVC4 {
+
+StreamFormatScope::StreamFormatScope(std::ostream& out)
+    : d_out(out), d_format_flags(out.flags()), d_precision(out.precision())
+{
+}
+
+StreamFormatScope::~StreamFormatScope()
+{
+  d_out.precision(d_precision);
+  d_out.flags(d_format_flags);
+}
+
+}  // namespace CVC4

diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h
new file mode 100644 (file)
index 0000000..e047caa
--- /dev/null
+++ b/src/util/ostream_util.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file ostream_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for using ostreams.
+ **
+ ** Utilities for using ostreams.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTIL__OSTREAM_UTIL_H
+#define __CVC4__UTIL__OSTREAM_UTIL_H
+
+#include <ios>
+#include <ostream>
+
+namespace CVC4 {
+
+// Saves the formatting of an ostream and restores the previous settings on
+// destruction. Example usage:
+//   void Foo::Print(std::ostream& out) {
+//     StreamFormatScope format_scope(out);
+//     out << std::setprecision(6) << bar();
+//   }
+class StreamFormatScope
+{
+ public:
+  // `out` must outlive StreamFormatScope.
+  StreamFormatScope(std::ostream& out);
+  ~StreamFormatScope();
+
+ private:
+  // Does not own the memory of d_out
+  std::ostream& d_out;
+  std::ios_base::fmtflags d_format_flags;
+  std::streamsize d_precision;
+};
+
+}  // namespace CVC4
+
+#endif /* __CVC4__UTIL__OSTREAM_UTIL_H */

diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 61dbccbeeb42cb375f981c5480b7a6c45abdbddc..504d58b0e3b6331241f3f5119e024cccd52b01fc 100644 (file)
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -30,6 +30,7 @@
 
 #include "base/cvc4_assert.h"
 #include "options/set_language.h"
+#include "util/ostream_util.h"
 #include "util/smt2_quote_string.h"
 
 namespace CVC4 {
@@ -219,6 +220,8 @@ void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
 
 void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
                         OutputLanguage language, int indent) {
+  StreamFormatScope scope(out);
+
   if (sexpr.isInteger()) {
     out << sexpr.getIntegerValue();
   } else if (sexpr.isRational()) {

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 11afb99ed7583f6450bba6ed2cb12e8cbcacfa50..4e2b06d5317410ea28a0020b70c502025cdd2927 100644 (file)
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -19,7 +19,7 @@
 
 #include "base/cvc4_assert.h"
 #include "lib/clock_gettime.h"
-
+#include "util/ostream_util.h"
 
 #ifdef CVC4_STATISTICS_ON
 #  define __CVC4_USE_STATISTICS true
@@ -134,6 +134,7 @@ inline bool operator>=(const timespec& a, const timespec& b) {
 /** Output a timespec on an output stream. */
 std::ostream& operator<<(std::ostream& os, const timespec& t) {
   // assumes t.tv_nsec is in range
+  StreamFormatScope format_scope(os);
   return os << t.tv_sec << "."
             << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
 }