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

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

namespace options {

// clang-format off

enum class CegisSampleMode

{

  NONE,

  USE,

  TRUST

};

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

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

enum class CegqiBvIneqMode

{

  EQ_BOUNDARY,

  EQ_SLACK,

  KEEP

};

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

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

enum class InstWhenMode

{

  FULL,

  PRE_FULL,

  FULL_DELAY,

  LAST_CALL,

  FULL_LAST_CALL,

  FULL_DELAY_LAST_CALL

};

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

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

enum class IteLiftQuantMode

{

  NONE,

  SIMPLE,

  ALL

};

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

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

enum class LiteralMatchMode

{

  NONE,

  AGG_PREDICATE,

  USE,

  AGG

};

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

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

enum class MacrosQuantMode

{

  GROUND,

  ALL,

  GROUND_UF

};

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

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

enum class MbqiMode

{

  NONE,

  FMC,

  TRUST

};

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

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

enum class PrenexQuantMode

{

  NONE,

  SIMPLE,

  NORMAL

};

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

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

enum class QcfMode

{

  CONFLICT_ONLY,

  PROP_EQ,

  PARTIAL

};

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

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

enum class QcfWhenMode

{

  LAST_CALL,

  STD,

  DEFAULT,

  STD_H

};

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

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

enum class QuantDSplitMode

{

  NONE,

  DEFAULT,

  AGG

};

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

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

enum class QuantRepMode

{

  DEPTH,

  EE,

  FIRST

};

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

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

enum class SygusActiveGenMode

{

  VAR_AGNOSTIC,

  NONE,

  ENUM_BASIC,

  AUTO,

  ENUM

};

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

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

enum class SygusFilterSolMode

{

  NONE,

  WEAK,

  STRONG

};

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

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

enum class SygusGrammarConsMode

{

  ANY_TERM,

  SIMPLE,

  ANY_TERM_CONCISE,

  ANY_CONST

};

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

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

enum class SygusInstMode

{

  INTERLEAVE,

  PRIORITY_INST,

  PRIORITY_EVAL

};

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

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

enum class SygusInstScope

{

  IN,

  OUT,

  BOTH

};

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

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

enum class SygusInstTermSelMode

{

  MIN,

  BOTH,

  MAX

};

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

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

enum class SygusInvTemplMode

{

  NONE,

  POST,

  PRE

};

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

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

enum class SygusQueryDumpFilesMode

{

  NONE,

  ALL,

  UNSOLVED

};

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

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

enum class CegqiSingleInvRconsMode

{

  NONE,

  ALL,

  ALL_LIMIT,

  TRY

};

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

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

enum class CegqiSingleInvMode

{

  NONE,

  ALL,

  USE

};

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

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

enum class SygusUnifPiMode

{

  CENUM,

  NONE,

  COMPLETE,

  CENUM_IGAIN

};

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

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

enum class TermDbMode

{

  ALL,

  RELEVANT

};

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

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

enum class TriggerActiveSelMode

{

  MIN,

  ALL,

  MAX

};

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

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

enum class TriggerSelMode

{

  MIN,

  MIN_SINGLE_MAX,

  MIN_SINGLE_ALL,

  ALL,

  MAX

};

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

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

enum class UserPatMode

{

  INTERLEAVE,

  RESORT,

  IGNORE,

  USE,

  TRUST

};

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 aggressiveMiniscopeQuant__setByUser__ = false;

  CegisSampleMode cegisSample = CegisSampleMode::NONE;\

  bool cegisSample__setByUser__ = false;

  bool cegqi = false;\

  bool cegqi__setByUser__ = false;

  bool cegqiAll = false;\

  bool cegqiAll__setByUser__ = false;

  bool cegqiBv = true;\

  bool cegqiBv__setByUser__ = false;

  bool cegqiBvConcInv = true;\

  bool cegqiBvConcInv__setByUser__ = false;

