/******************************************************************************

 * Top contributors (to current version):

 *   Tim King, Morgan Deters, Paul Meng

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * Global (command-line, set-option, ...) parameters for SMT.

 */

#include "cvc5_public.h"

#ifndef CVC5__OPTIONS__OPTIONS_H

#define CVC5__OPTIONS__OPTIONS_H

#include <iosfwd>

#include <memory>

#include <string>

#include <vector>

#include "base/listener.h"

#include "cvc5_export.h"

#include "options/language.h"

#include "options/printer_modes.h"

namespace cvc5 {

namespace api {

class Solver;

}

namespace options {

  struct OptionsHolder;

  class OptionsHandler;

// clang-format off

  struct HolderARITH;

  struct HolderARRAYS;

  struct HolderBASE;

  struct HolderBOOLEANS;

  struct HolderBUILTIN;

  struct HolderBV;

  struct HolderDATATYPES;

  struct HolderDECISION;

  struct HolderEXPR;

  struct HolderFP;

  struct HolderDRIVER;

  struct HolderPARSER;

  struct HolderPRINTER;

  struct HolderPROOF;

  struct HolderPROP;

  struct HolderQUANTIFIERS;

  struct HolderRESMAN;

  struct HolderSEP;

  struct HolderSETS;

  struct HolderSMT;

  struct HolderSTRINGS;

  struct HolderTHEORY;

  struct HolderUF;

// clang-format on

  }  // namespace options

class OptionsListener;

class CVC5_EXPORT Options

{

  friend api::Solver;

  /** The handler for the options of the theory. */

  options::OptionsHandler* d_handler;

// clang-format off

    std::unique_ptr<options::HolderARITH> d_arith;

    std::unique_ptr<options::HolderARRAYS> d_arrays;

    std::unique_ptr<options::HolderBASE> d_base;

    std::unique_ptr<options::HolderBOOLEANS> d_booleans;

    std::unique_ptr<options::HolderBUILTIN> d_builtin;

    std::unique_ptr<options::HolderBV> d_bv;

    std::unique_ptr<options::HolderDATATYPES> d_datatypes;

    std::unique_ptr<options::HolderDECISION> d_decision;

    std::unique_ptr<options::HolderEXPR> d_expr;

    std::unique_ptr<options::HolderFP> d_fp;

    std::unique_ptr<options::HolderDRIVER> d_driver;

    std::unique_ptr<options::HolderPARSER> d_parser;

    std::unique_ptr<options::HolderPRINTER> d_printer;

    std::unique_ptr<options::HolderPROOF> d_proof;

    std::unique_ptr<options::HolderPROP> d_prop;

    std::unique_ptr<options::HolderQUANTIFIERS> d_quantifiers;

    std::unique_ptr<options::HolderRESMAN> d_resman;

    std::unique_ptr<options::HolderSEP> d_sep;

    std::unique_ptr<options::HolderSETS> d_sets;

    std::unique_ptr<options::HolderSMT> d_smt;

    std::unique_ptr<options::HolderSTRINGS> d_strings;

    std::unique_ptr<options::HolderTHEORY> d_theory;

    std::unique_ptr<options::HolderUF> d_uf;

// clang-format on

  /** The current Options in effect */

  static thread_local Options* s_current;

  /** Low-level assignment function for options */

  template <class T>

  void assign(T, std::string option, std::string value);

  /** Low-level assignment function for bool-valued options */

  template <class T>

  void assignBool(T, std::string option, bool value);

  friend class options::OptionsHandler;

  /**

   * Options cannot be copied as they are given an explicit list of

   * Listeners to respond to.

   */

  Options(const Options& options) = delete;

  /**

   * Options cannot be assigned as they are given an explicit list of

   * Listeners to respond to.

   */

  Options& operator=(const Options& options) = delete;

  static std::string formatThreadOptionException(const std::string& option);

public:

 class OptionsScope

 {

  private:

    Options* d_oldOptions;

  public:

    {

 };

  /** Return true if current Options are null */

  }

