1 /********************* */ 2 /*! \file main.cpp 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King, Christopher L. Conway 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Main driver for CVC4 executable 13 ** 14 ** Main driver for CVC4 executable. 15 **/ 16 #include "main/main.h" 17 18 #include <cstdlib> 19 #include <cstring> 20 #include <fstream> 21 #include <iostream> 22 #include <stdio.h> 23 #include <unistd.h> 24 25 #include "base/configuration.h" 26 #include "base/output.h" 27 #include "expr/expr_manager.h" 28 #include "main/command_executor.h" 29 #include "main/interactive_shell.h" 30 #include "options/language.h" 31 #include "options/options.h" 32 #include "parser/parser.h" 33 #include "parser/parser_builder.h" 34 #include "parser/parser_exception.h" 35 #include "smt/command.h" 36 #include "smt/smt_engine.h" 37 #include "util/result.h" 38 #include "util/statistics.h" 39 40 using namespace std; 41 using namespace CVC4; 42 using namespace CVC4::main; 43 using namespace CVC4::language; 44 45 /** 46 * CVC4's main() routine is just an exception-safe wrapper around CVC4. 47 * Please don't construct anything here. Even if the constructor is 48 * inside the try { }, an exception during destruction can cause 49 * problems. That's why main() wraps runCvc4() in the first place. 50 * Put everything in runCvc4(). 51 */ main(int argc,char * argv[])52int main(int argc, char* argv[]) { 53 Options opts; 54 try { 55 return runCvc4(argc, argv, opts); 56 } catch(OptionException& e) { 57 #ifdef CVC4_COMPETITION_MODE 58 *opts.getOut() << "unknown" << endl; 59 #endif 60 cerr << "CVC4 Error:" << endl << e << endl << endl 61 << "Please use --help to get help on command-line options." 62 << endl; 63 } catch(Exception& e) { 64 #ifdef CVC4_COMPETITION_MODE 65 *opts.getOut() << "unknown" << endl; 66 #endif 67 if (language::isOutputLang_smt2(opts.getOutputLanguage())) 68 { 69 *opts.getOut() << "(error \"" << e << "\")" << endl; 70 } else { 71 *opts.getErr() << "CVC4 Error:" << endl << e << endl; 72 } 73 if(opts.getStatistics() && pExecutor != NULL) { 74 pTotalTime->stop(); 75 pExecutor->flushStatistics(*opts.getErr()); 76 } 77 } 78 exit(1); 79 } 80