src/main/driver_unified.cpp

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