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 693baede25dcd2a2a0206585ba6486ff165f4610..050935422ab91b916a2ee4b13fa7f2dc151aeacd 100644 (file)
--- 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 7f6d3db9d238b1eee1f132831a927af677b2e974..7374c8ca9d70420697473556d5d794fdc1fe0e9e 100644 (file)
--- 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