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 // This must come before PORTFOLIO_BUILD.
  26 #include "cvc4autoconfig.h"
  27
  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
  34 #ifdef PORTFOLIO_BUILD
  35 #  include "main/command_executor_portfolio.h"
  36 #endif
  37
  38 #include "main/interactive_shell.h"
  39 #include "main/main.h"
  40 #include "options/options.h"
  41 #include "options/set_language.h"
  42 #include "parser/parser.h"
  43 #include "parser/parser_builder.h"
  44 #include "parser/parser_exception.h"
  45 #include "smt/command.h"
  46 #include "util/result.h"
  47 #include "util/statistics_registry.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.getBinaryName() << " [options] [input-file]"
  78      << endl << endl
  79      << "Without an input file, or with `-', CVC4 reads from standard input."
  80      << endl << endl
  81      << "CVC4 options:" << endl;
  82   if(full) {
  83     Options::printUsage( ss.str(), *(opts.getOut()) );
  84   } else {
  85     Options::printShortUsage( ss.str(), *(opts.getOut()) );
  86   }
  87 }
  88
  89 int runCvc4(int argc, char* argv[], Options& opts) {
  90
  91   // Timer statistic
  92   pTotalTime = new TimerStat("totalTime");
  93   pTotalTime->start();
  94
  95   // For the signal handlers' benefit
  96   pOptions = &opts;
  97
  98   // Initialize the signal handlers
  99   cvc4_init();
 100
 101   progPath = argv[0];
 102
 103   // Parse the options
 104   vector<string> filenames = Options::parseOptions(&opts, argc, argv);
 105
 106 # ifndef PORTFOLIO_BUILD
 107   if( opts.wasSetByUserThreads() ||
 108       opts.wasSetByUserThreadStackSize() ||
 109       (! opts.getThreadArgv().empty()) ) {
 110     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
 111   }
 112 # endif
 113
 114   progName = opts.getBinaryName().c_str();
 115
 116   if( opts.getHelp() ) {
 117     printUsage(opts, true);
 118     exit(1);
 119   } else if( opts.getLanguageHelp() ) {
 120     Options::printLanguageHelp(*(opts.getOut()));
 121     exit(1);
 122   } else if( opts.getVersion() ) {
 123     *(opts.getOut()) << Configuration::about().c_str() << flush;
 124     exit(0);
 125   }
 126
 127   segvSpin = opts.getSegvSpin();
 128
 129   // If in competition mode, set output stream option to flush immediately
 130 #ifdef CVC4_COMPETITION_MODE
 131   *(opts.getOut()) << unitbuf;
 132 #endif /* CVC4_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.wasSetByUserInteractive()) {
 144     opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
 145   }
 146
 147   // Auto-detect input language by filename extension
 148   const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
 149
 150   if(opts.getInputLanguage() == language::input::LANG_AUTO) {
 151     if( inputFromStdin ) {
 152       // We can't do any fancy detection on stdin
 153       opts.setInputLanguage(language::input::LANG_CVC4);
 154     } else {
 155       unsigned len = strlen(filename);
 156       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 157         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_0);
 158       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
 159         opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
 160       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
 161         opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
 162       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 163                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 164         opts.setInputLanguage(language::input::LANG_TPTP);
 165       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 166                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 167         opts.setInputLanguage(language::input::LANG_CVC4);
 168       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 169                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 170         opts.setInputLanguage(language::input::LANG_SYGUS);
 171         //since there is no sygus output language, set this to SMT lib 2
 172         //opts.setOutputLanguage(language::output::LANG_SMTLIB_V2_0);
 173       }
 174     }
 175   }
 176
 177   if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
 178     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
 179   }
 180
 181   // if doing sygus, turn on CEGQI by default
 182   if(opts.getInputLanguage() == language::input::LANG_SYGUS ){
 183     if( !opts.wasSetByUserCeGuidedInst()) {
 184       opts.setCeGuidedInst(true);
 185     }
 186     if( !opts.wasSetByUserDumpSynth()) {
 187       opts.setDumpSynth(true);
 188     }
 189   }
 190
 191   // Determine which messages to show based on smtcomp_mode and verbosity
 192   if(Configuration::isMuzzledBuild()) {
 193     DebugChannel.setStream(&CVC4::null_os);
 194     TraceChannel.setStream(&CVC4::null_os);
 195     NoticeChannel.setStream(&CVC4::null_os);
 196     ChatChannel.setStream(&CVC4::null_os);
 197     MessageChannel.setStream(&CVC4::null_os);
 198     WarningChannel.setStream(&CVC4::null_os);
 199   }
 200
 201   // important even for muzzled builds (to get result output right)
 202   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 203
 204   // Create the expression manager using appropriate options
 205   ExprManager* exprMgr;
 206 # ifndef PORTFOLIO_BUILD
 207   exprMgr = new ExprManager(opts);
 208   pExecutor = new CommandExecutor(*exprMgr, opts);
 209 # else
 210   OptionsList threadOpts;
 211   parseThreadSpecificOptions(threadOpts, opts);
 212
 213   bool useParallelExecutor = true;
 214   // incremental?
 215   if(opts.wasSetByUserIncrementalSolving() &&
 216      opts.getIncrementalSolving() &&
 217      (! opts.getIncrementalParallel()) ) {
 218     Notice() << "Notice: In --incremental mode, using the sequential solver"
 219              << " unless forced by...\n"
 220              << "Notice: ...the experimental --incremental-parallel option.\n";
 221     useParallelExecutor = false;
 222   }
 223   // proofs?
 224   if(opts.getCheckProofs()) {
 225     if(opts.getFallbackSequential()) {
 226       Warning() << "Warning: Falling back to sequential mode, as cannot run"
 227                 << " portfolio in check-proofs mode.\n";
 228       useParallelExecutor = false;
 229     }
 230     else {
 231       throw OptionException("Cannot run portfolio in check-proofs mode.");
 232     }
 233   }
 234   // pick appropriate one
 235   if(useParallelExecutor) {
 236     exprMgr = new ExprManager(threadOpts[0]);
 237     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
 238   } else {
 239     exprMgr = new ExprManager(opts);
 240     pExecutor = new CommandExecutor(*exprMgr, opts);
 241   }
 242 # endif
 243
 244   Parser* replayParser = NULL;
 245   if( opts.getReplayInputFilename() != "" ) {
 246     std::string replayFilename = opts.getReplayInputFilename();
 247     ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts);
 248
 249     if( replayFilename == "-") {
 250       if( inputFromStdin ) {
 251         throw OptionException("Replay file and input file can't both be stdin.");
 252       }
 253       replayParserBuilder.withStreamInput(cin);
 254     }
 255     replayParser = replayParserBuilder.build();
 256     pExecutor->setReplayStream(new Parser::ExprStream(replayParser));
 257   }
 258
 259   int returnValue = 0;
 260   {
 261     // Timer statistic
 262     RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(),
 263                                     pTotalTime);
 264
 265     // Filename statistics
 266     ReferenceStat< const char* > s_statFilename("filename", filename);
 267     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
 268                                       &s_statFilename);
 269
 270     // Parse and execute commands until we are done
 271     Command* cmd;
 272     bool status = true;
 273     if(opts.getInteractive() && inputFromStdin) {
 274       if(opts.getTearDownIncremental() > 0) {
 275         throw OptionException(
 276             "--tear-down-incremental doesn't work in interactive mode");
 277       }
 278 #ifndef PORTFOLIO_BUILD
 279       if(!opts.wasSetByUserIncrementalSolving()) {
 280         cmd = new SetOptionCommand("incremental", SExpr(true));
 281         cmd->setMuted(true);
 282         pExecutor->doCommand(cmd);
 283         delete cmd;
 284       }
 285 #endif /* PORTFOLIO_BUILD */
 286       InteractiveShell shell(*exprMgr, opts);
 287       if(opts.getInteractivePrompt()) {
 288         Message() << Configuration::getPackageName()
 289                   << " " << Configuration::getVersionString();
 290         if(Configuration::isGitBuild()) {
 291           Message() << " [" << Configuration::getGitId() << "]";
 292         } else if(Configuration::isSubversionBuild()) {
 293           Message() << " [" << Configuration::getSubversionId() << "]";
 294         }
 295         Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 296                   << " assertions:"
 297                   << (Configuration::isAssertionBuild() ? "on" : "off")
 298                   << endl;
 299       }
 300       if(replayParser != NULL) {
 301         // have the replay parser use the declarations input interactively
 302         replayParser->useDeclarationsFrom(shell.getParser());
 303       }
 304
 305       while(true) {
 306         try {
 307           cmd = shell.readCommand();
 308         } catch(UnsafeInterruptException& e) {
 309           (*opts.getOut()) << CommandInterrupted();
 310           break;
 311         }
 312         if (cmd == NULL)
 313           break;
 314         status = pExecutor->doCommand(cmd) && status;
 315         if (cmd->interrupted()) {
 316           delete cmd;
 317           break;
 318         }
 319         delete cmd;
 320       }
 321     } else if( opts.getTearDownIncremental() > 0) {
 322       if(!opts.getIncrementalSolving()) {
 323         cmd = new SetOptionCommand("incremental", SExpr(true));
 324         cmd->setMuted(true);
 325         pExecutor->doCommand(cmd);
 326         delete cmd;
 327         // if(opts.wasSetByUserIncrementalSolving()) {
 328         //   throw OptionException(
 329         //     "--tear-down-incremental incompatible with --incremental");
 330         // }
 331
 332         // cmd = new SetOptionCommand("incremental", SExpr(false));
 333         // cmd->setMuted(true);
 334         // pExecutor->doCommand(cmd);
 335         // delete cmd;
 336       }
 337
 338       ParserBuilder parserBuilder(exprMgr, filename, opts);
 339
 340       if( inputFromStdin ) {
 341 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 342         parserBuilder.withStreamInput(cin);
 343 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 344         parserBuilder.withLineBufferedStreamInput(cin);
 345 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 346       }
 347
 348       vector< vector<Command*> > allCommands;
 349       allCommands.push_back(vector<Command*>());
 350       Parser *parser = parserBuilder.build();
 351       if(replayParser != NULL) {
 352         // have the replay parser use the file's declarations
 353         replayParser->useDeclarationsFrom(parser);
 354       }
 355       int needReset = 0;
 356       // true if one of the commands was interrupted
 357       bool interrupted = false;
 358       while (status || opts.getContinuedExecution()) {
 359         if (interrupted) {
 360           (*opts.getOut()) << CommandInterrupted();
 361           break;
 362         }
 363
 364         try {
 365           cmd = parser->nextCommand();
 366           if (cmd == NULL) break;
 367         } catch (UnsafeInterruptException& e) {
 368           interrupted = true;
 369           continue;
 370         }
 371
 372         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
 373           if(needReset >= opts.getTearDownIncremental()) {
 374             pExecutor->reset();
 375             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 376               if (interrupted) break;
 377               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 378               {
 379                 Command* cmd = allCommands[i][j]->clone();
 380                 cmd->setMuted(true);
 381                 pExecutor->doCommand(cmd);
 382                 if(cmd->interrupted()) {
 383                   interrupted = true;
 384                 }
 385                 delete cmd;
 386               }
 387             }
 388             needReset = 0;
 389           }
 390           allCommands.push_back(vector<Command*>());
 391           Command* copy = cmd->clone();
 392           allCommands.back().push_back(copy);
 393           status = pExecutor->doCommand(cmd);
 394           if(cmd->interrupted()) {
 395             interrupted = true;
 396             continue;
 397           }
 398         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
 399           allCommands.pop_back(); // fixme leaks cmds here
 400           if (needReset >= opts.getTearDownIncremental()) {
 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               {
 405                 Command* cmd = allCommands[i][j]->clone();
 406                 cmd->setMuted(true);
 407                 pExecutor->doCommand(cmd);
 408                 if(cmd->interrupted()) {
 409                   interrupted = true;
 410                 }
 411                 delete cmd;
 412               }
 413             }
 414             if (interrupted) continue;
 415             (*opts.getOut()) << CommandSuccess();
 416             needReset = 0;
 417           } else {
 418             status = pExecutor->doCommand(cmd);
 419             if(cmd->interrupted()) {
 420               interrupted = true;
 421               continue;
 422             }
 423           }
 424         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
 425                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
 426           if(needReset >= opts.getTearDownIncremental()) {
 427             pExecutor->reset();
 428             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 429               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 430               {
 431                 Command* cmd = allCommands[i][j]->clone();
 432                 cmd->setMuted(true);
 433                 pExecutor->doCommand(cmd);
 434                 if(cmd->interrupted()) {
 435                   interrupted = true;
 436                 }
 437                 delete cmd;
 438               }
 439             }
 440             needReset = 0;
 441           } else {
 442             ++needReset;
 443           }
 444           if (interrupted) {
 445             continue;
 446           }
 447
 448           status = pExecutor->doCommand(cmd);
 449           if(cmd->interrupted()) {
 450             interrupted = true;
 451             continue;
 452           }
 453         } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
 454           pExecutor->doCommand(cmd);
 455           allCommands.clear();
 456           allCommands.push_back(vector<Command*>());
 457         } else {
 458           // We shouldn't copy certain commands, because they can cause
 459           // an error on replay since there's no associated sat/unsat check
 460           // preceding them.
 461           if(dynamic_cast<GetUnsatCoreCommand*>(cmd) == NULL &&
 462              dynamic_cast<GetProofCommand*>(cmd) == NULL &&
 463              dynamic_cast<GetValueCommand*>(cmd) == NULL &&
 464              dynamic_cast<GetModelCommand*>(cmd) == NULL &&
 465              dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
 466              dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL &&
 467              dynamic_cast<GetAssertionsCommand*>(cmd) == NULL &&
 468              dynamic_cast<GetInfoCommand*>(cmd) == NULL &&
 469              dynamic_cast<GetOptionCommand*>(cmd) == NULL &&
 470              dynamic_cast<EchoCommand*>(cmd) == NULL) {
 471             Command* copy = cmd->clone();
 472             allCommands.back().push_back(copy);
 473           }
 474           status = pExecutor->doCommand(cmd);
 475           if(cmd->interrupted()) {
 476             interrupted = true;
 477             continue;
 478           }
 479
 480           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 481             delete cmd;
 482             break;
 483           }
 484         }
 485         delete cmd;
 486       }
 487       // Remove the parser
 488       delete parser;
 489     } else {
 490       if(!opts.wasSetByUserIncrementalSolving()) {
 491         cmd = new SetOptionCommand("incremental", SExpr(false));
 492         cmd->setMuted(true);
 493         pExecutor->doCommand(cmd);
 494         delete cmd;
 495       }
 496
 497       ParserBuilder parserBuilder(exprMgr, filename, opts);
 498
 499       if( inputFromStdin ) {
 500 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 501         parserBuilder.withStreamInput(cin);
 502 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 503         parserBuilder.withLineBufferedStreamInput(cin);
 504 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 505       }
 506
 507       Parser *parser = parserBuilder.build();
 508       if(replayParser != NULL) {
 509         // have the replay parser use the file's declarations
 510         replayParser->useDeclarationsFrom(parser);
 511       }
 512       bool interrupted = false;
 513       while(status || opts.getContinuedExecution()) {
 514         if (interrupted) {
 515           (*opts.getOut()) << CommandInterrupted();
 516           pExecutor->reset();
 517           break;
 518         }
 519         try {
 520           cmd = parser->nextCommand();
 521           if (cmd == NULL) break;
 522         } catch (UnsafeInterruptException& e) {
 523           interrupted = true;
 524           continue;
 525         }
 526
 527         status = pExecutor->doCommand(cmd);
 528         if (cmd->interrupted() && status == 0) {
 529           interrupted = true;
 530           break;
 531         }
 532
 533         if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 534           delete cmd;
 535           break;
 536         }
 537         delete cmd;
 538       }
 539       // Remove the parser
 540       delete parser;
 541     }
 542
 543     Result result;
 544     if(status) {
 545       result = pExecutor->getResult();
 546       returnValue = 0;
 547     } else {
 548       // there was some kind of error
 549       returnValue = 1;
 550     }
 551
 552 #ifdef CVC4_COMPETITION_MODE
 553     opts.flushOut();
 554     // exit, don't return (don't want destructors to run)
 555     // _exit() from unistd.h doesn't run global destructors
 556     // or other on_exit/atexit stuff.
 557     _exit(returnValue);
 558 #endif /* CVC4_COMPETITION_MODE */
 559
 560     ReferenceStat< Result > s_statSatResult("sat/unsat", result);
 561     RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
 562                                        &s_statSatResult);
 563
 564     pTotalTime->stop();
 565
 566     // Tim: I think that following comment is out of date?
 567     // Set the global executor pointer to NULL first.  If we get a
 568     // signal while dumping statistics, we don't want to try again.
 569     pExecutor->flushOutputStreams();
 570
 571 #ifdef CVC4_DEBUG
 572     if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
 573       _exit(returnValue);
 574     }
 575 #else /* CVC4_DEBUG */
 576     if(opts.getEarlyExit()) {
 577       _exit(returnValue);
 578     }
 579 #endif /* CVC4_DEBUG */
 580   }
 581
 582   // On exceptional exit, these are leaked, but that's okay... they
 583   // need to be around in that case for main() to print statistics.
 584   delete pTotalTime;
 585   delete pExecutor;
 586   delete exprMgr;
 587
 588   pTotalTime = NULL;
 589   pExecutor = NULL;
 590
 591   cvc4_shutdown();
 592
 593   return returnValue;
 594 }