  /** Get the current Options in effect */

  }

  Options(OptionsListener* ol = nullptr);

  ~Options();

// clang-format off

  const options::HolderARITH& arith() const;

  options::HolderARITH& arith();

  const options::HolderARRAYS& arrays() const;

  options::HolderARRAYS& arrays();

  const options::HolderBASE& base() const;

  options::HolderBASE& base();

  const options::HolderBOOLEANS& booleans() const;

  options::HolderBOOLEANS& booleans();

  const options::HolderBUILTIN& builtin() const;

  options::HolderBUILTIN& builtin();

  const options::HolderBV& bv() const;

  options::HolderBV& bv();

  const options::HolderDATATYPES& datatypes() const;

  options::HolderDATATYPES& datatypes();

  const options::HolderDECISION& decision() const;

  options::HolderDECISION& decision();

  const options::HolderEXPR& expr() const;

  options::HolderEXPR& expr();

  const options::HolderFP& fp() const;

  options::HolderFP& fp();

  const options::HolderDRIVER& driver() const;

  options::HolderDRIVER& driver();

  const options::HolderPARSER& parser() const;

  options::HolderPARSER& parser();

  const options::HolderPRINTER& printer() const;

  options::HolderPRINTER& printer();

  const options::HolderPROOF& proof() const;

  options::HolderPROOF& proof();

  const options::HolderPROP& prop() const;

  options::HolderPROP& prop();

  const options::HolderQUANTIFIERS& quantifiers() const;

  options::HolderQUANTIFIERS& quantifiers();

  const options::HolderRESMAN& resman() const;

  options::HolderRESMAN& resman();

  const options::HolderSEP& sep() const;

  options::HolderSEP& sep();

  const options::HolderSETS& sets() const;

  options::HolderSETS& sets();

  const options::HolderSMT& smt() const;

  options::HolderSMT& smt();

  const options::HolderSTRINGS& strings() const;

  options::HolderSTRINGS& strings();

  const options::HolderTHEORY& theory() const;

  options::HolderTHEORY& theory();

  const options::HolderUF& uf() const;

  options::HolderUF& uf();

// clang-format on

  /**

   * Copies the value of the options stored in OptionsHolder into the current

   * Options object.

   * This does not copy the listeners in the Options object.

   */

  void copyValues(const Options& options);

  /**

   * Set the value of the given option.  Uses `ref()`, which causes a

   * compile-time error if the given option is read-only.

   */

  template <class T>

  /**

   * Set the default value of the given option. Is equivalent to calling `set()`

   * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time

   * error if the given option is read-only.

   */

  template <class T>

