diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-13 13:14:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-13 13:14:41 -0500 |
| commit | fb2a0d9aa09aa21f465aa8d62eab8492610052c3 (patch) | |
| tree | 6567fc9f3824ecf0b0aa55843db239262873ab46 | |
| parent | e6f55a60a3a65c55c04cb8bd88d47d6207677a29 (diff) | |
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.
| -rw-r--r-- | src/smt/dump.h | 11 | ||||
| -rw-r--r-- | 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 |