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/base_options.h"
  37 #include "options/options.h"
  38 #include "options/parser_options.h"
  39 #include "options/main_options.h"
  40 #include "options/set_language.h"
  41 #include "parser/parser.h"
  42 #include "parser/parser_builder.h"
  43 #include "smt/command.h"
  44 #include "smt/smt_engine.h"
  45 #include "util/result.h"
  46
  47 using namespace std;
  48 using namespace cvc5;
  49 using namespace cvc5::parser;
  50 using namespace cvc5::main;
  51
  52 namespace cvc5 {
  53 namespace main {
  54 /** Global options variable */
  55 thread_local Options* pOptions;
  56
  57 /** Full argv[0] */
  58 const char* progPath;
  59
  60 /** Just the basename component of argv[0] */
  61 std::string progName;
  62
  63 /** A pointer to the CommandExecutor (the signal handlers need it) */
  64 std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
  65
  66 /** The time point the binary started, accessible to signal handlers */
  67 std::unique_ptr<TotalTimer> totalTime;
  68
  69 TotalTimer::~TotalTimer()
  70 {
  71   if (pExecutor != nullptr)
  72   {
  73     auto duration = std::chrono::steady_clock::now() - d_start;
  74     pExecutor->getSmtEngine()->setTotalTimeStatistic(
  75         std::chrono::duration<double>(duration).count());
  76   }
  77     }
  78
  79     }  // namespace main
  80     }  // namespace cvc5
  81
  82 void printUsage(Options& opts, bool full) {
  83   stringstream ss;
  84   ss << "usage: " << progName << " [options] [input-file]"
  85      << endl
  86      << endl
  87      << "Without an input file, or with `-', cvc5 reads from standard input."
  88      << endl
  89      << endl
  90      << "cvc5 options:" << endl;
  91   if(full) {
  92     Options::printUsage(ss.str(), *opts.base.out);
  93   } else {
  94     Options::printShortUsage(ss.str(), *opts.base.out);
  95   }
  96 }
  97
  98 int runCvc5(int argc, char* argv[], Options& opts)
  99 {
 100   main::totalTime = std::make_unique<TotalTimer>();
 101   // For the signal handlers' benefit
 102   pOptions = &opts;
 103
 104   // Initialize the signal handlers
 105   signal_handlers::install();
 106
 107   progPath = argv[0];
 108
 109   // Parse the options
 110   std::vector<string> filenames =
 111       Options::parseOptions(&opts, argc, argv, progName);
 112
 113   auto limit = install_time_limit(opts);
 114
 115   if (opts.driver.help)
 116   {
 117     printUsage(opts, true);
 118     exit(1);
 119   }
 120   else if (opts.base.languageHelp)
 121   {
 122     Options::printLanguageHelp(*opts.base.out);
 123     exit(1);
 124   }
 125   else if (opts.driver.version)
 126   {
 127     *opts.base.out << Configuration::about().c_str() << flush;
 128     exit(0);
 129   }
 130
 131   segvSpin = opts.driver.segvSpin;
 132
 133   // If in competition mode, set output stream option to flush immediately
 134 #ifdef CVC5_COMPETITION_MODE
 135   *opts.base.out << unitbuf;
 136 #endif /* CVC5_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.driver.interactiveWasSetByUser)
 148   {
 149     opts.driver.interactive = inputFromStdin && isatty(fileno(stdin));
 150   }
 151
 152   // Auto-detect input language by filename extension
 153   std::string filenameStr("<stdin>");
 154   if (!inputFromStdin) {
 155     // Use swap to avoid copying the string
 156     // TODO: use std::move() when switching to c++11
 157     filenameStr.swap(filenames[0]);
 158   }
 159   const char* filename = filenameStr.c_str();
 160
 161   if (opts.base.inputLanguage == language::input::LANG_AUTO)
 162   {
 163     if( inputFromStdin ) {
 164       // We can't do any fancy detection on stdin
 165       opts.base.inputLanguage = language::input::LANG_CVC;
 166     } else {
 167       size_t len = filenameStr.size();
 168       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 169         opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
 170       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 171                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 172         opts.base.inputLanguage = language::input::LANG_TPTP;
 173       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 174                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 175         opts.base.inputLanguage = language::input::LANG_CVC;
 176       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
 177                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
 178         // version 2 sygus is the default
 179         opts.base.inputLanguage = language::input::LANG_SYGUS_V2;
 180       }
 181     }
 182   }
 183
 184   if (opts.base.outputLanguage == language::output::LANG_AUTO)
 185   {
 186     opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage);
 187   }
 188
 189   // Determine which messages to show based on smtcomp_mode and verbosity
 190   if(Configuration::isMuzzledBuild()) {
 191     DebugChannel.setStream(&cvc5::null_os);
 192     TraceChannel.setStream(&cvc5::null_os);
 193     NoticeChannel.setStream(&cvc5::null_os);
 194     ChatChannel.setStream(&cvc5::null_os);
 195     MessageChannel.setStream(&cvc5::null_os);
 196     WarningChannel.setStream(&cvc5::null_os);
 197   }
 198
 199   // important even for muzzled builds (to get result output right)
 200   (*opts.base.out)
 201       << language::SetLanguage(opts.base.outputLanguage);
 202
 203   // Create the command executor to execute the parsed commands
 204   pExecutor = std::make_unique<CommandExecutor>(opts);
 205
 206   int returnValue = 0;
 207   {
 208     // notify SmtEngine that we are starting to parse
 209     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 210
 211     // Parse and execute commands until we are done
 212     std::unique_ptr<Command> cmd;
 213     bool status = true;
 214     if (opts.driver.interactive && inputFromStdin)
 215     {
 216       if (opts.driver.tearDownIncremental > 0)
 217       {
 218         throw Exception(
 219             "--tear-down-incremental doesn't work in interactive mode");
 220       }
 221       if (!opts.base.incrementalSolvingWasSetByUser)
 222       {
 223         cmd.reset(new SetOptionCommand("incremental", "true"));
 224         cmd->setMuted(true);
 225         pExecutor->doCommand(cmd);
 226       }
 227       InteractiveShell shell(pExecutor->getSolver(),
 228                              pExecutor->getSymbolManager());
 229       if (opts.driver.interactivePrompt)
 230       {
 231         CVC5Message() << Configuration::getPackageName() << " "
 232                       << Configuration::getVersionString();
 233         if(Configuration::isGitBuild()) {
 234           CVC5Message() << " [" << Configuration::getGitId() << "]";
 235         }
 236         CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 237                       << " assertions:"
 238                       << (Configuration::isAssertionBuild() ? "on" : "off")
 239                       << endl
 240                       << endl;
 241         CVC5Message() << Configuration::copyright() << endl;
 242       }
 243
 244       while(true) {
 245         try {
 246           cmd.reset(shell.readCommand());
 247         } catch(UnsafeInterruptException& e) {
 248           *opts.base.out << CommandInterrupted();
 249           break;
 250         }
 251         if (cmd == nullptr)
 252           break;
 253         status = pExecutor->doCommand(cmd) && status;
 254         if (cmd->interrupted()) {
 255           break;
 256         }
 257       }
 258     }
 259     else if (opts.driver.tearDownIncremental > 0)
 260     {
 261       if (!opts.base.incrementalSolving
 262           && opts.driver.tearDownIncremental > 1)
 263       {
 264         // For tear-down-incremental values greater than 1, need incremental
 265         // on too.
 266         cmd.reset(new SetOptionCommand("incremental", "true"));
 267         cmd->setMuted(true);
 268         pExecutor->doCommand(cmd);
 269         // if(opts.base.incrementalWasSetByUser) {
 270         //   throw OptionException(
 271         //     "--tear-down-incremental incompatible with --incremental");
 272         // }
 273
 274         // cmd.reset(new SetOptionCommand("incremental", "false"));
 275         // cmd->setMuted(true);
 276         // pExecutor->doCommand(cmd);
 277       }
 278
 279       ParserBuilder parserBuilder(pExecutor->getSolver(),
 280                                   pExecutor->getSymbolManager(),
 281                                   opts);
 282       std::unique_ptr<Parser> parser(parserBuilder.build());
 283       if( inputFromStdin ) {
 284         parser->setInput(Input::newStreamInput(
 285             opts.base.inputLanguage, cin, filename));
 286       }
 287       else
 288       {
 289         parser->setInput(Input::newFileInput(opts.base.inputLanguage,
 290                                              filename,
 291                                              opts.parser.memoryMap));
 292       }
 293
 294       vector< vector<Command*> > allCommands;
 295       allCommands.push_back(vector<Command*>());
 296       int needReset = 0;
 297       // true if one of the commands was interrupted
 298       bool interrupted = false;
 299       while (status)
 300       {
 301         if (interrupted) {
 302           *opts.base.out << CommandInterrupted();
 303           break;
 304         }
 305
 306         try {
 307           cmd.reset(parser->nextCommand());
 308           if (cmd == nullptr) break;
 309         } catch (UnsafeInterruptException& e) {
 310           interrupted = true;
 311           continue;
 312         }
 313
 314         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
 315           if (needReset >= opts.driver.tearDownIncremental)
 316           {
 317             pExecutor->reset();
 318             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
 319               if (interrupted) break;
 320               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
 321               {
 322                 Command* ccmd = allCommands[i][j]->clone();
 323                 ccmd->setMuted(true);
 324                 pExecutor->doCommand(ccmd);
 325                 if (ccmd->interrupted())
 326                 {
 327                   interrupted = true;
 328                 }
 329                 delete ccmd;
 330               }
 331             }
 332             needReset = 0;
 333           }
 334           allCommands.push_back(vector<Command*>());
 335           Command* copy = cmd->clone();
 336           allCommands.back().push_back(copy);
 337           status = pExecutor->doCommand(cmd);
 338           if(cmd->interrupted()) {
 339             interrupted = true;
 340             continue;
 341           }
 342         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
 343           allCommands.pop_back(); // fixme leaks cmds here
 344           if (needReset >= opts.driver.tearDownIncremental)
 345           {
 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                 std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
 351                 ccmd->setMuted(true);
 352                 pExecutor->doCommand(ccmd);
 353                 if (ccmd->interrupted())
 354                 {
 355                   interrupted = true;
 356                 }
 357               }
 358             }
 359             if (interrupted) continue;
 360             *opts.base.out << CommandSuccess();
 361             needReset = 0;
 362           }
 363           else
 364           {
 365             status = pExecutor->doCommand(cmd);
 366             if(cmd->interrupted()) {
 367               interrupted = true;
 368               continue;
 369             }
 370           }
 371         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
 372                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
 373           if (needReset >= opts.driver.tearDownIncremental)
 374           {
 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* ccmd = allCommands[i][j]->clone();
 380                 ccmd->setMuted(true);
 381                 pExecutor->doCommand(ccmd);
 382                 if (ccmd->interrupted())
 383                 {
 384                   interrupted = true;
 385                 }
 386                 delete ccmd;
 387               }
 388             }
 389             needReset = 0;
 390           }
 391           else
 392           {
 393             ++needReset;
 394           }
 395           if (interrupted) {
 396             continue;
 397           }
 398
 399           status = pExecutor->doCommand(cmd);
 400           if(cmd->interrupted()) {
 401             interrupted = true;
 402             continue;
 403           }
 404         } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
 405           pExecutor->doCommand(cmd);
 406           allCommands.clear();
 407           allCommands.push_back(vector<Command*>());
 408         } else {
 409           // We shouldn't copy certain commands, because they can cause
 410           // an error on replay since there's no associated sat/unsat check
 411           // preceding them.
 412           if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
 413              dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
 414              dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
 415              dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
 416              dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
 417              dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
 418              dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
 419              dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
 420              dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
 421              dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
 422             Command* copy = cmd->clone();
 423             allCommands.back().push_back(copy);
 424           }
 425           status = pExecutor->doCommand(cmd);
 426           if(cmd->interrupted()) {
 427             interrupted = true;
 428             continue;
 429           }
 430
 431           if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 432             break;
 433           }
 434         }
 435       }
 436     }
 437     else
 438     {
 439       if (!opts.base.incrementalSolvingWasSetByUser)
 440       {
 441         cmd.reset(new SetOptionCommand("incremental", "false"));
 442         cmd->setMuted(true);
 443         pExecutor->doCommand(cmd);
 444       }
 445
 446       ParserBuilder parserBuilder(pExecutor->getSolver(),
 447                                   pExecutor->getSymbolManager(),
 448                                   opts);
 449       std::unique_ptr<Parser> parser(parserBuilder.build());
 450       if( inputFromStdin ) {
 451         parser->setInput(Input::newStreamInput(
 452             opts.base.inputLanguage, cin, filename));
 453       }
 454       else
 455       {
 456         parser->setInput(Input::newFileInput(opts.base.inputLanguage,
 457                                              filename,
 458                                              opts.parser.memoryMap));
 459       }
 460
 461       bool interrupted = false;
 462       while (status)
 463       {
 464         if (interrupted) {
 465           *opts.base.out << CommandInterrupted();
 466           pExecutor->reset();
 467           break;
 468         }
 469         try {
 470           cmd.reset(parser->nextCommand());
 471           if (cmd == nullptr) break;
 472         } catch (UnsafeInterruptException& e) {
 473           interrupted = true;
 474           continue;
 475         }
 476
 477         status = pExecutor->doCommand(cmd);
 478         if (cmd->interrupted() && status == 0) {
 479           interrupted = true;
 480           break;
 481         }
 482
 483         if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
 484           break;
 485         }
 486       }
 487     }
 488
 489     api::Result result;
 490     if(status) {
 491       result = pExecutor->getResult();
 492       returnValue = 0;
 493     } else {
 494       // there was some kind of error
 495       returnValue = 1;
 496     }
 497
 498 #ifdef CVC5_COMPETITION_MODE
 499     if (opts.base.out != nullptr)
 500     {
 501       *opts.base.out << std::flush;
 502     }
 503     // exit, don't return (don't want destructors to run)
 504     // _exit() from unistd.h doesn't run global destructors
 505     // or other on_exit/atexit stuff.
 506     _exit(returnValue);
 507 #endif /* CVC5_COMPETITION_MODE */
 508
 509     totalTime.reset();
 510     pExecutor->flushOutputStreams();
 511
 512 #ifdef CVC5_DEBUG
 513     if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser)
 514     {
 515       _exit(returnValue);
 516     }
 517 #else  /* CVC5_DEBUG */
 518     if (opts.driver.earlyExit)
 519     {
 520       _exit(returnValue);
 521     }
 522 #endif /* CVC5_DEBUG */
 523   }
 524
 525   pExecutor.reset();
 526
 527   signal_handlers::cleanup();
 528
 529   return returnValue;
 530 }