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