src/main/main.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Morgan Deters, Aina Niemetz, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Main driver for cvc5 executable.
  14  */
  15 #include "main/main.h"
  16
  17 #include <stdio.h>
  18 #include <unistd.h>
  19
  20 #include <cstdlib>
  21 #include <cstring>
  22 #include <fstream>
  23 #include <iostream>
  24
  25 #include "api/cpp/cvc5.h"
  26 #include "base/configuration.h"
  27 #include "base/output.h"
  28 #include "main/command_executor.h"
  29 #include "main/interactive_shell.h"
  30 #include "options/base_options.h"
  31 #include "options/language.h"
  32 #include "options/option_exception.h"
  33 #include "options/options.h"
  34 #include "parser/parser.h"
  35 #include "parser/parser_builder.h"
  36 #include "parser/parser_exception.h"
  37 #include "util/result.h"
  38
  39 using namespace std;
  40 using namespace cvc5;
  41 using namespace cvc5::main;
  42 using namespace cvc5::language;
  43
  44 /**
  45  * cvc5's main() routine is just an exception-safe wrapper around cvc5.
  46  * Please don't construct anything here.  Even if the constructor is
  47  * inside the try { }, an exception during destruction can cause
  48  * problems.  That's why main() wraps runCvc5() in the first place.
  49  * Put everything in runCvc5().
  50  */
  51 int main(int argc, char* argv[])
  52 {
  53   std::unique_ptr<api::Solver> solver;
  54   try
  55   {
  56     solver = std::make_unique<api::Solver>();
  57     return runCvc5(argc, argv, solver);
  58   }
  59   catch (cvc5::api::CVC5ApiOptionException& e)
  60   {
  61 #ifdef CVC5_COMPETITION_MODE
  62     solver->getDriverOptions().out() << "unknown" << std::endl;
  63 #endif
  64     cerr << "(error \"" << e.getMessage() << "\")" << endl
  65          << endl
  66          << "Please use --help to get help on command-line options." << endl;
  67   }
  68   catch (OptionException& e)
  69   {
  70 #ifdef CVC5_COMPETITION_MODE
  71     solver->getDriverOptions().out() << "unknown" << std::endl;
  72 #endif
  73     cerr << "(error \"" << e.getMessage() << "\")" << endl
  74          << endl
  75          << "Please use --help to get help on command-line options." << endl;
  76   }
  77   catch (Exception& e)
  78   {
  79 #ifdef CVC5_COMPETITION_MODE
  80     solver->getDriverOptions().out() << "unknown" << std::endl;
  81 #endif
  82     if (language::isLangSmt2(solver->getOptions().base.outputLanguage))
  83     {
  84       solver->getDriverOptions().out()
  85           << "(error \"" << e << "\")" << std::endl;
  86     }
  87     else
  88     {
  89       solver->getDriverOptions().err()
  90           << "(error \"" << e << "\")" << std::endl;
  91     }
  92     if (solver->getOptions().base.statistics && pExecutor != nullptr)
  93     {
  94       totalTime.reset();
  95       pExecutor->printStatistics(solver->getDriverOptions().err());
  96     }
  97   }
  98   exit(1);
  99 }