src/main/driver_unified.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Morgan Deters, Liana Hadarean, Tim King
   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  * Driver for cvc5 executable (cvc5).
  14  */
  15
  16 #include <stdio.h>
  17 #include <unistd.h>
  18
  19 #include <chrono>
  20 #include <cstdlib>
  21 #include <cstring>
  22 #include <fstream>
  23 #include <iostream>
  24 #include <memory>
  25 #include <new>
  26
  27 #include "api/cpp/cvc5.h"
  28 #include "base/configuration.h"
  29 #include "base/cvc5config.h"
  30 #include "base/output.h"
  31 #include "main/command_executor.h"
  32 #include "main/interactive_shell.h"
  33 #include "main/main.h"
  34 #include "main/options.h"
  35 #include "main/signal_handlers.h"
  36 #include "main/time_limit.h"
  37 #include "options/base_options.h"
  38 #include "options/main_options.h"
  39 #include "options/option_exception.h"
  40 #include "options/options.h"
  41 #include "options/options_public.h"
  42 #include "options/parser_options.h"
  43 #include "options/set_language.h"
  44 #include "parser/parser.h"
  45 #include "parser/parser_builder.h"
  46 #include "smt/command.h"
  47 #include "smt/smt_engine.h"
  48 #include "util/result.h"
  49
  50 using namespace std;
  51 using namespace cvc5;
  52 using namespace cvc5::parser;
  53 using namespace cvc5::main;
  54
  55 namespace cvc5 {
  56 namespace main {
  57
  58 /** Full argv[0] */
  59 const char* progPath;
  60
  61 /** Just the basename component of argv[0] */
  62 std::string progName;
  63
  64 /** A pointer to the CommandExecutor (the signal handlers need it) */
  65 std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
  66
  67 /** The time point the binary started, accessible to signal handlers */
  68 std::unique_ptr<TotalTimer> totalTime;
  69
  70 TotalTimer::~TotalTimer()
  71 {
  72   if (pExecutor != nullptr)
  73   {
  74     auto duration = std::chrono::steady_clock::now() - d_start;
  75     pExecutor->getSmtEngine()->setTotalTimeStatistic(
  76         std::chrono::duration<double>(duration).count());
  77   }
  78     }
  79
  80     }  // namespace main
  81     }  // namespace cvc5
  82
  83     void printUsage(const api::DriverOptions& dopts, bool full)
  84     {
  85       std::stringstream ss;
  86       ss << "usage: " << progName << " [options] [input-file]" << std::endl
  87          << std::endl
  88          << "Without an input file, or with `-', cvc5 reads from standard "
  89             "input."
  90          << std::endl
  91          << std::endl
  92          << "cvc5 options:" << std::endl;
  93       if (full)
  94       {
  95         main::printUsage(ss.str(), dopts.out());
  96       }
  97       else
  98       {
  99         main::printShortUsage(ss.str(), dopts.out());
 100       }
 101     }
 102
 103 int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 104 {
 105   main::totalTime = std::make_unique<TotalTimer>();
 106
 107   // Initialize the signal handlers
 108   signal_handlers::install();
 109
 110   progPath = argv[0];
 111
 112   // Create the command executor to execute the parsed commands
 113   pExecutor = std::make_unique<CommandExecutor>(solver);
 114   api::DriverOptions dopts = solver->getDriverOptions();
 115   Options* opts = &pExecutor->getOptions();
 116
 117   // Parse the options
 118   std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
 119
 120   auto limit = install_time_limit(*opts);
 121
 122   if (opts->driver.help)
 123   {
 124     printUsage(dopts, true);
 125     exit(1);
 126   }
 127   else if (opts->base.languageHelp)
 128   {
 129     main::printLanguageHelp(dopts.out());
 130     exit(1);
 131   }
 132   else if (opts->driver.version)
 133   {
 134     dopts.out() << Configuration::about().c_str() << flush;
 135     exit(0);
 136   }
 137
 138   segvSpin = opts->driver.segvSpin;
 139
 140   // If in competition mode, set output stream option to flush immediately
 141 #ifdef CVC5_COMPETITION_MODE
 142   dopts.out() << unitbuf;
 143 #endif /* CVC5_COMPETITION_MODE */
 144
 145   // We only accept one input file
 146   if(filenames.size() > 1) {
 147     throw Exception("Too many input files specified.");
 148   }
 149
 150   // If no file supplied we will read from standard input
 151   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 152
 153   // if we're reading from stdin on a TTY, default to interactive mode
 154   if (!opts->driver.interactiveWasSetByUser)
 155   {
 156     opts->driver.interactive = inputFromStdin && isatty(fileno(stdin));
 157   }
 158
 159   // Auto-detect input language by filename extension
 160   std::string filenameStr("<stdin>");
 161   if (!inputFromStdin) {
 162     filenameStr = std::move(filenames[0]);
 163   }
 164   const char* filename = filenameStr.c_str();
 165
 166   if (solver->getOption("input-language") == "LANG_AUTO")
 167   {
 168     if( inputFromStdin ) {
 169       // We can't do any fancy detection on stdin
 170       solver->setOption("input-language", "cvc");
 171     } else {
 172       size_t len = filenameStr.size();
 173       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 174         solver->setOption("input-language", "smt2");
 175       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 176                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 177         solver->setOption("input-language", "tptp");
 178       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 179                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 180         solver->setOption("input-language", "cvc");
 181       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 182                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 183         // version 2 sygus is the default
 184         solver->setOption("input-language", "sygus2");
 185       }
 186     }
 187   }
 188
 189   if (solver->getOption("output-language") == "LANG_AUTO")
 190   {
 191     solver->setOption("output-language", solver->getOption("input-language"));
 192   }
 193   pExecutor->storeOptionsAsOriginal();
 194
 195   // Determine which messages to show based on smtcomp_mode and verbosity
 196   if(Configuration::isMuzzledBuild()) {
 197     DebugChannel.setStream(&cvc5::null_os);
 198     TraceChannel.setStream(&cvc5::null_os);
 199     NoticeChannel.setStream(&cvc5::null_os);
 200     ChatChannel.setStream(&cvc5::null_os);
 201     MessageChannel.setStream(&cvc5::null_os);
 202     WarningChannel.setStream(&cvc5::null_os);
 203   }
 204
 205   int returnValue = 0;
 206   {
 207     // notify SmtEngine that we are starting to parse
 208     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 209
 210     // Parse and execute commands until we are done
 211     std::unique_ptr<Command> cmd;
 212     bool status = true;
 213     if (opts->driver.interactive && inputFromStdin)
 214     {
 215       if (!opts->base.incrementalSolvingWasSetByUser)
 216       {
 217         cmd.reset(new SetOptionCommand("incremental", "true"));
 218         cmd->setMuted(true);
 219         pExecutor->doCommand(cmd);
 220       }
 221       InteractiveShell shell(pExecutor->getSolver(),
 222                              pExecutor->getSymbolManager());
 223
 224       CVC5Message() << Configuration::getPackageName() << " "
 225                     << Configuration::getVersionString();
 226       if (Configuration::isGitBuild())
 227       {
 228         CVC5Message() << " [" << Configuration::getGitId() << "]";
 229       }
 230       CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 231                     << " assertions:"
 232                     << (Configuration::isAssertionBuild() ? "on" : "off")
 233                     << endl
 234                     << endl;
 235       CVC5Message() << Configuration::copyright() << endl;
 236
 237       while(true) {
 238         try {
 239           cmd.reset(shell.readCommand());
 240         } catch(UnsafeInterruptException& e) {
 241           dopts.out() << CommandInterrupted();
 242           break;
 243         }
 244         if (cmd == nullptr)
 245           break;
 246         status = pExecutor->doCommand(cmd) && status;
 247         opts = &pExecutor->getOptions();
 248         if (cmd->interrupted()) {
 249           break;
 250         }
 251       }
 252     }
 253     else
 254     {
 255       if (!opts->base.incrementalSolvingWasSetByUser)
 256       {
 257         cmd.reset(new SetOptionCommand("incremental", "false"));
 258         cmd->setMuted(true);
 259         pExecutor->doCommand(cmd);
 260       }
 261
 262       ParserBuilder parserBuilder(
 263           pExecutor->getSolver(), pExecutor->getSymbolManager(), true);
 264       std::unique_ptr<Parser> parser(parserBuilder.build());
 265       if( inputFromStdin ) {
 266         parser->setInput(Input::newStreamInput(
 267             solver->getOption("input-language"), cin, filename));
 268       }
 269       else
 270       {
 271         parser->setInput(
 272             Input::newFileInput(solver->getOption("input-language"),
 273                                 filename,
 274                                 solver->getOption("mmap") == "true"));
 275       }
 276
 277       bool interrupted = false;
 278       while (status)
 279       {
 280         if (interrupted) {
 281           dopts.out() << CommandInterrupted();
 282           pExecutor->reset();
 283           opts = &pExecutor->getOptions();
 284           break;
 285         }
 286         try {
 287           cmd.reset(parser->nextCommand());
 288           if (cmd == nullptr) break;
 289         } catch (UnsafeInterruptException& e) {
 290           interrupted = true;
 291           continue;
 292         }
 293
 294         status = pExecutor->doCommand(cmd);
 295         opts = &pExecutor->getOptions();
 296         if (cmd->interrupted() && status == 0) {
 297           interrupted = true;
 298           break;
 299         }
 300
 301         if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 302           break;
 303         }
 304       }
 305     }
 306
 307     api::Result result;
 308     if(status) {
 309       result = pExecutor->getResult();
 310       returnValue = 0;
 311     } else {
 312       // there was some kind of error
 313       returnValue = 1;
 314     }
 315
 316 #ifdef CVC5_COMPETITION_MODE
 317     dopts.out() << std::flush;
 318     // exit, don't return (don't want destructors to run)
 319     // _exit() from unistd.h doesn't run global destructors
 320     // or other on_exit/atexit stuff.
 321     _exit(returnValue);
 322 #endif /* CVC5_COMPETITION_MODE */
 323
 324     totalTime.reset();
 325     pExecutor->flushOutputStreams();
 326
 327 #ifdef CVC5_DEBUG
 328     if (opts->driver.earlyExit && opts->driver.earlyExitWasSetByUser)
 329     {
 330       _exit(returnValue);
 331     }
 332 #else  /* CVC5_DEBUG */
 333     if (opts->driver.earlyExit)
 334     {
 335       _exit(returnValue);
 336     }
 337 #endif /* CVC5_DEBUG */
 338   }
 339
 340   pExecutor.reset();
 341
 342   signal_handlers::cleanup();
 343
 344   return returnValue;
 345 }