  CegqiBvIneqMode cegqiBvIneqMode = CegqiBvIneqMode::EQ_BOUNDARY;\

  bool cegqiBvIneqMode__setByUser__ = false;

  bool cegqiBvInterleaveValue = false;\

  bool cegqiBvInterleaveValue__setByUser__ = false;

  bool cegqiBvLinearize = true;\

  bool cegqiBvLinearize__setByUser__ = false;

  bool cegqiBvRmExtract = true;\

  bool cegqiBvRmExtract__setByUser__ = false;

  bool cegqiBvSolveNl = false;\

  bool cegqiBvSolveNl__setByUser__ = false;

  bool cegqiFullEffort = false;\

  bool cegqiFullEffort__setByUser__ = false;

  bool cegqiInnermost = true;\

  bool cegqiInnermost__setByUser__ = false;

  bool cegqiMidpoint = false;\

  bool cegqiMidpoint__setByUser__ = false;

  bool cegqiMinBounds = false;\

  bool cegqiMinBounds__setByUser__ = false;

  bool cegqiModel = true;\

  bool cegqiModel__setByUser__ = false;

  bool cegqiMultiInst = false;\

  bool cegqiMultiInst__setByUser__ = false;

  bool cegqiNestedQE = false;\

  bool cegqiNestedQE__setByUser__ = false;

  bool cegqiNopt = true;\

  bool cegqiNopt__setByUser__ = false;

  bool cegqiRepeatLit = false;\

  bool cegqiRepeatLit__setByUser__ = false;

  bool cegqiRoundUpLowerLia = false;\

  bool cegqiRoundUpLowerLia__setByUser__ = false;

  bool cegqiSat = true;\

  bool cegqiSat__setByUser__ = false;

  bool cegqiUseInfInt = false;\

  bool cegqiUseInfInt__setByUser__ = false;

  bool cegqiUseInfReal = false;\

  bool cegqiUseInfReal__setByUser__ = false;

  bool condVarSplitQuantAgg = false;\

  bool condVarSplitQuantAgg__setByUser__ = false;

  bool condVarSplitQuant = true;\

  bool condVarSplitQuant__setByUser__ = false;

  bool conjectureFilterActiveTerms = true;\

  bool conjectureFilterActiveTerms__setByUser__ = false;

  bool conjectureFilterCanonical = true;\

  bool conjectureFilterCanonical__setByUser__ = false;

  bool conjectureFilterModel = true;\

  bool conjectureFilterModel__setByUser__ = false;

  bool conjectureGen = false;\

  bool conjectureGen__setByUser__ = false;

  int conjectureGenGtEnum = 50;\

  bool conjectureGenGtEnum__setByUser__ = false;

  int conjectureGenMaxDepth = 3;\

  bool conjectureGenMaxDepth__setByUser__ = false;

  int conjectureGenPerRound = 1;\

  bool conjectureGenPerRound__setByUser__ = false;

  bool conjectureUeeIntro = false;\

  bool conjectureUeeIntro__setByUser__ = false;

  bool conjectureNoFilter = false;\

  bool conjectureNoFilter__setByUser__ = false;

  bool debugInst = false;\

  bool debugInst__setByUser__ = false;

  bool debugSygus = false;\

  bool debugSygus__setByUser__ = false;

  bool dtStcInduction = false;\

  bool dtStcInduction__setByUser__ = false;

  bool dtVarExpandQuant = true;\

  bool dtVarExpandQuant__setByUser__ = false;

  bool eMatching = true;\

  bool eMatching__setByUser__ = false;

  bool elimTautQuant = true;\

  bool elimTautQuant__setByUser__ = false;

  bool extRewriteQuant = false;\

  bool extRewriteQuant__setByUser__ = false;

  bool finiteModelFind = false;\

  bool finiteModelFind__setByUser__ = false;

  bool fmfBound = false;\

  bool fmfBound__setByUser__ = false;

