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