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