diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-12 20:38:10 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-12 20:38:10 +0000 |
commit | 13a6669a35aee32c03f8d29fe386aca95d2fbd8f (patch) | |
tree | b126afb6c384dd45db0249e8096cf733a74daa95 /src/include | |
parent | 5b5474281c4cdc880bff8b9e38b84dc84f88e50c (diff) |
parser, minisat, other things..
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/Makefile.am | 14 | ||||
-rw-r--r-- | src/include/exception.h | 47 | ||||
-rw-r--r-- | src/include/parser.h | 75 | ||||
-rw-r--r-- | src/include/parser_exception.h | 36 | ||||
-rw-r--r-- | src/include/parser_temp.h | 76 |
5 files changed, 205 insertions, 43 deletions
diff --git a/src/include/Makefile.am b/src/include/Makefile.am deleted file mode 100644 index fa37abd9a..000000000 --- a/src/include/Makefile.am +++ /dev/null @@ -1,14 +0,0 @@ -EXTRA_DIST = \ - assert.h \ - attr_type.h \ - command.h - expr_attribute.h \ - expr_builder.h \ - expr.h \ - expr_manager.h \ - expr_value.h \ - kind.h \ - parser.h \ - sat.h \ - unique_id.h \ - vc.h diff --git a/src/include/exception.h b/src/include/exception.h new file mode 100644 index 000000000..3502fdf0c --- /dev/null +++ b/src/include/exception.h @@ -0,0 +1,47 @@ +/********************* -*- C++ -*- */ +/** exception.h + ** This file is part of the CVC4 prototype. + ** + ** Exception class. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXCEPTION_H +#ifndef __CVC4_EXCEPTION_H + +#include <string> +#include <iostream> + +namespace CVC4 { + + class Exception { + protected: + std::string d_msg; + public: + // Constructors + Exception(): d_msg("Unknown exception") { } + Exception(const std::string& msg): d_msg(msg) { } + Exception(const char* msg): d_msg(msg) { } + // Destructor + virtual ~Exception() { } + // NON-VIRTUAL METHODs for setting and printing the error message + void setMessage(const std::string& msg) { d_msg = msg; } + // Printing: feel free to redefine toString(). When inherited, + // it's recommended that this method print the type of exception + // before the actual message. + virtual std::string toString() const { return d_msg; } + // No need to overload operator<< for the inherited classes + friend std::ostream& operator<<(std::ostream& os, const Exception& e); + + }; // end of class Exception + + inline std::ostream& operator<<(std::ostream& os, const Exception& e) { + return os << e.toString(); + } + +}/* CVC4 namespace */ + +#endif /* __CVC4_EXCEPTION_H */ diff --git a/src/include/parser.h b/src/include/parser.h index c5af769e3..63a448b28 100644 --- a/src/include/parser.h +++ b/src/include/parser.h @@ -2,6 +2,8 @@ /** parser.h ** This file is part of the CVC4 prototype. ** + ** Parser abstraction. + ** ** The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University @@ -10,37 +12,52 @@ #ifndef __CVC4_PARSER_H #define __CVC4_PARSER_H -#include <iostream> -#include "vc.h" -#include "expr.h" +#include "exception.h" +#include "lang.h" 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 */ + class ValidityChecker; + class Expr; + + // Internal parser state and other data + class ParserData; + + class Parser { + private: + ParserData* d_data; + // Internal methods for constructing and destroying the actual parser + void initParser(); + void deleteParser(); + public: + // Constructors + Parser(ValidityChecker* vc, InputLanguage lang, + // The 'interactive' flag is ignored when fileName != "" + bool interactive = true, + const std::string& fileName = ""); + Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is, + bool interactive = false); + // Destructor + ~Parser(); + // Read the next command. + Expr next(); + // Check if we are done (end of input has been reached) + bool done() const; + // The same check can be done by using the class Parser's value as + // a Boolean + operator bool() const { return done(); } + void printLocation(std::ostream & out) const; + // Reset any local data that depends on validity checker + void reset(); + }; // end of class Parser + + // The global pointer to ParserTemp. Each instance of class Parser + // sets this pointer before any calls to the lexer. We do it this + // way because flex and bison use global vars, and we want each + // Parser object to appear independent. + class ParserTemp; + extern ParserTemp* parserTemp; + +}/* CVC4 namespace */ #endif /* __CVC4_PARSER_H */ diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h new file mode 100644 index 000000000..8bad801f4 --- /dev/null +++ b/src/include/parser_exception.h @@ -0,0 +1,36 @@ +/********************* -*- C++ -*- */ +/** exception.h + ** This file is part of the CVC4 prototype. + ** + ** Exception class. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_PARSER_EXCEPTION_H +#define __CVC4_PARSER_EXCEPTION_H + +#include "exception.h" +#include <string> +#include <iostream> + +namespace CVC4 { + + class ParserException: public Exception { + public: + // Constructors + ParserException() { } + ParserException(const std::string& msg): Exception(msg) { } + ParserException(const char* msg): Exception(msg) { } + // Destructor + virtual ~ParserException() { } + virtual std::string toString() const { + return "Parse Error: " + d_msg; + } + }; // end of class ParserException + +}/* CVC4 namespace */ + +#endif /* __CVC4_PARSER_EXCEPTION_H */ diff --git a/src/include/parser_temp.h b/src/include/parser_temp.h new file mode 100644 index 000000000..d64a770e4 --- /dev/null +++ b/src/include/parser_temp.h @@ -0,0 +1,76 @@ +/********************* -*- C++ -*- */ +/** parser_temp.h + ** This file is part of the CVC4 prototype. + ** + ** A temporary holder for data used with the parser. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_PARSER_TEMP_H +#define __CVC4_PARSER_TEMP_H + +#include <iostream> + +#include "expr.h" +#include "exception.h" + +namespace CVC4 { + + class ValidityChecker; + + class ParserTemp { + private: + // Counter for uniqueID of bound variables + int d_uid; + // The main prompt when running interactive + std::string prompt1; + // The interactive prompt in the middle of a multi-line command + std::string prompt2; + // The currently used prompt + std::string prompt; + public: + ValidityChecker* vc; + std::istream* is; + // The current input line + int lineNum; + // File name + std::string fileName; + // The last parsed Expr + Expr expr; + // Whether we are done or not + bool done; + // Whether we are running interactive + bool interactive; + // Whether arrays are enabled for smt-lib format + bool arrFlag; + // Whether bit-vectors are enabled for smt-lib format + bool bvFlag; + // Size of bit-vectors for smt-lib format + int bvSize; + // Did we encounter a formula query (smtlib) + bool queryParsed; + // Default constructor + ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "), + prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { } + // Parser error handling (implemented in parser.cpp) + int error(const std::string& s); + // Get the next uniqueID as a string + std::string uniqueID() { + std::ostringstream ss; + ss << d_uid++; + return ss.str(); + } + // Get the current prompt + std::string getPrompt() { return prompt; } + // Set the prompt to the main one + void setPrompt1() { prompt = prompt1; } + // Set the prompt to the secondary one + void setPrompt2() { prompt = prompt2; } + }; + +}/* CVC4 namespace */ + +#endif /* __CVC4_PARSER_TEMP_H */ |