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

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

#define CVC5__OPTIONS__QUANTIFIERS_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5::options {

// clang-format off

enum class CegisSampleMode

{

  USE,

  TRUST,

  NONE

};

static constexpr size_t CegisSampleMode__numValues = 3;

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

CegisSampleMode stringToCegisSampleMode(const std::string& optarg);

enum class CegqiBvIneqMode

{

  KEEP,

  EQ_SLACK,

  EQ_BOUNDARY

};

static constexpr size_t CegqiBvIneqMode__numValues = 3;

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

CegqiBvIneqMode stringToCegqiBvIneqMode(const std::string& optarg);

enum class InstWhenMode

{

  LAST_CALL,

  FULL_DELAY,

  FULL_LAST_CALL,

  FULL_DELAY_LAST_CALL,

  FULL,

  PRE_FULL

};

static constexpr size_t InstWhenMode__numValues = 6;

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

InstWhenMode stringToInstWhenMode(const std::string& optarg);

enum class IteLiftQuantMode

{

  SIMPLE,

  ALL,

  NONE

};

static constexpr size_t IteLiftQuantMode__numValues = 3;

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

IteLiftQuantMode stringToIteLiftQuantMode(const std::string& optarg);

enum class LiteralMatchMode

{

  USE,

  AGG_PREDICATE,

  AGG,

  NONE

};

static constexpr size_t LiteralMatchMode__numValues = 4;

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

LiteralMatchMode stringToLiteralMatchMode(const std::string& optarg);

enum class MacrosQuantMode

{

  GROUND_UF,

  ALL,

  GROUND

};

static constexpr size_t MacrosQuantMode__numValues = 3;

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

MacrosQuantMode stringToMacrosQuantMode(const std::string& optarg);

enum class MbqiMode

{

  TRUST,

  FMC,

  NONE

};

static constexpr size_t MbqiMode__numValues = 3;

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

MbqiMode stringToMbqiMode(const std::string& optarg);

enum class PrenexQuantMode

{

  SIMPLE,

  NORMAL,

  NONE

};

static constexpr size_t PrenexQuantMode__numValues = 3;

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

PrenexQuantMode stringToPrenexQuantMode(const std::string& optarg);

enum class QcfMode

{

  PROP_EQ,

  CONFLICT_ONLY,

  PARTIAL

};

static constexpr size_t QcfMode__numValues = 3;

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

QcfMode stringToQcfMode(const std::string& optarg);

enum class QcfWhenMode

{

  LAST_CALL,

  STD_H,

  DEFAULT,

  STD

};

static constexpr size_t QcfWhenMode__numValues = 4;

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

QcfWhenMode stringToQcfWhenMode(const std::string& optarg);

enum class QuantDSplitMode

{

  AGG,

  DEFAULT,

  NONE

};

static constexpr size_t QuantDSplitMode__numValues = 3;

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

QuantDSplitMode stringToQuantDSplitMode(const std::string& optarg);

enum class QuantRepMode

{

  DEPTH,

  FIRST,

  EE

};

static constexpr size_t QuantRepMode__numValues = 3;

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

QuantRepMode stringToQuantRepMode(const std::string& optarg);

enum class SygusActiveGenMode

{

  ENUM_BASIC,

  AUTO,

  ENUM,

  VAR_AGNOSTIC,

  NONE

};

static constexpr size_t SygusActiveGenMode__numValues = 5;

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

SygusActiveGenMode stringToSygusActiveGenMode(const std::string& optarg);

enum class SygusFilterSolMode

{

  WEAK,

  STRONG,

  NONE

};

static constexpr size_t SygusFilterSolMode__numValues = 3;

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

SygusFilterSolMode stringToSygusFilterSolMode(const std::string& optarg);

enum class SygusGrammarConsMode

{

  SIMPLE,

  ANY_CONST,

  ANY_TERM,

  ANY_TERM_CONCISE

};

static constexpr size_t SygusGrammarConsMode__numValues = 4;

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

SygusGrammarConsMode stringToSygusGrammarConsMode(const std::string& optarg);

enum class SygusInstMode

{

  PRIORITY_EVAL,

  PRIORITY_INST,

  INTERLEAVE

};

static constexpr size_t SygusInstMode__numValues = 3;

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

SygusInstMode stringToSygusInstMode(const std::string& optarg);

enum class SygusInstScope

{

  OUT,

  BOTH,

  IN

};

static constexpr size_t SygusInstScope__numValues = 3;

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

SygusInstScope stringToSygusInstScope(const std::string& optarg);

enum class SygusInstTermSelMode

{

  MAX,

  BOTH,

  MIN

};

static constexpr size_t SygusInstTermSelMode__numValues = 3;

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

SygusInstTermSelMode stringToSygusInstTermSelMode(const std::string& optarg);

enum class SygusInvTemplMode

{

  POST,

  PRE,

  NONE

};

static constexpr size_t SygusInvTemplMode__numValues = 3;

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

SygusInvTemplMode stringToSygusInvTemplMode(const std::string& optarg);

enum class SygusQueryDumpFilesMode

{

  ALL,

  UNSOLVED,

  NONE

};

static constexpr size_t SygusQueryDumpFilesMode__numValues = 3;

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

SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode(const std::string& optarg);

enum class CegqiSingleInvRconsMode

{

  TRY,

  ALL,

  ALL_LIMIT,

  NONE

};