  bool fmfBoundInt = false;\

  bool fmfBoundInt__setByUser__ = false;

  bool fmfBoundLazy = false;\

  bool fmfBoundLazy__setByUser__ = false;

  bool fmfFmcSimple = true;\

  bool fmfFmcSimple__setByUser__ = false;

  bool fmfFreshDistConst = false;\

  bool fmfFreshDistConst__setByUser__ = false;

  bool fmfFunWellDefined = false;\

  bool fmfFunWellDefined__setByUser__ = false;

  bool fmfFunWellDefinedRelevant = false;\

  bool fmfFunWellDefinedRelevant__setByUser__ = false;

  bool fmfInstEngine = false;\

  bool fmfInstEngine__setByUser__ = false;

  int fmfTypeCompletionThresh = 1000;\

  bool fmfTypeCompletionThresh__setByUser__ = false;

  bool fullSaturateInterleave = false;\

  bool fullSaturateInterleave__setByUser__ = false;

  bool fullSaturateStratify = false;\

  bool fullSaturateStratify__setByUser__ = false;

  bool fullSaturateSum = false;\

  bool fullSaturateSum__setByUser__ = false;

  bool fullSaturateQuant = false;\

  bool fullSaturateQuant__setByUser__ = false;

  int fullSaturateLimit = -1;\

  bool fullSaturateLimit__setByUser__ = false;

  bool fullSaturateQuantRd = true;\

  bool fullSaturateQuantRd__setByUser__ = false;

  bool globalNegate = false;\

  bool globalNegate__setByUser__ = false;

  bool hoElim = false;\

  bool hoElim__setByUser__ = false;

  bool hoElimStoreAx = true;\

  bool hoElimStoreAx__setByUser__ = false;

  bool hoMatching = true;\

  bool hoMatching__setByUser__ = false;

  bool hoMatchingVarArgPriority = true;\

  bool hoMatchingVarArgPriority__setByUser__ = false;

  bool hoMergeTermDb = true;\

  bool hoMergeTermDb__setByUser__ = false;

  bool incrementTriggers = true;\

  bool incrementTriggers__setByUser__ = false;

  bool instLevelInputOnly = true;\

  bool instLevelInputOnly__setByUser__ = false;

  int instMaxLevel = -1;\

  bool instMaxLevel__setByUser__ = false;

  bool instNoEntail = true;\

  bool instNoEntail__setByUser__ = false;

  int instWhenPhase = 2;\

  bool instWhenPhase__setByUser__ = false;

  bool instWhenStrictInterleave = true;\

  bool instWhenStrictInterleave__setByUser__ = false;

  bool instWhenTcFirst = true;\

  bool instWhenTcFirst__setByUser__ = false;

  InstWhenMode instWhenMode = InstWhenMode::FULL_LAST_CALL;\

  bool instWhenMode__setByUser__ = false;

  bool intWfInduction = false;\

  bool intWfInduction__setByUser__ = false;

  bool iteDtTesterSplitQuant = false;\

  bool iteDtTesterSplitQuant__setByUser__ = false;

  IteLiftQuantMode iteLiftQuant = IteLiftQuantMode::SIMPLE;\

  bool iteLiftQuant__setByUser__ = false;

  LiteralMatchMode literalMatchMode = LiteralMatchMode::USE;\

  bool literalMatchMode__setByUser__ = false;

  bool macrosQuant = false;\

  bool macrosQuant__setByUser__ = false;

  MacrosQuantMode macrosQuantMode = MacrosQuantMode::GROUND_UF;\

  bool macrosQuantMode__setByUser__ = false;

  bool mbqiInterleave = false;\

  bool mbqiInterleave__setByUser__ = false;

  bool fmfOneInstPerRound = false;\

  bool fmfOneInstPerRound__setByUser__ = false;

  MbqiMode mbqiMode = MbqiMode::FMC;\

  bool mbqiMode__setByUser__ = false;

