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

 * 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

{

  SYGUS_GRAMMAR, TRIGGER, RAW_BENCHMARK, NONE, INST, SYGUS,

  __MAX_VALUE = SYGUS

};

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;

  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::bitset<static_cast<size_t>(OutputTag::__MAX_VALUE)+1> outputTagHolder;

  bool outputTagHolderWasSetByUser = false;

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

  bool resourceWeightHolderWasSetByUser = 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 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 int64_t verbosity() { return Options::current().base.verbosity; }

inline std::bitset<static_cast<size_t>(OutputTag::__MAX_VALUE)+1> outputTagHolder() { return Options::current().base.outputTagHolder; }

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

// clang-format on

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__BASE_H */