static constexpr size_t CegqiSingleInvRconsMode__numValues = 4;

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

CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode(const std::string& optarg);

enum class CegqiSingleInvMode

{

  USE,

  ALL,

  NONE

};

static constexpr size_t CegqiSingleInvMode__numValues = 3;

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

CegqiSingleInvMode stringToCegqiSingleInvMode(const std::string& optarg);

enum class SygusUnifPiMode

{

  CENUM_IGAIN,

  COMPLETE,

  CENUM,

  NONE

};

static constexpr size_t SygusUnifPiMode__numValues = 4;

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

SygusUnifPiMode stringToSygusUnifPiMode(const std::string& optarg);

enum class TermDbMode

{

  ALL,

  RELEVANT

};

static constexpr size_t TermDbMode__numValues = 2;

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

TermDbMode stringToTermDbMode(const std::string& optarg);

enum class TriggerActiveSelMode

{

  MAX,

  ALL,

  MIN

};

static constexpr size_t TriggerActiveSelMode__numValues = 3;

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

TriggerActiveSelMode stringToTriggerActiveSelMode(const std::string& optarg);

enum class TriggerSelMode

{

  MIN_SINGLE_ALL,

  MAX,

  ALL,

  MIN_SINGLE_MAX,

  MIN

};

static constexpr size_t TriggerSelMode__numValues = 5;

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

TriggerSelMode stringToTriggerSelMode(const std::string& optarg);

enum class UserPatMode

{

  USE,

  IGNORE,

  TRUST,

  STRICT,

  RESORT,

  INTERLEAVE

};

static constexpr size_t UserPatMode__numValues = 6;

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

