From 541379b3d361e255cd664207f8b2e278a5b5e3eb Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 3 Nov 2009 03:07:58 +0000
Subject: additional headers

---
 src/include/parser.h | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'src/include/parser.h')

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 */
-- 
cgit v1.2.3