Branch data     Line data    Source code

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