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

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

#define CVC5__OPTIONS__DATATYPES_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class SygusFairMode

{

  NONE,

  DT_SIZE,

  DIRECT,

  DT_SIZE_PRED,

  DT_HEIGHT_PRED

};

static constexpr size_t SygusFairMode__numValues = 5;

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

SygusFairMode stringToSygusFairMode(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 cdtBisimilar = true;

  bool cdtBisimilarWasSetByUser = false;

  bool dtBinarySplit = false;

  bool dtBinarySplitWasSetByUser = false;

  bool dtBlastSplits = false;

  bool dtBlastSplitsWasSetByUser = false;

  bool dtCyclic = true;

  bool dtCyclicWasSetByUser = false;

  bool dtForceAssignment = false;

  bool dtForceAssignmentWasSetByUser = false;

  bool dtInferAsLemmas = false;

  bool dtInferAsLemmasWasSetByUser = false;

  bool dtNestedRec = false;

  bool dtNestedRecWasSetByUser = false;

  bool dtPoliteOptimize = true;

  bool dtPoliteOptimizeWasSetByUser = false;

  bool dtRewriteErrorSel = false;

  bool dtRewriteErrorSelWasSetByUser = false;

  bool dtSharedSelectors = true;

  bool dtSharedSelectorsWasSetByUser = false;

  int sygusAbortSize = -1;

  bool sygusAbortSizeWasSetByUser = false;

  bool sygusFairMax = true;

  bool sygusFairMaxWasSetByUser = false;

  SygusFairMode sygusFair = SygusFairMode::DT_SIZE;

  bool sygusFairWasSetByUser = false;

  bool sygusSymBreak = true;

  bool sygusSymBreakWasSetByUser = false;

  bool sygusSymBreakAgg = true;

  bool sygusSymBreakAggWasSetByUser = false;

  bool sygusSymBreakDynamic = true;

  bool sygusSymBreakDynamicWasSetByUser = false;

  bool sygusSymBreakLazy = true;

  bool sygusSymBreakLazyWasSetByUser = false;

  bool sygusSymBreakPbe = true;

  bool sygusSymBreakPbeWasSetByUser = false;

  bool sygusSymBreakRlv = true;

  bool sygusSymBreakRlvWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct cdtBisimilar__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cdtBisimilar;

extern struct dtBinarySplit__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtBinarySplit;

extern struct dtBlastSplits__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtBlastSplits;

extern struct dtCyclic__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtCyclic;

extern struct dtForceAssignment__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtForceAssignment;

extern struct dtInferAsLemmas__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtInferAsLemmas;

extern struct dtNestedRec__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtNestedRec;

extern struct dtPoliteOptimize__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtPoliteOptimize;

extern struct dtRewriteErrorSel__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtRewriteErrorSel;

extern struct dtSharedSelectors__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtSharedSelectors;

extern struct sygusAbortSize__option_t

{

  typedef int type;

  type operator()() const;

} thread_local sygusAbortSize;

extern struct sygusFairMax__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusFairMax;

extern struct sygusFair__option_t

{

  typedef SygusFairMode type;

  type operator()() const;

} thread_local sygusFair;

extern struct sygusSymBreak__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusSymBreak;

extern struct sygusSymBreakAgg__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusSymBreakAgg;

extern struct sygusSymBreakDynamic__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusSymBreakDynamic;

extern struct sygusSymBreakLazy__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusSymBreakLazy;

extern struct sygusSymBreakPbe__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusSymBreakPbe;

extern struct sygusSymBreakRlv__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local sygusSymBreakRlv;

// clang-format on

namespace datatypes

{

// clang-format off

static constexpr const char* cdtBisimilar__name = "cdt-bisimilar";

static constexpr const char* dtBinarySplit__name = "dt-binary-split";

static constexpr const char* dtBlastSplits__name = "dt-blast-splits";

static constexpr const char* dtCyclic__name = "dt-cyclic";

static constexpr const char* dtForceAssignment__name = "dt-force-assignment";

static constexpr const char* dtInferAsLemmas__name = "dt-infer-as-lemmas";

static constexpr const char* dtNestedRec__name = "dt-nested-rec";

static constexpr const char* dtPoliteOptimize__name = "dt-polite-optimize";

static constexpr const char* dtRewriteErrorSel__name = "dt-rewrite-error-sel";

static constexpr const char* dtSharedSelectors__name = "dt-share-sel";

static constexpr const char* sygusAbortSize__name = "sygus-abort-size";

static constexpr const char* sygusFairMax__name = "sygus-fair-max";

static constexpr const char* sygusFair__name = "sygus-fair";

static constexpr const char* sygusSymBreak__name = "sygus-sym-break";

static constexpr const char* sygusSymBreakAgg__name = "sygus-sym-break-agg";

static constexpr const char* sygusSymBreakDynamic__name = "sygus-sym-break-dynamic";

static constexpr const char* sygusSymBreakLazy__name = "sygus-sym-break-lazy";

static constexpr const char* sygusSymBreakPbe__name = "sygus-sym-break-pbe";

static constexpr const char* sygusSymBreakRlv__name = "sygus-sym-break-rlv";

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

// clang-format on

namespace datatypes

{

// clang-format off

void setDefaultCdtBisimilar(Options& opts, bool value);

void setDefaultDtBinarySplit(Options& opts, bool value);

void setDefaultDtBlastSplits(Options& opts, bool value);

void setDefaultDtCyclic(Options& opts, bool value);

void setDefaultDtForceAssignment(Options& opts, bool value);

void setDefaultDtInferAsLemmas(Options& opts, bool value);

void setDefaultDtNestedRec(Options& opts, bool value);

void setDefaultDtPoliteOptimize(Options& opts, bool value);

void setDefaultDtRewriteErrorSel(Options& opts, bool value);

void setDefaultDtSharedSelectors(Options& opts, bool value);

void setDefaultSygusAbortSize(Options& opts, int value);

void setDefaultSygusFairMax(Options& opts, bool value);

void setDefaultSygusFair(Options& opts, SygusFairMode value);

void setDefaultSygusSymBreak(Options& opts, bool value);

void setDefaultSygusSymBreakAgg(Options& opts, bool value);

void setDefaultSygusSymBreakDynamic(Options& opts, bool value);

void setDefaultSygusSymBreakLazy(Options& opts, bool value);

void setDefaultSygusSymBreakPbe(Options& opts, bool value);

void setDefaultSygusSymBreakRlv(Options& opts, bool value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__DATATYPES_H */