diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2009-06-10 09:13:20 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2009-06-10 09:13:20 +0000 |
commit | 930bf13e988c169c585da158c4410bdb49cc5ec6 (patch) | |
tree | e681646e5859bdb400c44981d92b30825548e32c | |
parent | f029d8ad70310b400612d85e60e8925101194e32 (diff) | |
download | klee-930bf13e988c169c585da158c4410bdb49cc5ec6.tar.gz |
Removed CVC3's Parser class.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73166 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | lib/SMT/parser.cpp | 151 |
1 files changed, 0 insertions, 151 deletions
diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp deleted file mode 100644 index 439e189c..00000000 --- a/lib/SMT/parser.cpp +++ /dev/null @@ -1,151 +0,0 @@ -/*****************************************************************************/ -/*! - * \file parser.cpp - * \brief The top-level API to the parser. See parser.h for details. - * - * Author: Sergey Berezin - * - * Created: Wed Feb 5 11:46:57 2003 - * - * <hr> - * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - * <hr> - * - */ -/*****************************************************************************/ - -#include <fstream> -#include <iomanip> -#include <iostream> -#include <stdlib.h> -#include "parser_temp.h" -#include "parser.h" - -using namespace std; - -// The communication entry points of the actual parsers - -// for smtlib language (smtlib.y and smtlib.lex) -extern int smtlibparse(); -extern void *smtlib_createBuffer(int); -extern void smtlib_deleteBuffer(void *); -extern void smtlib_switchToBuffer(void *); -extern int smtlib_bufSize(); -extern void *smtlibBufState(); -void smtlib_setInteractive(bool); - -namespace CVC3 { - - // 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. - - // FIXME: This should probably go away eventually, when I figure out - // flex++ -- Sergey. - ParserTemp* parserTemp; - - int ParserTemp::error(const string& s) { - // FIXME: Fail better? - std::cerr << "error: " << s << "\n"; - exit(1); - return 0; - } - - // Internal storage class; I'll use member names without 'd_'s here - class ParserData { - public: - // Is the input given by the file name or as istream? - bool useName; - ParserTemp temp; - // Internal buffer used by the parser - void* buffer; - }; - - // Constructors - Parser::Parser(bool interactive, const std::string& fileName) - : d_data(new ParserData) { - if(fileName == "") { - // Use std::cin - d_data->useName = false; - d_data->temp.is = &cin; - d_data->temp.fileName = "stdin"; - d_data->temp.interactive = interactive; - } else { - // Open the file by name - d_data->useName = true; - d_data->temp.fileName = fileName; - d_data->temp.is = new ifstream(fileName.c_str()); - if (!(*d_data->temp.is)) { - // FIXME: Fail better? - std::cerr << "error: File not found: " << fileName << "\n"; - exit(1); - } - d_data->temp.interactive = false; - } - initParser(); - } - - Parser::Parser(std::istream& is, bool interactive) - : d_data(new ParserData) { - d_data->useName = false; - d_data->temp.is = &is; - d_data->temp.fileName = "stdin"; - d_data->temp.interactive = interactive; - initParser(); - } - - // Destructor - Parser::~Parser() { - if(d_data->useName) // Stream is ours; delete it - delete d_data->temp.is; - deleteParser(); - delete d_data; - } - - // Initialize the actual parser - void Parser::initParser() { - d_data->buffer = smtlib_createBuffer(smtlib_bufSize()); - d_data->temp.lineNum = 1; - } - - // Clean up the parser's internal data structures - void Parser::deleteParser() { - smtlib_deleteBuffer(d_data->buffer); - } - - - klee::expr::ExprHandle Parser::next() { - // If no more commands are available, return a Null Expr - if(d_data->temp.done) return NULL;//Expr(); - // Set the global var so the parser uses the right stream and EM - parserTemp = &(d_data->temp); - // Switch to our buffer, in case there are multiple instances of - // the parser running - smtlib_switchToBuffer(d_data->buffer); - smtlib_setInteractive(d_data->temp.interactive); - smtlibparse(); - // Reset the prompt to the main one - d_data->temp.setPrompt1(); - return d_data->temp.expr; - } - - bool Parser::done() const { return d_data->temp.done; } - - void Parser::printLocation(ostream & out) const - { - out << d_data->temp.fileName << ":" << d_data->temp.lineNum; - } - - void Parser::reset() - { - d_data->temp.expr = NULL;//Expr(); - } - - -} // end of namespace CVC3 |