UserPatMode stringToUserPatMode(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 aggressiveMiniscopeQuant = false;

  bool aggressiveMiniscopeQuantWasSetByUser = false;

  CegisSampleMode cegisSample = CegisSampleMode::NONE;

  bool cegisSampleWasSetByUser = false;

  bool cegqi = false;

  bool cegqiWasSetByUser = false;

  bool cegqiAll = false;

  bool cegqiAllWasSetByUser = false;

  bool cegqiBv = true;

  bool cegqiBvWasSetByUser = false;

  bool cegqiBvConcInv = true;

  bool cegqiBvConcInvWasSetByUser = false;

  CegqiBvIneqMode cegqiBvIneqMode = CegqiBvIneqMode::EQ_BOUNDARY;

  bool cegqiBvIneqModeWasSetByUser = false;

  bool cegqiBvInterleaveValue = false;

  bool cegqiBvInterleaveValueWasSetByUser = false;

  bool cegqiBvLinearize = true;

  bool cegqiBvLinearizeWasSetByUser = false;

  bool cegqiBvRmExtract = true;

  bool cegqiBvRmExtractWasSetByUser = false;

  bool cegqiBvSolveNl = false;

  bool cegqiBvSolveNlWasSetByUser = false;

  bool cegqiFullEffort = false;

  bool cegqiFullEffortWasSetByUser = false;

  bool cegqiInnermost = true;

  bool cegqiInnermostWasSetByUser = false;

  bool cegqiMidpoint = false;

  bool cegqiMidpointWasSetByUser = false;

  bool cegqiMinBounds = false;

  bool cegqiMinBoundsWasSetByUser = false;

  bool cegqiModel = true;

  bool cegqiModelWasSetByUser = false;

  bool cegqiMultiInst = false;

  bool cegqiMultiInstWasSetByUser = false;

  bool cegqiNestedQE = false;

  bool cegqiNestedQEWasSetByUser = false;

  bool cegqiNopt = true;

  bool cegqiNoptWasSetByUser = false;

  bool cegqiRepeatLit = false;

  bool cegqiRepeatLitWasSetByUser = false;

  bool cegqiRoundUpLowerLia = false;

  bool cegqiRoundUpLowerLiaWasSetByUser = false;

  bool cegqiSat = true;

  bool cegqiSatWasSetByUser = false;

  bool cegqiUseInfInt = false;

  bool cegqiUseInfIntWasSetByUser = false;

  bool cegqiUseInfReal = false;

  bool cegqiUseInfRealWasSetByUser = false;

  bool condVarSplitQuantAgg = false;

  bool condVarSplitQuantAggWasSetByUser = false;

  bool condVarSplitQuant = true;

  bool condVarSplitQuantWasSetByUser = false;

  bool conjectureFilterActiveTerms = true;

  bool conjectureFilterActiveTermsWasSetByUser = false;

  bool conjectureFilterCanonical = true;

  bool conjectureFilterCanonicalWasSetByUser = false;

  bool conjectureFilterModel = true;

  bool conjectureFilterModelWasSetByUser = false;

  bool conjectureGen = false;

  bool conjectureGenWasSetByUser = false;

  int64_t conjectureGenGtEnum = 50;

  bool conjectureGenGtEnumWasSetByUser = false;

  int64_t conjectureGenMaxDepth = 3;

  bool conjectureGenMaxDepthWasSetByUser = false;

  int64_t conjectureGenPerRound = 1;

  bool conjectureGenPerRoundWasSetByUser = false;

  bool conjectureUeeIntro = false;

  bool conjectureUeeIntroWasSetByUser = false;

  bool conjectureNoFilter = false;

  bool conjectureNoFilterWasSetByUser = false;

  bool dtStcInduction = false;

  bool dtStcInductionWasSetByUser = false;

  bool dtVarExpandQuant = true;

  bool dtVarExpandQuantWasSetByUser = false;

  bool eMatching = true;

  bool eMatchingWasSetByUser = false;

  bool elimTautQuant = true;

  bool elimTautQuantWasSetByUser = false;

  bool extRewriteQuant = false;

  bool extRewriteQuantWasSetByUser = false;

  bool finiteModelFind = false;

  bool finiteModelFindWasSetByUser = false;

  bool fmfBound = false;

  bool fmfBoundWasSetByUser = false;

  bool fmfBoundInt = false;

  bool fmfBoundIntWasSetByUser = false;

  bool fmfBoundLazy = false;

  bool fmfBoundLazyWasSetByUser = false;

  bool fmfFmcSimple = true;

  bool fmfFmcSimpleWasSetByUser = false;

  bool fmfFreshDistConst = false;

  bool fmfFreshDistConstWasSetByUser = false;

  bool fmfFunWellDefined = false;

  bool fmfFunWellDefinedWasSetByUser = false;

  bool fmfFunWellDefinedRelevant = false;

  bool fmfFunWellDefinedRelevantWasSetByUser = false;

  bool fmfInstEngine = false;

  bool fmfInstEngineWasSetByUser = false;

  int64_t fmfTypeCompletionThresh = 1000;

  bool fmfTypeCompletionThreshWasSetByUser = false;

  bool fullSaturateInterleave = false;

  bool fullSaturateInterleaveWasSetByUser = false;

  bool fullSaturateStratify = false;

  bool fullSaturateStratifyWasSetByUser = false;

  bool fullSaturateSum = false;

  bool fullSaturateSumWasSetByUser = false;

  bool fullSaturateQuant = false;

  bool fullSaturateQuantWasSetByUser = false;

  int64_t fullSaturateLimit = -1;

  bool fullSaturateLimitWasSetByUser = false;

  bool fullSaturateQuantRd = true;

  bool fullSaturateQuantRdWasSetByUser = false;

  bool globalNegate = false;

  bool globalNegateWasSetByUser = false;

  bool hoElim = false;

  bool hoElimWasSetByUser = false;

  bool hoElimStoreAx = true;

  bool hoElimStoreAxWasSetByUser = false;

  bool hoMatching = true;

  bool hoMatchingWasSetByUser = false;

  bool hoMatchingVarArgPriority = true;

  bool hoMatchingVarArgPriorityWasSetByUser = false;

  bool hoMergeTermDb = true;

  bool hoMergeTermDbWasSetByUser = false;

  bool incrementTriggers = true;

  bool incrementTriggersWasSetByUser = false;

  bool instLevelInputOnly = true;

  bool instLevelInputOnlyWasSetByUser = false;

  int64_t instMaxLevel = -1;

  bool instMaxLevelWasSetByUser = false;

  int64_t instMaxRounds = -1;

  bool instMaxRoundsWasSetByUser = false;

  bool instNoEntail = true;

  bool instNoEntailWasSetByUser = false;

  int64_t instWhenPhase = 2;

  bool instWhenPhaseWasSetByUser = false;

  bool instWhenStrictInterleave = true;

  bool instWhenStrictInterleaveWasSetByUser = false;

  bool instWhenTcFirst = true;

  bool instWhenTcFirstWasSetByUser = false;

  InstWhenMode instWhenMode = InstWhenMode::FULL_LAST_CALL;

  bool instWhenModeWasSetByUser = false;

  bool intWfInduction = false;

  bool intWfInductionWasSetByUser = false;

  bool iteDtTesterSplitQuant = false;

  bool iteDtTesterSplitQuantWasSetByUser = false;

  IteLiftQuantMode iteLiftQuant = IteLiftQuantMode::SIMPLE;

  bool iteLiftQuantWasSetByUser = false;

  LiteralMatchMode literalMatchMode = LiteralMatchMode::USE;

  bool literalMatchModeWasSetByUser = false;

  bool macrosQuant = false;

  bool macrosQuantWasSetByUser = false;

  MacrosQuantMode macrosQuantMode = MacrosQuantMode::GROUND_UF;

  bool macrosQuantModeWasSetByUser = false;

  bool mbqiInterleave = false;

  bool mbqiInterleaveWasSetByUser = false;

  bool fmfOneInstPerRound = false;

  bool fmfOneInstPerRoundWasSetByUser = false;

  MbqiMode mbqiMode = MbqiMode::FMC;

  bool mbqiModeWasSetByUser = false;

  bool miniscopeQuant = true;

  bool miniscopeQuantWasSetByUser = false;

  bool miniscopeQuantFreeVar = true;

  bool miniscopeQuantFreeVarWasSetByUser = false;

  bool multiTriggerCache = false;

  bool multiTriggerCacheWasSetByUser = false;

  bool multiTriggerLinear = true;

  bool multiTriggerLinearWasSetByUser = false;

  bool multiTriggerPriority = false;

  bool multiTriggerPriorityWasSetByUser = false;

  bool multiTriggerWhenSingle = false;

  bool multiTriggerWhenSingleWasSetByUser = false;

  bool partialTriggers = false;

  bool partialTriggersWasSetByUser = false;

  bool poolInst = true;

  bool poolInstWasSetByUser = false;

  bool preSkolemQuant = false;

  bool preSkolemQuantWasSetByUser = false;

  bool preSkolemQuantAgg = true;

  bool preSkolemQuantAggWasSetByUser = false;

  bool preSkolemQuantNested = true;

  bool preSkolemQuantNestedWasSetByUser = false;

  bool prenexQuantUser = false;

  bool prenexQuantUserWasSetByUser = false;

  PrenexQuantMode prenexQuant = PrenexQuantMode::SIMPLE;

  bool prenexQuantWasSetByUser = false;

  bool purifyTriggers = false;

  bool purifyTriggersWasSetByUser = false;

  bool qcfAllConflict = false;

  bool qcfAllConflictWasSetByUser = false;

  bool qcfEagerCheckRd = true;

  bool qcfEagerCheckRdWasSetByUser = false;

  bool qcfEagerTest = true;

  bool qcfEagerTestWasSetByUser = false;

  bool qcfNestedConflict = false;

  bool qcfNestedConflictWasSetByUser = false;

  bool qcfSkipRd = false;

  bool qcfSkipRdWasSetByUser = false;

  bool qcfTConstraint = false;

  bool qcfTConstraintWasSetByUser = false;

  bool qcfVoExp = false;

  bool qcfVoExpWasSetByUser = false;

  bool quantAlphaEquiv = true;

  bool quantAlphaEquivWasSetByUser = false;

  bool quantConflictFind = true;

  bool quantConflictFindWasSetByUser = false;

  QcfMode qcfMode = QcfMode::PROP_EQ;

  bool qcfModeWasSetByUser = false;

  QcfWhenMode qcfWhenMode = QcfWhenMode::DEFAULT;

  bool qcfWhenModeWasSetByUser = false;

  QuantDSplitMode quantDynamicSplit = QuantDSplitMode::DEFAULT;

  bool quantDynamicSplitWasSetByUser = false;

  bool quantFunWellDefined = false;

  bool quantFunWellDefinedWasSetByUser = false;

  bool quantInduction = false;

  bool quantInductionWasSetByUser = false;

  QuantRepMode quantRepMode = QuantRepMode::FIRST;

  bool quantRepModeWasSetByUser = false;

  bool quantSplit = true;

  bool quantSplitWasSetByUser = false;

  bool registerQuantBodyTerms = false;

  bool registerQuantBodyTermsWasSetByUser = false;

  bool relationalTriggers = false;

  bool relationalTriggersWasSetByUser = false;

  bool relevantTriggers = false;

  bool relevantTriggersWasSetByUser = false;

  bool sygus = false;

  bool sygusWasSetByUser = false;

  uint64_t sygusActiveGenEnumConsts = 5;

  bool sygusActiveGenEnumConstsWasSetByUser = false;

  SygusActiveGenMode sygusActiveGenMode = SygusActiveGenMode::AUTO;

  bool sygusActiveGenModeWasSetByUser = false;

  bool sygusAddConstGrammar = false;

  bool sygusAddConstGrammarWasSetByUser = false;

  bool sygusArgRelevant = false;

  bool sygusArgRelevantWasSetByUser = false;

  bool sygusInvAutoUnfold = true;

  bool sygusInvAutoUnfoldWasSetByUser = false;

  bool sygusBoolIteReturnConst = true;

  bool sygusBoolIteReturnConstWasSetByUser = false;

  bool sygusCoreConnective = false;

  bool sygusCoreConnectiveWasSetByUser = false;

  bool sygusConstRepairAbort = false;

  bool sygusConstRepairAbortWasSetByUser = false;

  bool sygusEvalOpt = true;

  bool sygusEvalOptWasSetByUser = false;

  bool sygusEvalUnfold = true;

  bool sygusEvalUnfoldWasSetByUser = false;

  bool sygusEvalUnfoldBool = true;

  bool sygusEvalUnfoldBoolWasSetByUser = false;

  uint64_t sygusExprMinerCheckTimeout;

  bool sygusExprMinerCheckTimeoutWasSetByUser = false;

  bool sygusExtRew = true;

  bool sygusExtRewWasSetByUser = false;

  bool sygusFilterSolRevSubsume = false;

  bool sygusFilterSolRevSubsumeWasSetByUser = false;

  SygusFilterSolMode sygusFilterSolMode = SygusFilterSolMode::NONE;

  bool sygusFilterSolModeWasSetByUser = false;

  SygusGrammarConsMode sygusGrammarConsMode = SygusGrammarConsMode::SIMPLE;

  bool sygusGrammarConsModeWasSetByUser = false;

  bool sygusGrammarNorm = false;

  bool sygusGrammarNormWasSetByUser = false;

  bool sygusInference = false;

  bool sygusInferenceWasSetByUser = false;

  bool sygusInst = false;

  bool sygusInstWasSetByUser = false;

  SygusInstMode sygusInstMode = SygusInstMode::PRIORITY_INST;

  bool sygusInstModeWasSetByUser = false;

  SygusInstScope sygusInstScope = SygusInstScope::IN;

  bool sygusInstScopeWasSetByUser = false;

  SygusInstTermSelMode sygusInstTermSel = SygusInstTermSelMode::MIN;

  bool sygusInstTermSelWasSetByUser = false;

  bool sygusInvTemplWhenSyntax = false;

  bool sygusInvTemplWhenSyntaxWasSetByUser = false;

  SygusInvTemplMode sygusInvTemplMode = SygusInvTemplMode::POST;

  bool sygusInvTemplModeWasSetByUser = false;

  bool sygusMinGrammar = true;

  bool sygusMinGrammarWasSetByUser = false;

  bool sygusUnifPbe = true;

  bool sygusUnifPbeWasSetByUser = false;

  bool sygusPbeMultiFair = false;

  bool sygusPbeMultiFairWasSetByUser = false;

  int64_t sygusPbeMultiFairDiff = 0;

  bool sygusPbeMultiFairDiffWasSetByUser = false;

  bool sygusQePreproc = false;

  bool sygusQePreprocWasSetByUser = false;

  bool sygusQueryGen = false;

  bool sygusQueryGenWasSetByUser = false;

  bool sygusQueryGenCheck = true;

  bool sygusQueryGenCheckWasSetByUser = false;

  SygusQueryDumpFilesMode sygusQueryGenDumpFiles = SygusQueryDumpFilesMode::NONE;

  bool sygusQueryGenDumpFilesWasSetByUser = false;

  uint64_t sygusQueryGenThresh = 5;

  bool sygusQueryGenThreshWasSetByUser = false;

  bool sygusRecFun = true;

  bool sygusRecFunWasSetByUser = false;

  uint64_t sygusRecFunEvalLimit = 1000;

  bool sygusRecFunEvalLimitWasSetByUser = false;

  bool sygusRepairConst = false;

  bool sygusRepairConstWasSetByUser = false;

  uint64_t sygusRepairConstTimeout;

  bool sygusRepairConstTimeoutWasSetByUser = false;

  bool sygusRew = false;

  bool sygusRewWasSetByUser = false;

  bool sygusRewSynth = false;

  bool sygusRewSynthWasSetByUser = false;

  bool sygusRewSynthAccel = false;

  bool sygusRewSynthAccelWasSetByUser = false;

  bool sygusRewSynthCheck = false;

  bool sygusRewSynthCheckWasSetByUser = false;

  bool sygusRewSynthFilterCong = true;

  bool sygusRewSynthFilterCongWasSetByUser = false;

  bool sygusRewSynthFilterMatch = true;

  bool sygusRewSynthFilterMatchWasSetByUser = false;

  bool sygusRewSynthFilterNonLinear = false;

  bool sygusRewSynthFilterNonLinearWasSetByUser = false;

  bool sygusRewSynthFilterOrder = true;

  bool sygusRewSynthFilterOrderWasSetByUser = false;

  bool sygusRewSynthInput = false;

  bool sygusRewSynthInputWasSetByUser = false;

  int64_t sygusRewSynthInputNVars = 3;

  bool sygusRewSynthInputNVarsWasSetByUser = false;

  bool sygusRewSynthInputUseBool = false;

  bool sygusRewSynthInputUseBoolWasSetByUser = false;

  bool sygusRewSynthRec = false;

  bool sygusRewSynthRecWasSetByUser = false;

  bool sygusRewVerify = false;

  bool sygusRewVerifyWasSetByUser = false;

  bool sygusRewVerifyAbort = true;

  bool sygusRewVerifyAbortWasSetByUser = false;

  bool sygusSampleFpUniform = false;

  bool sygusSampleFpUniformWasSetByUser = false;

  bool sygusSampleGrammar = true;

  bool sygusSampleGrammarWasSetByUser = false;

  int64_t sygusSamples = 1000;

  bool sygusSamplesWasSetByUser = false;

  bool cegqiSingleInvAbort = false;

  bool cegqiSingleInvAbortWasSetByUser = false;

  bool cegqiSingleInvPartial = false;

  bool cegqiSingleInvPartialWasSetByUser = false;

  int64_t cegqiSingleInvReconstructLimit = 10000;

  bool cegqiSingleInvReconstructLimitWasSetByUser = false;

  CegqiSingleInvRconsMode cegqiSingleInvReconstruct = CegqiSingleInvRconsMode::ALL_LIMIT;

  bool cegqiSingleInvReconstructWasSetByUser = false;

  bool cegqiSingleInvReconstructConst = true;

  bool cegqiSingleInvReconstructConstWasSetByUser = false;

  CegqiSingleInvMode cegqiSingleInvMode = CegqiSingleInvMode::NONE;

  bool cegqiSingleInvModeWasSetByUser = false;

  bool sygusStream = false;

  bool sygusStreamWasSetByUser = false;

  bool sygusTemplEmbedGrammar = false;

  bool sygusTemplEmbedGrammarWasSetByUser = false;

  bool sygusUnifCondIndNoRepeatSol = true;

  bool sygusUnifCondIndNoRepeatSolWasSetByUser = false;

  SygusUnifPiMode sygusUnifPi = SygusUnifPiMode::NONE;

  bool sygusUnifPiWasSetByUser = false;

  bool sygusUnifShuffleCond = false;

  bool sygusUnifShuffleCondWasSetByUser = false;

  int64_t sygusVerifyInstMaxRounds = 3;

  bool sygusVerifyInstMaxRoundsWasSetByUser = false;

  bool termDbCd = true;

  bool termDbCdWasSetByUser = false;

  TermDbMode termDbMode = TermDbMode::ALL;

  bool termDbModeWasSetByUser = false;

  TriggerActiveSelMode triggerActiveSelMode = TriggerActiveSelMode::ALL;

  bool triggerActiveSelModeWasSetByUser = false;

  TriggerSelMode triggerSelMode = TriggerSelMode::MIN;

  bool triggerSelModeWasSetByUser = false;

  UserPatMode userPatternsQuant = UserPatMode::TRUST;

  bool userPatternsQuantWasSetByUser = false;

  bool varElimQuant = true;

  bool varElimQuantWasSetByUser = false;

  bool varIneqElimQuant = true;

  bool varIneqElimQuantWasSetByUser = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

inline bool conjectureNoFilter() { return Options::current().quantifiers.conjectureNoFilter; }

inline bool fmfBoundInt() { return Options::current().quantifiers.fmfBoundInt; }

inline bool quantInduction() { return Options::current().quantifiers.quantInduction; }

inline bool sygusRew() { return Options::current().quantifiers.sygusRew; }

inline bool cegqiSingleInvPartial() { return Options::current().quantifiers.cegqiSingleInvPartial; }

inline bool cegqiSingleInvReconstructConst() { return Options::current().quantifiers.cegqiSingleInvReconstructConst; }

inline int64_t sygusVerifyInstMaxRounds() { return Options::current().quantifiers.sygusVerifyInstMaxRounds; }

// clang-format on

namespace quantifiers

{

// clang-format off

static constexpr const char* aggressiveMiniscopeQuant__name = "ag-miniscope-quant";

static constexpr const char* cegisSample__name = "cegis-sample";

static constexpr const char* cegqi__name = "cegqi";

static constexpr const char* cegqiAll__name = "cegqi-all";

static constexpr const char* cegqiBv__name = "cegqi-bv";

static constexpr const char* cegqiBvConcInv__name = "cegqi-bv-concat-inv";

static constexpr const char* cegqiBvIneqMode__name = "cegqi-bv-ineq";

static constexpr const char* cegqiBvInterleaveValue__name = "cegqi-bv-interleave-value";

static constexpr const char* cegqiBvLinearize__name = "cegqi-bv-linear";

static constexpr const char* cegqiBvRmExtract__name = "cegqi-bv-rm-extract";

static constexpr const char* cegqiBvSolveNl__name = "cegqi-bv-solve-nl";

static constexpr const char* cegqiFullEffort__name = "cegqi-full";

static constexpr const char* cegqiInnermost__name = "cegqi-innermost";

static constexpr const char* cegqiMidpoint__name = "cegqi-midpoint";

static constexpr const char* cegqiMinBounds__name = "cegqi-min-bounds";

static constexpr const char* cegqiModel__name = "cegqi-model";

static constexpr const char* cegqiMultiInst__name = "cegqi-multi-inst";

static constexpr const char* cegqiNestedQE__name = "cegqi-nested-qe";

static constexpr const char* cegqiNopt__name = "cegqi-nopt";

static constexpr const char* cegqiRepeatLit__name = "cegqi-repeat-lit";

static constexpr const char* cegqiRoundUpLowerLia__name = "cegqi-round-up-lia";

static constexpr const char* cegqiSat__name = "cegqi-sat";

static constexpr const char* cegqiUseInfInt__name = "cegqi-use-inf-int";

static constexpr const char* cegqiUseInfReal__name = "cegqi-use-inf-real";

static constexpr const char* condVarSplitQuantAgg__name = "cond-var-split-agg-quant";

static constexpr const char* condVarSplitQuant__name = "cond-var-split-quant";

static constexpr const char* conjectureFilterActiveTerms__name = "conjecture-filter-active-terms";

static constexpr const char* conjectureFilterCanonical__name = "conjecture-filter-canonical";

static constexpr const char* conjectureFilterModel__name = "conjecture-filter-model";

static constexpr const char* conjectureGen__name = "conjecture-gen";

static constexpr const char* conjectureGenGtEnum__name = "conjecture-gen-gt-enum";

static constexpr const char* conjectureGenMaxDepth__name = "conjecture-gen-max-depth";

static constexpr const char* conjectureGenPerRound__name = "conjecture-gen-per-round";

static constexpr const char* conjectureUeeIntro__name = "conjecture-gen-uee-intro";

static constexpr const char* conjectureNoFilter__name = "conjecture-no-filter";

static constexpr const char* dtStcInduction__name = "dt-stc-ind";

static constexpr const char* dtVarExpandQuant__name = "dt-var-exp-quant";

static constexpr const char* eMatching__name = "e-matching";

static constexpr const char* elimTautQuant__name = "elim-taut-quant";

static constexpr const char* extRewriteQuant__name = "ext-rewrite-quant";

static constexpr const char* finiteModelFind__name = "finite-model-find";

static constexpr const char* fmfBound__name = "fmf-bound";

static constexpr const char* fmfBoundInt__name = "fmf-bound-int";

static constexpr const char* fmfBoundLazy__name = "fmf-bound-lazy";

static constexpr const char* fmfFmcSimple__name = "fmf-fmc-simple";

static constexpr const char* fmfFreshDistConst__name = "fmf-fresh-dc";

static constexpr const char* fmfFunWellDefined__name = "fmf-fun";

static constexpr const char* fmfFunWellDefinedRelevant__name = "fmf-fun-rlv";

static constexpr const char* fmfInstEngine__name = "fmf-inst-engine";

static constexpr const char* fmfTypeCompletionThresh__name = "fmf-type-completion-thresh";

static constexpr const char* fullSaturateInterleave__name = "fs-interleave";

static constexpr const char* fullSaturateStratify__name = "fs-stratify";

static constexpr const char* fullSaturateSum__name = "fs-sum";

static constexpr const char* fullSaturateQuant__name = "full-saturate-quant";

static constexpr const char* fullSaturateLimit__name = "full-saturate-quant-limit";

static constexpr const char* fullSaturateQuantRd__name = "full-saturate-quant-rd";

static constexpr const char* globalNegate__name = "global-negate";

static constexpr const char* hoElim__name = "ho-elim";

static constexpr const char* hoElimStoreAx__name = "ho-elim-store-ax";

static constexpr const char* hoMatching__name = "ho-matching";

static constexpr const char* hoMatchingVarArgPriority__name = "ho-matching-var-priority";

static constexpr const char* hoMergeTermDb__name = "ho-merge-term-db";

static constexpr const char* incrementTriggers__name = "increment-triggers";

static constexpr const char* instLevelInputOnly__name = "inst-level-input-only";

static constexpr const char* instMaxLevel__name = "inst-max-level";

static constexpr const char* instMaxRounds__name = "inst-max-rounds";

static constexpr const char* instNoEntail__name = "inst-no-entail";

static constexpr const char* instWhenPhase__name = "inst-when-phase";

static constexpr const char* instWhenStrictInterleave__name = "inst-when-strict-interleave";

static constexpr const char* instWhenTcFirst__name = "inst-when-tc-first";

static constexpr const char* instWhenMode__name = "inst-when";

static constexpr const char* intWfInduction__name = "int-wf-ind";

static constexpr const char* iteDtTesterSplitQuant__name = "ite-dtt-split-quant";

static constexpr const char* iteLiftQuant__name = "ite-lift-quant";

static constexpr const char* literalMatchMode__name = "literal-matching";

static constexpr const char* macrosQuant__name = "macros-quant";

static constexpr const char* macrosQuantMode__name = "macros-quant-mode";

static constexpr const char* mbqiInterleave__name = "mbqi-interleave";

static constexpr const char* fmfOneInstPerRound__name = "mbqi-one-inst-per-round";

static constexpr const char* mbqiMode__name = "mbqi";

static constexpr const char* miniscopeQuant__name = "miniscope-quant";

static constexpr const char* miniscopeQuantFreeVar__name = "miniscope-quant-fv";

static constexpr const char* multiTriggerCache__name = "multi-trigger-cache";

static constexpr const char* multiTriggerLinear__name = "multi-trigger-linear";

static constexpr const char* multiTriggerPriority__name = "multi-trigger-priority";

static constexpr const char* multiTriggerWhenSingle__name = "multi-trigger-when-single";

static constexpr const char* partialTriggers__name = "partial-triggers";

static constexpr const char* poolInst__name = "pool-inst";

static constexpr const char* preSkolemQuant__name = "pre-skolem-quant";

static constexpr const char* preSkolemQuantAgg__name = "pre-skolem-quant-agg";

static constexpr const char* preSkolemQuantNested__name = "pre-skolem-quant-nested";

static constexpr const char* prenexQuantUser__name = "prenex-quant-user";

static constexpr const char* prenexQuant__name = "prenex-quant";

static constexpr const char* purifyTriggers__name = "purify-triggers";

static constexpr const char* qcfAllConflict__name = "qcf-all-conflict";

static constexpr const char* qcfEagerCheckRd__name = "qcf-eager-check-rd";

static constexpr const char* qcfEagerTest__name = "qcf-eager-test";

static constexpr const char* qcfNestedConflict__name = "qcf-nested-conflict";

static constexpr const char* qcfSkipRd__name = "qcf-skip-rd";

static constexpr const char* qcfTConstraint__name = "qcf-tconstraint";

static constexpr const char* qcfVoExp__name = "qcf-vo-exp";

static constexpr const char* quantAlphaEquiv__name = "quant-alpha-equiv";

static constexpr const char* quantConflictFind__name = "quant-cf";

static constexpr const char* qcfMode__name = "quant-cf-mode";

static constexpr const char* qcfWhenMode__name = "quant-cf-when";

static constexpr const char* quantDynamicSplit__name = "quant-dsplit-mode";

static constexpr const char* quantFunWellDefined__name = "quant-fun-wd";

static constexpr const char* quantInduction__name = "quant-ind";

static constexpr const char* quantRepMode__name = "quant-rep-mode";

static constexpr const char* quantSplit__name = "quant-split";

static constexpr const char* registerQuantBodyTerms__name = "register-quant-body-terms";

static constexpr const char* relationalTriggers__name = "relational-triggers";

static constexpr const char* relevantTriggers__name = "relevant-triggers";

static constexpr const char* sygus__name = "sygus";

static constexpr const char* sygusActiveGenEnumConsts__name = "sygus-active-gen-cfactor";

static constexpr const char* sygusActiveGenMode__name = "sygus-active-gen";

static constexpr const char* sygusAddConstGrammar__name = "sygus-add-const-grammar";

static constexpr const char* sygusArgRelevant__name = "sygus-arg-relevant";

static constexpr const char* sygusInvAutoUnfold__name = "sygus-auto-unfold";

static constexpr const char* sygusBoolIteReturnConst__name = "sygus-bool-ite-return-const";

static constexpr const char* sygusCoreConnective__name = "sygus-core-connective";

static constexpr const char* sygusConstRepairAbort__name = "sygus-crepair-abort";

static constexpr const char* sygusEvalOpt__name = "sygus-eval-opt";

static constexpr const char* sygusEvalUnfold__name = "sygus-eval-unfold";

static constexpr const char* sygusEvalUnfoldBool__name = "sygus-eval-unfold-bool";

static constexpr const char* sygusExprMinerCheckTimeout__name = "sygus-expr-miner-check-timeout";

static constexpr const char* sygusExtRew__name = "sygus-ext-rew";

static constexpr const char* sygusFilterSolRevSubsume__name = "sygus-filter-sol-rev";

static constexpr const char* sygusFilterSolMode__name = "sygus-filter-sol";

static constexpr const char* sygusGrammarConsMode__name = "sygus-grammar-cons";

static constexpr const char* sygusGrammarNorm__name = "sygus-grammar-norm";

static constexpr const char* sygusInference__name = "sygus-inference";

static constexpr const char* sygusInst__name = "sygus-inst";

static constexpr const char* sygusInstMode__name = "sygus-inst-mode";

static constexpr const char* sygusInstScope__name = "sygus-inst-scope";

static constexpr const char* sygusInstTermSel__name = "sygus-inst-term-sel";

static constexpr const char* sygusInvTemplWhenSyntax__name = "sygus-inv-templ-when-sg";

static constexpr const char* sygusInvTemplMode__name = "sygus-inv-templ";

static constexpr const char* sygusMinGrammar__name = "sygus-min-grammar";

static constexpr const char* sygusUnifPbe__name = "sygus-pbe";

static constexpr const char* sygusPbeMultiFair__name = "sygus-pbe-multi-fair";

static constexpr const char* sygusPbeMultiFairDiff__name = "sygus-pbe-multi-fair-diff";

static constexpr const char* sygusQePreproc__name = "sygus-qe-preproc";

static constexpr const char* sygusQueryGen__name = "sygus-query-gen";

static constexpr const char* sygusQueryGenCheck__name = "sygus-query-gen-check";

static constexpr const char* sygusQueryGenDumpFiles__name = "sygus-query-gen-dump-files";

static constexpr const char* sygusQueryGenThresh__name = "sygus-query-gen-thresh";

static constexpr const char* sygusRecFun__name = "sygus-rec-fun";

static constexpr const char* sygusRecFunEvalLimit__name = "sygus-rec-fun-eval-limit";

static constexpr const char* sygusRepairConst__name = "sygus-repair-const";

static constexpr const char* sygusRepairConstTimeout__name = "sygus-repair-const-timeout";

static constexpr const char* sygusRew__name = "sygus-rr";

static constexpr const char* sygusRewSynth__name = "sygus-rr-synth";

static constexpr const char* sygusRewSynthAccel__name = "sygus-rr-synth-accel";

static constexpr const char* sygusRewSynthCheck__name = "sygus-rr-synth-check";

static constexpr const char* sygusRewSynthFilterCong__name = "sygus-rr-synth-filter-cong";

static constexpr const char* sygusRewSynthFilterMatch__name = "sygus-rr-synth-filter-match";

static constexpr const char* sygusRewSynthFilterNonLinear__name = "sygus-rr-synth-filter-nl";

static constexpr const char* sygusRewSynthFilterOrder__name = "sygus-rr-synth-filter-order";

static constexpr const char* sygusRewSynthInput__name = "sygus-rr-synth-input";

static constexpr const char* sygusRewSynthInputNVars__name = "sygus-rr-synth-input-nvars";

static constexpr const char* sygusRewSynthInputUseBool__name = "sygus-rr-synth-input-use-bool";

static constexpr const char* sygusRewSynthRec__name = "sygus-rr-synth-rec";

static constexpr const char* sygusRewVerify__name = "sygus-rr-verify";

static constexpr const char* sygusRewVerifyAbort__name = "sygus-rr-verify-abort";

static constexpr const char* sygusSampleFpUniform__name = "sygus-sample-fp-uniform";

static constexpr const char* sygusSampleGrammar__name = "sygus-sample-grammar";

static constexpr const char* sygusSamples__name = "sygus-samples";

static constexpr const char* cegqiSingleInvAbort__name = "sygus-si-abort";

static constexpr const char* cegqiSingleInvPartial__name = "sygus-si-partial";

static constexpr const char* cegqiSingleInvReconstructLimit__name = "sygus-si-rcons-limit";

static constexpr const char* cegqiSingleInvReconstruct__name = "sygus-si-rcons";

static constexpr const char* cegqiSingleInvReconstructConst__name = "sygus-si-reconstruct-const";

static constexpr const char* cegqiSingleInvMode__name = "sygus-si";

static constexpr const char* sygusStream__name = "sygus-stream";

static constexpr const char* sygusTemplEmbedGrammar__name = "sygus-templ-embed-grammar";

static constexpr const char* sygusUnifCondIndNoRepeatSol__name = "sygus-unif-cond-independent-no-repeat-sol";

static constexpr const char* sygusUnifPi__name = "sygus-unif-pi";

static constexpr const char* sygusUnifShuffleCond__name = "sygus-unif-shuffle-cond";

static constexpr const char* sygusVerifyInstMaxRounds__name = "sygus-verify-inst-max-rounds";

static constexpr const char* termDbCd__name = "term-db-cd";

static constexpr const char* termDbMode__name = "term-db-mode";

static constexpr const char* triggerActiveSelMode__name = "trigger-active-sel";