  {

    {

    }

  /**

   * Get a non-const reference to the value of the given option. Causes a

   * compile-time error if the given option is read-only. Writeable options

   * specialize this template with a real implementation.

   */

  template <class T>

  typename T::type& ref(T) {

    // Flag a compile-time error.

    T::you_are_trying_to_get_nonconst_access_to_a_read_only_option;

    // Ensure the compiler does not complain about the return value.

    return *static_cast<typename T::type*>(nullptr);

  }

  /**

   * Set the value of the given option by key.

   *

   * Throws OptionException or ModalException on failures.

   */

  void setOption(const std::string& key, const std::string& optionarg);

  /** Get the value of the given option.  Const access only. */

  template <class T>

  const typename T::type& operator[](T) const;

  /**

   * Gets the value of the given option by key and returns value as a string.

   *

   * Throws OptionException on failures, such as key not being the name of an

   * option.

   */

  std::string getOption(const std::string& key) const;

  // Get accessor functions.

  InputLanguage getInputLanguage() const;

  options::InstFormatMode getInstFormatMode() const;

  OutputLanguage getOutputLanguage() const;

  bool getUfHo() const;

  bool getDumpInstantiations() const;

  bool getDumpModels() const;

  bool getDumpProofs() const;

  bool getDumpUnsatCores() const;

  bool getEarlyExit() const;

  bool getFilesystemAccess() const;

  bool getForceNoLimitCpuWhileDump() const;

  bool getHelp() const;

  bool getIncrementalSolving() const;

  bool getInteractive() const;

  bool getInteractivePrompt() const;

  bool getLanguageHelp() const;

  bool getMemoryMap() const;

  bool getParseOnly() const;

  bool getProduceModels() const;

  bool getSegvSpin() const;

  bool getSemanticChecks() const;

  bool getStatistics() const;

  bool getStatsEveryQuery() const;

  bool getStrictParsing() const;

  int getTearDownIncremental() const;

  uint64_t getCumulativeTimeLimit() const;

  bool getVersion() const;

  const std::string& getForceLogicString() const;

  int getVerbosity() const;

  std::istream* getIn() const;

  std::ostream* getErr();

  std::ostream* getOut();

  std::ostream* getOutConst() const; // TODO: Remove this.

  std::string getBinaryName() const;

  // TODO: Document these.

  void setInputLanguage(InputLanguage);

  void setInteractive(bool);

  void setOut(std::ostream*);

  void setOutputLanguage(OutputLanguage);

  bool wasSetByUserEarlyExit() const;

  bool wasSetByUserForceLogicString() const;

  bool wasSetByUserIncrementalSolving() const;

  bool wasSetByUserInteractive() const;

  // Static accessor functions.

  // TODO: Document these.

  static std::ostream* currentGetOut();

  /**

   * Returns true iff the value of the given option was set

   * by the user via a command-line option or SmtEngine::setOption().

   * (Options::set() is low-level and doesn't count.)  Returns false

   * otherwise.

   */

  template <class T>

  bool wasSetByUser(T) const;

  /**

   * Get a description of the command-line flags accepted by

   * parseOptions.  The returned string will be escaped so that it is

   * suitable as an argument to printf. */

  std::string getDescription() const;

  /**

   * Print overall command-line option usage message, prefixed by

   * "msg"---which could be an error message causing the usage

   * output in the first place, e.g. "no such option --foo"

   */

  static void printUsage(const std::string msg, std::ostream& out);

  /**

   * Print command-line option usage message for only the most-commonly

   * used options.  The message is prefixed by "msg"---which could be

   * an error message causing the usage output in the first place, e.g.

   * "no such option --foo"

   */

  static void printShortUsage(const std::string msg, std::ostream& out);

  /** Print help for the --lang command line option */

  static void printLanguageHelp(std::ostream& out);

  /**

   * Initialize the Options object options based on the given

   * command-line arguments given in argc and argv.  The return value

   * is what's left of the command line (that is, the non-option

   * arguments).

   *

   * This function uses getopt_long() and is not thread safe.

   *

   * Throws OptionException on failures.

   *

   * Preconditions: options and argv must be non-null.

   */

  static std::vector<std::string> parseOptions(Options* options,

                                               int argc,

                                               char* argv[]);

  /**

   * Get the setting for all options.

   */

  std::vector<std::vector<std::string> > getOptions() const;

  /** Set the generic listener associated with this class to ol */

  void setListener(OptionsListener* ol);

  /** Sends a std::flush to getErr(). */

  void flushErr();

  /** Sends a std::flush to getOut(). */

  void flushOut();

 private:

  /** Pointer to the options listener, if one exists */

  OptionsListener* d_olisten;

  /**

   * Helper method for setOption, updates this object for setting the given

   * option.

   */

  void setOptionInternal(const std::string& key, const std::string& optionarg);

  /**

   * Internal procedure for implementing the parseOptions function.

   * Initializes the options object based on the given command-line

   * arguments. The command line arguments are stored in argc/argv.

   * Nonoptions are stored into nonoptions.

   *

   * This is not thread safe.

   *

   * Throws OptionException on failures.

   *

   * Preconditions: options, extender and nonoptions are non-null.

   */

  void parseOptionsRecursive(int argc,

                                    char* argv[],

                                    std::vector<std::string>* nonoptions);

}; /* class Options */

}  // namespace cvc5

#endif /* CVC5__OPTIONS__OPTIONS_H */