  bool miniscopeQuant = true;\

  bool miniscopeQuant__setByUser__ = false;

  bool miniscopeQuantFreeVar = true;\

  bool miniscopeQuantFreeVar__setByUser__ = false;

  bool multiTriggerCache = false;\

  bool multiTriggerCache__setByUser__ = false;

  bool multiTriggerLinear = true;\

  bool multiTriggerLinear__setByUser__ = false;

  bool multiTriggerPriority = false;\

  bool multiTriggerPriority__setByUser__ = false;

  bool multiTriggerWhenSingle = false;\

  bool multiTriggerWhenSingle__setByUser__ = false;

  bool partialTriggers = false;\

  bool partialTriggers__setByUser__ = false;

  bool poolInst = true;\

  bool poolInst__setByUser__ = false;

  bool preSkolemQuant = false;\

  bool preSkolemQuant__setByUser__ = false;

  bool preSkolemQuantAgg = true;\

  bool preSkolemQuantAgg__setByUser__ = false;

  bool preSkolemQuantNested = true;\

  bool preSkolemQuantNested__setByUser__ = false;

  bool prenexQuantUser = false;\

  bool prenexQuantUser__setByUser__ = false;

  PrenexQuantMode prenexQuant = PrenexQuantMode::SIMPLE;\

  bool prenexQuant__setByUser__ = false;

  bool purifyTriggers = false;\

  bool purifyTriggers__setByUser__ = false;

  bool qcfAllConflict = false;\

  bool qcfAllConflict__setByUser__ = false;

  bool qcfEagerCheckRd = true;\

  bool qcfEagerCheckRd__setByUser__ = false;

  bool qcfEagerTest = true;\

  bool qcfEagerTest__setByUser__ = false;

  bool qcfNestedConflict = false;\

  bool qcfNestedConflict__setByUser__ = false;

  bool qcfSkipRd = false;\

  bool qcfSkipRd__setByUser__ = false;

  bool qcfTConstraint = false;\

  bool qcfTConstraint__setByUser__ = false;

  bool qcfVoExp = false;\

  bool qcfVoExp__setByUser__ = false;

  bool quantAlphaEquiv = true;\

  bool quantAlphaEquiv__setByUser__ = false;

  bool quantConflictFind = true;\

  bool quantConflictFind__setByUser__ = false;

  QcfMode qcfMode = QcfMode::PROP_EQ;\

  bool qcfMode__setByUser__ = false;

  QcfWhenMode qcfWhenMode = QcfWhenMode::DEFAULT;\

  bool qcfWhenMode__setByUser__ = false;

  QuantDSplitMode quantDynamicSplit = QuantDSplitMode::DEFAULT;\

  bool quantDynamicSplit__setByUser__ = false;

  bool quantFunWellDefined = false;\

  bool quantFunWellDefined__setByUser__ = false;

  bool quantInduction = false;\

  bool quantInduction__setByUser__ = false;

  QuantRepMode quantRepMode = QuantRepMode::FIRST;\

  bool quantRepMode__setByUser__ = false;

  bool quantSplit = true;\

  bool quantSplit__setByUser__ = false;

  bool registerQuantBodyTerms = false;\

  bool registerQuantBodyTerms__setByUser__ = false;

  bool relationalTriggers = false;\

  bool relationalTriggers__setByUser__ = false;

  bool relevantTriggers = false;\

  bool relevantTriggers__setByUser__ = false;

  bool strictTriggers = false;\

  bool strictTriggers__setByUser__ = false;

  bool sygus = false;\

  bool sygus__setByUser__ = false;

  unsigned long sygusActiveGenEnumConsts = 5;\

  bool sygusActiveGenEnumConsts__setByUser__ = false;

  SygusActiveGenMode sygusActiveGenMode = SygusActiveGenMode::AUTO;\

  bool sygusActiveGenMode__setByUser__ = false;

  bool sygusAddConstGrammar = false;\

