From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Aug 2020 18:14:41 +0000 (-0500)
Subject: More basic fix for dumping synth-fun (#4886)
X-Git-Tag: cvc5-1.0.0~3006
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb2a0d9aa09aa21f465aa8d62eab8492610052c3;p=cvc5.git

More basic fix for dumping synth-fun (#4886)

The commit (079a04b) appears to have broken the nightlies due to compile issues related a necessary addition to the Dump class (so that std::string could be printing on Dump streams).

This changes the temporary solution so that we simply print a string on the standard output, when the Dump is enabled. This is required for temporarily keeping dump=raw-benchmark working for synth-fun commands.
---

diff --git a/src/smt/dump.h b/src/smt/dump.h
index 693baede2..050935422 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -40,17 +40,6 @@ class CVC4_PUBLIC CVC4dumpstream
     return *this;
   }
 
-  // Note(abdoo8080): temporarily overloading operator<< for strings to allow us
-  // to print commands provided as strings
-  CVC4dumpstream& operator<<(const std::string& str)
-  {
-    if (d_os != nullptr)
-    {
-      (*d_os) << str << std::endl;
-    }
-    return *this;
-  }
-
  private:
   std::ostream* d_os;
 }; /* class CVC4dumpstream */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7f6d3db9d..7374c8ca9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1350,8 +1350,11 @@ void SmtEngine::declareSynthFun(const std::string& id,
                 : TypeNode::fromType(func.getType()),
             isInv,
             TypeNode::fromType(sygusType));
-
-    Dump("raw-benchmark") << ss.str();
+    
+    // must print it on the standard output channel since it is not possible
+    // to print anything except for commands with Dump.
+    std::ostream& out = *d_options.getOut();
+    out << ss.str() << std::endl;
   }
 
   // sygus conjecture is now stale