diff options
| -rw-r--r-- | configure.ac | 10 | ||||
| -rw-r--r-- | src/smt/dump.h | 86 |
2 files changed, 48 insertions, 48 deletions
diff --git a/configure.ac b/configure.ac index de4a410ad..81fff6c93 100644 --- a/configure.ac +++ b/configure.ac @@ -424,6 +424,16 @@ fi AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln]) AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp]) +# Dumping cannot be used in a portfolio build. Disable dumping by default when +# a portfolio build has been requested, throw an error if dumping has been +# explicitly requested with a portfolio build. +if test "$with_portfolio" = yes; then + if test "$enable_dumping" = yes; then + AC_MSG_ERROR([Dumping is not supported with a portfolio build]) + fi + enable_dumping=no +fi + # construct the build string AC_MSG_CHECKING([for appropriate build string]) if test -z "$ac_confdir"; then diff --git a/src/smt/dump.h b/src/smt/dump.h index cdab598bb..9de8eb0ce 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -24,63 +24,49 @@ namespace CVC4 { -class CVC4_PUBLIC CVC4dumpstream { - -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - std::ostream* d_os; -#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ - -#ifdef CVC4_PORTFOLIO - CommandSequence* d_commands; -#endif /* CVC4_PORTFOLIO */ +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && !defined(CVC4_PORTFOLIO) +class CVC4_PUBLIC CVC4dumpstream +{ public: - CVC4dumpstream() -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(NULL), d_commands(NULL) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(NULL) -#elif defined(CVC4_PORTFOLIO) - : d_commands(NULL) -#endif /* CVC4_PORTFOLIO */ - { } - - CVC4dumpstream(std::ostream& os, CommandSequence& commands) -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(&os), d_commands(&commands) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(&os) -#elif defined(CVC4_PORTFOLIO) - : d_commands(&commands) -#endif /* CVC4_PORTFOLIO */ - { } + CVC4dumpstream() : d_os(nullptr) {} + CVC4dumpstream(std::ostream& os) : d_os(&os) {} CVC4dumpstream& operator<<(const Command& c) { -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - if(d_os != NULL) { + if (d_os != nullptr) + { (*d_os) << c << std::endl; } -#endif -#if defined(CVC4_PORTFOLIO) - if(d_commands != NULL) { - d_commands->addCommand(c.clone()); - } -#endif return *this; } -};/* class CVC4dumpstream */ -/** The dump class */ -class CVC4_PUBLIC DumpC { - std::set<std::string> d_tags; - CommandSequence d_commands; + private: + std::ostream* d_os; +}; /* class CVC4dumpstream */ - static const std::string s_dumpHelp; +#else + +/** + * Dummy implementation of the dump stream when dumping is disabled or the + * build is muzzled. + */ +class CVC4_PUBLIC CVC4dumpstream +{ + public: + CVC4dumpstream() {} + CVC4dumpstream(std::ostream& os) {} + CVC4dumpstream& operator<<(const Command& c) { return *this; } +}; /* class CVC4dumpstream */ + +#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ -public: +/** The dump class */ +class CVC4_PUBLIC DumpC +{ + public: CVC4dumpstream operator()(const char* tag) { if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); + return CVC4dumpstream(getStream()); } else { return CVC4dumpstream(); } @@ -88,15 +74,12 @@ public: CVC4dumpstream operator()(std::string tag) { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); + return CVC4dumpstream(getStream()); } else { return CVC4dumpstream(); } } - void clear() { d_commands.clear(); } - const CommandSequence& getCommands() const { return d_commands; } - bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } bool on (std::string tag) { d_tags.insert(tag); return true; } bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } @@ -111,6 +94,13 @@ public: std::ostream* getStreamPointer(); void setDumpFromString(const std::string& optarg); + + private: + /** Set of dumping tags that are currently active. */ + std::set<std::string> d_tags; + + /** The message printed on `--dump help`. */ + static const std::string s_dumpHelp; };/* class DumpC */ /** The dump singleton */ |