summaryrefslogtreecommitdiff
path: root/src/printer/printer.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-06-08 21:21:42 +0000
committerMorgan Deters <mdeters@gmail.com>2012-06-08 21:21:42 +0000
commit58372a2ad23298810ae886a16db3c57f9df251af (patch)
tree7dd58f171e5b972f883a106f404aba989065c179 /src/printer/printer.h
parentf1b4a985be64e08b1a440b1eaf75d3f8e2105d01 (diff)
Extend Printer infrastructure also to the "Result" class, meaning that different output languages can write "sat", "unsat", etc., in different ways. No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.
Diffstat (limited to 'src/printer/printer.h')
-rw-r--r--src/printer/printer.h10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 9bcbba3b0..04b435060 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -62,6 +62,16 @@ public:
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
+ /**
+ * Write a Result out to a stream with this Printer.
+ *
+ * The default implementation writes a reasonable string in lowercase
+ * for sat, unsat, valid, invalid, or unknown results. This behavior
+ * is overridable by each Printer, since sometimes an output language
+ * has a particular preference for how results should appear.
+ */
+ virtual void toStream(std::ostream& out, const Result& r) const throw();
+
};/* class Printer */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback