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