  bool sygusAddConstGrammar__setByUser__ = false;

  bool sygusArgRelevant = false;\

  bool sygusArgRelevant__setByUser__ = false;

  bool sygusInvAutoUnfold = true;\

  bool sygusInvAutoUnfold__setByUser__ = false;

  bool sygusBoolIteReturnConst = true;\

  bool sygusBoolIteReturnConst__setByUser__ = false;

  bool sygusCoreConnective = false;\

  bool sygusCoreConnective__setByUser__ = false;

  bool sygusConstRepairAbort = false;\

  bool sygusConstRepairAbort__setByUser__ = false;

  bool sygusEvalOpt = true;\

  bool sygusEvalOpt__setByUser__ = false;

  bool sygusEvalUnfold = true;\

  bool sygusEvalUnfold__setByUser__ = false;

  bool sygusEvalUnfoldBool = true;\

  bool sygusEvalUnfoldBool__setByUser__ = false;

  unsigned long sygusExprMinerCheckTimeout;\

  bool sygusExprMinerCheckTimeout__setByUser__ = false;

  bool sygusExtRew = true;\

  bool sygusExtRew__setByUser__ = false;

  bool sygusFilterSolRevSubsume = false;\

  bool sygusFilterSolRevSubsume__setByUser__ = false;

  SygusFilterSolMode sygusFilterSolMode = SygusFilterSolMode::NONE;\

  bool sygusFilterSolMode__setByUser__ = false;

  SygusGrammarConsMode sygusGrammarConsMode = SygusGrammarConsMode::SIMPLE;\

  bool sygusGrammarConsMode__setByUser__ = false;

  bool sygusGrammarNorm = false;\

  bool sygusGrammarNorm__setByUser__ = false;

  bool sygusInference = false;\

  bool sygusInference__setByUser__ = false;

  bool sygusInst = false;\

  bool sygusInst__setByUser__ = false;

  SygusInstMode sygusInstMode = SygusInstMode::PRIORITY_INST;\

  bool sygusInstMode__setByUser__ = false;

  SygusInstScope sygusInstScope = SygusInstScope::IN;\

  bool sygusInstScope__setByUser__ = false;

  SygusInstTermSelMode sygusInstTermSel = SygusInstTermSelMode::MIN;\

  bool sygusInstTermSel__setByUser__ = false;

  bool sygusInvTemplWhenSyntax = false;\

  bool sygusInvTemplWhenSyntax__setByUser__ = false;

  SygusInvTemplMode sygusInvTemplMode = SygusInvTemplMode::POST;\

  bool sygusInvTemplMode__setByUser__ = false;

  bool sygusMinGrammar = true;\

  bool sygusMinGrammar__setByUser__ = false;

  bool sygusUnifPbe = true;\

  bool sygusUnifPbe__setByUser__ = false;

  bool sygusPbeMultiFair = false;\

  bool sygusPbeMultiFair__setByUser__ = false;

  int sygusPbeMultiFairDiff = 0;\

  bool sygusPbeMultiFairDiff__setByUser__ = false;

  bool sygusQePreproc = false;\

  bool sygusQePreproc__setByUser__ = false;

  bool sygusQueryGen = false;\

  bool sygusQueryGen__setByUser__ = false;

  bool sygusQueryGenCheck = true;\

  bool sygusQueryGenCheck__setByUser__ = false;

  SygusQueryDumpFilesMode sygusQueryGenDumpFiles = SygusQueryDumpFilesMode::NONE;\

  bool sygusQueryGenDumpFiles__setByUser__ = false;

  unsigned sygusQueryGenThresh = 5;\

  bool sygusQueryGenThresh__setByUser__ = false;

  bool sygusRecFun = true;\

  bool sygusRecFun__setByUser__ = false;

  unsigned sygusRecFunEvalLimit = 1000;\

  bool sygusRecFunEvalLimit__setByUser__ = false;

