diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-09 23:14:40 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-09 23:14:40 +0000 |
commit | 2f121daa042c6f25a3f9ed8ece60ac5dccb11976 (patch) | |
tree | 58ee28d73e8638b100abe09e961bc3dbdf9d79d9 /src/parser/smt/smt_parser.h | |
parent | d697d1e91be226339a28bd7e8dce3862901cba8a (diff) |
some fixes and organizational adjustments to assert code, parsers/lexers, and build process
Diffstat (limited to 'src/parser/smt/smt_parser.h')
-rw-r--r-- | src/parser/smt/smt_parser.h | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h new file mode 100644 index 000000000..a68f0e783 --- /dev/null +++ b/src/parser/smt/smt_parser.h @@ -0,0 +1,77 @@ +/********************* -*- C++ -*- */ +/** smt_parser.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** SMT-LIB language parser abstraction. + **/ + +#ifndef __CVC4__PARSER__SMT_PARSER_H +#define __CVC4__PARSER__SMT_PARSER_H + +#include <string> +#include <iostream> +#include <fstream> +#include "cvc4_config.h" +#include "parser/parser_exception.h" +#include "parser/parser.h" + +namespace CVC4 { +namespace parser { + +/** + * The SMT parser. + */ +class CVC4_PUBLIC SmtParser : public Parser { + +public: + + /** + * Construct the parser that uses the given expression manager and parses + * from the given input stream. + * @param em the expression manager to use + * @param input the input stream to parse + * @param file_name the name of the file (for diagnostic output) + */ + SmtParser(ExprManager* em, std::istream& input, const char* file_name = ""); + + /** + * Destructor. + */ + ~SmtParser(); + + /** + * Parses the next command. By default, the SMT-LIB parser produces + * one CommandSequence command. If parsing is successful, we should + * be done after the first call to this command. + * @return the CommandSequence command that includes the whole + * benchmark + */ + Command* parseNextCommand() throw(ParserException); + + /** + * Parses the next complete expression of the stream. + * @return the expression parsed + */ + Expr parseNextExpression() throw(ParserException); + +protected: + + /** The ANTLR smt lexer */ + AntlrSmtLexer* d_antlr_lexer; + + /** The ANTLR smt parser */ + AntlrSmtParser* d_antlr_parser; + + /** The file stream we might be using */ + std::istream& d_input; +}; + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__SMT_PARSER_H */ |