additional headers

1 files changed, 25 insertions, 0 deletions

diff --git a/src/include/parser.h b/src/include/parser.h
index 0cfc89a28..8f1032286 100644
--- a/src/include/parser.h
+++ b/src/include/parser.h
@@ -12,6 +12,31 @@
 
 namespace CVC4 {
 
+// In terms of abstraction, this is below (and provides services to)
+// the main CVC4 binary and above (and requires the services of)
+// ValidityChecker.
+
+class Parser {
+private:// maybe protected is better ?
+  ValidityChecker *d_vc;
+
+public:
+  Parser(ValidityChecker* vc);
+
+  /**
+   * Process a file.  Overridden in subclasses to support SMT-LIB
+   * format, CVC4 presentation language, etc.  In subclasses, this
+   * function should parse terms, build Command objects, and pass them
+   * to dispatch().
+   */
+  virtual Expr process(std::istream&) = 0;
+
+  /**
+   * Dispatch a command.
+   */
+  void dispatch(const Command&);
+};/* class Parser */
+
 } /* CVC4 namespace */
 
 #endif /* __CVC4_PARSER_H */