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

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

namespace options {

// clang-format off

enum class RegExpInterMode

{

  ALL,

  CONSTANT,

  ONE_CONSTANT,

  NONE

};

static constexpr size_t RegExpInterMode__numValues = 4;

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

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

enum class ProcessLoopMode

{

  FULL,

  ABORT,

  SIMPLE_ABORT,

  NONE,

  SIMPLE

};

static constexpr size_t ProcessLoopMode__numValues = 5;

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;

  bool stringCheckEntailLen = true;

  bool stringCheckEntailLenWasSetByUser = 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 stringLenPropCsp = false;

  bool stringLenPropCspWasSetByUser = 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

extern struct regExpElim__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local regExpElim;

extern struct regExpElimAgg__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local regExpElimAgg;

extern struct stringRegExpInterMode__option_t

{

  typedef RegExpInterMode type;

  type operator()() const;

} thread_local stringRegExpInterMode;

extern struct stringCheckEntailLen__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringCheckEntailLen;

extern struct stringEager__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringEager;

extern struct stringEagerEval__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringEagerEval;

extern struct stringEagerLen__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringEagerLen;

extern struct stringExp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringExp;

extern struct stringFlatForms__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringFlatForms;

extern struct stringFMF__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringFMF;

extern struct stringGuessModel__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringGuessModel;

extern struct stringInferAsLemmas__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringInferAsLemmas;

extern struct stringInferSym__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringInferSym;

extern struct stringLazyPreproc__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringLazyPreproc;

extern struct stringLenNorm__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringLenNorm;

extern struct stringLenPropCsp__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringLenPropCsp;

extern struct stringMinPrefixExplain__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringMinPrefixExplain;

extern struct stringProcessLoopMode__option_t

{

  typedef ProcessLoopMode type;

  type operator()() const;

} thread_local stringProcessLoopMode;

extern struct stringRExplainLemmas__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringRExplainLemmas;

extern struct stringUnifiedVSpt__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local stringUnifiedVSpt;

// clang-format on

namespace strings

{

// clang-format off

static constexpr const char* regExpElim__name = "re-elim";

static constexpr const char* regExpElimAgg__name = "re-elim-agg";

static constexpr const char* stringRegExpInterMode__name = "re-inter-mode";

static constexpr const char* stringCheckEntailLen__name = "strings-check-entail-len";

static constexpr const char* stringEager__name = "strings-eager";

static constexpr const char* stringEagerEval__name = "strings-eager-eval";

static constexpr const char* stringEagerLen__name = "strings-eager-len";

static constexpr const char* stringExp__name = "strings-exp";

static constexpr const char* stringFlatForms__name = "strings-ff";

static constexpr const char* stringFMF__name = "strings-fmf";

static constexpr const char* stringGuessModel__name = "strings-guess-model";

static constexpr const char* stringInferAsLemmas__name = "strings-infer-as-lemmas";

static constexpr const char* stringInferSym__name = "strings-infer-sym";

static constexpr const char* stringLazyPreproc__name = "strings-lazy-pp";

static constexpr const char* stringLenNorm__name = "strings-len-norm";

static constexpr const char* stringLenPropCsp__name = "strings-lprop-csp";

static constexpr const char* stringMinPrefixExplain__name = "strings-min-prefix-explain";

static constexpr const char* stringProcessLoopMode__name = "strings-process-loop-mode";

static constexpr const char* stringRExplainLemmas__name = "strings-rexplain-lemmas";

static constexpr const char* stringUnifiedVSpt__name = "strings-unified-vspt";

// clang-format on

}

}  // namespace options

// clang-format off

// clang-format on

namespace options {

// clang-format off

inline bool stringLenPropCsp__option_t::operator()() const

{ return Options::current().strings.stringLenPropCsp; }

// clang-format on

namespace strings

{

// clang-format off

void setDefaultRegExpElim(Options& opts, bool value);

void setDefaultRegExpElimAgg(Options& opts, bool value);

void setDefaultStringRegExpInterMode(Options& opts, RegExpInterMode value);

void setDefaultStringCheckEntailLen(Options& opts, bool value);

void setDefaultStringEager(Options& opts, bool value);

void setDefaultStringEagerEval(Options& opts, bool value);

void setDefaultStringEagerLen(Options& opts, bool value);

void setDefaultStringExp(Options& opts, bool value);

void setDefaultStringFlatForms(Options& opts, bool value);

void setDefaultStringFMF(Options& opts, bool value);

void setDefaultStringGuessModel(Options& opts, bool value);

void setDefaultStringInferAsLemmas(Options& opts, bool value);

void setDefaultStringInferSym(Options& opts, bool value);

void setDefaultStringLazyPreproc(Options& opts, bool value);

void setDefaultStringLenNorm(Options& opts, bool value);

void setDefaultStringLenPropCsp(Options& opts, bool value);

void setDefaultStringMinPrefixExplain(Options& opts, bool value);

void setDefaultStringProcessLoopMode(Options& opts, ProcessLoopMode value);

void setDefaultStringRExplainLemmas(Options& opts, bool value);

void setDefaultStringUnifiedVSpt(Options& opts, bool value);

// clang-format on

}

}  // namespace options

}  // namespace cvc5

#endif /* CVC5__OPTIONS__STRINGS_H */