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

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

#define CVC5__OPTIONS__STRINGS_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5::options {

// clang-format off

enum class RegExpInterMode

{

  ONE_CONSTANT, ALL, NONE, CONSTANT,

  __MAX_VALUE = CONSTANT

};

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

RegExpInterMode stringToRegExpInterMode(const std::string& optarg);

enum class ProcessLoopMode

{

  SIMPLE, SIMPLE_ABORT, NONE, FULL, ABORT,

  __MAX_VALUE = ABORT

};

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

ProcessLoopMode stringToProcessLoopMode(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 regExpElim = false;

  bool regExpElimWasSetByUser = false;

  bool regExpElimAgg = false;

  bool regExpElimAggWasSetByUser = false;

  RegExpInterMode stringRegExpInterMode = RegExpInterMode::CONSTANT;

  bool stringRegExpInterModeWasSetByUser = false;

  uint64_t stringsAlphaCard = 196608;

  bool stringsAlphaCardWasSetByUser = false;

  bool stringCheckEntailLen = true;

  bool stringCheckEntailLenWasSetByUser = false;

  bool stringsDeqExt = false;

  bool stringsDeqExtWasSetByUser = false;

  bool stringEager = false;

  bool stringEagerWasSetByUser = false;

  bool stringEagerEval = true;

  bool stringEagerEvalWasSetByUser = false;

  bool stringEagerLen = true;

  bool stringEagerLenWasSetByUser = false;

  bool stringExp = false;

  bool stringExpWasSetByUser = false;

  bool stringFlatForms = true;

  bool stringFlatFormsWasSetByUser = false;

  bool stringFMF = false;

  bool stringFMFWasSetByUser = false;

  bool stringGuessModel = false;

  bool stringGuessModelWasSetByUser = false;

  bool stringInferAsLemmas = false;

  bool stringInferAsLemmasWasSetByUser = false;

  bool stringInferSym = true;

  bool stringInferSymWasSetByUser = false;

  bool stringLazyPreproc = true;

  bool stringLazyPreprocWasSetByUser = false;

  bool stringLenNorm = true;

  bool stringLenNormWasSetByUser = false;

  bool stringMinPrefixExplain = true;

  bool stringMinPrefixExplainWasSetByUser = false;

  ProcessLoopMode stringProcessLoopMode = ProcessLoopMode::FULL;

  bool stringProcessLoopModeWasSetByUser = false;

  bool stringRExplainLemmas = true;

  bool stringRExplainLemmasWasSetByUser = false;

  bool stringUnifiedVSpt = true;

  bool stringUnifiedVSptWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

inline uint64_t stringsAlphaCard() { return Options::current().strings.stringsAlphaCard; }

inline bool stringLazyPreproc() { return Options::current().strings.stringLazyPreproc; }

// clang-format on

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__STRINGS_H */