From d5cff960ae096569194835502bd2b821fe5e6c8a Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 17 Dec 2009 02:32:49 +0000 Subject: [PATCH] Minor changes from code review --- src/main/getopt.cpp | 11 +++++++---- src/main/main.cpp | 42 ++++++++++++++++++++++++++++++------------ src/main/main.h | 4 +++- 3 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 7f515c58b..ec4ee11a5 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -7,7 +7,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Contains code for handling command-line options **/ #include @@ -26,6 +26,7 @@ #include "usage.h" #include "about.h" #include "util/output.h" +#include "util/options.h" using namespace std; using namespace CVC4; @@ -34,7 +35,7 @@ namespace CVC4 { namespace main { static const char lang_help[] = "\ -Languages currently supported to the -L / --lang option:\n\ +Languages currently supported as arguments to the -L / --lang option:\n\ auto attempt to automatically determine the input language\n\ pl | cvc4 CVC4 presentation language\n\ smt | smtlib SMT-LIB format\n\ @@ -63,8 +64,9 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti // find the base name of the program const char *x = strrchr(progName, '/'); - if(x != NULL) + if(x != NULL) { progName = x + 1; + } opts->binary_name = string(progName); while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) { @@ -99,8 +101,9 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti break; } - if(strcmp(optarg, "help")) + if(strcmp(optarg, "help")) { throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); + } fputs(lang_help, stdout); exit(1); diff --git a/src/main/main.cpp b/src/main/main.cpp index d9d3988f1..4e408823f 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -7,7 +7,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Main driver for CVC4 executable. **/ #include @@ -26,6 +26,7 @@ #include "smt/smt_engine.h" #include "util/command.h" #include "util/output.h" +#include "util/options.h" using namespace std; using namespace CVC4; @@ -44,13 +45,15 @@ int main(int argc, char *argv[]) { // Parse the options int firstArgIndex = parseOptions(argc, argv, &options); - // If in competition mode, we flush the stdout immediately - if(options.smtcomp_mode) + // If in competition mode, set output stream option to flush immediately + if(options.smtcomp_mode) { cout << unitbuf; + } // We only accept one input file - if(argc > firstArgIndex + 1) + if(argc > firstArgIndex + 1) { throw new Exception("Too many input files specified."); + } // Create the expression manager ExprManager exprMgr; @@ -61,14 +64,18 @@ int main(int argc, char *argv[]) { // If no file supplied we read from standard input bool inputFromStdin = firstArgIndex >= argc; + // Auto-detect input language by filename extension if(!inputFromStdin && options.lang == Options::LANG_AUTO) { - if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4)) + if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4)) { options.lang = Options::LANG_SMTLIB; + } else if(!strcmp(".cvc", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4) || - !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5)) + !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5)) { options.lang = Options::LANG_CVC4; + } } + // Determine which messages to show based on smtcomp_mode and verbosity if(options.smtcomp_mode) { Debug.setStream(CVC4::null_os); Trace.setStream(CVC4::null_os); @@ -76,14 +83,18 @@ int main(int argc, char *argv[]) { Chat.setStream(CVC4::null_os); Warning.setStream(CVC4::null_os); } else { - if(options.verbosity < 2) + if(options.verbosity < 2) { Chat.setStream(CVC4::null_os); - if(options.verbosity < 1) + } + if(options.verbosity < 1) { Notice.setStream(CVC4::null_os); - if(options.verbosity < 0) + } + if(options.verbosity < 0) { Warning.setStream(CVC4::null_os); + } } + // Set up the input stream, either cin or a file const char* fname; istream* in; ifstream* file; @@ -128,24 +139,31 @@ int main(int argc, char *argv[]) { // Remove the parser delete parser; + // Delete handle to input file delete file; } catch(OptionException& e) { - if(options.smtcomp_mode) + if(options.smtcomp_mode) { cout << "unknown" << endl; + } cerr << "CVC4 Error:" << endl << e << endl; printf(usage, options.binary_name.c_str()); abort(); } catch(CVC4::Exception& e) { - if(options.smtcomp_mode) + if(options.smtcomp_mode) { cout << "unknown" << endl; + } cerr << "CVC4 Error:" << endl << e << endl; abort(); } catch(bad_alloc) { - if(options.smtcomp_mode) + if(options.smtcomp_mode) { cout << "unknown" << endl; + } cerr << "CVC4 ran out of memory." << endl; abort(); } catch(...) { + if(options.smtcomp_mode) { + cout << "unknown" << endl; + } cerr << "CVC4 threw an exception of unknown type." << endl; abort(); } diff --git a/src/main/main.h b/src/main/main.h index 60817d976..ff19110c4 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -15,12 +15,14 @@ #include "config.h" #include "util/exception.h" -#include "util/options.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H namespace CVC4 { + +struct Options; + namespace main { class OptionException : public CVC4::Exception { -- 2.30.2