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

 * Top contributors (to current version):

 *   Mathias Preiner, Aina Niemetz

 *

 * 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.

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

 *

 * Contains code for handling command-line options.

 *

 * For each <module>_options.toml configuration file, mkoptions.py

 * expands this template and generates a <module>_options.h file.

 */

#include "cvc5_public.h"

#ifndef CVC5__OPTIONS__BASE_H

#define CVC5__OPTIONS__BASE_H

#include "options/options.h"

// clang-format off

#include "options/language.h"

#include "options/managed_streams.h"

#include <bitset>

#include <iostream>

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class OutputTag

{

  INST,

  SYGUS,

  TRIGGER

};

static constexpr size_t OutputTag__numValues = 3;

std::ostream& operator<<(std::ostream& os, OutputTag mode);

OutputTag stringToOutputTag(const std::string& optarg);

// clang-format on

#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)

#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false

#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */

#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true

#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */

{

// clang-format off

  ManagedErr err;

  bool errWasSetByUser = false;

  ManagedIn in;

  bool inWasSetByUser = false;

  bool incrementalSolving = true;

  bool incrementalSolvingWasSetByUser = false;

  InputLanguage inputLanguage = language::input::LANG_AUTO;

  bool inputLanguageWasSetByUser = false;

  bool languageHelp;

  bool languageHelpWasSetByUser = false;

  ManagedOut out;

  bool outWasSetByUser = false;

  OutputLanguage outputLanguage = language::output::LANG_AUTO;

  bool outputLanguageWasSetByUser = false;

  OutputTag outputTag;

  bool outputTagWasSetByUser = false;

  std::bitset<OutputTag__numValues> outputTagHolder;

  bool outputTagHolderWasSetByUser = false;

  bool parseOnly;

  bool parseOnlyWasSetByUser = false;

  bool preprocessOnly;

  bool preprocessOnlyWasSetByUser = false;

  bool printSuccess;

  bool printSuccessWasSetByUser = false;

  std::vector<std::string> resourceWeightHolder;

  bool resourceWeightHolderWasSetByUser = false;

  uint64_t perCallResourceLimit;

  bool perCallResourceLimitWasSetByUser = false;

  uint64_t cumulativeResourceLimit;

  bool cumulativeResourceLimitWasSetByUser = false;

  bool statistics;

  bool statisticsWasSetByUser = false;

  bool statisticsAll;

  bool statisticsAllWasSetByUser = false;

  bool statisticsEveryQuery = false;

  bool statisticsEveryQueryWasSetByUser = false;

  bool statisticsExpert;

  bool statisticsExpertWasSetByUser = false;

  uint64_t perCallMillisecondLimit;

  bool perCallMillisecondLimitWasSetByUser = false;

  uint64_t cumulativeMillisecondLimit;

  bool cumulativeMillisecondLimitWasSetByUser = false;

  int64_t verbosity = 0;

  bool verbosityWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct err__option_t

{

  typedef ManagedErr type;

  type operator()() const;

} thread_local err;

extern struct in__option_t

{

  typedef ManagedIn type;

  type operator()() const;

} thread_local in;

extern struct incrementalSolving__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local incrementalSolving;

extern struct inputLanguage__option_t

{

  typedef InputLanguage type;

  type operator()() const;

} thread_local inputLanguage;

extern struct languageHelp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local languageHelp;

extern struct out__option_t

{

  typedef ManagedOut type;

  type operator()() const;

} thread_local out;

extern struct outputLanguage__option_t

{

  typedef OutputLanguage type;

  type operator()() const;

} thread_local outputLanguage;

extern struct outputTag__option_t

{

  typedef OutputTag type;

  type operator()() const;

} thread_local outputTag;

extern struct outputTagHolder__option_t

{

  typedef std::bitset<OutputTag__numValues> type;

  type operator()() const;

} thread_local outputTagHolder;

extern struct parseOnly__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local parseOnly;

extern struct preprocessOnly__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local preprocessOnly;

extern struct printSuccess__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local printSuccess;

extern struct resourceWeightHolder__option_t

{

  typedef std::vector<std::string> type;

  type operator()() const;

} thread_local resourceWeightHolder;

extern struct perCallResourceLimit__option_t

{

  typedef uint64_t type;

  type operator()() const;

} thread_local perCallResourceLimit;

extern struct cumulativeResourceLimit__option_t

{

  typedef uint64_t type;

  type operator()() const;

} thread_local cumulativeResourceLimit;

extern struct statistics__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local statistics;

extern struct statisticsAll__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local statisticsAll;

extern struct statisticsEveryQuery__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local statisticsEveryQuery;

extern struct statisticsExpert__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local statisticsExpert;

extern struct perCallMillisecondLimit__option_t

{

  typedef uint64_t type;

  type operator()() const;

} thread_local perCallMillisecondLimit;

extern struct cumulativeMillisecondLimit__option_t

{

  typedef uint64_t type;

  type operator()() const;

} thread_local cumulativeMillisecondLimit;

extern struct verbosity__option_t

{

  typedef int64_t type;

  type operator()() const;

} thread_local verbosity;

// clang-format on

namespace base

{

// clang-format off

static constexpr const char* err__name = "err";

static constexpr const char* in__name = "in";

static constexpr const char* incrementalSolving__name = "incremental";

static constexpr const char* inputLanguage__name = "lang";

static constexpr const char* languageHelp__name = "";

static constexpr const char* out__name = "out";

static constexpr const char* outputLanguage__name = "output-lang";

static constexpr const char* outputTag__name = "output";

static constexpr const char* outputTagHolder__name = "";

static constexpr const char* parseOnly__name = "parse-only";

static constexpr const char* preprocessOnly__name = "preprocess-only";

static constexpr const char* printSuccess__name = "print-success";

static constexpr const char* resourceWeightHolder__name = "";

static constexpr const char* perCallResourceLimit__name = "rlimit-per";

static constexpr const char* cumulativeResourceLimit__name = "rlimit";

static constexpr const char* statistics__name = "stats";

static constexpr const char* statisticsAll__name = "stats-all";

static constexpr const char* statisticsEveryQuery__name = "stats-every-query";

static constexpr const char* statisticsExpert__name = "stats-expert";

static constexpr const char* perCallMillisecondLimit__name = "tlimit-per";

static constexpr const char* cumulativeMillisecondLimit__name = "tlimit";

static constexpr const char* verbosity__name = "verbosity";

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

inline ManagedErr err__option_t::operator()() const

{ return Options::current().base.err; }

inline ManagedIn in__option_t::operator()() const

{ return Options::current().base.in; }

inline bool languageHelp__option_t::operator()() const

{ return Options::current().base.languageHelp; }

inline ManagedOut out__option_t::operator()() const

{ return Options::current().base.out; }

inline OutputTag outputTag__option_t::operator()() const

{ return Options::current().base.outputTag; }

inline bool parseOnly__option_t::operator()() const

{ return Options::current().base.parseOnly; }

inline bool printSuccess__option_t::operator()() const

{ return Options::current().base.printSuccess; }

inline std::vector<std::string> resourceWeightHolder__option_t::operator()() const

{ return Options::current().base.resourceWeightHolder; }

inline uint64_t perCallResourceLimit__option_t::operator()() const

{ return Options::current().base.perCallResourceLimit; }

inline uint64_t cumulativeResourceLimit__option_t::operator()() const

{ return Options::current().base.cumulativeResourceLimit; }

inline bool statistics__option_t::operator()() const

{ return Options::current().base.statistics; }

inline bool statisticsEveryQuery__option_t::operator()() const

{ return Options::current().base.statisticsEveryQuery; }

inline uint64_t perCallMillisecondLimit__option_t::operator()() const

{ return Options::current().base.perCallMillisecondLimit; }

inline uint64_t cumulativeMillisecondLimit__option_t::operator()() const

{ return Options::current().base.cumulativeMillisecondLimit; }

// clang-format on

namespace base

{

// clang-format off

void setDefaultErr(Options& opts, ManagedErr value);

void setDefaultIn(Options& opts, ManagedIn value);

void setDefaultIncrementalSolving(Options& opts, bool value);

void setDefaultInputLanguage(Options& opts, InputLanguage value);

void setDefaultLanguageHelp(Options& opts, bool value);

void setDefaultOut(Options& opts, ManagedOut value);

void setDefaultOutputLanguage(Options& opts, OutputLanguage value);

void setDefaultOutputTag(Options& opts, OutputTag value);

void setDefaultOutputTagHolder(Options& opts, std::bitset<OutputTag__numValues> value);

void setDefaultParseOnly(Options& opts, bool value);

void setDefaultPreprocessOnly(Options& opts, bool value);

void setDefaultPrintSuccess(Options& opts, bool value);

void setDefaultResourceWeightHolder(Options& opts, std::vector<std::string> value);

void setDefaultPerCallResourceLimit(Options& opts, uint64_t value);

void setDefaultCumulativeResourceLimit(Options& opts, uint64_t value);

void setDefaultStatistics(Options& opts, bool value);

void setDefaultStatisticsAll(Options& opts, bool value);

void setDefaultStatisticsEveryQuery(Options& opts, bool value);

void setDefaultStatisticsExpert(Options& opts, bool value);

void setDefaultPerCallMillisecondLimit(Options& opts, uint64_t value);

void setDefaultCumulativeMillisecondLimit(Options& opts, uint64_t value);

void setDefaultVerbosity(Options& opts, int64_t value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__BASE_H */