CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file main.cpp 00004 * \brief Main program for cvc3 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Wed Dec 4 17:21:10 2002 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 * 00019 */ 00020 /*****************************************************************************/ 00021 00022 #include <signal.h> 00023 #include <fstream> 00024 #include <iomanip> 00025 00026 #include "os.h" 00027 #include "vc.h" 00028 #include "parser.h" 00029 #include "vc_cmd.h" 00030 #include "command_line_flags.h" 00031 #include "statistics.h" 00032 00033 #ifdef _MSC_VER 00034 #include <windows.h> 00035 #else 00036 #include <unistd.h> 00037 #endif 00038 00039 00040 using namespace std; 00041 using namespace CVC3; 00042 00043 00044 static void parse_args(int argc, char **argv, CLFlags &flags, 00045 string& fileName); 00046 static void printUsage(const CLFlags& flags, bool followDisplay); 00047 00048 // Our own name 00049 static string programName; 00050 00051 static ValidityChecker* vc = NULL; 00052 IF_DEBUG(static DebugTimer* pRuntime = NULL;) 00053 00054 #ifndef _MSC_VER 00055 void sighandler(int signum) { 00056 cerr << "\nInterrupted by signal " << signum; 00057 if(signum == SIGALRM) 00058 cerr << " (self-timeout)"; 00059 cerr << ". " << programName << " is aborting.\n"; 00060 // Print the debugging info 00061 IF_DEBUG(if (pRuntime != NULL) CVC3::debugger.setElapsed(*pRuntime);) 00062 IF_DEBUG(debugger.printAll();) 00063 if(vc != NULL && vc->getFlags()["stats"].getBool()) 00064 cout << vc->getStatistics() << endl; 00065 abort(); 00066 } 00067 #else 00068 DWORD WINAPI thread_timeout(PVOID timeout) { 00069 Sleep((int)timeout * 1000); 00070 cerr << "(self-timeout)." << endl; 00071 ExitProcess(1); 00072 } 00073 #endif 00074 00075 00076 int main(int argc, char **argv) 00077 { 00078 CLFlags flags(ValidityChecker::createFlags()); 00079 programName = string(argv[0]); 00080 IF_DEBUG(DebugTimer runtime(CVC3::debugger.timer("total runtime"));) 00081 IF_DEBUG(pRuntime = &runtime;) 00082 00083 #ifndef _MSC_VER 00084 signal(SIGINT, sighandler); 00085 signal(SIGTERM, sighandler); 00086 signal(SIGQUIT, sighandler); 00087 signal(SIGALRM, sighandler); 00088 #endif 00089 00090 string fileName(""); 00091 00092 try { 00093 parse_args(argc, argv, flags, fileName); 00094 } catch(Exception& e) { 00095 cerr << "*** " << e; 00096 cerr << "\n\nRun with -help option for usage information." << endl; 00097 exit(1); 00098 } 00099 00100 // Set the timeout, if given in the command line options 00101 int timeout = flags["timeout"].getInt(); 00102 if(timeout > 0) { 00103 #ifndef _MSC_VER 00104 alarm(timeout); 00105 #else 00106 // http://msdn2.microsoft.com/en-us/library/ms682453.aspx 00107 CreateThread(NULL, 0, thread_timeout, (PVOID)timeout, 0, NULL); 00108 #endif 00109 } 00110 00111 /* 00112 * Create and run the validity checker 00113 */ 00114 00115 // Debugging code may throw an exception 00116 try { 00117 vc = ValidityChecker::create(flags); 00118 } catch(Exception& e) { 00119 cerr << "*** Fatal exception: " << e << endl; 00120 exit(1); 00121 } 00122 00123 // -h flag sets "help" to false (+h would make it true, but that's 00124 // not what the user normally types in). 00125 if(!vc->getFlags()["help"].getBool()) { 00126 printUsage(vc->getFlags(), true); 00127 return 0; 00128 } 00129 if(!vc->getFlags()["unsupported"].getBool()) { 00130 printUsage(vc->getFlags(), false); 00131 return 0; 00132 } 00133 #ifndef VERSION 00134 #define VERSION "unknown" 00135 #endif 00136 // Similarly, -version sets the flag "version" to false 00137 if(!vc->getFlags()["version"].getBool()) { 00138 cout << "This is CVC3 version " << VERSION 00139 IF_DEBUG( << " (debug build)") 00140 << "\n\n"; 00141 cout << 00142 "Copyright (C) 2003-2010 by the Board of Trustees of Leland Stanford Junior\n" 00143 "University, New York University, and the University of Iowa.\n\n" 00144 "THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. " 00145 "USE IT AT YOUR OWN RISK.\n" 00146 << endl; 00147 return 0; 00148 } 00149 00150 try { 00151 // Calling getOutputLang() tests if the output language is 00152 // correctly specified; if not, an exception will be thrown 00153 InputLanguage outlang = vc->getEM()->getOutputLang(); 00154 if(outlang == SPASS_LANG && 00155 vc->getFlags()["translate"].getBool() && 00156 !vc->getFlags()["liftITE"].modified()) { 00157 // SPASS doesn't support ITE; make sure there are none 00158 vc->getFlags().setFlag("liftITE", true); 00159 } 00160 // Set the timer 00161 IF_DEBUG(CVC3::debugger.setCurrentTime(runtime);) 00162 // Read the input file 00163 vc->loadFile(fileName, vc->getEM()->getInputLang(), 00164 flags["interactive"].getBool()); 00165 } catch(Exception& e) { 00166 cerr << "*** Fatal exception: " << e << endl; 00167 exit(1); 00168 } 00169 00170 IF_DEBUG(CVC3::debugger.setElapsed(runtime);) 00171 00172 // Print the debugging info 00173 IF_DEBUG(debugger.printAll();) 00174 // Print statistics 00175 if(vc->getFlags()["stats"].getBool()) vc->printStatistics(); 00176 // Destruct the system 00177 TRACE_MSG("delete", "Deleting ValidityChecker [last trace from main.cpp]"); 00178 try { 00179 delete vc; 00180 } catch(Exception& e) { 00181 cerr << "*** Fatal exception: " << e << endl; 00182 exit(1); 00183 } 00184 00185 return 0; 00186 } 00187 00188 void printUsage(const CLFlags& flags, bool followDisplay) { 00189 cout << "Usage: " << programName << " [options]\n" 00190 << programName << " will read the input from STDIN and \n" 00191 << "print the result on STDOUT.\n" 00192 << "Boolean (b) options are set 'on' by +option and 'off' by -option\n" 00193 << "(for instance, +model or -model).\n" 00194 << "Integer (i), string (s) and vector (v) options \n" 00195 << "require a parameter, e.g. -width 80\n" 00196 << "Also, (v) options can appear multiple times setting " 00197 << "args on and off,\n" 00198 << "as in +trace \"enable this\" -trace \"disable that\".\n" 00199 << "Option names can be abbreviated to the " 00200 << "shortest unambiguous prefix.\n\n" 00201 << "The options are:\n"; 00202 vector<string> names; 00203 // Get all the names of options (they all match the empty string) 00204 flags.countFlags("", names); 00205 for(size_t i=0,iend=names.size(); i!=iend; ++i) { 00206 const CLFlag& f(flags[names[i]]); 00207 if (f.display() != followDisplay) continue; 00208 string tpStr; // Print type of the option 00209 string pref; // Print + or - in front of the option 00210 string name(names[i]); // Print name and optionally the value 00211 CLFlagType tp = f.getType(); 00212 switch(tp) { 00213 case CLFLAG_NULL: tpStr = "(null)"; break; 00214 case CLFLAG_BOOL: 00215 tpStr = "(b)"; pref = (f.getBool())? "+" : "-"; 00216 break; 00217 case CLFLAG_INT: 00218 tpStr = "(i)"; pref = "-"; name = name+" "+int2string(f.getInt()); 00219 break; 00220 case CLFLAG_STRING: 00221 tpStr = "(s)"; pref = "-"; name = name+" "+f.getString(); 00222 break; 00223 case CLFLAG_STRVEC: 00224 tpStr = "(v)"; pref = "-"; name = name; 00225 break; 00226 default: 00227 DebugAssert(false, "printUsage: unknown flag type"); 00228 } 00229 cout << " " << tpStr << " " << pref << setw(25); 00230 cout.setf(ios::left); 00231 cout << name << " " << f.getHelp() << "\n"; 00232 } 00233 cout << endl; 00234 } 00235 00236 00237 void parse_args(int argc, char **argv, CLFlags &flags, string& fileName) { 00238 /* skip 0'th argument */ 00239 argv++; 00240 argc--; 00241 bool seenFileName(false); 00242 00243 for( ; argc > 0; argc--, argv++) { 00244 if((*argv)[0] == '-' || (*argv)[0] == '+') { 00245 // A command-line option 00246 vector<string> names; 00247 bool val = ((*argv)[0] == '+'); 00248 size_t n = flags.countFlags((*argv)+1, names); 00249 if(n == 0) 00250 throw CLException(string(*argv) + " does not match any known option"); 00251 else if(n > 1) { 00252 ostringstream ss; 00253 ss << *argv << " is ambiguous. Possible matches are:\n"; 00254 for(size_t i=0,iend=names.size(); i!=iend; ++i) { 00255 ss << " " << names[i] << "\n"; 00256 } 00257 throw CLException(ss.str()); 00258 } else { 00259 string name = names[0]; 00260 // Single match; process the option 00261 CLFlagType tp = flags[name].getType(); 00262 switch(tp) { 00263 case CLFLAG_BOOL: flags.setFlag(name, val); break; 00264 case CLFLAG_INT: 00265 argc--; 00266 if(argc <= 0) 00267 throw CLException(string(*argv)+" (-"+name 00268 +") expects an integer argument."); 00269 argv++; 00270 // FIXME: test for *argv being an integer string 00271 flags.setFlag(name, atoi(*argv)); 00272 break; 00273 case CLFLAG_STRING: 00274 argc--; 00275 if(argc <= 0) 00276 throw CLException(string(*argv)+" (-"+name 00277 +") expects a string argument."); 00278 argv++; 00279 flags.setFlag(name, *argv); 00280 break; 00281 case CLFLAG_STRVEC: 00282 argc--; 00283 if(argc <= 0) 00284 throw CLException(string(*argv)+" (-"+name 00285 +") expects a string argument."); 00286 argv++; 00287 flags.setFlag(name, pair<string,bool>(*argv,val)); 00288 break; 00289 default: 00290 DebugAssert(false, "parse_args: Bad flag type: "+int2string(tp)); 00291 } 00292 } 00293 } else if(seenFileName) { 00294 throw CLException("More than one file name given: "+fileName 00295 +" and "+string(*argv)); 00296 } else { 00297 fileName = string(*argv); 00298 seenFileName = true; 00299 } 00300 } 00301 }