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

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

#define CVC5__OPTIONS__ARRAYS_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5::options {

// clang-format off

// 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

  int64_t arraysConfig = 0;

  bool arraysConfigWasSetByUser = false;

  bool arraysEagerIndexSplitting = true;

  bool arraysEagerIndexSplittingWasSetByUser = false;

  bool arraysEagerLemmas = false;

  bool arraysEagerLemmasWasSetByUser = false;

  bool arraysExp = false;

  bool arraysExpWasSetByUser = false;

  bool arraysModelBased = false;

  bool arraysModelBasedWasSetByUser = false;

  bool arraysOptimizeLinear = true;

  bool arraysOptimizeLinearWasSetByUser = false;

  int64_t arraysPropagate = 2;

  bool arraysPropagateWasSetByUser = false;

  bool arraysReduceSharing = false;

  bool arraysReduceSharingWasSetByUser = false;

  bool arraysWeakEquivalence = false;

  bool arraysWeakEquivalenceWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

inline int64_t arraysConfig() { return Options::current().arrays.arraysConfig; }

inline bool arraysExp() { return Options::current().arrays.arraysExp; }

inline bool arraysModelBased() { return Options::current().arrays.arraysModelBased; }

// clang-format on

namespace arrays

{

// clang-format off

static constexpr const char* arraysConfig__name = "arrays-config";

static constexpr const char* arraysEagerIndexSplitting__name = "arrays-eager-index";

static constexpr const char* arraysEagerLemmas__name = "arrays-eager-lemmas";

static constexpr const char* arraysExp__name = "arrays-exp";

static constexpr const char* arraysModelBased__name = "arrays-model-based";

static constexpr const char* arraysOptimizeLinear__name = "arrays-optimize-linear";

static constexpr const char* arraysPropagate__name = "arrays-prop";

static constexpr const char* arraysReduceSharing__name = "arrays-reduce-sharing";

static constexpr const char* arraysWeakEquivalence__name = "arrays-weak-equiv";

void setDefaultArraysConfig(Options& opts, int64_t value);void setDefaultArraysEagerIndexSplitting(Options& opts, bool value);void setDefaultArraysEagerLemmas(Options& opts, bool value);void setDefaultArraysExp(Options& opts, bool value);void setDefaultArraysModelBased(Options& opts, bool value);void setDefaultArraysOptimizeLinear(Options& opts, bool value);void setDefaultArraysPropagate(Options& opts, int64_t value);void setDefaultArraysReduceSharing(Options& opts, bool value);void setDefaultArraysWeakEquivalence(Options& opts, bool value);

// clang-format on

}

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__ARRAYS_H */