  bool sygusRepairConst = false;\

  bool sygusRepairConst__setByUser__ = false;

  unsigned long sygusRepairConstTimeout;\

  bool sygusRepairConstTimeout__setByUser__ = false;

  bool sygusRew = false;\

  bool sygusRew__setByUser__ = false;

  bool sygusRewSynth = false;\

  bool sygusRewSynth__setByUser__ = false;

  bool sygusRewSynthAccel = false;\

  bool sygusRewSynthAccel__setByUser__ = false;

  bool sygusRewSynthCheck = false;\

  bool sygusRewSynthCheck__setByUser__ = false;

  bool sygusRewSynthFilterCong = true;\

  bool sygusRewSynthFilterCong__setByUser__ = false;

  bool sygusRewSynthFilterMatch = true;\

  bool sygusRewSynthFilterMatch__setByUser__ = false;

  bool sygusRewSynthFilterNonLinear = false;\

  bool sygusRewSynthFilterNonLinear__setByUser__ = false;

  bool sygusRewSynthFilterOrder = true;\

  bool sygusRewSynthFilterOrder__setByUser__ = false;

  bool sygusRewSynthInput = false;\

  bool sygusRewSynthInput__setByUser__ = false;

  int sygusRewSynthInputNVars = 3;\

  bool sygusRewSynthInputNVars__setByUser__ = false;

  bool sygusRewSynthInputUseBool = false;\

  bool sygusRewSynthInputUseBool__setByUser__ = false;

  bool sygusRewSynthRec = false;\

  bool sygusRewSynthRec__setByUser__ = false;

  bool sygusRewVerify = false;\

  bool sygusRewVerify__setByUser__ = false;

  bool sygusRewVerifyAbort = true;\

  bool sygusRewVerifyAbort__setByUser__ = false;

  bool sygusSampleFpUniform = false;\

  bool sygusSampleFpUniform__setByUser__ = false;

  bool sygusSampleGrammar = true;\

  bool sygusSampleGrammar__setByUser__ = false;

  int sygusSamples = 1000;\

  bool sygusSamples__setByUser__ = false;

  bool cegqiSingleInvAbort = false;\

  bool cegqiSingleInvAbort__setByUser__ = false;

  bool cegqiSingleInvPartial = false;\

  bool cegqiSingleInvPartial__setByUser__ = false;

  int cegqiSingleInvReconstructLimit = 10000;\

  bool cegqiSingleInvReconstructLimit__setByUser__ = false;

  CegqiSingleInvRconsMode cegqiSingleInvReconstruct = CegqiSingleInvRconsMode::ALL_LIMIT;\

  bool cegqiSingleInvReconstruct__setByUser__ = false;

  bool cegqiSingleInvReconstructConst = true;\

  bool cegqiSingleInvReconstructConst__setByUser__ = false;

  CegqiSingleInvMode cegqiSingleInvMode = CegqiSingleInvMode::NONE;\

  bool cegqiSingleInvMode__setByUser__ = false;

  bool sygusStream = false;\

  bool sygusStream__setByUser__ = false;

  bool sygusTemplEmbedGrammar = false;\

  bool sygusTemplEmbedGrammar__setByUser__ = false;

  bool sygusUnifCondIndNoRepeatSol = true;\

  bool sygusUnifCondIndNoRepeatSol__setByUser__ = false;

  SygusUnifPiMode sygusUnifPi = SygusUnifPiMode::NONE;\

  bool sygusUnifPi__setByUser__ = false;

  bool sygusUnifShuffleCond = false;\

  bool sygusUnifShuffleCond__setByUser__ = false;

  bool termDbCd = true;\

  bool termDbCd__setByUser__ = false;

  TermDbMode termDbMode = TermDbMode::ALL;\

  bool termDbMode__setByUser__ = false;

  TriggerActiveSelMode triggerActiveSelMode = TriggerActiveSelMode::ALL;\

