summaryrefslogtreecommitdiff
path: root/src/smt/dump.h
diff options
context:
space:
mode:
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>2020-08-12 17:51:48 -0500
committerGitHub <noreply@github.com>2020-08-12 17:51:48 -0500
commit079a04b0b16f7caa31a15b97ddc9794ad0d8b862 (patch)
treea8c56b4ca8ed13fdfddbca7692504624069cf5e2 /src/smt/dump.h
parent103b5ea715e532e021e91f9b03ea7d7876a3ccbf (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.h11
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback