src/main/driver_unified.cpp

   1 /*********************                                                        */
   2 /*! \file driver_unified.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Liana Hadarean, Tim King
   6  ** This file is part of the CVC4 project.
   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.\endverbatim
  11  **
  12  ** \brief Driver for CVC4 executable (cvc4)
  13  **/
  14
  15 #include <stdio.h>
  16 #include <unistd.h>
  17
  18 #include <chrono>
  19 #include <cstdlib>
  20 #include <cstring>
  21 #include <fstream>
  22 #include <iostream>
  23 #include <memory>
  24 #include <new>
  25
  26 #include "cvc4autoconfig.h"
  27
  28 #include "api/cvc4cpp.h"
  29 #include "base/configuration.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/options.h"
  37 #include "options/set_language.h"
  38 #include "parser/parser.h"
  39 #include "parser/parser_builder.h"
  40 #include "smt/command.h"
  41 #include "util/result.h"
  42
  43 using namespace std;
  44 using namespace CVC4;
  45 using namespace CVC4::parser;
  46 using namespace CVC4::main;
  47
  48 namespace CVC4 {
  49   namespace main {
  50     /** Global options variable */
  51     thread_local Options* pOptions;
  52
  53     /** Full argv[0] */
  54     const char *progPath;
  55
  56     /** Just the basename component of argv[0] */
  57     const std::string *progName;
  58
  59     /** A pointer to the CommandExecutor (the signal handlers need it) */
  60     CVC4::main::CommandExecutor* pExecutor = nullptr;
  61
  62   }/* CVC4::main namespace */
  63 }/* CVC4 namespace */
  64
  65
  66 void printUsage(Options& opts, bool full) {
  67   stringstream ss;
  68   ss << "usage: " << opts.getBinaryName() << " [options] [input-file]"
  69      << endl << endl
  70      << "Without an input file, or with `-', CVC4 reads from standard input."
  71      << endl << endl
  72      << "CVC4 options:" << endl;
  73   if(full) {
  74     Options::printUsage( ss.str(), *(opts.getOut()) );
  75   } else {
  76     Options::printShortUsage( ss.str(), *(opts.getOut()) );
  77   }
  78 }
  79
  80 int runCvc4(int argc, char* argv[], Options& opts) {
  81
  82   std::chrono::time_point totalTimeStart = std::chrono::steady_clock::now();
  83   // For the signal handlers' benefit
  84   pOptions = &opts;
  85
  86   // Initialize the signal handlers
  87   signal_handlers::install();
  88
  89   progPath = argv[0];
  90
  91   // Parse the options
  92   vector<string> filenames = Options::parseOptions(&opts, argc, argv);
  93
  94   auto limit = install_time_limit(opts);
  95
  96   string progNameStr = opts.getBinaryName();
  97   progName = &progNameStr;
  98
  99   if( opts.getHelp() ) {
 100     printUsage(opts, true);
 101     exit(1);
 102   } else if( opts.getLanguageHelp() ) {
 103     Options::printLanguageHelp(*(opts.getOut()));
 104     exit(1);
 105   } else if( opts.getVersion() ) {
 106     *(opts.getOut()) << Configuration::about().c_str() << flush;
 107     exit(0);
 108   }
 109
 110   segvSpin = opts.getSegvSpin();
 111
 112   // If in competition mode, set output stream option to flush immediately
 113 #ifdef CVC4_COMPETITION_MODE
 114   *(opts.getOut()) << unitbuf;
 115 #endif /* CVC4_COMPETITION_MODE */
 116
 117   // We only accept one input file
 118   if(filenames.size() > 1) {
 119     throw Exception("Too many input files specified.");
 120   }
 121
 122   // If no file supplied we will read from standard input
 123   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 124
 125   // if we're reading from stdin on a TTY, default to interactive mode
 126   if(!opts.wasSetByUserInteractive()) {
 127     opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
 128   }
 129
 130   // Auto-detect input language by filename extension
 131   std::string filenameStr("<stdin>");
 132   if (!inputFromStdin) {
 133     // Use swap to avoid copying the string
 134     // TODO: use std::move() when switching to c++11
 135     filenameStr.swap(filenames[0]);
 136   }
 137   const char* filename = filenameStr.c_str();
 138
 139   if(opts.getInputLanguage() == language::input::LANG_AUTO) {
 140     if( inputFromStdin ) {
 141       // We can't do any fancy detection on stdin
 142       opts.setInputLanguage(language::input::LANG_CVC4);
 143     } else {
 144       unsigned len = filenameStr.size();
 145       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 146         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
 147       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 148                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 149         opts.setInputLanguage(language::input::LANG_TPTP);
 150       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 151                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 152         opts.setInputLanguage(language::input::LANG_CVC4);
 153       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 154                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 155         // version 2 sygus is the default
 156         opts.setInputLanguage(language::input::LANG_SYGUS_V2);
 157       }
 158     }
 159   }
 160
 161   if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
 162     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
 163   }
 164
 165   // Determine which messages to show based on smtcomp_mode and verbosity
 166   if(Configuration::isMuzzledBuild()) {
 167     DebugChannel.setStream(&CVC4::null_os);
 168     TraceChannel.setStream(&CVC4::null_os);
 169     NoticeChannel.setStream(&CVC4::null_os);
 170     ChatChannel.setStream(&CVC4::null_os);
 171     MessageChannel.setStream(&CVC4::null_os);
 172     WarningChannel.setStream(&CVC4::null_os);
 173   }
 174
 175   // important even for muzzled builds (to get result output right)
 176   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 177
 178   // Create the command executor to execute the parsed commands
 179   pExecutor = new CommandExecutor(opts);
 180
 181   int returnValue = 0;
 182   {
 183     // notify SmtEngine that we are starting to parse
 184     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 185
 186     // Parse and execute commands until we are done
 187     std::unique_ptr<Command> cmd;
 188     bool status = true;
 189     if(opts.getInteractive() && inputFromStdin) {
 190       if(opts.getTearDownIncremental() > 0) {
 191         throw Exception(
 192             "--tear-down-incremental doesn't work in interactive mode");
 193       }
 194       if(!opts.wasSetByUserIncrementalSolving()) {
 195         cmd.reset(new SetOptionCommand("incremental", "true"));
 196         cmd->setMuted(true);
 197         pExecutor->doCommand(cmd);
 198       }
 199       InteractiveShell shell(pExecutor->getSolver(),
 200                              pExecutor->getSymbolManager());
 201       if(opts.getInteractivePrompt()) {
 202         CVC4Message() << Configuration::getPackageName() << " "
 203                       << Configuration::getVersionString();
 204         if(Configuration::isGitBuild()) {
 205           CVC4Message() << " [" << Configuration::getGitId() << "]";
 206         }
 207         CVC4Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 208                       << " assertions:"
 209                       << (Configuration::isAssertionBuild() ? "on" : "off")
 210                       << endl
 211                       << endl;
 212         CVC4Message() << Configuration::copyright() << endl;
 213       }
 214
 215       while(true) {
 216         try {
 217           cmd.reset(shell.readCommand());
 218         } catch(UnsafeInterruptException& e) {
 219           (*opts.getOut()) << CommandInterrupted();
 220           break;
 221         }
 222         if (cmd == nullptr)
 223           break;
 224         status = pExecutor->doCommand(cmd) && status;
 225         if (cmd->interrupted()) {
 226           break;
 227         }
 228       }
 229     } else if( opts.getTearDownIncremental() > 0) {
 230       if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
 231         // For tear-down-incremental values greater than 1, need incremental
 232         // on too.
 233         cmd.reset(new SetOptionCommand("incremental", "true"));
 234         cmd->setMuted(true);
 235         pExecutor->doCommand(cmd);
 236         // if(opts.wasSetByUserIncrementalSolving()) {
 237         //   throw OptionException(
 238         //     "--tear-down-incremental incompatible with --incremental");
 239         // }
 240
 241         // cmd.reset(new SetOptionCommand("incremental", "false"));
 242         // cmd->setMuted(true);
 243         // pExecutor->doCommand(cmd);
 244       }
 245
 246       ParserBuilder parserBuilder(pExecutor->getSolver(),
 247                                   pExecutor->getSymbolManager(),
 248                                   filename,
 249                                   opts);
 250
 251       if( inputFromStdin ) {
 252 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 253         parserBuilder.withStreamInput(cin);
 254 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 255         parserBuilder.withLineBufferedStreamInput(cin);
 256 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 257       }
 258
 259       vector< vector<Command*> > allCommands;
 260       allCommands.push_back(vector<Command*>());
 261       std::unique_ptr<Parser> parser(parserBuilder.build());
 262       int needReset = 0;
 263       // true if one of the commands was interrupted
 264       bool interrupted = false;
 265       while (status)
 266       {
 267         if (interrupted) {
 268           (*opts.getOut()) << CommandInterrupted();
 269           break;
 270         }
 271
 272         try {
 273           cmd.reset(parser->nextCommand());
 274           if (cmd == nullptr) break;
 275         } catch (UnsafeInterruptException& e) {
 276           interrupted = true;
 277           continue;
 278         }
 279
 280         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
 281           if(needReset >= opts.getTearDownIncremental()) {
 282             pExecutor->reset();
 283             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 284               if (interrupted) break;
 285               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 286               {
 287                 Command* ccmd = allCommands[i][j]->clone();
 288                 ccmd->setMuted(true);
 289                 pExecutor->doCommand(ccmd);
 290                 if (ccmd->interrupted())
 291                 {
 292                   interrupted = true;
 293                 }
 294                 delete ccmd;
 295               }
 296             }
 297             needReset = 0;
 298           }
 299           allCommands.push_back(vector<Command*>());
 300           Command* copy = cmd->clone();
 301           allCommands.back().push_back(copy);
 302           status = pExecutor->doCommand(cmd);
 303           if(cmd->interrupted()) {
 304             interrupted = true;
 305             continue;
 306           }
 307         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
 308           allCommands.pop_back(); // fixme leaks cmds here
 309           if (needReset >= opts.getTearDownIncremental()) {
 310             pExecutor->reset();
 311             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 312               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 313               {
 314                 std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
 315                 ccmd->setMuted(true);
 316                 pExecutor->doCommand(ccmd);
 317                 if (ccmd->interrupted())
 318                 {
 319                   interrupted = true;
 320                 }
 321               }
 322             }
 323             if (interrupted) continue;
 324             (*opts.getOut()) << CommandSuccess();
 325             needReset = 0;
 326           } else {
 327             status = pExecutor->doCommand(cmd);
 328             if(cmd->interrupted()) {
 329               interrupted = true;
 330               continue;
 331             }
 332           }
 333         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
 334                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
 335           if(needReset >= opts.getTearDownIncremental()) {
 336             pExecutor->reset();
 337             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 338               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 339               {
 340                 Command* ccmd = allCommands[i][j]->clone();
 341                 ccmd->setMuted(true);
 342                 pExecutor->doCommand(ccmd);
 343                 if (ccmd->interrupted())
 344                 {
 345                   interrupted = true;
 346                 }
 347                 delete ccmd;
 348               }
 349             }
 350             needReset = 0;
 351           } else {
 352             ++needReset;
 353           }
 354           if (interrupted) {
 355             continue;
 356           }
 357
 358           status = pExecutor->doCommand(cmd);
 359           if(cmd->interrupted()) {
 360             interrupted = true;
 361             continue;
 362           }
 363         } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
 364           pExecutor->doCommand(cmd);
 365           allCommands.clear();
 366           allCommands.push_back(vector<Command*>());
 367         } else {
 368           // We shouldn't copy certain commands, because they can cause
 369           // an error on replay since there's no associated sat/unsat check
 370           // preceding them.
 371           if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
 372              dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
 373              dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
 374              dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
 375              dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
 376              dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
 377              dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
 378              dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
 379              dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
 380              dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
 381             Command* copy = cmd->clone();
 382             allCommands.back().push_back(copy);
 383           }
 384           status = pExecutor->doCommand(cmd);
 385           if(cmd->interrupted()) {
 386             interrupted = true;
 387             continue;
 388           }
 389
 390           if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 391             break;
 392           }
 393         }
 394       }
 395     } else {
 396       if(!opts.wasSetByUserIncrementalSolving()) {
 397         cmd.reset(new SetOptionCommand("incremental", "false"));
 398         cmd->setMuted(true);
 399         pExecutor->doCommand(cmd);
 400       }
 401
 402       ParserBuilder parserBuilder(pExecutor->getSolver(),
 403                                   pExecutor->getSymbolManager(),
 404                                   filename,
 405                                   opts);
 406
 407       if( inputFromStdin ) {
 408 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 409         parserBuilder.withStreamInput(cin);
 410 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 411         parserBuilder.withLineBufferedStreamInput(cin);
 412 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 413       }
 414
 415       std::unique_ptr<Parser> parser(parserBuilder.build());
 416       bool interrupted = false;
 417       while (status)
 418       {
 419         if (interrupted) {
 420           (*opts.getOut()) << CommandInterrupted();
 421           pExecutor->reset();
 422           break;
 423         }
 424         try {
 425           cmd.reset(parser->nextCommand());
 426           if (cmd == nullptr) break;
 427         } catch (UnsafeInterruptException& e) {
 428           interrupted = true;
 429           continue;
 430         }
 431
 432         status = pExecutor->doCommand(cmd);
 433         if (cmd->interrupted() && status == 0) {
 434           interrupted = true;
 435           break;
 436         }
 437
 438         if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 439           break;
 440         }
 441       }
 442     }
 443
 444     api::Result result;
 445     if(status) {
 446       result = pExecutor->getResult();
 447       returnValue = 0;
 448     } else {
 449       // there was some kind of error
 450       returnValue = 1;
 451     }
 452
 453 #ifdef CVC4_COMPETITION_MODE
 454     opts.flushOut();
 455     // exit, don't return (don't want destructors to run)
 456     // _exit() from unistd.h doesn't run global destructors
 457     // or other on_exit/atexit stuff.
 458     _exit(returnValue);
 459 #endif /* CVC4_COMPETITION_MODE */
 460     pExecutor->getSmtEngine()->setResultStatistic(result.toString());
 461     std::chrono::duration totalTime = std::chrono::steady_clock::now() - totalTimeStart;
 462     pExecutor->getSmtEngine()->setTotalTimeStatistic(std::chrono::duration<double>(totalTime).count());
 463
 464     pExecutor->flushOutputStreams();
 465
 466 #ifdef CVC4_DEBUG
 467     if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
 468       _exit(returnValue);
 469     }
 470 #else /* CVC4_DEBUG */
 471     if(opts.getEarlyExit()) {
 472       _exit(returnValue);
 473     }
 474 #endif /* CVC4_DEBUG */
 475   }
 476
 477   delete pExecutor;
 478
 479   pExecutor = nullptr;
 480
 481   signal_handlers::cleanup();
 482
 483   return returnValue;
 484 }