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