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