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                 :            :  * An additional layer between commands and invoking them.
      11                 :            :  */
      12                 :            : 
      13                 :            : #ifndef CVC5__MAIN__COMMAND_EXECUTOR_H
      14                 :            : #define CVC5__MAIN__COMMAND_EXECUTOR_H
      15                 :            : 
      16                 :            : #include <cvc5/cvc5.h>
      17                 :            : #include <cvc5/cvc5_parser.h>
      18                 :            : 
      19                 :            : #include <iosfwd>
      20                 :            : #include <string>
      21                 :            : 
      22                 :            : namespace cvc5 {
      23                 :            : 
      24                 :            : namespace parser {
      25                 :            : class Command;
      26                 :            : }
      27                 :            : 
      28                 :            : namespace main {
      29                 :            : 
      30                 :            : class CommandExecutor
      31                 :            : {
      32                 :            :  protected:
      33                 :            :   /**
      34                 :            :    * The solver object, which is allocated by this class and is used for
      35                 :            :    * executing most commands (e.g. check-sat).
      36                 :            :    */
      37                 :            :   std::unique_ptr<cvc5::Solver>& d_solver;
      38                 :            :   /**
      39                 :            :    * The symbol manager, which is allocated by this class. This manages
      40                 :            :    * all things related to definitions of symbols and their impact on behaviors
      41                 :            :    * for commands (e.g. get-unsat-core, get-model, get-assignment), as well
      42                 :            :    * as tracking expression names. Note the symbol manager is independent from
      43                 :            :    * the parser, which uses this symbol manager given a text input.
      44                 :            :    *
      45                 :            :    * Certain commands (e.g. reset-assertions) have a specific impact on the
      46                 :            :    * symbol manager.
      47                 :            :    */
      48                 :            :   std::unique_ptr<parser::SymbolManager> d_symman;
      49                 :            : 
      50                 :            :   cvc5::Result d_result;
      51                 :            : 
      52                 :            :   /** Cache option value of parse-only option. */
      53                 :            :   bool d_parseOnly;
      54                 :            : 
      55                 :            :  public:
      56                 :            :   CommandExecutor(std::unique_ptr<cvc5::Solver>& solver);
      57                 :            : 
      58                 :            :   virtual ~CommandExecutor();
      59                 :            : 
      60                 :            :   /**
      61                 :            :    * Executes a command. Recursively handles if cmd is a command
      62                 :            :    * sequence.  Eventually uses doCommandSingleton (which can be
      63                 :            :    * overridden by a derived class).
      64                 :            :    */
      65                 :            :   bool doCommand(cvc5::parser::Command* cmd);
      66                 :            : 
      67                 :            :   bool doCommand(std::unique_ptr<cvc5::parser::Command>& cmd)
      68                 :            :   {
      69                 :            :     return doCommand(cmd.get());
      70                 :            :   }
      71                 :            : 
      72                 :            :   /** Get a pointer to the solver object owned by this CommandExecutor. */
      73                 :      48764 :   cvc5::Solver* getSolver() { return d_solver.get(); }
      74                 :            : 
      75                 :            :   /** Get a pointer to the symbol manager owned by this CommandExecutor */
      76                 :      24390 :   parser::SymbolManager* getSymbolManager() { return d_symman.get(); }
      77                 :            : 
      78                 :          0 :   cvc5::Result getResult() const { return d_result; }
      79                 :            :   void reset();
      80                 :            : 
      81                 :            :   /** Store the current options as the original options */
      82                 :            :   void storeOptionsAsOriginal();
      83                 :            : 
      84                 :            :   /**
      85                 :            :    * Set option internal. This method should be used to set options on the
      86                 :            :    * underlying solver that do not originate from the user. We do this to
      87                 :            :    * set expert or undocumented options that should not throw an exception
      88                 :            :    * e.g. when using --safe-options.
      89                 :            :    * @param key The option to set
      90                 :            :    * @param value The value to set
      91                 :            :    */
      92                 :            :   void setOptionInternal(const std::string& key, const std::string& value);
      93                 :            : 
      94                 :            :   /**
      95                 :            :    * Prints statistics to an output stream.
      96                 :            :    * Checks whether statistics should be printed according to the options.
      97                 :            :    * Thus, this method can always be called without checking the options.
      98                 :            :    */
      99                 :            :   virtual void printStatistics(std::ostream& out) const;
     100                 :            : 
     101                 :            :   /**
     102                 :            :    * Safely prints statistics to a file descriptor.
     103                 :            :    * This method is safe to be used within a signal handler.
     104                 :            :    * Checks whether statistics should be printed according to the options.
     105                 :            :    * Thus, this method can always be called without checking the options.
     106                 :            :    */
     107                 :            :   void printStatisticsSafe(int fd) const;
     108                 :            : 
     109                 :            :   void flushOutputStreams();
     110                 :            : 
     111                 :            :  protected:
     112                 :            :   /** Executes treating cmd as a singleton */
     113                 :            :   virtual bool doCommandSingleton(parser::Cmd* cmd);
     114                 :            : 
     115                 :            :  private:
     116                 :            :   CommandExecutor();
     117                 :            : 
     118                 :            :   bool solverInvoke(cvc5::Solver* solver,
     119                 :            :                     parser::SymManager* sm,
     120                 :            :                     parser::Cmd* cmd);
     121                 :            : }; /* class CommandExecutor */
     122                 :            : 
     123                 :            : }  // namespace main
     124                 :            : }  // namespace cvc5
     125                 :            : 
     126                 :            : #endif /* CVC5__MAIN__COMMAND_EXECUTOR_H */