Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Andrew Reynolds
       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 intermediary between the parser and the command executor, optionally using
      14                 :            :  * predefined portfolio strategies.
      15                 :            :  */
      16                 :            : 
      17                 :            : #ifndef CVC5__MAIN__PORTFOLIO_DRIVER_H
      18                 :            : #define CVC5__MAIN__PORTFOLIO_DRIVER_H
      19                 :            : 
      20                 :            : #include <cvc5/cvc5.h>
      21                 :            : #include <cvc5/cvc5_parser.h>
      22                 :            : 
      23                 :            : #include <optional>
      24                 :            : 
      25                 :            : #include "base/check.h"
      26                 :            : #include "main/command_executor.h"
      27                 :            : 
      28                 :            : namespace cvc5::main {
      29                 :            : 
      30                 :            : /**
      31                 :            :  * Holds the command executor and provides a few convenience methods for parsing
      32                 :            :  * and executing commands with the executor.
      33                 :            :  */
      34                 :            : 
      35                 :            : class ExecutionContext
      36                 :            : {
      37                 :            :  public:
      38                 :            :   /** The command executor used for solving */
      39                 :            :   CommandExecutor* d_executor;
      40                 :            :   /** The logic, if it has been set by a command */
      41                 :            :   std::optional<std::string> d_logic;
      42                 :            : 
      43                 :            :   /** Retrieve the solver object from the command executor */
      44                 :      23622 :   Solver& solver() { return *d_executor->getSolver(); }
      45                 :            : 
      46                 :            :   /**
      47                 :            :    * Read commands from the parser and continuously execute them. If
      48                 :            :    * stopAtSetLogic is true, stop when the logic has been set to some value.
      49                 :            :    * If this happens, d_logic is set to the respective value.
      50                 :            :    * Otherwise (if stopAtSetLogic is false or the logic is never set) all
      51                 :            :    * commands are executed until a quit command is found or the whole input
      52                 :            :    * has been parsed.
      53                 :            :    * Returns true if the commands have been executed without being interrupted.
      54                 :            :    */
      55                 :            :   bool solveContinuous(parser::InputParser* parser, bool stopAtSetLogic);
      56                 :            : 
      57                 :            :   /**
      58                 :            :    * Execute the given commands.
      59                 :            :    * Returns true if the commands have been executed without being interrupted.
      60                 :            :    */
      61                 :            :   bool solveCommands(std::vector<cvc5::parser::Command>& cmds);
      62                 :            : 
      63                 :            :   /** Parse the remaining input from d_parser into a vector of commands */
      64                 :            :   std::vector<cvc5::parser::Command> parseCommands(parser::InputParser* parser);
      65                 :            : };
      66                 :            : 
      67                 :            : /**
      68                 :            :  * Represents a single configuration within a portfolio strategy, consisting of
      69                 :            :  * a set of command line options and a timeout (as part of a total timeout).
      70                 :            :  */
      71                 :            : struct PortfolioConfig
      72                 :            : {
      73                 :            :   /**
      74                 :            :    * Set timeout as part of the total timeout. The given number should be at
      75                 :            :    * most 1.
      76                 :            :    */
      77                 :         23 :   PortfolioConfig(double timeout = 0.0) : d_timeout(timeout)
      78                 :            :   {
      79 [ -  + ][ -  + ]:         23 :     Assert(timeout <= 1)
                 [ -  - ]
      80                 :          0 :         << "The given timeout should be given as part of the total timeout";
      81                 :         23 :   }
      82                 :            :   /**
      83                 :            :    * Set a command line option. While no formal restriction is imposed, they
      84                 :            :    * are only set after parsing has already started. Thus, options that affect
      85                 :            :    * how the parser behaves should not be specified here.
      86                 :            :    * The value is optional and defaults to "true".
      87                 :            :    */
      88                 :         53 :   PortfolioConfig& set(const std::string& option,
      89                 :            :                        const std::string& value = "true")
      90                 :            :   {
      91                 :         53 :     d_options.emplace_back(option, value);
      92                 :         53 :     return *this;
      93                 :            :   }
      94                 :            :   /** Convenience function to set option to "false". */
      95                 :          7 :   PortfolioConfig& unset(const std::string& option)
      96                 :            :   {
      97                 :          7 :     return set(option, "false");
      98                 :            :   }
      99                 :            : 
     100                 :            :   /** Apply configured options to a solver object */
     101                 :          0 :   void applyOptions(Solver& solver) const
     102                 :            :   {
     103         [ -  - ]:          0 :     for (const auto& o : d_options)
     104                 :            :     {
     105                 :          0 :       solver.setOption(o.first, o.second);
     106                 :            :     }
     107                 :          0 :   }
     108                 :            :   /** To option string */
     109                 :            :   std::string toOptionString() const;
     110                 :            :   /** List of options as pair of name and value */
     111                 :            :   std::vector<std::pair<std::string, std::string>> d_options;
     112                 :            :   /** Timeout as part of the total timeout */
     113                 :            :   double d_timeout = 0;
     114                 :            : };
     115                 :            : std::ostream& operator<<(std::ostream& os, const PortfolioConfig& config);
     116                 :            : 
     117                 :            : /**
     118                 :            :  * Represents a portfolio strategy, consisting of a list of configurations.
     119                 :            :  */
     120                 :            : struct PortfolioStrategy
     121                 :            : {
     122                 :            :   /** Add a new configurations */
     123                 :         23 :   PortfolioConfig& add(double timeout = 0)
     124                 :            :   {
     125                 :         23 :     d_strategies.emplace_back(timeout);
     126                 :         23 :     return d_strategies.back();
     127                 :            :   }
     128                 :            : 
     129                 :            :   std::vector<PortfolioConfig> d_strategies;
     130                 :            : };
     131                 :            : 
     132                 :            : class PortfolioDriver
     133                 :            : {
     134                 :            :  public:
     135                 :      23615 :   PortfolioDriver(std::unique_ptr<parser::InputParser>& parser)
     136                 :      23615 :       : d_parser(parser.get())
     137                 :            :   {
     138                 :      23615 :   }
     139                 :            : 
     140                 :            :   /**
     141                 :            :    * Solve the input obtained from the parser using the given executor.
     142                 :            :    * Internally runs the appropriate portfolio strategy if a logic is set.
     143                 :            :    * Returns true if the input was executed without being interrupted.
     144                 :            :    */
     145                 :            :   bool solve(std::unique_ptr<CommandExecutor>& executor);
     146                 :            : 
     147                 :            :  private:
     148                 :            :   PortfolioStrategy getStrategy(const std::string& logic);
     149                 :            : 
     150                 :            :   /** The parser we use to get the commands */
     151                 :            :   parser::InputParser* d_parser;
     152                 :            : };
     153                 :            : 
     154                 :            : }  // namespace cvc5::main
     155                 :            : 
     156                 :            : #endif /* CVC5__MAIN__PORTFOLIO_DRIVER_H */