Branch data     Line data    Source code

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