src/main/driver_unified.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Morgan Deters, Liana Hadarean, Tim King
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Driver for cvc5 executable (cvc5).
  14  */
  15
  16 #include <stdio.h>
  17 #include <unistd.h>
  18
  19 #include <chrono>
  20 #include <cstdlib>
  21 #include <cstring>
  22 #include <fstream>
  23 #include <iostream>
  24 #include <memory>
  25 #include <new>
  26
  27 #include "api/cpp/cvc5.h"
  28 #include "base/configuration.h"
  29 #include "base/cvc5config.h"
  30 #include "base/output.h"
  31 #include "main/command_executor.h"
  32 #include "main/interactive_shell.h"
  33 #include "main/main.h"
  34 #include "main/signal_handlers.h"
  35 #include "main/time_limit.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 "smt/command.h"
  41 #include "smt/smt_engine.h"
  42 #include "util/result.h"
  43
  44 using namespace std;
  45 using namespace cvc5;
  46 using namespace cvc5::parser;
  47 using namespace cvc5::main;
  48
  49 namespace cvc5 {
  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 std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
  62
  63 /** The time point the binary started, accessible to signal handlers */
  64 std::unique_ptr<TotalTimer> totalTime;
  65
  66 TotalTimer::~TotalTimer()
  67 {
  68   if (pExecutor != nullptr)
  69   {
  70     auto duration = std::chrono::steady_clock::now() - d_start;
  71     pExecutor->getSmtEngine()->setTotalTimeStatistic(
  72         std::chrono::duration<double>(duration).count());
  73   }
  74     }
  75
  76     }  // namespace main
  77     }  // namespace cvc5
  78
  79 void printUsage(Options& opts, bool full) {
  80   stringstream ss;
  81   ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl
  82      << endl
  83      << "Without an input file, or with `-', cvc5 reads from standard input."
  84      << endl
  85      << endl
  86      << "cvc5 options:" << endl;
  87   if(full) {
  88     Options::printUsage( ss.str(), *(opts.getOut()) );
  89   } else {
  90     Options::printShortUsage( ss.str(), *(opts.getOut()) );
  91   }
  92 }
  93
  94 int runCvc5(int argc, char* argv[], Options& opts)
  95 {
  96   main::totalTime = std::make_unique<TotalTimer>();
  97   // For the signal handlers' benefit
  98   pOptions = &opts;
  99
 100   // Initialize the signal handlers
 101   signal_handlers::install();
 102
 103   progPath = argv[0];
 104
 105   // Parse the options
 106   vector<string> filenames = Options::parseOptions(&opts, argc, argv);
 107
 108   auto limit = install_time_limit(opts);
 109
 110   string progNameStr = opts.getBinaryName();
 111   progName = &progNameStr;
 112
 113   if( opts.getHelp() ) {
 114     printUsage(opts, true);
 115     exit(1);
 116   } else if( opts.getLanguageHelp() ) {
 117     Options::printLanguageHelp(*(opts.getOut()));
 118     exit(1);
 119   } else if( opts.getVersion() ) {
 120     *(opts.getOut()) << Configuration::about().c_str() << flush;
 121     exit(0);
 122   }
 123
 124   segvSpin = opts.getSegvSpin();
 125
 126   // If in competition mode, set output stream option to flush immediately
 127 #ifdef CVC5_COMPETITION_MODE
 128   *(opts.getOut()) << unitbuf;
 129 #endif /* CVC5_COMPETITION_MODE */
 130
 131   // We only accept one input file
 132   if(filenames.size() > 1) {
 133     throw Exception("Too many input files specified.");
 134   }
 135
 136   // If no file supplied we will read from standard input
 137   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 138
 139   // if we're reading from stdin on a TTY, default to interactive mode
 140   if(!opts.wasSetByUserInteractive()) {
 141     opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
 142   }
 143
 144   // Auto-detect input language by filename extension
 145   std::string filenameStr("<stdin>");
 146   if (!inputFromStdin) {
 147     // Use swap to avoid copying the string
 148     // TODO: use std::move() when switching to c++11
 149     filenameStr.swap(filenames[0]);
 150   }
 151   const char* filename = filenameStr.c_str();
 152
 153   if(opts.getInputLanguage() == language::input::LANG_AUTO) {
 154     if( inputFromStdin ) {
 155       // We can't do any fancy detection on stdin
 156       opts.setInputLanguage(language::input::LANG_CVC);
 157     } else {
 158       unsigned len = filenameStr.size();
 159       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 160         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
 161       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 162                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 163         opts.setInputLanguage(language::input::LANG_TPTP);
 164       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 165                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 166         opts.setInputLanguage(language::input::LANG_CVC);
 167       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 168                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 169         // version 2 sygus is the default
 170         opts.setInputLanguage(language::input::LANG_SYGUS_V2);
 171       }
 172     }
 173   }
 174
 175   if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
 176     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
 177   }
 178
 179   // Determine which messages to show based on smtcomp_mode and verbosity
 180   if(Configuration::isMuzzledBuild()) {
 181     DebugChannel.setStream(&cvc5::null_os);
 182     TraceChannel.setStream(&cvc5::null_os);
 183     NoticeChannel.setStream(&cvc5::null_os);
 184     ChatChannel.setStream(&cvc5::null_os);
 185     MessageChannel.setStream(&cvc5::null_os);
 186     WarningChannel.setStream(&cvc5::null_os);
 187   }
 188
 189   // important even for muzzled builds (to get result output right)
 190   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 191
 192   // Create the command executor to execute the parsed commands
 193   pExecutor = std::make_unique<CommandExecutor>(opts);
 194
 195   int returnValue = 0;
 196   {
 197     // notify SmtEngine that we are starting to parse
 198     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 199
 200     // Parse and execute commands until we are done
 201     std::unique_ptr<Command> cmd;
 202     bool status = true;
 203     if(opts.getInteractive() && inputFromStdin) {
 204       if(opts.getTearDownIncremental() > 0) {
 205         throw Exception(
 206             "--tear-down-incremental doesn't work in interactive mode");
 207       }
 208       if(!opts.wasSetByUserIncrementalSolving()) {
 209         cmd.reset(new SetOptionCommand("incremental", "true"));
 210         cmd->setMuted(true);
 211         pExecutor->doCommand(cmd);
 212       }
 213       InteractiveShell shell(pExecutor->getSolver(),
 214                              pExecutor->getSymbolManager());
 215       if(opts.getInteractivePrompt()) {
 216         CVC5Message() << Configuration::getPackageName() << " "
 217                       << Configuration::getVersionString();
 218         if(Configuration::isGitBuild()) {
 219           CVC5Message() << " [" << Configuration::getGitId() << "]";
 220         }
 221         CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 222                       << " assertions:"
 223                       << (Configuration::isAssertionBuild() ? "on" : "off")
 224                       << endl
 225                       << endl;
 226         CVC5Message() << Configuration::copyright() << endl;
 227       }
 228
 229       while(true) {
 230         try {
 231           cmd.reset(shell.readCommand());
 232         } catch(UnsafeInterruptException& e) {
 233           (*opts.getOut()) << CommandInterrupted();
 234           break;
 235         }
 236         if (cmd == nullptr)
 237           break;
 238         status = pExecutor->doCommand(cmd) && status;
 239         if (cmd->interrupted()) {
 240           break;
 241         }
 242       }
 243     } else if( opts.getTearDownIncremental() > 0) {
 244       if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
 245         // For tear-down-incremental values greater than 1, need incremental
 246         // on too.
 247         cmd.reset(new SetOptionCommand("incremental", "true"));
 248         cmd->setMuted(true);
 249         pExecutor->doCommand(cmd);
 250         // if(opts.wasSetByUserIncrementalSolving()) {
 251         //   throw OptionException(
 252         //     "--tear-down-incremental incompatible with --incremental");
 253         // }
 254
 255         // cmd.reset(new SetOptionCommand("incremental", "false"));
 256         // cmd->setMuted(true);
 257         // pExecutor->doCommand(cmd);
 258       }
 259
 260       ParserBuilder parserBuilder(pExecutor->getSolver(),
 261                                   pExecutor->getSymbolManager(),
 262                                   filename,
 263                                   opts);
 264
 265       if( inputFromStdin ) {
 266         parserBuilder.withStreamInput(cin);
 267       }
 268
 269       vector< vector<Command*> > allCommands;
 270       allCommands.push_back(vector<Command*>());
 271       std::unique_ptr<Parser> parser(parserBuilder.build());
 272       int needReset = 0;
 273       // true if one of the commands was interrupted
 274       bool interrupted = false;
 275       while (status)
 276       {
 277         if (interrupted) {
 278           (*opts.getOut()) << CommandInterrupted();
 279           break;
 280         }
 281
 282         try {
 283           cmd.reset(parser->nextCommand());
 284           if (cmd == nullptr) break;
 285         } catch (UnsafeInterruptException& e) {
 286           interrupted = true;
 287           continue;
 288         }
 289
 290         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
 291           if(needReset >= opts.getTearDownIncremental()) {
 292             pExecutor->reset();
 293             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 294               if (interrupted) break;
 295               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 296               {
 297                 Command* ccmd = allCommands[i][j]->clone();
 298                 ccmd->setMuted(true);
 299                 pExecutor->doCommand(ccmd);
 300                 if (ccmd->interrupted())
 301                 {
 302                   interrupted = true;
 303                 }
 304                 delete ccmd;
 305               }
 306             }
 307             needReset = 0;
 308           }
 309           allCommands.push_back(vector<Command*>());
 310           Command* copy = cmd->clone();
 311           allCommands.back().push_back(copy);
 312           status = pExecutor->doCommand(cmd);
 313           if(cmd->interrupted()) {
 314             interrupted = true;
 315             continue;
 316           }
 317         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
 318           allCommands.pop_back(); // fixme leaks cmds here
 319           if (needReset >= opts.getTearDownIncremental()) {
 320             pExecutor->reset();
 321             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 322               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 323               {
 324                 std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
 325                 ccmd->setMuted(true);
 326                 pExecutor->doCommand(ccmd);
 327                 if (ccmd->interrupted())
 328                 {
 329                   interrupted = true;
 330                 }
 331               }
 332             }
 333             if (interrupted) continue;
 334             (*opts.getOut()) << CommandSuccess();
 335             needReset = 0;
 336           } else {
 337             status = pExecutor->doCommand(cmd);
 338             if(cmd->interrupted()) {
 339               interrupted = true;
 340               continue;
 341             }
 342           }
 343         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
 344                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
 345           if(needReset >= opts.getTearDownIncremental()) {
 346             pExecutor->reset();
 347             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 348               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 349               {
 350                 Command* ccmd = allCommands[i][j]->clone();
 351                 ccmd->setMuted(true);
 352                 pExecutor->doCommand(ccmd);
 353                 if (ccmd->interrupted())
 354                 {
 355                   interrupted = true;
 356                 }
 357                 delete ccmd;
 358               }
 359             }
 360             needReset = 0;
 361           } else {
 362             ++needReset;
 363           }
 364           if (interrupted) {
 365             continue;
 366           }
 367
 368           status = pExecutor->doCommand(cmd);
 369           if(cmd->interrupted()) {
 370             interrupted = true;
 371             continue;
 372           }
 373         } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
 374           pExecutor->doCommand(cmd);
 375           allCommands.clear();
 376           allCommands.push_back(vector<Command*>());
 377         } else {
 378           // We shouldn't copy certain commands, because they can cause
 379           // an error on replay since there's no associated sat/unsat check
 380           // preceding them.
 381           if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
 382              dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
 383              dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
 384              dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
 385              dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
 386              dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
 387              dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
 388              dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
 389              dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
 390              dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
 391             Command* copy = cmd->clone();
 392             allCommands.back().push_back(copy);
 393           }
 394           status = pExecutor->doCommand(cmd);
 395           if(cmd->interrupted()) {
 396             interrupted = true;
 397             continue;
 398           }
 399
 400           if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 401             break;
 402           }
 403         }
 404       }
 405     } else {
 406       if(!opts.wasSetByUserIncrementalSolving()) {
 407         cmd.reset(new SetOptionCommand("incremental", "false"));
 408         cmd->setMuted(true);
 409         pExecutor->doCommand(cmd);
 410       }
 411
 412       ParserBuilder parserBuilder(pExecutor->getSolver(),
 413                                   pExecutor->getSymbolManager(),
 414                                   filename,
 415                                   opts);
 416
 417       if( inputFromStdin ) {
 418         parserBuilder.withStreamInput(cin);
 419       }
 420
 421       std::unique_ptr<Parser> parser(parserBuilder.build());
 422       bool interrupted = false;
 423       while (status)
 424       {
 425         if (interrupted) {
 426           (*opts.getOut()) << CommandInterrupted();
 427           pExecutor->reset();
 428           break;
 429         }
 430         try {
 431           cmd.reset(parser->nextCommand());
 432           if (cmd == nullptr) break;
 433         } catch (UnsafeInterruptException& e) {
 434           interrupted = true;
 435           continue;
 436         }
 437
 438         status = pExecutor->doCommand(cmd);
 439         if (cmd->interrupted() && status == 0) {
 440           interrupted = true;
 441           break;
 442         }
 443
 444         if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 445           break;
 446         }
 447       }
 448     }
 449
 450     api::Result result;
 451     if(status) {
 452       result = pExecutor->getResult();
 453       returnValue = 0;
 454     } else {
 455       // there was some kind of error
 456       returnValue = 1;
 457     }
 458
 459 #ifdef CVC5_COMPETITION_MODE
 460     opts.flushOut();
 461     // exit, don't return (don't want destructors to run)
 462     // _exit() from unistd.h doesn't run global destructors
 463     // or other on_exit/atexit stuff.
 464     _exit(returnValue);
 465 #endif /* CVC5_COMPETITION_MODE */
 466
 467     totalTime.reset();
 468     pExecutor->flushOutputStreams();
 469
 470 #ifdef CVC5_DEBUG
 471     if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
 472       _exit(returnValue);
 473     }
 474 #else  /* CVC5_DEBUG */
 475     if(opts.getEarlyExit()) {
 476       _exit(returnValue);
 477     }
 478 #endif /* CVC5_DEBUG */
 479   }
 480
 481   pExecutor.reset();
 482
 483   signal_handlers::cleanup();
 484
 485   return returnValue;
 486 }