CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file parser_temp.h 00004 * 00005 * Author: Sergey Berezin 00006 * 00007 * Created: Wed Feb 5 17:53:02 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 * A class used to communicate with the actual parser. No one else 00019 * should use it. 00020 */ 00021 /*****************************************************************************/ 00022 00023 #ifndef _cvc3__parser_temp_h_ 00024 #define _cvc3__parser_temp_h_ 00025 00026 #include "expr.h" 00027 #include "exception.h" 00028 00029 namespace CVC3 { 00030 00031 class ValidityChecker; 00032 class Translator; 00033 00034 class ParserTemp { 00035 private: 00036 // Counter for uniqueID of bound variables 00037 int d_uid; 00038 // The main prompt when running interactive 00039 std::string prompt1; 00040 // The interactive prompt in the middle of a multi-line command 00041 std::string prompt2; 00042 // The currently used prompt 00043 std::string prompt; 00044 public: 00045 ValidityChecker* vc; 00046 Translator* translator; 00047 std::istream* is; 00048 // The current input line 00049 int lineNum; 00050 // File name 00051 std::string fileName; 00052 // The last parsed Expr 00053 Expr expr; 00054 // Whether we are done or not 00055 bool done; 00056 // Whether we are running interactive 00057 bool interactive; 00058 // Whether arrays are enabled for smt-lib format 00059 bool arrFlag; 00060 // Whether bit-vectors are enabled for smt-lib format 00061 bool bvFlag; 00062 // Size of bit-vectors for smt-lib format 00063 int bvSize; 00064 // Did we encounter a formula query (smtlib) 00065 bool queryParsed; 00066 // Default constructor 00067 ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "), 00068 prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { } 00069 // Parser error handling (implemented in parser.cpp) 00070 int error(const std::string& s); 00071 // Get the next uniqueID as a string 00072 std::string uniqueID() { 00073 std::ostringstream ss; 00074 ss << d_uid++; 00075 return ss.str(); 00076 } 00077 // Get the current prompt 00078 std::string getPrompt() { return prompt; } 00079 // Set the prompt to the main one 00080 void setPrompt1() { prompt = prompt1; } 00081 // Set the prompt to the secondary one 00082 void setPrompt2() { prompt = prompt2; } 00083 }; 00084 00085 } // end of namespace CVC3 00086 00087 #endif