Fix muzzled builds (#5093)

Commit 2c2f05c moved some function
definitions from dump.h to dump.cpp, which is good. However, the
corresponding definitions for muzzled builds weren't moved, so muzzled builds
defined the operator << multiple times. This made our nightly
competition build fail. This commit fixes the issue by moving the
alternative definitions to the source file as well.

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 28cf8a34f34baf78040a84e61dc03920728a6021..ab2bf3bf28ef33eddf311a909d920b8d15c75401 100644 (file)
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -24,6 +24,8 @@
 
 namespace CVC4 {
 
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+
 CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c)
 {
   if (d_os != nullptr)
@@ -42,6 +44,16 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc)
   return *this;
 }
 
+#else
+
+CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) { return *this; }
+CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc)
+{
+  return *this;
+}
+
+#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
+
 DumpC DumpChannel CVC4_PUBLIC;
 
 std::ostream& DumpC::setStream(std::ostream* os) {

diff --git a/src/smt/dump.h b/src/smt/dump.h
index ec13a9ae9f90f409462b02f605ee02821db7907d..832dfb93669aec2a356acd71079cb9e18a71891f 100644 (file)
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -58,8 +58,8 @@ class CVC4_PUBLIC CVC4dumpstream
  public:
   CVC4dumpstream() {}
   CVC4dumpstream(std::ostream& os) {}
-  CVC4dumpstream& operator<<(const Command& c) { return *this; }
-  CVC4dumpstream& operator<<(const NodeCommand& nc) { return *this; }
+  CVC4dumpstream& operator<<(const Command& c);
+  CVC4dumpstream& operator<<(const NodeCommand& nc);
 }; /* class CVC4dumpstream */
 
 #endif /* CVC4_DUMPING && !CVC4_MUZZLE */