Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Gereon Kremer, Morgan Deters
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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 <cvc5/cvc5.h>
      17                 :            : #include <cvc5/cvc5_parser.h>
      18                 :            : #include <stdio.h>
      19                 :            : #include <unistd.h>
      20                 :            : 
      21                 :            : #include <cstdlib>
      22                 :            : #include <cstring>
      23                 :            : #include <fstream>
      24                 :            : #include <iostream>
      25                 :            : #include <memory>
      26                 :            : #include <new>
      27                 :            : #include <optional>
      28                 :            : 
      29                 :            : #include "base/configuration.h"
      30                 :            : #include "base/cvc5config.h"
      31                 :            : #include "base/output.h"
      32                 :            : #include "main/command_executor.h"
      33                 :            : #include "main/interactive_shell.h"
      34                 :            : #include "main/main.h"
      35                 :            : #include "main/options.h"
      36                 :            : #include "main/portfolio_driver.h"
      37                 :            : #include "main/signal_handlers.h"
      38                 :            : #include "main/time_limit.h"
      39                 :            : #include "smt/solver_engine.h"
      40                 :            : #include "util/result.h"
      41                 :            : 
      42                 :            : using namespace std;
      43                 :            : using namespace cvc5::internal;
      44                 :            : using namespace cvc5::parser;
      45                 :            : using namespace cvc5::main;
      46                 :            : 
      47                 :            : namespace cvc5::main {
      48                 :            : 
      49                 :            : /** Full argv[0] */
      50                 :            : const char* progPath;
      51                 :            : 
      52                 :            : /** Just the basename component of argv[0] */
      53                 :            : std::string progName;
      54                 :            : 
      55                 :            : /** A pointer to the CommandExecutor (the signal handlers need it) */
      56                 :            : std::unique_ptr<CommandExecutor> pExecutor;
      57                 :            : 
      58                 :            : }  // namespace cvc5::main
      59                 :            : 
      60                 :      27848 : int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::Solver>& solver)
      61                 :            : {
      62                 :            :   // Initialize the signal handlers
      63                 :      27848 :   signal_handlers::install();
      64                 :            : 
      65                 :      27848 :   progPath = argv[0];
      66                 :            : 
      67                 :            :   // Create the command executor to execute the parsed commands
      68                 :      27848 :   pExecutor = std::make_unique<CommandExecutor>(solver);
      69                 :      27848 :   cvc5::DriverOptions dopts = solver->getDriverOptions();
      70                 :            : 
      71                 :            :   // Parse the options
      72                 :      51544 :   std::vector<string> filenames = parse(*solver, argc, argv, progName);
      73         [ +  + ]:      27843 :   if (solver->getOptionInfo("help").boolValue())
      74                 :            :   {
      75                 :          1 :     printUsage(progName, dopts.out());
      76                 :          1 :     exit(1);
      77                 :            :   }
      78         [ -  + ]:      27842 :   else if (solver->getOptionInfo("help-regular").boolValue())
      79                 :            :   {
      80                 :          0 :     printUsage(progName, dopts.out(), true);
      81                 :          0 :     exit(1);
      82                 :            :   }
      83         [ -  + ]:      27842 :   else if (solver->getOptionInfo("help-option-categories").boolValue())
      84                 :            :   {
      85                 :          0 :     printUsageCategories(*solver.get(), dopts.out());
      86                 :          0 :     exit(1);
      87                 :            :   }
      88                 :      94793 :   for (const auto& name : {"show-config",
      89                 :            :                            "copyright",
      90                 :            :                            "show-trace-tags",
      91         [ +  + ]:     122635 :                            "version"})
      92                 :            :   {
      93         [ +  + ]:      98939 :     if (solver->getOptionInfo(name).boolValue())
      94                 :            :     {
      95                 :       4146 :       std::exit(0);
      96                 :            :     }
      97                 :            :   }
      98                 :            : 
      99                 :      71088 :   auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue());
     100                 :      23696 :   segvSpin = solver->getOptionInfo("segv-spin").boolValue();
     101                 :            : 
     102                 :            :   // If in competition mode, set output stream option to flush immediately
     103                 :            : #ifdef CVC5_COMPETITION_MODE
     104                 :            :   dopts.out() << unitbuf;
     105                 :            : #endif /* CVC5_COMPETITION_MODE */
     106                 :            : 
     107                 :            :   // We only accept one input file
     108         [ -  + ]:      23696 :   if(filenames.size() > 1) {
     109                 :          0 :     throw Exception("Too many input files specified.");
     110                 :            :   }
     111                 :            : 
     112                 :            :   // If no file supplied we will read from standard input
     113 [ +  - ][ -  + ]:      23696 :   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
     114                 :            : 
     115                 :            :   // If we're reading from stdin, use interactive mode if we are a TTY.
     116         [ +  - ]:      23696 :   if (!solver->getOptionInfo("interactive").setByUser)
     117                 :            :   {
     118         [ -  + ]:      23696 :     pExecutor->setOptionInternal(
     119                 :            :         "interactive",
     120         [ -  - ]:          0 :         (inputFromStdin && isatty(fileno(stdin))) ? "true"  : "false");
     121                 :            :   }
     122                 :            : 
     123                 :            :   // Auto-detect input language by filename extension
     124                 :      23756 :   std::string filenameStr("<stdin>");
     125         [ +  - ]:      23696 :   if (!inputFromStdin) {
     126                 :      23696 :     filenameStr = std::move(filenames[0]);
     127                 :            :   }
     128                 :      23696 :   const char* filename = filenameStr.c_str();
     129                 :            :   cvc5::modes::InputLanguage ilang;
     130         [ +  + ]:      23696 :   if (solver->getOption("input-language") == "LANG_AUTO")
     131                 :            :   {
     132         [ -  + ]:      18891 :     if( inputFromStdin ) {
     133                 :            :       // We can't do any fancy detection on stdin
     134                 :          0 :       pExecutor->setOptionInternal("input-language", "smt2");
     135                 :            :     } else {
     136                 :      18891 :       size_t len = filenameStr.size();
     137 [ +  - ][ +  + ]:      18891 :       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
     138                 :      18712 :         pExecutor->setOptionInternal("input-language", "smt2");
     139 [ +  - ][ -  + ]:        179 :       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
     140 [ -  - ][ -  - ]:          0 :                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
     141                 :            :         // version 2 sygus is the default
     142                 :        179 :         pExecutor->setOptionInternal("input-language", "sygus2");
     143                 :            :       }
     144                 :            :     }
     145                 :            :   }
     146         [ +  + ]:      23696 :   if (solver->getOption("input-language") == "LANG_SYGUS_V2")
     147                 :            :   {
     148                 :            :     // Enable the sygus API. We set this here instead of in set defaults 
     149                 :            :     // to simplify checking at the API level. In particular, the sygus
     150                 :            :     // option is the authority on whether sygus commands are currently
     151                 :            :     // allowed in the API.
     152                 :        962 :     pExecutor->setOptionInternal("sygus", "true");
     153                 :        962 :     ilang = cvc5::modes::InputLanguage::SYGUS_2_1;
     154                 :            :   }
     155                 :            :   else
     156                 :            :   {
     157                 :      22734 :     ilang = cvc5::modes::InputLanguage::SMT_LIB_2_6;
     158                 :            :   }
     159                 :            : 
     160         [ -  + ]:      23696 :   if (solver->getOption("output-language") == "LANG_AUTO")
     161                 :            :   {
     162                 :          0 :     pExecutor->setOptionInternal("output-language",
     163                 :          0 :                                  solver->getOption("input-language"));
     164                 :            :   }
     165                 :            : 
     166                 :            :   // Determine which messages to show based on smtcomp_mode and verbosity
     167         [ -  + ]:      23696 :   if(Configuration::isMuzzledBuild()) {
     168                 :          0 :     TraceChannel.setStream(&cvc5::internal::null_os);
     169                 :          0 :     WarningChannel.setStream(&cvc5::internal::null_os);
     170                 :            :   }
     171                 :            : 
     172                 :      23696 :   int returnValue = 0;
     173                 :            :   {
     174                 :      23696 :     solver->setInfo("filename", filenameStr);
     175                 :            : 
     176                 :            :     // Parse and execute commands until we are done
     177                 :      23696 :     if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin)
     178                 :            :     {
     179                 :            :       // We use the interactive shell when piping from stdin, even some cases
     180                 :            :       // where the input stream is not a TTY. We do this to avoid memory issues
     181                 :            :       // involving tokens that span multiple lines.
     182                 :            :       // We compute whether the interactive shell is actually interactive
     183                 :            :       // (via isatty). If we are not interactive, we disable certain output
     184                 :            :       // information, e.g. for querying the user.
     185                 :          0 :       bool isInteractive = isatty(fileno(stdin));
     186                 :            :       // set incremental if we are in interactive mode
     187         [ -  - ]:          0 :       if (!solver->getOptionInfo("incremental").setByUser)
     188                 :            :       {
     189         [ -  - ]:          0 :         pExecutor->setOptionInternal("incremental",
     190                 :            :                                      isInteractive ? "true" : "false");
     191                 :            :       }
     192                 :            :       // now store options as original
     193                 :          0 :       pExecutor->storeOptionsAsOriginal();
     194                 :            :       InteractiveShell shell(
     195                 :          0 :           pExecutor.get(), dopts.in(), dopts.out(), isInteractive);
     196                 :            : 
     197         [ -  - ]:          0 :       if (isInteractive)
     198                 :            :       {
     199                 :          0 :         auto& out = solver->getDriverOptions().out();
     200                 :          0 :         out << Configuration::getPackageName() << " "
     201                 :          0 :             << Configuration::getVersionString();
     202         [ -  - ]:          0 :         if (Configuration::isGitBuild())
     203                 :            :         {
     204                 :          0 :           out << " [" << Configuration::getGitInfo() << "]";
     205                 :            :         }
     206                 :          0 :         out << (Configuration::isDebugBuild() ? " DEBUG" : "") << " assertions:"
     207                 :          0 :             << (Configuration::isAssertionBuild() ? "on" : "off") << std::endl
     208                 :          0 :             << std::endl
     209                 :          0 :             << Configuration::copyright() << std::endl;
     210                 :            :       }
     211                 :            : 
     212                 :            :       while (true)
     213                 :            :       {
     214                 :            :         // read and execute all available commands
     215         [ -  - ]:          0 :         if (!shell.readAndExecCommands())
     216                 :            :         {
     217                 :          0 :           break;
     218                 :            :         }
     219                 :            :       }
     220                 :            :     }
     221                 :            :     else
     222                 :            :     {
     223         [ +  + ]:      23696 :       if (!solver->getOptionInfo("incremental").setByUser)
     224                 :            :       {
     225                 :      22301 :         pExecutor->setOptionInternal("incremental", "false");
     226                 :            :       }
     227                 :            :       // we don't need to check that terms passed to API methods are well
     228                 :            :       // formed, since this should be an invariant of the parser
     229         [ +  - ]:      23696 :       if (!solver->getOptionInfo("wf-checking").setByUser)
     230                 :            :       {
     231                 :      23696 :         pExecutor->setOptionInternal("wf-checking", "false");
     232                 :            :       }
     233                 :            :       // now store options as original
     234                 :      23696 :       pExecutor->storeOptionsAsOriginal();
     235                 :            : 
     236                 :            :       std::unique_ptr<InputParser> parser(new InputParser(
     237                 :      23756 :           pExecutor->getSolver(), pExecutor->getSymbolManager()));
     238         [ -  + ]:      23696 :       if( inputFromStdin ) {
     239                 :          0 :         parser->setStreamInput(ilang, cin, filename);
     240                 :            :       }
     241                 :            :       else
     242                 :            :       {
     243                 :      23696 :         parser->setFileInput(ilang, filename);
     244                 :            :       }
     245                 :            : 
     246                 :      23696 :       PortfolioDriver driver(parser);
     247         [ +  + ]:      23696 :       returnValue = driver.solve(pExecutor) ? 0 : 1;
     248                 :            :     }
     249                 :            : 
     250                 :            : #ifdef CVC5_COMPETITION_MODE
     251                 :            :     dopts.out() << std::flush;
     252                 :            :     // exit, don't return (don't want destructors to run)
     253                 :            :     // _exit() from unistd.h doesn't run global destructors
     254                 :            :     // or other on_exit/atexit stuff.
     255                 :            :     _exit(returnValue);
     256                 :            : #endif /* CVC5_COMPETITION_MODE */
     257                 :            : 
     258                 :      23636 :     pExecutor->flushOutputStreams();
     259                 :            : 
     260                 :            : #ifdef CVC5_DEBUG
     261                 :            :     {
     262                 :      70908 :       auto info = solver->getOptionInfo("early-exit");
     263 [ +  + ][ -  + ]:      23636 :       if (info.boolValue() && info.setByUser)
                 [ -  + ]
     264                 :            :       {
     265                 :          0 :         _exit(returnValue);
     266                 :            :       }
     267                 :            :     }
     268                 :            : #else  /* CVC5_DEBUG */
     269                 :            :     if (solver->getOptionInfo("early-exit").boolValue())
     270                 :            :     {
     271                 :            :       _exit(returnValue);
     272                 :            :     }
     273                 :            : #endif /* CVC5_DEBUG */
     274                 :            :   }
     275                 :            : 
     276                 :      23636 :   pExecutor.reset();
     277                 :            : 
     278                 :      23636 :   signal_handlers::cleanup();
     279                 :            : 
     280                 :      47272 :   return returnValue;
     281                 :            : }