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

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

#define CVC5__OPTIONS__UF_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class UfssMode

{

  FULL,

  NO_MINIMAL,

  NONE

};

static constexpr size_t UfssMode__numValues = 3;

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

UfssMode stringToUfssMode(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

  bool ufSymmetryBreaker = true;

  bool ufSymmetryBreakerWasSetByUser = false;

  bool ufHo = false;

  bool ufHoWasSetByUser = false;

  bool ufHoExt = true;

  bool ufHoExtWasSetByUser = false;

  int ufssAbortCardinality = -1;

  bool ufssAbortCardinalityWasSetByUser = false;

  bool ufssFairness = true;

  bool ufssFairnessWasSetByUser = false;

  bool ufssFairnessMonotone = false;

  bool ufssFairnessMonotoneWasSetByUser = false;

  int ufssTotalityLimited = -1;

  bool ufssTotalityLimitedWasSetByUser = false;

  bool ufssTotalitySymBreak = false;

  bool ufssTotalitySymBreakWasSetByUser = false;

  UfssMode ufssMode = UfssMode::FULL;

  bool ufssModeWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct ufSymmetryBreaker__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ufSymmetryBreaker;

extern struct ufHo__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ufHo;

extern struct ufHoExt__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ufHoExt;

extern struct ufssAbortCardinality__option_t

{

  typedef int type;

  type operator()() const;

} thread_local ufssAbortCardinality;

extern struct ufssFairness__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ufssFairness;

extern struct ufssFairnessMonotone__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ufssFairnessMonotone;

extern struct ufssTotalityLimited__option_t

{

  typedef int type;

  type operator()() const;

} thread_local ufssTotalityLimited;

extern struct ufssTotalitySymBreak__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local ufssTotalitySymBreak;

extern struct ufssMode__option_t

{

  typedef UfssMode type;

  type operator()() const;

} thread_local ufssMode;

// clang-format on

namespace uf

{

// clang-format off

static constexpr const char* ufSymmetryBreaker__name = "symmetry-breaker";

static constexpr const char* ufHo__name = "uf-ho";

static constexpr const char* ufHoExt__name = "uf-ho-ext";

static constexpr const char* ufssAbortCardinality__name = "uf-ss-abort-card";

static constexpr const char* ufssFairness__name = "uf-ss-fair";

static constexpr const char* ufssFairnessMonotone__name = "uf-ss-fair-monotone";

static constexpr const char* ufssTotalityLimited__name = "uf-ss-totality-limited";

static constexpr const char* ufssTotalitySymBreak__name = "uf-ss-totality-sym-break";

static constexpr const char* ufssMode__name = "uf-ss";

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

inline int ufssTotalityLimited__option_t::operator()() const

{ return Options::current().uf.ufssTotalityLimited; }

inline bool ufssTotalitySymBreak__option_t::operator()() const

{ return Options::current().uf.ufssTotalitySymBreak; }

// clang-format on

namespace uf

{

// clang-format off

void setDefaultUfSymmetryBreaker(Options& opts, bool value);

void setDefaultUfHo(Options& opts, bool value);

void setDefaultUfHoExt(Options& opts, bool value);

void setDefaultUfssAbortCardinality(Options& opts, int value);

void setDefaultUfssFairness(Options& opts, bool value);

void setDefaultUfssFairnessMonotone(Options& opts, bool value);

void setDefaultUfssTotalityLimited(Options& opts, int value);

void setDefaultUfssTotalitySymBreak(Options& opts, bool value);

void setDefaultUfssMode(Options& opts, UfssMode value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__UF_H */