CVC3

main.cpp

Go to the documentation of this file.
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 }