src/main/driver_unified.cpp

   1 /*********************                                                        */
   2 /*! \file driver_unified.cpp
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Driver for CVC4 executable (cvc4) unified for both
  13  ** sequential and portfolio versions
  14  **/
  15
  16 #include <cstdlib>
  17 #include <cstring>
  18 #include <fstream>
  19 #include <iostream>
  20 #include <new>
  21 #include <unistd.h>
  22
  23 #include <stdio.h>
  24 #include <unistd.h>
  25
  26 #include "cvc4autoconfig.h"
  27 #include "main/main.h"
  28 #include "main/interactive_shell.h"
  29 #include "main/options.h"
  30 #include "parser/parser.h"
  31 #include "parser/parser_builder.h"
  32 #include "parser/parser_exception.h"
  33 #include "expr/expr_manager.h"
  34 #include "expr/command.h"
  35 #include "util/configuration.h"
  36 #include "options/options.h"
  37 #include "theory/quantifiers/options.h"
  38 #include "main/command_executor.h"
  39
  40 #ifdef PORTFOLIO_BUILD
  41 #  include "main/command_executor_portfolio.h"
  42 #endif
  43
  44 #include "main/options.h"
  45 #include "smt/options.h"
  46 #include "util/output.h"
  47 #include "util/result.h"
  48 #include "util/statistics_registry.h"
  49
  50 using namespace std;
  51 using namespace CVC4;
  52 using namespace CVC4::parser;
  53 using namespace CVC4::main;
  54
  55 namespace CVC4 {
  56   namespace main {
  57     /** Global options variable */
  58     CVC4_THREADLOCAL(Options*) pOptions;
  59
  60     /** Full argv[0] */
  61     const char *progPath;
  62
  63     /** Just the basename component of argv[0] */
  64     const char *progName;
  65
  66     /** A pointer to the CommandExecutor (the signal handlers need it) */
  67     CVC4::main::CommandExecutor* pExecutor = NULL;
  68
  69     /** A pointer to the totalTime driver stat (the signal handlers need it) */
  70     CVC4::TimerStat* pTotalTime = NULL;
  71
  72   }/* CVC4::main namespace */
  73 }/* CVC4 namespace */
  74
  75
  76 void printUsage(Options& opts, bool full) {
  77   stringstream ss;
  78   ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
  79       << endl
  80       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
  81       << endl
  82       << "CVC4 options:" << endl;
  83   if(full) {
  84     Options::printUsage( ss.str(), *opts[options::out] );
  85   } else {
  86     Options::printShortUsage( ss.str(), *opts[options::out] );
  87   }
  88 }
  89
  90 void printStatsFilterZeros(std::ostream& out, const std::string& statsString) {
  91   // read each line, if a number, check zero and skip if so
  92   // Stat are assumed to one-per line: "<statName>, <statValue>"
  93
  94   std::istringstream iss(statsString);
  95   std::string statName, statValue;
  96
  97   std::getline(iss, statName, ',');
  98
  99   while( !iss.eof() ) {
 100
 101     std::getline(iss, statValue, '\n');
 102
 103     double curFloat;
 104     bool isFloat = (std::istringstream(statValue) >> curFloat);
 105
 106     if( (isFloat && curFloat == 0) ||
 107         statValue == " \"0\"" ||
 108         statValue == " \"[]\"") {
 109       // skip
 110     } else {
 111       out << statName << "," << statValue << std::endl;
 112     }
 113
 114     std::getline(iss, statName, ',');
 115   }
 116
 117 }
 118
 119 int runCvc4(int argc, char* argv[], Options& opts) {
 120
 121   // Timer statistic
 122   pTotalTime = new TimerStat("totalTime");
 123   pTotalTime->start();
 124
 125   // For the signal handlers' benefit
 126   pOptions = &opts;
 127
 128   // Initialize the signal handlers
 129   cvc4_init();
 130
 131   progPath = argv[0];
 132
 133   // Parse the options
 134   vector<string> filenames = opts.parseOptions(argc, argv);
 135
 136 # ifndef PORTFOLIO_BUILD
 137   if( opts.wasSetByUser(options::threads) ||
 138       opts.wasSetByUser(options::threadStackSize) ||
 139       ! opts[options::threadArgv].empty() ) {
 140     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
 141   }
 142 # else
 143   if( opts[options::checkProofs] ) {
 144     throw OptionException("Cannot run portfolio in check-proofs mode.");
 145   }
 146 # endif
 147
 148   progName = opts[options::binary_name].c_str();
 149
 150   if( opts[options::help] ) {
 151     printUsage(opts, true);
 152     exit(1);
 153   } else if( opts[options::languageHelp] ) {
 154     Options::printLanguageHelp(*opts[options::out]);
 155     exit(1);
 156   } else if( opts[options::version] ) {
 157     *opts[options::out] << Configuration::about().c_str() << flush;
 158     exit(0);
 159   }
 160
 161   segvSpin = opts[options::segvSpin];
 162
 163   // If in competition mode, set output stream option to flush immediately
 164 #ifdef CVC4_COMPETITION_MODE
 165   *opts[options::out] << unitbuf;
 166 #endif /* CVC4_COMPETITION_MODE */
 167
 168   // We only accept one input file
 169   if(filenames.size() > 1) {
 170     throw Exception("Too many input files specified.");
 171   }
 172
 173   // If no file supplied we will read from standard input
 174   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 175
 176   // if we're reading from stdin on a TTY, default to interactive mode
 177   if(!opts.wasSetByUser(options::interactive)) {
 178     opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
 179   }
 180
 181   // Auto-detect input language by filename extension
 182   const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
 183
 184   if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
 185     if( inputFromStdin ) {
 186       // We can't do any fancy detection on stdin
 187       opts.set(options::inputLanguage, language::input::LANG_CVC4);
 188     } else {
 189       unsigned len = strlen(filename);
 190       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 191         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_0);
 192       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
 193         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
 194       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
 195         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
 196       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 197                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 198         opts.set(options::inputLanguage, language::input::LANG_TPTP);
 199       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 200                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 201         opts.set(options::inputLanguage, language::input::LANG_CVC4);
 202       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 203                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 204         opts.set(options::inputLanguage, language::input::LANG_SYGUS);
 205         //since there is no sygus output language, set this to SMT lib 2
 206         //opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0);
 207       }
 208     }
 209   }
 210
 211   if(opts[options::outputLanguage] == language::output::LANG_AUTO) {
 212     opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
 213   }
 214
 215   // if doing sygus, turn on CEGQI by default
 216   if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){
 217     if( !opts.wasSetByUser(options::ceGuidedInst)) {
 218       opts.set(options::ceGuidedInst, true);
 219     }
 220     if( !opts.wasSetByUser(options::dumpSynth)) {
 221       opts.set(options::dumpSynth, true);
 222     }
 223   }
 224
 225   // Determine which messages to show based on smtcomp_mode and verbosity
 226   if(Configuration::isMuzzledBuild()) {
 227     DebugChannel.setStream(CVC4::null_os);
 228     TraceChannel.setStream(CVC4::null_os);
 229     NoticeChannel.setStream(CVC4::null_os);
 230     ChatChannel.setStream(CVC4::null_os);
 231     MessageChannel.setStream(CVC4::null_os);
 232     WarningChannel.setStream(CVC4::null_os);
 233   }
 234
 235   // important even for muzzled builds (to get result output right)
 236   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
 237
 238   // Create the expression manager using appropriate options
 239   ExprManager* exprMgr;
 240 # ifndef PORTFOLIO_BUILD
 241   exprMgr = new ExprManager(opts);
 242   pExecutor = new CommandExecutor(*exprMgr, opts);
 243 # else
 244   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
 245   if(opts.wasSetByUser(options::incrementalSolving) &&
 246      opts[options::incrementalSolving] &&
 247      !opts[options::incrementalParallel]) {
 248     Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
 249              << "Notice: ...the experimental --incremental-parallel option.\n";
 250     exprMgr = new ExprManager(opts);
 251     pExecutor = new CommandExecutor(*exprMgr, opts);
 252   } else {
 253     exprMgr = new ExprManager(threadOpts[0]);
 254     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
 255   }
 256 # endif
 257
 258   Parser* replayParser = NULL;
 259   if( opts[options::replayFilename] != "" ) {
 260     ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts);
 261
 262     if( opts[options::replayFilename] == "-") {
 263       if( inputFromStdin ) {
 264         throw OptionException("Replay file and input file can't both be stdin.");
 265       }
 266       replayParserBuilder.withStreamInput(cin);
 267     }
 268     replayParser = replayParserBuilder.build();
 269     opts.set(options::replayStream, new Parser::ExprStream(replayParser));
 270   }
 271   if( opts[options::replayLog] != NULL ) {
 272     *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
 273   }
 274
 275   int returnValue = 0;
 276   {
 277     // Timer statistic
 278     RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), pTotalTime);
 279
 280     // Filename statistics
 281     ReferenceStat< const char* > s_statFilename("filename", filename);
 282     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename);
 283
 284     // Parse and execute commands until we are done
 285     Command* cmd;
 286     bool status = true;
 287     if(opts[options::interactive] && inputFromStdin) {
 288       if(opts[options::tearDownIncremental]) {
 289         throw OptionException("--tear-down-incremental doesn't work in interactive mode");
 290       }
 291 #ifndef PORTFOLIO_BUILD
 292       if(!opts.wasSetByUser(options::incrementalSolving)) {
 293         cmd = new SetOptionCommand("incremental", true);
 294         cmd->setMuted(true);
 295         pExecutor->doCommand(cmd);
 296         delete cmd;
 297       }
 298 #endif /* PORTFOLIO_BUILD */
 299       InteractiveShell shell(*exprMgr, opts);
 300       if(opts[options::interactivePrompt]) {
 301         Message() << Configuration::getPackageName()
 302                   << " " << Configuration::getVersionString();
 303         if(Configuration::isGitBuild()) {
 304           Message() << " [" << Configuration::getGitId() << "]";
 305         } else if(Configuration::isSubversionBuild()) {
 306           Message() << " [" << Configuration::getSubversionId() << "]";
 307         }
 308         Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 309                   << " assertions:"
 310                   << (Configuration::isAssertionBuild() ? "on" : "off")
 311                   << endl;
 312       }
 313       if(replayParser != NULL) {
 314         // have the replay parser use the declarations input interactively
 315         replayParser->useDeclarationsFrom(shell.getParser());
 316       }
 317
 318       while(true) {
 319         try {
 320           cmd = shell.readCommand();
 321         } catch(UnsafeInterruptException& e) {
 322           *opts[options::out] << CommandInterrupted();
 323           break;
 324         }
 325         if (cmd == NULL)
 326           break;
 327         status = pExecutor->doCommand(cmd) && status;
 328         if (cmd->interrupted()) {
 329           delete cmd;
 330           break;
 331         }
 332         delete cmd;
 333       }
 334     } else if(opts[options::tearDownIncremental]) {
 335       if(opts[options::incrementalSolving]) {
 336         if(opts.wasSetByUser(options::incrementalSolving)) {
 337           throw OptionException("--tear-down-incremental incompatible with --incremental");
 338         }
 339
 340         cmd = new SetOptionCommand("incremental", false);
 341         cmd->setMuted(true);
 342         pExecutor->doCommand(cmd);
 343         delete cmd;
 344       }
 345
 346       ParserBuilder parserBuilder(exprMgr, filename, opts);
 347
 348       if( inputFromStdin ) {
 349 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 350         parserBuilder.withStreamInput(cin);
 351 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 352         parserBuilder.withLineBufferedStreamInput(cin);
 353 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 354       }
 355
 356       vector< vector<Command*> > allCommands;
 357       allCommands.push_back(vector<Command*>());
 358       Parser *parser = parserBuilder.build();
 359       if(replayParser != NULL) {
 360         // have the replay parser use the file's declarations
 361         replayParser->useDeclarationsFrom(parser);
 362       }
 363       bool needReset = false;
 364       // true if one of the commands was interrupted
 365       bool interrupted = false;
 366       while (status || opts[options::continuedExecution]) {
 367         if (interrupted) {
 368           *opts[options::out] << CommandInterrupted();
 369           break;
 370         }
 371
 372         try {
 373           cmd = parser->nextCommand();
 374           if (cmd == NULL) break;
 375         } catch (UnsafeInterruptException& e) {
 376           interrupted = true;
 377           continue;
 378         }
 379
 380         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
 381           if(needReset) {
 382             pExecutor->reset();
 383             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 384               if (interrupted) break;
 385               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
 386                 Command* cmd = allCommands[i][j]->clone();
 387                 cmd->setMuted(true);
 388                 pExecutor->doCommand(cmd);
 389                 if(cmd->interrupted()) {
 390                   interrupted = true;
 391                 }
 392                 delete cmd;
 393               }
 394             }
 395             needReset = false;
 396           }
 397           *opts[options::out] << CommandSuccess();
 398           allCommands.push_back(vector<Command*>());
 399         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
 400           allCommands.pop_back(); // fixme leaks cmds here
 401           pExecutor->reset();
 402           for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 403             for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
 404               Command* cmd = allCommands[i][j]->clone();
 405               cmd->setMuted(true);
 406               pExecutor->doCommand(cmd);
 407               if(cmd->interrupted()) {
 408                 interrupted = true;
 409               }
 410               delete cmd;
 411             }
 412           }
 413           if (interrupted) continue;
 414           *opts[options::out] << CommandSuccess();
 415         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
 416                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
 417           if(needReset) {
 418             pExecutor->reset();
 419             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 420               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
 421                 Command* cmd = allCommands[i][j]->clone();
 422                 cmd->setMuted(true);
 423                 pExecutor->doCommand(cmd);
 424                 if(cmd->interrupted()) {
 425                   interrupted = true;
 426                 }
 427                 delete cmd;
 428               }
 429             }
 430           }
 431           if (interrupted) {
 432             continue;
 433           }
 434
 435           status = pExecutor->doCommand(cmd);
 436           if(cmd->interrupted()) {
 437             interrupted = true;
 438             continue;
 439           }
 440           needReset = true;
 441         } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
 442           pExecutor->doCommand(cmd);
 443           allCommands.clear();
 444           allCommands.push_back(vector<Command*>());
 445         } else {
 446           // We shouldn't copy certain commands, because they can cause
 447           // an error on replay since there's no associated sat/unsat check
 448           // preceding them.
 449           if(dynamic_cast<GetUnsatCoreCommand*>(cmd) == NULL &&
 450              dynamic_cast<GetProofCommand*>(cmd) == NULL &&
 451              dynamic_cast<GetValueCommand*>(cmd) == NULL &&
 452              dynamic_cast<GetModelCommand*>(cmd) == NULL &&
 453              dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
 454              dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL &&
 455              dynamic_cast<GetAssertionsCommand*>(cmd) == NULL &&
 456              dynamic_cast<GetInfoCommand*>(cmd) == NULL &&
 457              dynamic_cast<GetOptionCommand*>(cmd) == NULL &&
 458              dynamic_cast<EchoCommand*>(cmd) == NULL) {
 459             Command* copy = cmd->clone();
 460             allCommands.back().push_back(copy);
 461           }
 462           status = pExecutor->doCommand(cmd);
 463           if(cmd->interrupted()) {
 464             interrupted = true;
 465             continue;
 466           }
 467
 468           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 469             delete cmd;
 470             break;
 471           }
 472         }
 473         delete cmd;
 474       }
 475       // Remove the parser
 476       delete parser;
 477     } else {
 478       if(!opts.wasSetByUser(options::incrementalSolving)) {
 479         cmd = new SetOptionCommand("incremental", false);
 480         cmd->setMuted(true);
 481         pExecutor->doCommand(cmd);
 482         delete cmd;
 483       }
 484
 485       ParserBuilder parserBuilder(exprMgr, filename, opts);
 486
 487       if( inputFromStdin ) {
 488 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 489         parserBuilder.withStreamInput(cin);
 490 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 491         parserBuilder.withLineBufferedStreamInput(cin);
 492 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 493       }
 494
 495       Parser *parser = parserBuilder.build();
 496       if(replayParser != NULL) {
 497         // have the replay parser use the file's declarations
 498         replayParser->useDeclarationsFrom(parser);
 499       }
 500       bool interrupted = false;
 501       while(status || opts[options::continuedExecution]) {
 502         if (interrupted) {
 503           *opts[options::out] << CommandInterrupted();
 504           pExecutor->reset();
 505           break;
 506         }
 507         try {
 508           cmd = parser->nextCommand();
 509           if (cmd == NULL) break;
 510         } catch (UnsafeInterruptException& e) {
 511           interrupted = true;
 512           continue;
 513         }
 514
 515         status = pExecutor->doCommand(cmd);
 516         if (cmd->interrupted() && status == 0) {
 517           interrupted = true;
 518           break;
 519         }
 520
 521         if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 522           delete cmd;
 523           break;
 524         }
 525         delete cmd;
 526       }
 527       // Remove the parser
 528       delete parser;
 529     }
 530
 531     if( opts[options::replayStream] != NULL ) {
 532       // this deletes the expression parser too
 533       delete opts[options::replayStream];
 534       opts.set(options::replayStream, NULL);
 535     }
 536
 537     Result result;
 538     if(status) {
 539       result = pExecutor->getResult();
 540       returnValue = 0;
 541     } else {
 542       // there was some kind of error
 543       returnValue = 1;
 544     }
 545
 546 #ifdef CVC4_COMPETITION_MODE
 547     *opts[options::out] << flush;
 548     // exit, don't return (don't want destructors to run)
 549     // _exit() from unistd.h doesn't run global destructors
 550     // or other on_exit/atexit stuff.
 551     _exit(returnValue);
 552 #endif /* CVC4_COMPETITION_MODE */
 553
 554     ReferenceStat< Result > s_statSatResult("sat/unsat", result);
 555     RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult);
 556
 557     pTotalTime->stop();
 558
 559     // Set the global executor pointer to NULL first.  If we get a
 560     // signal while dumping statistics, we don't want to try again.
 561     if(opts[options::statistics]) {
 562       if(opts[options::statsHideZeros] == false) {
 563         pExecutor->flushStatistics(*opts[options::err]);
 564       } else {
 565         std::ostringstream ossStats;
 566         pExecutor->flushStatistics(ossStats);
 567         printStatsFilterZeros(*opts[options::err], ossStats.str());
 568       }
 569     }
 570
 571     // make sure to flush replay output log before early-exit
 572     if( opts[options::replayLog] != NULL ) {
 573       *opts[options::replayLog] << flush;
 574     }
 575
 576     // make sure out and err streams are flushed too
 577     *opts[options::out] << flush;
 578     *opts[options::err] << flush;
 579
 580 #ifdef CVC4_DEBUG
 581     if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
 582       _exit(returnValue);
 583     }
 584 #else /* CVC4_DEBUG */
 585     if(opts[options::earlyExit]) {
 586       _exit(returnValue);
 587     }
 588 #endif /* CVC4_DEBUG */
 589   }
 590
 591   // On exceptional exit, these are leaked, but that's okay... they
 592   // need to be around in that case for main() to print statistics.
 593   delete pTotalTime;
 594   delete pExecutor;
 595   delete exprMgr;
 596
 597   pTotalTime = NULL;
 598   pExecutor = NULL;
 599
 600   return returnValue;
 601 }