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