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-2018 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 "api/cvc4cpp.h"
  30 #include "base/configuration.h"
  31 #include "base/output.h"
  32 #include "expr/expr_iomanip.h"
  33 #include "expr/expr_manager.h"
  34 #include "main/command_executor.h"
  35
  36 #ifdef PORTFOLIO_BUILD
  37 #  include "main/command_executor_portfolio.h"
  38 #endif
  39
  40 #include "main/interactive_shell.h"
  41 #include "main/main.h"
  42 #include "options/options.h"
  43 #include "options/set_language.h"
  44 #include "parser/parser.h"
  45 #include "parser/parser_builder.h"
  46 #include "parser/parser_exception.h"
  47 #include "smt/command.h"
  48 #include "util/result.h"
  49 #include "util/statistics_registry.h"
  50
  51 using namespace std;
  52 using namespace CVC4;
  53 using namespace CVC4::parser;
  54 using namespace CVC4::main;
  55
  56 namespace CVC4 {
  57   namespace main {
  58     /** Global options variable */
  59     thread_local Options* pOptions;
  60
  61     /** Full argv[0] */
  62     const char *progPath;
  63
  64     /** Just the basename component of argv[0] */
  65     const std::string *progName;
  66
  67     /** A pointer to the CommandExecutor (the signal handlers need it) */
  68     CVC4::main::CommandExecutor* pExecutor = NULL;
  69
  70     /** A pointer to the totalTime driver stat (the signal handlers need it) */
  71     CVC4::TimerStat* pTotalTime = NULL;
  72
  73   }/* CVC4::main namespace */
  74 }/* CVC4 namespace */
  75
  76
  77 void printUsage(Options& opts, bool full) {
  78   stringstream ss;
  79   ss << "usage: " << opts.getBinaryName() << " [options] [input-file]"
  80      << endl << endl
  81      << "Without an input file, or with `-', CVC4 reads from standard input."
  82      << endl << endl
  83      << "CVC4 options:" << endl;
  84   if(full) {
  85     Options::printUsage( ss.str(), *(opts.getOut()) );
  86   } else {
  87     Options::printShortUsage( ss.str(), *(opts.getOut()) );
  88   }
  89 }
  90
  91 int runCvc4(int argc, char* argv[], Options& opts) {
  92
  93   // Timer statistic
  94   pTotalTime = new TimerStat("totalTime");
  95   pTotalTime->start();
  96
  97   // For the signal handlers' benefit
  98   pOptions = &opts;
  99
 100   // Initialize the signal handlers
 101   cvc4_init();
 102
 103   progPath = argv[0];
 104
 105   // Parse the options
 106   vector<string> filenames = Options::parseOptions(&opts, argc, argv);
 107
 108 # ifndef PORTFOLIO_BUILD
 109   if( opts.wasSetByUserThreads() ||
 110       opts.wasSetByUserThreadStackSize() ||
 111       (! opts.getThreadArgv().empty()) ) {
 112     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
 113   }
 114 # endif
 115
 116   string progNameStr = opts.getBinaryName();
 117   progName = &progNameStr;
 118
 119   if( opts.getHelp() ) {
 120     printUsage(opts, true);
 121     exit(1);
 122   } else if( opts.getLanguageHelp() ) {
 123     Options::printLanguageHelp(*(opts.getOut()));
 124     exit(1);
 125   } else if( opts.getVersion() ) {
 126     *(opts.getOut()) << Configuration::about().c_str() << flush;
 127     exit(0);
 128   }
 129
 130   segvSpin = opts.getSegvSpin();
 131
 132   // If in competition mode, set output stream option to flush immediately
 133 #ifdef CVC4_COMPETITION_MODE
 134   *(opts.getOut()) << unitbuf;
 135 #endif /* CVC4_COMPETITION_MODE */
 136
 137   // We only accept one input file
 138   if(filenames.size() > 1) {
 139     throw Exception("Too many input files specified.");
 140   }
 141
 142   // If no file supplied we will read from standard input
 143   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 144
 145   // if we're reading from stdin on a TTY, default to interactive mode
 146   if(!opts.wasSetByUserInteractive()) {
 147     opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
 148   }
 149
 150   // Auto-detect input language by filename extension
 151   std::string filenameStr("<stdin>");
 152   if (!inputFromStdin) {
 153     // Use swap to avoid copying the string
 154     // TODO: use std::move() when switching to c++11
 155     filenameStr.swap(filenames[0]);
 156   }
 157   const char* filename = filenameStr.c_str();
 158
 159   if(opts.getInputLanguage() == language::input::LANG_AUTO) {
 160     if( inputFromStdin ) {
 161       // We can't do any fancy detection on stdin
 162       opts.setInputLanguage(language::input::LANG_CVC4);
 163     } else {
 164       unsigned len = filenameStr.size();
 165       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 166         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
 167       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
 168         opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
 169       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
 170         opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
 171       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 172                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 173         opts.setInputLanguage(language::input::LANG_TPTP);
 174       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 175                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 176         opts.setInputLanguage(language::input::LANG_CVC4);
 177       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 178                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 179         opts.setInputLanguage(language::input::LANG_SYGUS);
 180         //since there is no sygus output language, set this to SMT lib 2
 181         //opts.setOutputLanguage(language::output::LANG_SMTLIB_V2_0);
 182       }
 183     }
 184   }
 185
 186   if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
 187     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
 188   }
 189
 190   // Determine which messages to show based on smtcomp_mode and verbosity
 191   if(Configuration::isMuzzledBuild()) {
 192     DebugChannel.setStream(&CVC4::null_os);
 193     TraceChannel.setStream(&CVC4::null_os);
 194     NoticeChannel.setStream(&CVC4::null_os);
 195     ChatChannel.setStream(&CVC4::null_os);
 196     MessageChannel.setStream(&CVC4::null_os);
 197     WarningChannel.setStream(&CVC4::null_os);
 198   }
 199
 200   // important even for muzzled builds (to get result output right)
 201   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 202
 203   // Create the expression manager using appropriate options
 204   std::unique_ptr<api::Solver> solver;
 205 # ifndef PORTFOLIO_BUILD
 206   solver.reset(new api::Solver(&opts));
 207   pExecutor = new CommandExecutor(solver.get(), opts);
 208 # else
 209   OptionsList threadOpts;
 210   parseThreadSpecificOptions(threadOpts, opts);
 211
 212   bool useParallelExecutor = true;
 213   // incremental?
 214   if(opts.wasSetByUserIncrementalSolving() &&
 215      opts.getIncrementalSolving() &&
 216      (! opts.getIncrementalParallel()) ) {
 217     Notice() << "Notice: In --incremental mode, using the sequential solver"
 218              << " unless forced by...\n"
 219              << "Notice: ...the experimental --incremental-parallel option.\n";
 220     useParallelExecutor = false;
 221   }
 222   // proofs?
 223   if(opts.getCheckProofs()) {
 224     if(opts.getFallbackSequential()) {
 225       Warning() << "Warning: Falling back to sequential mode, as cannot run"
 226                 << " portfolio in check-proofs mode.\n";
 227       useParallelExecutor = false;
 228     }
 229     else {
 230       throw OptionException("Cannot run portfolio in check-proofs mode.");
 231     }
 232   }
 233   // pick appropriate one
 234   if (useParallelExecutor)
 235   {
 236     solver.reset(new api::Solver(&threadOpts[0]));
 237     pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts);
 238   }
 239   else
 240   {
 241     solver.reset(new api::Solver(&opts));
 242     pExecutor = new CommandExecutor(solver.get(), opts);
 243   }
 244 # endif
 245
 246   std::unique_ptr<Parser> replayParser;
 247   if (opts.getReplayInputFilename() != "")
 248   {
 249     std::string replayFilename = opts.getReplayInputFilename();
 250     ParserBuilder replayParserBuilder(solver.get(), replayFilename, opts);
 251
 252     if( replayFilename == "-") {
 253       if( inputFromStdin ) {
 254         throw OptionException("Replay file and input file can't both be stdin.");
 255       }
 256       replayParserBuilder.withStreamInput(cin);
 257     }
 258     replayParser.reset(replayParserBuilder.build());
 259     pExecutor->setReplayStream(new Parser::ExprStream(replayParser.get()));
 260   }
 261
 262   int returnValue = 0;
 263   {
 264     // Timer statistic
 265     RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(),
 266                                     pTotalTime);
 267
 268     // Filename statistics
 269     ReferenceStat<std::string> s_statFilename("filename", filenameStr);
 270     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
 271                                       &s_statFilename);
 272
 273     // Parse and execute commands until we are done
 274     Command* cmd;
 275     bool status = true;
 276     if(opts.getInteractive() && inputFromStdin) {
 277       if(opts.getTearDownIncremental() > 0) {
 278         throw OptionException(
 279             "--tear-down-incremental doesn't work in interactive mode");
 280       }
 281 #ifndef PORTFOLIO_BUILD
 282       if(!opts.wasSetByUserIncrementalSolving()) {
 283         cmd = new SetOptionCommand("incremental", SExpr(true));
 284         cmd->setMuted(true);
 285         pExecutor->doCommand(cmd);
 286         delete cmd;
 287       }
 288 #endif /* PORTFOLIO_BUILD */
 289       InteractiveShell shell(solver.get());
 290       if(opts.getInteractivePrompt()) {
 291         Message() << Configuration::getPackageName()
 292                   << " " << Configuration::getVersionString();
 293         if(Configuration::isGitBuild()) {
 294           Message() << " [" << Configuration::getGitId() << "]";
 295         }
 296         Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 297                   << " assertions:"
 298                   << (Configuration::isAssertionBuild() ? "on" : "off")
 299                   << endl << endl;
 300         Message() << Configuration::copyright() << endl;
 301       }
 302       if(replayParser) {
 303         // have the replay parser use the declarations input interactively
 304         replayParser->useDeclarationsFrom(shell.getParser());
 305       }
 306
 307       while(true) {
 308         try {
 309           cmd = shell.readCommand();
 310         } catch(UnsafeInterruptException& e) {
 311           (*opts.getOut()) << CommandInterrupted();
 312           break;
 313         }
 314         if (cmd == NULL)
 315           break;
 316         status = pExecutor->doCommand(cmd) && status;
 317         if (cmd->interrupted()) {
 318           delete cmd;
 319           break;
 320         }
 321         delete cmd;
 322       }
 323     } else if( opts.getTearDownIncremental() > 0) {
 324       if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
 325         // For tear-down-incremental values greater than 1, need incremental
 326         // on too.
 327         cmd = new SetOptionCommand("incremental", SExpr(true));
 328         cmd->setMuted(true);
 329         pExecutor->doCommand(cmd);
 330         delete cmd;
 331         // if(opts.wasSetByUserIncrementalSolving()) {
 332         //   throw OptionException(
 333         //     "--tear-down-incremental incompatible with --incremental");
 334         // }
 335
 336         // cmd = new SetOptionCommand("incremental", SExpr(false));
 337         // cmd->setMuted(true);
 338         // pExecutor->doCommand(cmd);
 339         // delete cmd;
 340       }
 341
 342       ParserBuilder parserBuilder(solver.get(), filename, opts);
 343
 344       if( inputFromStdin ) {
 345 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 346         parserBuilder.withStreamInput(cin);
 347 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 348         parserBuilder.withLineBufferedStreamInput(cin);
 349 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 350       }
 351
 352       vector< vector<Command*> > allCommands;
 353       allCommands.push_back(vector<Command*>());
 354       std::unique_ptr<Parser> parser(parserBuilder.build());
 355       if(replayParser) {
 356         // have the replay parser use the file's declarations
 357         replayParser->useDeclarationsFrom(parser.get());
 358       }
 359       int needReset = 0;
 360       // true if one of the commands was interrupted
 361       bool interrupted = false;
 362       while (status || opts.getContinuedExecution()) {
 363         if (interrupted) {
 364           (*opts.getOut()) << CommandInterrupted();
 365           break;
 366         }
 367
 368         try {
 369           cmd = parser->nextCommand();
 370           if (cmd == NULL) break;
 371         } catch (UnsafeInterruptException& e) {
 372           interrupted = true;
 373           continue;
 374         }
 375
 376         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
 377           if(needReset >= opts.getTearDownIncremental()) {
 378             pExecutor->reset();
 379             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 380               if (interrupted) break;
 381               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 382               {
 383                 Command* cmd = allCommands[i][j]->clone();
 384                 cmd->setMuted(true);
 385                 pExecutor->doCommand(cmd);
 386                 if(cmd->interrupted()) {
 387                   interrupted = true;
 388                 }
 389                 delete cmd;
 390               }
 391             }
 392             needReset = 0;
 393           }
 394           allCommands.push_back(vector<Command*>());
 395           Command* copy = cmd->clone();
 396           allCommands.back().push_back(copy);
 397           status = pExecutor->doCommand(cmd);
 398           if(cmd->interrupted()) {
 399             interrupted = true;
 400             continue;
 401           }
 402         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
 403           allCommands.pop_back(); // fixme leaks cmds here
 404           if (needReset >= opts.getTearDownIncremental()) {
 405             pExecutor->reset();
 406             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 407               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 408               {
 409                 Command* cmd = allCommands[i][j]->clone();
 410                 cmd->setMuted(true);
 411                 pExecutor->doCommand(cmd);
 412                 if(cmd->interrupted()) {
 413                   interrupted = true;
 414                 }
 415                 delete cmd;
 416               }
 417             }
 418             if (interrupted) continue;
 419             (*opts.getOut()) << CommandSuccess();
 420             needReset = 0;
 421           } else {
 422             status = pExecutor->doCommand(cmd);
 423             if(cmd->interrupted()) {
 424               interrupted = true;
 425               continue;
 426             }
 427           }
 428         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
 429                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
 430           if(needReset >= opts.getTearDownIncremental()) {
 431             pExecutor->reset();
 432             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 433               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 434               {
 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             needReset = 0;
 445           } else {
 446             ++needReset;
 447           }
 448           if (interrupted) {
 449             continue;
 450           }
 451
 452           status = pExecutor->doCommand(cmd);
 453           if(cmd->interrupted()) {
 454             interrupted = true;
 455             continue;
 456           }
 457         } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
 458           pExecutor->doCommand(cmd);
 459           allCommands.clear();
 460           allCommands.push_back(vector<Command*>());
 461         } else {
 462           // We shouldn't copy certain commands, because they can cause
 463           // an error on replay since there's no associated sat/unsat check
 464           // preceding them.
 465           if(dynamic_cast<GetUnsatCoreCommand*>(cmd) == NULL &&
 466              dynamic_cast<GetProofCommand*>(cmd) == NULL &&
 467              dynamic_cast<GetValueCommand*>(cmd) == NULL &&
 468              dynamic_cast<GetModelCommand*>(cmd) == NULL &&
 469              dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
 470              dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL &&
 471              dynamic_cast<GetAssertionsCommand*>(cmd) == NULL &&
 472              dynamic_cast<GetInfoCommand*>(cmd) == NULL &&
 473              dynamic_cast<GetOptionCommand*>(cmd) == NULL &&
 474              dynamic_cast<EchoCommand*>(cmd) == NULL) {
 475             Command* copy = cmd->clone();
 476             allCommands.back().push_back(copy);
 477           }
 478           status = pExecutor->doCommand(cmd);
 479           if(cmd->interrupted()) {
 480             interrupted = true;
 481             continue;
 482           }
 483
 484           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 485             delete cmd;
 486             break;
 487           }
 488         }
 489         delete cmd;
 490       }
 491     } else {
 492       if(!opts.wasSetByUserIncrementalSolving()) {
 493         cmd = new SetOptionCommand("incremental", SExpr(false));
 494         cmd->setMuted(true);
 495         pExecutor->doCommand(cmd);
 496         delete cmd;
 497       }
 498
 499       ParserBuilder parserBuilder(solver.get(), 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       std::unique_ptr<Parser> parser(parserBuilder.build());
 510       if(replayParser) {
 511         // have the replay parser use the file's declarations
 512         replayParser->useDeclarationsFrom(parser.get());
 513       }
 514       bool interrupted = false;
 515       while(status || opts.getContinuedExecution()) {
 516         if (interrupted) {
 517           (*opts.getOut()) << 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     }
 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
 587   pTotalTime = NULL;
 588   pExecutor = NULL;
 589
 590   cvc4_shutdown();
 591
 592   return returnValue;
 593 }