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

 * 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_private.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::options {

// clang-format off

enum class OutputTag

{

  INST, RAW_BENCHMARK, NONE, SYGUS, TRIGGER

};

static constexpr size_t OutputTag__numValues = 5;

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;

  Language inputLanguage = Language::LANG_AUTO;

  bool inputLanguageWasSetByUser = false;

  bool languageHelp;

  bool languageHelpWasSetByUser = false;

  ManagedOut out;

  bool outWasSetByUser = false;

  OutputTag outputTag = OutputTag::NONE;

  bool outputTagWasSetByUser = false;

  Language outputLanguage = Language::LANG_AUTO;

  bool outputLanguageWasSetByUser = false;

  bool parseOnly;

  bool parseOnlyWasSetByUser = false;

  bool preprocessOnly;

  bool preprocessOnlyWasSetByUser = false;

  bool printSuccess;

  bool printSuccessWasSetByUser = false;

  uint64_t cumulativeResourceLimit;

  bool cumulativeResourceLimitWasSetByUser = false;

  uint64_t perCallResourceLimit;

  bool perCallResourceLimitWasSetByUser = false;

  bool statistics;

  bool statisticsWasSetByUser = false;

  bool statisticsAll;

  bool statisticsAllWasSetByUser = false;

  bool statisticsEveryQuery = false;

  bool statisticsEveryQueryWasSetByUser = false;

  bool statisticsExpert;

  bool statisticsExpertWasSetByUser = false;

  uint64_t cumulativeMillisecondLimit;

  bool cumulativeMillisecondLimitWasSetByUser = false;

  uint64_t perCallMillisecondLimit;

  bool perCallMillisecondLimitWasSetByUser = false;

  int64_t verbosity = 0;

  bool verbosityWasSetByUser = false;

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

  bool resourceWeightHolderWasSetByUser = false;

  std::bitset<OutputTag__numValues> outputTagHolder;

  bool outputTagHolderWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

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

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

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

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

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

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

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

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

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

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

inline bool statisticsAll() { return Options::current().base.statisticsAll; }

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

inline bool statisticsExpert() { return Options::current().base.statisticsExpert; }

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

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

inline std::vector<std::string> resourceWeightHolder() { return Options::current().base.resourceWeightHolder; }

inline std::bitset<OutputTag__numValues> outputTagHolder() { return Options::current().base.outputTagHolder; }

// 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 = "language-help";

static constexpr const char* out__name = "out";

static constexpr const char* outputTag__name = "output";

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

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* cumulativeResourceLimit__name = "rlimit";

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

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* cumulativeMillisecondLimit__name = "tlimit";

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

static constexpr const char* verbosity__name = "verbosity";

void setDefaultErr(Options& opts, ManagedErr value);

void setDefaultIn(Options& opts, ManagedIn value);

void setDefaultIncrementalSolving(Options& opts, bool value);

void setDefaultInputLanguage(Options& opts, Language value);

void setDefaultLanguageHelp(Options& opts, bool value);

void setDefaultOut(Options& opts, ManagedOut value);

void setDefaultOutputTag(Options& opts, OutputTag value);

void setDefaultOutputLanguage(Options& opts, Language value);

void setDefaultParseOnly(Options& opts, bool value);

void setDefaultPreprocessOnly(Options& opts, bool value);

void setDefaultPrintSuccess(Options& opts, bool value);

void setDefaultCumulativeResourceLimit(Options& opts, uint64_t value);

void setDefaultPerCallResourceLimit(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 setDefaultCumulativeMillisecondLimit(Options& opts, uint64_t value);

void setDefaultPerCallMillisecondLimit(Options& opts, uint64_t value);

void setDefaultVerbosity(Options& opts, int64_t value);

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

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

// clang-format on

}

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__BASE_H */