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 "main/command_executor.h"
  38 # ifdef PORTFOLIO_BUILD
  39 #    include "main/command_executor_portfolio.h"
  40 # endif
  41 #include "main/options.h"
  42 #include "smt/options.h"
  43 #include "theory/uf/options.h"
  44 #include "util/output.h"
  45 #include "util/result.h"
  46 #include "util/statistics_registry.h"
  47
  48 using namespace std;
  49 using namespace CVC4;
  50 using namespace CVC4::parser;
  51 using namespace CVC4::main;
  52
  53 namespace CVC4 {
  54   namespace main {
  55     /** Global options variable */
  56     CVC4_THREADLOCAL(Options*) pOptions;
  57
  58     /** Full argv[0] */
  59     const char *progPath;
  60
  61     /** Just the basename component of argv[0] */
  62     const char *progName;
  63
  64     /** A pointer to the CommandExecutor (the signal handlers need it) */
  65     CVC4::main::CommandExecutor* pExecutor = NULL;
  66
  67     /** A pointer to the totalTime driver stat (the signal handlers need it) */
  68     CVC4::TimerStat* pTotalTime = NULL;
  69
  70   }/* CVC4::main namespace */
  71 }/* CVC4 namespace */
  72
  73
  74 void printUsage(Options& opts, bool full) {
  75   stringstream ss;
  76   ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
  77       << endl
  78       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
  79       << endl
  80       << "CVC4 options:" << endl;
  81   if(full) {
  82     Options::printUsage( ss.str(), *opts[options::out] );
  83   } else {
  84     Options::printShortUsage( ss.str(), *opts[options::out] );
  85   }
  86 }
  87
  88 void printStatsFilterZeros(std::ostream& out, const std::string& statsString) {
  89   // read each line, if a number, check zero and skip if so
  90   // Stat are assumed to one-per line: "<statName>, <statValue>"
  91
  92   std::istringstream iss(statsString);
  93   std::string statName, statValue;
  94
  95   std::getline(iss, statName, ',');
  96
  97   while( !iss.eof() ) {
  98
  99     std::getline(iss, statValue, '\n');
 100
 101     double curFloat;
 102     bool isFloat = (std::istringstream(statValue) >> curFloat);
 103
 104     if( (isFloat && curFloat == 0) ||
 105         statValue == " \"0\"" ||
 106         statValue == " \"[]\"") {
 107       // skip
 108     } else {
 109       out << statName << "," << statValue << std::endl;
 110     }
 111
 112     std::getline(iss, statName, ',');
 113   }
 114
 115 }
 116
 117 int runCvc4(int argc, char* argv[], Options& opts) {
 118
 119   // Timer statistic
 120   pTotalTime = new TimerStat("totalTime");
 121   pTotalTime->start();
 122
 123   // For the signal handlers' benefit
 124   pOptions = &opts;
 125
 126   // Initialize the signal handlers
 127   cvc4_init();
 128
 129   progPath = argv[0];
 130
 131   // Parse the options
 132   vector<string> filenames = opts.parseOptions(argc, argv);
 133
 134 # ifndef PORTFOLIO_BUILD
 135   if( opts.wasSetByUser(options::threads) ||
 136       opts.wasSetByUser(options::threadStackSize) ||
 137       ! opts[options::threadArgv].empty() ) {
 138     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
 139   }
 140 # else
 141   if( opts[options::checkProofs] ) {
 142     throw OptionException("Cannot run portfolio in check-proofs mode.");
 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);
 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       }
 201     }
 202   }
 203
 204   if(opts[options::outputLanguage] == language::output::LANG_AUTO) {
 205     opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
 206   }
 207
 208   // Determine which messages to show based on smtcomp_mode and verbosity
 209   if(Configuration::isMuzzledBuild()) {
 210     DebugChannel.setStream(CVC4::null_os);
 211     TraceChannel.setStream(CVC4::null_os);
 212     NoticeChannel.setStream(CVC4::null_os);
 213     ChatChannel.setStream(CVC4::null_os);
 214     MessageChannel.setStream(CVC4::null_os);
 215     WarningChannel.setStream(CVC4::null_os);
 216   }
 217
 218   // important even for muzzled builds (to get result output right)
 219   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
 220
 221   // Create the expression manager using appropriate options
 222   ExprManager* exprMgr;
 223 # ifndef PORTFOLIO_BUILD
 224   exprMgr = new ExprManager(opts);
 225   pExecutor = new CommandExecutor(*exprMgr, opts);
 226 # else
 227   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
 228   if(opts.wasSetByUser(options::incrementalSolving) &&
 229      opts[options::incrementalSolving] &&
 230      !opts[options::incrementalParallel]) {
 231     Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
 232              << "Notice: ...the experimental --incremental-parallel option.\n";
 233     exprMgr = new ExprManager(opts);
 234     pExecutor = new CommandExecutor(*exprMgr, opts);
 235   } else {
 236     exprMgr = new ExprManager(threadOpts[0]);
 237     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
 238   }
 239 # endif
 240
 241   Parser* replayParser = NULL;
 242   if( opts[options::replayFilename] != "" ) {
 243     ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts);
 244
 245     if( opts[options::replayFilename] == "-") {
 246       if( inputFromStdin ) {
 247         throw OptionException("Replay file and input file can't both be stdin.");
 248       }
 249       replayParserBuilder.withStreamInput(cin);
 250     }
 251     replayParser = replayParserBuilder.build();
 252     opts.set(options::replayStream, new Parser::ExprStream(replayParser));
 253   }
 254   if( opts[options::replayLog] != NULL ) {
 255     *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
 256   }
 257
 258   int returnValue = 0;
 259   {
 260     // Timer statistic
 261     RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), pTotalTime);
 262
 263     // Filename statistics
 264     ReferenceStat< const char* > s_statFilename("filename", filename);
 265     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename);
 266
 267     // Parse and execute commands until we are done
 268     Command* cmd;
 269     bool status = true;
 270     if(opts[options::interactive] && inputFromStdin) {
 271       if(opts[options::tearDownIncremental] && opts[options::incrementalSolving]) {
 272         if(opts.wasSetByUser(options::incrementalSolving)) {
 273           throw OptionException("--tear-down-incremental incompatible with --incremental");
 274         }
 275
 276         cmd = new SetOptionCommand("incremental", false);
 277         cmd->setMuted(true);
 278         pExecutor->doCommand(cmd);
 279         delete cmd;
 280       }
 281 #ifndef PORTFOLIO_BUILD
 282       if(!opts.wasSetByUser(options::incrementalSolving)) {
 283         cmd = new SetOptionCommand("incremental", true);
 284         cmd->setMuted(true);
 285         pExecutor->doCommand(cmd);
 286         delete cmd;
 287       }
 288 #endif /* PORTFOLIO_BUILD */
 289       InteractiveShell shell(*exprMgr, opts);
 290       if(opts[options::interactivePrompt]) {
 291         Message() << Configuration::getPackageName()
 292                   << " " << Configuration::getVersionString();
 293         if(Configuration::isGitBuild()) {
 294           Message() << " [" << Configuration::getGitId() << "]";
 295         } else if(Configuration::isSubversionBuild()) {
 296           Message() << " [" << Configuration::getSubversionId() << "]";
 297         }
 298         Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 299                   << " assertions:"
 300                   << (Configuration::isAssertionBuild() ? "on" : "off")
 301                   << endl;
 302       }
 303       if(replayParser != NULL) {
 304         // have the replay parser use the declarations input interactively
 305         replayParser->useDeclarationsFrom(shell.getParser());
 306       }
 307       while((cmd = shell.readCommand())) {
 308         status = pExecutor->doCommand(cmd) && status;
 309         delete cmd;
 310       }
 311     } else if(opts[options::tearDownIncremental]) {
 312       if(opts[options::incrementalSolving]) {
 313         if(opts.wasSetByUser(options::incrementalSolving)) {
 314           throw OptionException("--tear-down-incremental incompatible with --incremental");
 315         }
 316
 317         cmd = new SetOptionCommand("incremental", false);
 318         cmd->setMuted(true);
 319         pExecutor->doCommand(cmd);
 320         delete cmd;
 321       }
 322
 323       ParserBuilder parserBuilder(exprMgr, filename, opts);
 324
 325       if( inputFromStdin ) {
 326 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 327         parserBuilder.withStreamInput(cin);
 328 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 329         parserBuilder.withLineBufferedStreamInput(cin);
 330 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 331       }
 332
 333       vector< vector<Command*> > allCommands;
 334       allCommands.push_back(vector<Command*>());
 335       Parser *parser = parserBuilder.build();
 336       if(replayParser != NULL) {
 337         // have the replay parser use the file's declarations
 338         replayParser->useDeclarationsFrom(parser);
 339       }
 340       bool needReset = false;
 341       while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) {
 342         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
 343           if(needReset) {
 344             pExecutor->reset();
 345             for(size_t i = 0; i < allCommands.size(); ++i) {
 346               for(size_t j = 0; j < allCommands[i].size(); ++j) {
 347                 Command* cmd = allCommands[i][j]->clone();
 348                 cmd->setMuted(true);
 349                 pExecutor->doCommand(cmd);
 350                 delete cmd;
 351               }
 352             }
 353             needReset = false;
 354           }
 355           *opts[options::out] << CommandSuccess();
 356           allCommands.push_back(vector<Command*>());
 357         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
 358           allCommands.pop_back(); // fixme leaks cmds here
 359           pExecutor->reset();
 360           for(size_t i = 0; i < allCommands.size(); ++i) {
 361             for(size_t j = 0; j < allCommands[i].size(); ++j) {
 362               Command* cmd = allCommands[i][j]->clone();
 363               cmd->setMuted(true);
 364               pExecutor->doCommand(cmd);
 365               delete cmd;
 366             }
 367           }
 368           *opts[options::out] << CommandSuccess();
 369         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
 370                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
 371           if(needReset) {
 372             pExecutor->reset();
 373             for(size_t i = 0; i < allCommands.size(); ++i) {
 374               for(size_t j = 0; j < allCommands[i].size(); ++j) {
 375                 Command* cmd = allCommands[i][j]->clone();
 376                 cmd->setMuted(true);
 377                 pExecutor->doCommand(cmd);
 378                 delete cmd;
 379               }
 380             }
 381           }
 382           status = pExecutor->doCommand(cmd);
 383           needReset = true;
 384         } else {
 385           Command* copy = cmd->clone();
 386           allCommands.back().push_back(copy);
 387           status = pExecutor->doCommand(cmd);
 388           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 389             delete cmd;
 390             break;
 391           }
 392         }
 393         delete cmd;
 394       }
 395       // Remove the parser
 396       delete parser;
 397     } else {
 398       if(!opts.wasSetByUser(options::incrementalSolving)) {
 399         cmd = new SetOptionCommand("incremental", false);
 400         cmd->setMuted(true);
 401         pExecutor->doCommand(cmd);
 402         delete cmd;
 403       }
 404
 405       ParserBuilder parserBuilder(exprMgr, filename, opts);
 406
 407       if( inputFromStdin ) {
 408 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 409         parserBuilder.withStreamInput(cin);
 410 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 411         parserBuilder.withLineBufferedStreamInput(cin);
 412 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 413       }
 414
 415       Parser *parser = parserBuilder.build();
 416       if(replayParser != NULL) {
 417         // have the replay parser use the file's declarations
 418         replayParser->useDeclarationsFrom(parser);
 419       }
 420       while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) {
 421         status = pExecutor->doCommand(cmd);
 422         if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 423           delete cmd;
 424           break;
 425         }
 426         delete cmd;
 427       }
 428       // Remove the parser
 429       delete parser;
 430     }
 431
 432     if( opts[options::replayStream] != NULL ) {
 433       // this deletes the expression parser too
 434       delete opts[options::replayStream];
 435       opts.set(options::replayStream, NULL);
 436     }
 437
 438     Result result;
 439     if(status) {
 440       result = pExecutor->getResult();
 441       returnValue = 0;
 442     } else {
 443       // there was some kind of error
 444       returnValue = 1;
 445     }
 446
 447 #ifdef CVC4_COMPETITION_MODE
 448     *opts[options::out] << flush;
 449     // exit, don't return (don't want destructors to run)
 450     // _exit() from unistd.h doesn't run global destructors
 451     // or other on_exit/atexit stuff.
 452     _exit(returnValue);
 453 #endif /* CVC4_COMPETITION_MODE */
 454
 455     ReferenceStat< Result > s_statSatResult("sat/unsat", result);
 456     RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult);
 457
 458     pTotalTime->stop();
 459
 460     // Set the global executor pointer to NULL first.  If we get a
 461     // signal while dumping statistics, we don't want to try again.
 462     if(opts[options::statistics]) {
 463       if(opts[options::statsHideZeros] == false) {
 464         pExecutor->flushStatistics(*opts[options::err]);
 465       } else {
 466         std::ostringstream ossStats;
 467         pExecutor->flushStatistics(ossStats);
 468         printStatsFilterZeros(*opts[options::err], ossStats.str());
 469       }
 470     }
 471
 472     // make sure to flush replay output log before early-exit
 473     if( opts[options::replayLog] != NULL ) {
 474       *opts[options::replayLog] << flush;
 475     }
 476
 477     // make sure out and err streams are flushed too
 478     *opts[options::out] << flush;
 479     *opts[options::err] << flush;
 480
 481 #ifdef CVC4_DEBUG
 482     if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
 483       _exit(returnValue);
 484     }
 485 #else /* CVC4_DEBUG */
 486     if(opts[options::earlyExit]) {
 487       _exit(returnValue);
 488     }
 489 #endif /* CVC4_DEBUG */
 490   }
 491
 492   // On exceptional exit, these are leaked, but that's okay... they
 493   // need to be around in that case for main() to print statistics.
 494   delete pTotalTime;
 495   delete pExecutor;
 496   delete exprMgr;
 497
 498   pTotalTime = NULL;
 499   pExecutor = NULL;
 500
 501   return returnValue;
 502 }