From fb2a0d9aa09aa21f465aa8d62eab8492610052c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 13 Aug 2020 13:14:41 -0500 Subject: [PATCH] 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. --- src/smt/dump.h | 11 ----------- src/smt/smt_engine.cpp | 7 +++++-- 2 files changed, 5 insertions(+), 13 deletions(-) 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 -- 2.30.2