diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-08-12 17:51:48 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 17:51:48 -0500 |
commit | 079a04b0b16f7caa31a15b97ddc9794ad0d8b862 (patch) | |
tree | a8c56b4ca8ed13fdfddbca7692504624069cf5e2 /src/smt/dump.h | |
parent | 103b5ea715e532e021e91f9b03ea7d7876a3ccbf (diff) |
Refactor functions that print commands (Part 1) (#4869)
This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.
Diffstat (limited to 'src/smt/dump.h')
-rw-r--r-- | src/smt/dump.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/smt/dump.h b/src/smt/dump.h index 050935422..693baede2 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -40,6 +40,17 @@ 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 */ |