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[])52 int 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