  bool triggerActiveSelMode__setByUser__ = false;

  TriggerSelMode triggerSelMode = TriggerSelMode::MIN;\

  bool triggerSelMode__setByUser__ = false;

  UserPatMode userPatternsQuant = UserPatMode::TRUST;\

  bool userPatternsQuant__setByUser__ = false;

  bool varElimQuant = true;\

  bool varElimQuant__setByUser__ = false;

  bool varIneqElimQuant = true;\

  bool varIneqElimQuant__setByUser__ = false;

// clang-format on

};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off

extern struct aggressiveMiniscopeQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local aggressiveMiniscopeQuant;

extern struct cegisSample__option_t

{

  typedef CegisSampleMode type;

  type operator()() const;

} thread_local cegisSample;

extern struct cegqi__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqi;

extern struct cegqiAll__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiAll;

extern struct cegqiBv__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiBv;

extern struct cegqiBvConcInv__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiBvConcInv;

extern struct cegqiBvIneqMode__option_t

{

  typedef CegqiBvIneqMode type;

  type operator()() const;

} thread_local cegqiBvIneqMode;

extern struct cegqiBvInterleaveValue__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiBvInterleaveValue;

extern struct cegqiBvLinearize__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiBvLinearize;

extern struct cegqiBvRmExtract__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiBvRmExtract;

extern struct cegqiBvSolveNl__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiBvSolveNl;

extern struct cegqiFullEffort__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiFullEffort;

extern struct cegqiInnermost__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiInnermost;

extern struct cegqiMidpoint__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiMidpoint;

extern struct cegqiMinBounds__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiMinBounds;

extern struct cegqiModel__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiModel;

extern struct cegqiMultiInst__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiMultiInst;

extern struct cegqiNestedQE__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiNestedQE;

extern struct cegqiNopt__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiNopt;

extern struct cegqiRepeatLit__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiRepeatLit;

extern struct cegqiRoundUpLowerLia__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiRoundUpLowerLia;

extern struct cegqiSat__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiSat;

extern struct cegqiUseInfInt__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiUseInfInt;

extern struct cegqiUseInfReal__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local cegqiUseInfReal;

extern struct condVarSplitQuantAgg__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local condVarSplitQuantAgg;

extern struct condVarSplitQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local condVarSplitQuant;

extern struct conjectureFilterActiveTerms__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local conjectureFilterActiveTerms;

extern struct conjectureFilterCanonical__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local conjectureFilterCanonical;

extern struct conjectureFilterModel__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local conjectureFilterModel;

extern struct conjectureGen__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local conjectureGen;

extern struct conjectureGenGtEnum__option_t

{

  typedef int type;

  type operator()() const;

} thread_local conjectureGenGtEnum;

extern struct conjectureGenMaxDepth__option_t

{

  typedef int type;

  type operator()() const;

} thread_local conjectureGenMaxDepth;

extern struct conjectureGenPerRound__option_t

{

  typedef int type;

  type operator()() const;

} thread_local conjectureGenPerRound;

extern struct conjectureUeeIntro__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local conjectureUeeIntro;

extern struct conjectureNoFilter__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local conjectureNoFilter;

extern struct debugInst__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local debugInst;

extern struct debugSygus__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local debugSygus;

extern struct dtStcInduction__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtStcInduction;

extern struct dtVarExpandQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local dtVarExpandQuant;

extern struct eMatching__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local eMatching;

extern struct elimTautQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local elimTautQuant;

extern struct extRewriteQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local extRewriteQuant;

extern struct finiteModelFind__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local finiteModelFind;

extern struct fmfBound__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfBound;

extern struct fmfBoundInt__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfBoundInt;

extern struct fmfBoundLazy__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfBoundLazy;

extern struct fmfFmcSimple__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfFmcSimple;

extern struct fmfFreshDistConst__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfFreshDistConst;

