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

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

#define CVC5__OPTIONS__DECISION_H

#include "options/options.h"

// clang-format off

#include "options/decision_weight.h"

// clang-format on

namespace cvc5 {

namespace options {

// clang-format off

enum class DecisionWeightInternal

{

  USR1,

  OFF,

  SUM,

  MAX

};

static constexpr size_t DecisionWeightInternal__numValues = 4;

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

DecisionWeightInternal stringToDecisionWeightInternal(const std::string& optarg);

enum class DecisionMode

{

  JUSTIFICATION,

  STOPONLY_OLD,

  JUSTIFICATION_OLD,

  INTERNAL,

  STOPONLY

};

static constexpr size_t DecisionMode__numValues = 5;

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

DecisionMode stringToDecisionMode(const std::string& optarg);

enum class JutificationSkolemRlvMode

{

  ALWAYS,

  ASSERT

};

static constexpr size_t JutificationSkolemRlvMode__numValues = 2;

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

JutificationSkolemRlvMode stringToJutificationSkolemRlvMode(const std::string& optarg);

enum class JutificationSkolemMode

{

  LAST,

  FIRST

};

static constexpr size_t JutificationSkolemMode__numValues = 2;

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

JutificationSkolemMode stringToJutificationSkolemMode(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

  int decisionRandomWeight = 0;

  bool decisionRandomWeightWasSetByUser = false;

  cvc5::decision::DecisionWeight decisionThreshold = 0;

  bool decisionThresholdWasSetByUser = false;

  bool decisionUseWeight = false;

  bool decisionUseWeightWasSetByUser = false;

  DecisionWeightInternal decisionWeightInternal = DecisionWeightInternal::OFF;

  bool decisionWeightInternalWasSetByUser = false;

  DecisionMode decisionMode = DecisionMode::INTERNAL;

  bool decisionModeWasSetByUser = false;

  bool jhRlvOrder = false;

  bool jhRlvOrderWasSetByUser = false;

  JutificationSkolemRlvMode jhSkolemRlvMode = JutificationSkolemRlvMode::ASSERT;

  bool jhSkolemRlvModeWasSetByUser = false;

  JutificationSkolemMode jhSkolemMode = JutificationSkolemMode::FIRST;

  bool jhSkolemModeWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct decisionRandomWeight__option_t

{

  typedef int type;

  type operator()() const;

} thread_local decisionRandomWeight;

extern struct decisionThreshold__option_t

{

  typedef cvc5::decision::DecisionWeight type;

  type operator()() const;

} thread_local decisionThreshold;

extern struct decisionUseWeight__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local decisionUseWeight;

extern struct decisionWeightInternal__option_t

{

  typedef DecisionWeightInternal type;

  type operator()() const;

} thread_local decisionWeightInternal;

extern struct decisionMode__option_t

{

  typedef DecisionMode type;

  type operator()() const;

} thread_local decisionMode;

extern struct jhRlvOrder__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local jhRlvOrder;

extern struct jhSkolemRlvMode__option_t

{

  typedef JutificationSkolemRlvMode type;

  type operator()() const;

} thread_local jhSkolemRlvMode;

extern struct jhSkolemMode__option_t

{

  typedef JutificationSkolemMode type;

  type operator()() const;

} thread_local jhSkolemMode;

// clang-format on

namespace decision

{

// clang-format off

static constexpr const char* decisionRandomWeight__name = "decision-random-weight";

static constexpr const char* decisionThreshold__name = "decision-threshold";

static constexpr const char* decisionUseWeight__name = "decision-use-weight";

static constexpr const char* decisionWeightInternal__name = "decision-weight-internal";

static constexpr const char* decisionMode__name = "decision";

static constexpr const char* jhRlvOrder__name = "jh-rlv-order";

static constexpr const char* jhSkolemRlvMode__name = "jh-skolem-rlv";

static constexpr const char* jhSkolemMode__name = "jh-skolem";

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

// clang-format on

namespace decision

{

// clang-format off

void setDefaultDecisionRandomWeight(Options& opts, int value);

void setDefaultDecisionThreshold(Options& opts, cvc5::decision::DecisionWeight value);

void setDefaultDecisionUseWeight(Options& opts, bool value);

void setDefaultDecisionWeightInternal(Options& opts, DecisionWeightInternal value);

void setDefaultDecisionMode(Options& opts, DecisionMode value);

void setDefaultJhRlvOrder(Options& opts, bool value);

void setDefaultJhSkolemRlvMode(Options& opts, JutificationSkolemRlvMode value);

void setDefaultJhSkolemMode(Options& opts, JutificationSkolemMode value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__DECISION_H */