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