extern struct fmfFunWellDefined__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfFunWellDefined;

extern struct fmfFunWellDefinedRelevant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfFunWellDefinedRelevant;

extern struct fmfInstEngine__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfInstEngine;

extern struct fmfTypeCompletionThresh__option_t

{

  typedef int type;

  type operator()() const;

} thread_local fmfTypeCompletionThresh;

extern struct fullSaturateInterleave__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fullSaturateInterleave;

extern struct fullSaturateStratify__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fullSaturateStratify;

extern struct fullSaturateSum__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fullSaturateSum;

extern struct fullSaturateQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fullSaturateQuant;

extern struct fullSaturateLimit__option_t

{

  typedef int type;

  type operator()() const;

} thread_local fullSaturateLimit;

extern struct fullSaturateQuantRd__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fullSaturateQuantRd;

extern struct globalNegate__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local globalNegate;

extern struct hoElim__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local hoElim;

extern struct hoElimStoreAx__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local hoElimStoreAx;

extern struct hoMatching__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local hoMatching;

extern struct hoMatchingVarArgPriority__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local hoMatchingVarArgPriority;

extern struct hoMergeTermDb__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local hoMergeTermDb;

extern struct incrementTriggers__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local incrementTriggers;

extern struct instLevelInputOnly__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local instLevelInputOnly;

extern struct instMaxLevel__option_t

{

  typedef int type;

  type operator()() const;

} thread_local instMaxLevel;

extern struct instNoEntail__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local instNoEntail;

extern struct instWhenPhase__option_t

{

  typedef int type;

  type operator()() const;

} thread_local instWhenPhase;

extern struct instWhenStrictInterleave__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local instWhenStrictInterleave;

extern struct instWhenTcFirst__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local instWhenTcFirst;

extern struct instWhenMode__option_t

{

  typedef InstWhenMode type;

  type operator()() const;

} thread_local instWhenMode;

extern struct intWfInduction__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local intWfInduction;

extern struct iteDtTesterSplitQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local iteDtTesterSplitQuant;

extern struct iteLiftQuant__option_t

{

  typedef IteLiftQuantMode type;

  type operator()() const;

} thread_local iteLiftQuant;

extern struct literalMatchMode__option_t

{

  typedef LiteralMatchMode type;

  type operator()() const;

} thread_local literalMatchMode;

extern struct macrosQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local macrosQuant;

extern struct macrosQuantMode__option_t

{

  typedef MacrosQuantMode type;

  type operator()() const;

} thread_local macrosQuantMode;

extern struct mbqiInterleave__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local mbqiInterleave;

extern struct fmfOneInstPerRound__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local fmfOneInstPerRound;

extern struct mbqiMode__option_t

{

  typedef MbqiMode type;

  type operator()() const;

} thread_local mbqiMode;

extern struct miniscopeQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local miniscopeQuant;

extern struct miniscopeQuantFreeVar__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local miniscopeQuantFreeVar;

extern struct multiTriggerCache__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local multiTriggerCache;

extern struct multiTriggerLinear__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local multiTriggerLinear;

extern struct multiTriggerPriority__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local multiTriggerPriority;

extern struct multiTriggerWhenSingle__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local multiTriggerWhenSingle;

extern struct partialTriggers__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local partialTriggers;

extern struct poolInst__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local poolInst;

extern struct preSkolemQuant__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local preSkolemQuant;

extern struct preSkolemQuantAgg__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local preSkolemQuantAgg;

extern struct preSkolemQuantNested__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local preSkolemQuantNested;

extern struct prenexQuantUser__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local prenexQuantUser;

extern struct prenexQuant__option_t

{

  typedef PrenexQuantMode type;

  type operator()() const;

} thread_local prenexQuant;

extern struct purifyTriggers__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local purifyTriggers;

extern struct qcfAllConflict__option_t

{

  typedef bool type;

  type operator()() const;

} thread_local qcfAllConflict;