Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/quantifiers_options.cpp	Lines:	49	1399	3.5 %
Date:	2021-08-01	Branches:	32	1067	3.0 %

/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Option template for option modules.
 *
 * For each <module>_options.toml configuration file, mkoptions.py
 * expands this template and generates a <module>_options.cpp file.
 */
#include "options/quantifiers_options.h"

#include <iostream>

#include "base/check.h"
#include "options/option_exception.h"

// clang-format off
namespace cvc5 {



namespace options {

thread_local struct aggressiveMiniscopeQuant__option_t aggressiveMiniscopeQuant;
thread_local struct cegisSample__option_t cegisSample;
thread_local struct cegqi__option_t cegqi;
thread_local struct cegqiAll__option_t cegqiAll;
thread_local struct cegqiBv__option_t cegqiBv;
thread_local struct cegqiBvConcInv__option_t cegqiBvConcInv;
thread_local struct cegqiBvIneqMode__option_t cegqiBvIneqMode;
thread_local struct cegqiBvInterleaveValue__option_t cegqiBvInterleaveValue;
thread_local struct cegqiBvLinearize__option_t cegqiBvLinearize;
thread_local struct cegqiBvRmExtract__option_t cegqiBvRmExtract;
thread_local struct cegqiBvSolveNl__option_t cegqiBvSolveNl;
thread_local struct cegqiFullEffort__option_t cegqiFullEffort;
thread_local struct cegqiInnermost__option_t cegqiInnermost;
thread_local struct cegqiMidpoint__option_t cegqiMidpoint;
thread_local struct cegqiMinBounds__option_t cegqiMinBounds;
thread_local struct cegqiModel__option_t cegqiModel;
thread_local struct cegqiMultiInst__option_t cegqiMultiInst;
thread_local struct cegqiNestedQE__option_t cegqiNestedQE;
thread_local struct cegqiNopt__option_t cegqiNopt;
thread_local struct cegqiRepeatLit__option_t cegqiRepeatLit;
thread_local struct cegqiRoundUpLowerLia__option_t cegqiRoundUpLowerLia;
thread_local struct cegqiSat__option_t cegqiSat;
thread_local struct cegqiUseInfInt__option_t cegqiUseInfInt;
thread_local struct cegqiUseInfReal__option_t cegqiUseInfReal;
thread_local struct condVarSplitQuantAgg__option_t condVarSplitQuantAgg;
thread_local struct condVarSplitQuant__option_t condVarSplitQuant;
thread_local struct conjectureFilterActiveTerms__option_t conjectureFilterActiveTerms;
thread_local struct conjectureFilterCanonical__option_t conjectureFilterCanonical;
thread_local struct conjectureFilterModel__option_t conjectureFilterModel;
thread_local struct conjectureGen__option_t conjectureGen;
thread_local struct conjectureGenGtEnum__option_t conjectureGenGtEnum;
thread_local struct conjectureGenMaxDepth__option_t conjectureGenMaxDepth;
thread_local struct conjectureGenPerRound__option_t conjectureGenPerRound;
thread_local struct conjectureUeeIntro__option_t conjectureUeeIntro;
thread_local struct conjectureNoFilter__option_t conjectureNoFilter;
thread_local struct dtStcInduction__option_t dtStcInduction;
thread_local struct dtVarExpandQuant__option_t dtVarExpandQuant;
thread_local struct eMatching__option_t eMatching;
thread_local struct elimTautQuant__option_t elimTautQuant;
thread_local struct extRewriteQuant__option_t extRewriteQuant;
thread_local struct finiteModelFind__option_t finiteModelFind;
thread_local struct fmfBound__option_t fmfBound;
thread_local struct fmfBoundInt__option_t fmfBoundInt;
thread_local struct fmfBoundLazy__option_t fmfBoundLazy;
thread_local struct fmfFmcSimple__option_t fmfFmcSimple;
thread_local struct fmfFreshDistConst__option_t fmfFreshDistConst;
thread_local struct fmfFunWellDefined__option_t fmfFunWellDefined;
thread_local struct fmfFunWellDefinedRelevant__option_t fmfFunWellDefinedRelevant;
thread_local struct fmfInstEngine__option_t fmfInstEngine;
thread_local struct fmfTypeCompletionThresh__option_t fmfTypeCompletionThresh;
thread_local struct fullSaturateInterleave__option_t fullSaturateInterleave;
thread_local struct fullSaturateStratify__option_t fullSaturateStratify;
thread_local struct fullSaturateSum__option_t fullSaturateSum;
thread_local struct fullSaturateQuant__option_t fullSaturateQuant;
thread_local struct fullSaturateLimit__option_t fullSaturateLimit;
thread_local struct fullSaturateQuantRd__option_t fullSaturateQuantRd;
thread_local struct globalNegate__option_t globalNegate;
thread_local struct hoElim__option_t hoElim;
thread_local struct hoElimStoreAx__option_t hoElimStoreAx;
thread_local struct hoMatching__option_t hoMatching;
thread_local struct hoMatchingVarArgPriority__option_t hoMatchingVarArgPriority;
thread_local struct hoMergeTermDb__option_t hoMergeTermDb;
thread_local struct incrementTriggers__option_t incrementTriggers;
thread_local struct instLevelInputOnly__option_t instLevelInputOnly;
thread_local struct instMaxLevel__option_t instMaxLevel;
thread_local struct instMaxRounds__option_t instMaxRounds;
thread_local struct instNoEntail__option_t instNoEntail;
thread_local struct instWhenPhase__option_t instWhenPhase;
thread_local struct instWhenStrictInterleave__option_t instWhenStrictInterleave;
thread_local struct instWhenTcFirst__option_t instWhenTcFirst;
thread_local struct instWhenMode__option_t instWhenMode;
thread_local struct intWfInduction__option_t intWfInduction;
thread_local struct iteDtTesterSplitQuant__option_t iteDtTesterSplitQuant;
thread_local struct iteLiftQuant__option_t iteLiftQuant;
thread_local struct literalMatchMode__option_t literalMatchMode;
thread_local struct macrosQuant__option_t macrosQuant;
thread_local struct macrosQuantMode__option_t macrosQuantMode;
thread_local struct mbqiInterleave__option_t mbqiInterleave;
thread_local struct fmfOneInstPerRound__option_t fmfOneInstPerRound;
thread_local struct mbqiMode__option_t mbqiMode;
thread_local struct miniscopeQuant__option_t miniscopeQuant;
thread_local struct miniscopeQuantFreeVar__option_t miniscopeQuantFreeVar;
thread_local struct multiTriggerCache__option_t multiTriggerCache;
thread_local struct multiTriggerLinear__option_t multiTriggerLinear;
thread_local struct multiTriggerPriority__option_t multiTriggerPriority;
thread_local struct multiTriggerWhenSingle__option_t multiTriggerWhenSingle;
thread_local struct partialTriggers__option_t partialTriggers;
thread_local struct poolInst__option_t poolInst;
thread_local struct preSkolemQuant__option_t preSkolemQuant;
thread_local struct preSkolemQuantAgg__option_t preSkolemQuantAgg;
thread_local struct preSkolemQuantNested__option_t preSkolemQuantNested;
thread_local struct prenexQuantUser__option_t prenexQuantUser;
thread_local struct prenexQuant__option_t prenexQuant;
thread_local struct purifyTriggers__option_t purifyTriggers;
thread_local struct qcfAllConflict__option_t qcfAllConflict;
thread_local struct qcfEagerCheckRd__option_t qcfEagerCheckRd;
thread_local struct qcfEagerTest__option_t qcfEagerTest;
thread_local struct qcfNestedConflict__option_t qcfNestedConflict;
thread_local struct qcfSkipRd__option_t qcfSkipRd;
thread_local struct qcfTConstraint__option_t qcfTConstraint;
thread_local struct qcfVoExp__option_t qcfVoExp;
thread_local struct quantAlphaEquiv__option_t quantAlphaEquiv;
thread_local struct quantConflictFind__option_t quantConflictFind;
thread_local struct qcfMode__option_t qcfMode;
thread_local struct qcfWhenMode__option_t qcfWhenMode;
thread_local struct quantDynamicSplit__option_t quantDynamicSplit;
thread_local struct quantFunWellDefined__option_t quantFunWellDefined;
thread_local struct quantInduction__option_t quantInduction;
thread_local struct quantRepMode__option_t quantRepMode;
thread_local struct quantSplit__option_t quantSplit;
thread_local struct registerQuantBodyTerms__option_t registerQuantBodyTerms;
thread_local struct relationalTriggers__option_t relationalTriggers;
thread_local struct relevantTriggers__option_t relevantTriggers;
thread_local struct strictTriggers__option_t strictTriggers;
thread_local struct sygus__option_t sygus;
thread_local struct sygusActiveGenEnumConsts__option_t sygusActiveGenEnumConsts;
thread_local struct sygusActiveGenMode__option_t sygusActiveGenMode;
thread_local struct sygusAddConstGrammar__option_t sygusAddConstGrammar;
thread_local struct sygusArgRelevant__option_t sygusArgRelevant;
thread_local struct sygusInvAutoUnfold__option_t sygusInvAutoUnfold;
thread_local struct sygusBoolIteReturnConst__option_t sygusBoolIteReturnConst;
thread_local struct sygusCoreConnective__option_t sygusCoreConnective;
thread_local struct sygusConstRepairAbort__option_t sygusConstRepairAbort;
thread_local struct sygusEvalOpt__option_t sygusEvalOpt;
thread_local struct sygusEvalUnfold__option_t sygusEvalUnfold;
thread_local struct sygusEvalUnfoldBool__option_t sygusEvalUnfoldBool;
thread_local struct sygusExprMinerCheckTimeout__option_t sygusExprMinerCheckTimeout;
thread_local struct sygusExtRew__option_t sygusExtRew;
thread_local struct sygusFilterSolRevSubsume__option_t sygusFilterSolRevSubsume;
thread_local struct sygusFilterSolMode__option_t sygusFilterSolMode;
thread_local struct sygusGrammarConsMode__option_t sygusGrammarConsMode;
thread_local struct sygusGrammarNorm__option_t sygusGrammarNorm;
thread_local struct sygusInference__option_t sygusInference;
thread_local struct sygusInst__option_t sygusInst;
thread_local struct sygusInstMode__option_t sygusInstMode;
thread_local struct sygusInstScope__option_t sygusInstScope;
thread_local struct sygusInstTermSel__option_t sygusInstTermSel;
thread_local struct sygusInvTemplWhenSyntax__option_t sygusInvTemplWhenSyntax;
thread_local struct sygusInvTemplMode__option_t sygusInvTemplMode;
thread_local struct sygusMinGrammar__option_t sygusMinGrammar;
thread_local struct sygusUnifPbe__option_t sygusUnifPbe;
thread_local struct sygusPbeMultiFair__option_t sygusPbeMultiFair;
thread_local struct sygusPbeMultiFairDiff__option_t sygusPbeMultiFairDiff;
thread_local struct sygusQePreproc__option_t sygusQePreproc;
thread_local struct sygusQueryGen__option_t sygusQueryGen;
thread_local struct sygusQueryGenCheck__option_t sygusQueryGenCheck;
thread_local struct sygusQueryGenDumpFiles__option_t sygusQueryGenDumpFiles;
thread_local struct sygusQueryGenThresh__option_t sygusQueryGenThresh;
thread_local struct sygusRecFun__option_t sygusRecFun;
thread_local struct sygusRecFunEvalLimit__option_t sygusRecFunEvalLimit;
thread_local struct sygusRepairConst__option_t sygusRepairConst;
thread_local struct sygusRepairConstTimeout__option_t sygusRepairConstTimeout;
thread_local struct sygusRew__option_t sygusRew;
thread_local struct sygusRewSynth__option_t sygusRewSynth;
thread_local struct sygusRewSynthAccel__option_t sygusRewSynthAccel;
thread_local struct sygusRewSynthCheck__option_t sygusRewSynthCheck;
thread_local struct sygusRewSynthFilterCong__option_t sygusRewSynthFilterCong;
thread_local struct sygusRewSynthFilterMatch__option_t sygusRewSynthFilterMatch;
thread_local struct sygusRewSynthFilterNonLinear__option_t sygusRewSynthFilterNonLinear;
thread_local struct sygusRewSynthFilterOrder__option_t sygusRewSynthFilterOrder;
thread_local struct sygusRewSynthInput__option_t sygusRewSynthInput;
thread_local struct sygusRewSynthInputNVars__option_t sygusRewSynthInputNVars;
thread_local struct sygusRewSynthInputUseBool__option_t sygusRewSynthInputUseBool;
thread_local struct sygusRewSynthRec__option_t sygusRewSynthRec;
thread_local struct sygusRewVerify__option_t sygusRewVerify;
thread_local struct sygusRewVerifyAbort__option_t sygusRewVerifyAbort;
thread_local struct sygusSampleFpUniform__option_t sygusSampleFpUniform;
thread_local struct sygusSampleGrammar__option_t sygusSampleGrammar;
thread_local struct sygusSamples__option_t sygusSamples;
thread_local struct cegqiSingleInvAbort__option_t cegqiSingleInvAbort;
thread_local struct cegqiSingleInvPartial__option_t cegqiSingleInvPartial;
thread_local struct cegqiSingleInvReconstructLimit__option_t cegqiSingleInvReconstructLimit;
thread_local struct cegqiSingleInvReconstruct__option_t cegqiSingleInvReconstruct;
thread_local struct cegqiSingleInvReconstructConst__option_t cegqiSingleInvReconstructConst;
thread_local struct cegqiSingleInvMode__option_t cegqiSingleInvMode;
thread_local struct sygusStream__option_t sygusStream;
thread_local struct sygusTemplEmbedGrammar__option_t sygusTemplEmbedGrammar;
thread_local struct sygusUnifCondIndNoRepeatSol__option_t sygusUnifCondIndNoRepeatSol;
thread_local struct sygusUnifPi__option_t sygusUnifPi;
thread_local struct sygusUnifShuffleCond__option_t sygusUnifShuffleCond;
thread_local struct sygusVerifyInstMaxRounds__option_t sygusVerifyInstMaxRounds;
thread_local struct termDbCd__option_t termDbCd;
thread_local struct termDbMode__option_t termDbMode;
thread_local struct triggerActiveSelMode__option_t triggerActiveSelMode;
thread_local struct triggerSelMode__option_t triggerSelMode;
thread_local struct userPatternsQuant__option_t userPatternsQuant;
thread_local struct varElimQuant__option_t varElimQuant;
thread_local struct varIneqElimQuant__option_t varIneqElimQuant;


std::ostream& operator<<(std::ostream& os, CegisSampleMode mode)
{
  switch(mode) {
    case CegisSampleMode::TRUST:
      return os << "CegisSampleMode::TRUST";
    case CegisSampleMode::USE:
      return os << "CegisSampleMode::USE";
    case CegisSampleMode::NONE:
      return os << "CegisSampleMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

CegisSampleMode stringToCegisSampleMode(const std::string& optarg)
{
  if (optarg == "trust")
  {
    return CegisSampleMode::TRUST;
  }
  else if (optarg == "use")
  {
    return CegisSampleMode::USE;
  }
  else if (optarg == "none")
  {
    return CegisSampleMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for sampling with counterexample-guided inductive synthesis (CEGIS).\n"
         "Available modes for --cegis-sample are:\n"
         "+ trust\n"
         "  Trust that when a solution for a conjecture is always true under sampling,\n"
         "  then it is indeed a solution. Note this option may print out spurious\n"
         "  solutions for synthesis conjectures.\n"
         "+ use\n"
         "  Use sampling to accelerate CEGIS. This will rule out solutions for a\n"
         "  conjecture when they are not satisfied by a sample point.\n"
         "+ none (default)\n"
         "  Do not use sampling with CEGIS.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --cegis-sample: `") +
                        optarg + "'.  Try --cegis-sample=help.");
}

std::ostream& operator<<(std::ostream& os, CegqiBvIneqMode mode)
{
  switch(mode) {
    case CegqiBvIneqMode::EQ_SLACK:
      return os << "CegqiBvIneqMode::EQ_SLACK";
    case CegqiBvIneqMode::KEEP:
      return os << "CegqiBvIneqMode::KEEP";
    case CegqiBvIneqMode::EQ_BOUNDARY:
      return os << "CegqiBvIneqMode::EQ_BOUNDARY";
    default:
      Unreachable();
  }
  return os;
}

CegqiBvIneqMode stringToCegqiBvIneqMode(const std::string& optarg)
{
  if (optarg == "eq-slack")
  {
    return CegqiBvIneqMode::EQ_SLACK;
  }
  else if (optarg == "keep")
  {
    return CegqiBvIneqMode::KEEP;
  }
  else if (optarg == "eq-boundary")
  {
    return CegqiBvIneqMode::EQ_BOUNDARY;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for handling bit-vector inequalities in counterexample-guided\n"
         "instantiation.\n"
         "Available modes for --cegqi-bv-ineq are:\n"
         "+ eq-slack\n"
         "  Solve for the inequality using the slack value in the model, e.g., t > s\n"
         "  becomes t = s + ( t-s )^M.\n"
         "+ keep\n"
         "  Solve for the inequality directly using side conditions for invertibility.\n"
         "+ eq-boundary (default)\n"
         "  Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --cegqi-bv-ineq: `") +
                        optarg + "'.  Try --cegqi-bv-ineq=help.");
}

std::ostream& operator<<(std::ostream& os, InstWhenMode mode)
{
  switch(mode) {
    case InstWhenMode::FULL:
      return os << "InstWhenMode::FULL";
    case InstWhenMode::FULL_DELAY_LAST_CALL:
      return os << "InstWhenMode::FULL_DELAY_LAST_CALL";
    case InstWhenMode::PRE_FULL:
      return os << "InstWhenMode::PRE_FULL";
    case InstWhenMode::FULL_DELAY:
      return os << "InstWhenMode::FULL_DELAY";
    case InstWhenMode::FULL_LAST_CALL:
      return os << "InstWhenMode::FULL_LAST_CALL";
    case InstWhenMode::LAST_CALL:
      return os << "InstWhenMode::LAST_CALL";
    default:
      Unreachable();
  }
  return os;
}

InstWhenMode stringToInstWhenMode(const std::string& optarg)
{
  if (optarg == "full")
  {
    return InstWhenMode::FULL;
  }
  else if (optarg == "full-delay-last-call")
  {
    return InstWhenMode::FULL_DELAY_LAST_CALL;
  }
  else if (optarg == "pre-full")
  {
    return InstWhenMode::PRE_FULL;
  }
  else if (optarg == "full-delay")
  {
    return InstWhenMode::FULL_DELAY;
  }
  else if (optarg == "full-last-call")
  {
    return InstWhenMode::FULL_LAST_CALL;
  }
  else if (optarg == "last-call")
  {
    return InstWhenMode::LAST_CALL;
  }
  else if (optarg == "help")
  {
    std::cerr << "Instantiation modes.\n"
         "Available modes for --inst-when are:\n"
         "+ full\n"
         "  Run instantiation round at full effort, before theory combination.\n"
         "+ full-delay-last-call\n"
         "  Alternate running instantiation rounds at full effort after all other theories\n"
         "  have finished, and last call.\n"
         "+ pre-full\n"
         "  Run instantiation round before full effort (possibly at standard effort).\n"
         "+ full-delay\n"
         "  Run instantiation round at full effort, before theory combination, after all\n"
         "  other theories have finished.\n"
         "+ full-last-call (default)\n"
         "  Alternate running instantiation rounds at full effort and last call.  In other\n"
         "  words, interleave instantiation and theory combination.\n"
         "+ last-call\n"
         "  Run instantiation at last call effort, after theory combination and and\n"
         "  theories report sat.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --inst-when: `") +
                        optarg + "'.  Try --inst-when=help.");
}

std::ostream& operator<<(std::ostream& os, IteLiftQuantMode mode)
{
  switch(mode) {
    case IteLiftQuantMode::SIMPLE:
      return os << "IteLiftQuantMode::SIMPLE";
    case IteLiftQuantMode::NONE:
      return os << "IteLiftQuantMode::NONE";
    case IteLiftQuantMode::ALL:
      return os << "IteLiftQuantMode::ALL";
    default:
      Unreachable();
  }
  return os;
}

IteLiftQuantMode stringToIteLiftQuantMode(const std::string& optarg)
{
  if (optarg == "simple")
  {
    return IteLiftQuantMode::SIMPLE;
  }
  else if (optarg == "none")
  {
    return IteLiftQuantMode::NONE;
  }
  else if (optarg == "all")
  {
    return IteLiftQuantMode::ALL;
  }
  else if (optarg == "help")
  {
    std::cerr << "ITE lifting modes for quantified formulas.\n"
         "Available modes for --ite-lift-quant are:\n"
         "+ simple (default)\n"
         "  Lift if-then-else in quantified formulas if results in smaller term size.\n"
         "+ none\n"
         "  Do not lift if-then-else in quantified formulas.\n"
         "+ all\n"
         "  Lift if-then-else in quantified formulas.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
                        optarg + "'.  Try --ite-lift-quant=help.");
}

std::ostream& operator<<(std::ostream& os, LiteralMatchMode mode)
{
  switch(mode) {
    case LiteralMatchMode::AGG:
      return os << "LiteralMatchMode::AGG";
    case LiteralMatchMode::USE:
      return os << "LiteralMatchMode::USE";
    case LiteralMatchMode::NONE:
      return os << "LiteralMatchMode::NONE";
    case LiteralMatchMode::AGG_PREDICATE:
      return os << "LiteralMatchMode::AGG_PREDICATE";
    default:
      Unreachable();
  }
  return os;
}

LiteralMatchMode stringToLiteralMatchMode(const std::string& optarg)
{
  if (optarg == "agg")
  {
    return LiteralMatchMode::AGG;
  }
  else if (optarg == "use")
  {
    return LiteralMatchMode::USE;
  }
  else if (optarg == "none")
  {
    return LiteralMatchMode::NONE;
  }
  else if (optarg == "agg-predicate")
  {
    return LiteralMatchMode::AGG_PREDICATE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Literal match modes.\n"
         "Available modes for --literal-matching are:\n"
         "+ agg\n"
         "  Consider the phase requirements aggressively for all triggers.\n"
         "+ use (default)\n"
         "  Consider phase requirements of triggers conservatively. For example, the\n"
         "  trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n"
         "  terms in the equivalence class of true, and likewise Q( x ) will not be\n"
         "  matched terms in the equivalence class of false. Extends to equality.\n"
         "+ none\n"
         "  Do not use literal matching.\n"
         "+ agg-predicate\n"
         "  Consider phase requirements aggressively for predicates. In the above example,\n"
         "  only match P( x ) with terms that are in the equivalence class of false.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --literal-matching: `") +
                        optarg + "'.  Try --literal-matching=help.");
}

std::ostream& operator<<(std::ostream& os, MacrosQuantMode mode)
{
  switch(mode) {
    case MacrosQuantMode::GROUND:
      return os << "MacrosQuantMode::GROUND";
    case MacrosQuantMode::ALL:
      return os << "MacrosQuantMode::ALL";
    case MacrosQuantMode::GROUND_UF:
      return os << "MacrosQuantMode::GROUND_UF";
    default:
      Unreachable();
  }
  return os;
}

MacrosQuantMode stringToMacrosQuantMode(const std::string& optarg)
{
  if (optarg == "ground")
  {
    return MacrosQuantMode::GROUND;
  }
  else if (optarg == "all")
  {
    return MacrosQuantMode::ALL;
  }
  else if (optarg == "ground-uf")
  {
    return MacrosQuantMode::GROUND_UF;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for quantifiers macro expansion.\n"
         "Available modes for --macros-quant-mode are:\n"
         "+ ground\n"
         "  Only infer ground definitions for functions.\n"
         "+ all\n"
         "  Infer definitions for functions, including those containing quantified\n"
         "  formulas.\n"
         "+ ground-uf (default)\n"
         "  Only infer ground definitions for functions that result in triggers for all\n"
         "  free variables.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
                        optarg + "'.  Try --macros-quant-mode=help.");
}

std::ostream& operator<<(std::ostream& os, MbqiMode mode)
{
  switch(mode) {
    case MbqiMode::FMC:
      return os << "MbqiMode::FMC";
    case MbqiMode::TRUST:
      return os << "MbqiMode::TRUST";
    case MbqiMode::NONE:
      return os << "MbqiMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

MbqiMode stringToMbqiMode(const std::string& optarg)
{
  if (optarg == "fmc")
  {
    return MbqiMode::FMC;
  }
  else if (optarg == "trust")
  {
    return MbqiMode::TRUST;
  }
  else if (optarg == "none")
  {
    return MbqiMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Model-based quantifier instantiation modes.\n"
         "Available modes for --mbqi are:\n"
         "+ fmc (default)\n"
         "  Use algorithm from Section 5.4.2 of thesis Finite Model Finding in\n"
         "  Satisfiability Modulo Theories.\n"
         "+ trust\n"
         "  Do not instantiate quantified formulas (incomplete technique).\n"
         "+ none\n"
         "  Disable model-based quantifier instantiation.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --mbqi: `") +
                        optarg + "'.  Try --mbqi=help.");
}

std::ostream& operator<<(std::ostream& os, PrenexQuantMode mode)
{
  switch(mode) {
    case PrenexQuantMode::SIMPLE:
      return os << "PrenexQuantMode::SIMPLE";
    case PrenexQuantMode::NORMAL:
      return os << "PrenexQuantMode::NORMAL";
    case PrenexQuantMode::NONE:
      return os << "PrenexQuantMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

PrenexQuantMode stringToPrenexQuantMode(const std::string& optarg)
{
  if (optarg == "simple")
  {
    return PrenexQuantMode::SIMPLE;
  }
  else if (optarg == "norm")
  {
    return PrenexQuantMode::NORMAL;
  }
  else if (optarg == "none")
  {
    return PrenexQuantMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Prenex quantifiers modes.\n"
         "Available modes for --prenex-quant are:\n"
         "+ simple (default)\n"
         "  Do simple prenexing of same sign quantifiers.\n"
         "+ norm\n"
         "  Prenex to prenex normal form.\n"
         "+ none\n"
         "  Do no prenex nested quantifiers.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --prenex-quant: `") +
                        optarg + "'.  Try --prenex-quant=help.");
}

std::ostream& operator<<(std::ostream& os, QcfMode mode)
{
  switch(mode) {
    case QcfMode::PARTIAL:
      return os << "QcfMode::PARTIAL";
    case QcfMode::PROP_EQ:
      return os << "QcfMode::PROP_EQ";
    case QcfMode::CONFLICT_ONLY:
      return os << "QcfMode::CONFLICT_ONLY";
    default:
      Unreachable();
  }
  return os;
}

QcfMode stringToQcfMode(const std::string& optarg)
{
  if (optarg == "partial")
  {
    return QcfMode::PARTIAL;
  }
  else if (optarg == "prop-eq")
  {
    return QcfMode::PROP_EQ;
  }
  else if (optarg == "conflict")
  {
    return QcfMode::CONFLICT_ONLY;
  }
  else if (optarg == "help")
  {
    std::cerr << "Quantifier conflict find modes.\n"
         "Available modes for --quant-cf-mode are:\n"
         "+ partial\n"
         "  Use QCF for conflicts, propagations and heuristic instantiations.\n"
         "+ prop-eq (default)\n"
         "  Apply QCF algorithm to propagate equalities as well as conflicts.\n"
         "+ conflict\n"
         "  Apply QCF algorithm to find conflicts only.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
                        optarg + "'.  Try --quant-cf-mode=help.");
}

std::ostream& operator<<(std::ostream& os, QcfWhenMode mode)
{
  switch(mode) {
    case QcfWhenMode::STD:
      return os << "QcfWhenMode::STD";
    case QcfWhenMode::STD_H:
      return os << "QcfWhenMode::STD_H";
    case QcfWhenMode::DEFAULT:
      return os << "QcfWhenMode::DEFAULT";
    case QcfWhenMode::LAST_CALL:
      return os << "QcfWhenMode::LAST_CALL";
    default:
      Unreachable();
  }
  return os;
}

QcfWhenMode stringToQcfWhenMode(const std::string& optarg)
{
  if (optarg == "std")
  {
    return QcfWhenMode::STD;
  }
  else if (optarg == "std-h")
  {
    return QcfWhenMode::STD_H;
  }
  else if (optarg == "default")
  {
    return QcfWhenMode::DEFAULT;
  }
  else if (optarg == "last-call")
  {
    return QcfWhenMode::LAST_CALL;
  }
  else if (optarg == "help")
  {
    std::cerr << "Quantifier conflict find modes.\n"
         "Available modes for --quant-cf-when are:\n"
         "+ std\n"
         "  Apply conflict finding at standard effort.\n"
         "+ std-h\n"
         "  Apply conflict finding at standard effort when heuristic says to.\n"
         "+ default\n"
         "  Default, apply conflict finding at full effort.\n"
         "+ last-call\n"
         "  Apply conflict finding at last call, after theory combination and and all\n"
         "  theories report sat.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --quant-cf-when: `") +
                        optarg + "'.  Try --quant-cf-when=help.");
}

std::ostream& operator<<(std::ostream& os, QuantDSplitMode mode)
{
  switch(mode) {
    case QuantDSplitMode::AGG:
      return os << "QuantDSplitMode::AGG";
    case QuantDSplitMode::DEFAULT:
      return os << "QuantDSplitMode::DEFAULT";
    case QuantDSplitMode::NONE:
      return os << "QuantDSplitMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

QuantDSplitMode stringToQuantDSplitMode(const std::string& optarg)
{
  if (optarg == "agg")
  {
    return QuantDSplitMode::AGG;
  }
  else if (optarg == "default")
  {
    return QuantDSplitMode::DEFAULT;
  }
  else if (optarg == "none")
  {
    return QuantDSplitMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for quantifiers splitting.\n"
         "Available modes for --quant-dsplit-mode are:\n"
         "+ agg\n"
         "  Aggressively split quantified formulas.\n"
         "+ default\n"
         "  Split quantified formulas over some finite datatypes when finite model finding\n"
         "  is enabled.\n"
         "+ none\n"
         "  Never split quantified formulas.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
                        optarg + "'.  Try --quant-dsplit-mode=help.");
}

std::ostream& operator<<(std::ostream& os, QuantRepMode mode)
{
  switch(mode) {
    case QuantRepMode::FIRST:
      return os << "QuantRepMode::FIRST";
    case QuantRepMode::DEPTH:
      return os << "QuantRepMode::DEPTH";
    case QuantRepMode::EE:
      return os << "QuantRepMode::EE";
    default:
      Unreachable();
  }
  return os;
}

QuantRepMode stringToQuantRepMode(const std::string& optarg)
{
  if (optarg == "first")
  {
    return QuantRepMode::FIRST;
  }
  else if (optarg == "depth")
  {
    return QuantRepMode::DEPTH;
  }
  else if (optarg == "ee")
  {
    return QuantRepMode::EE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for quantifiers representative selection.\n"
         "Available modes for --quant-rep-mode are:\n"
         "+ first (default)\n"
         "  Choose terms that appear first.\n"
         "+ depth\n"
         "  Choose terms that are of minimal depth.\n"
         "+ ee\n"
         "  Let equality engine choose representatives.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
                        optarg + "'.  Try --quant-rep-mode=help.");
}

std::ostream& operator<<(std::ostream& os, SygusActiveGenMode mode)
{
  switch(mode) {
    case SygusActiveGenMode::ENUM:
      return os << "SygusActiveGenMode::ENUM";
    case SygusActiveGenMode::ENUM_BASIC:
      return os << "SygusActiveGenMode::ENUM_BASIC";
    case SygusActiveGenMode::AUTO:
      return os << "SygusActiveGenMode::AUTO";
    case SygusActiveGenMode::NONE:
      return os << "SygusActiveGenMode::NONE";
    case SygusActiveGenMode::VAR_AGNOSTIC:
      return os << "SygusActiveGenMode::VAR_AGNOSTIC";
    default:
      Unreachable();
  }
  return os;
}

SygusActiveGenMode stringToSygusActiveGenMode(const std::string& optarg)
{
  if (optarg == "enum")
  {
    return SygusActiveGenMode::ENUM;
  }
  else if (optarg == "basic")
  {
    return SygusActiveGenMode::ENUM_BASIC;
  }
  else if (optarg == "auto")
  {
    return SygusActiveGenMode::AUTO;
  }
  else if (optarg == "none")
  {
    return SygusActiveGenMode::NONE;
  }
  else if (optarg == "var-agnostic")
  {
    return SygusActiveGenMode::VAR_AGNOSTIC;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for actively-generated sygus enumerators.\n"
         "Available modes for --sygus-active-gen are:\n"
         "+ enum\n"
         "  Use optimized enumerator for actively-generated sygus enumerators.\n"
         "+ basic\n"
         "  Use basic type enumerator for actively-generated sygus enumerators.\n"
         "+ auto (default)\n"
         "  Internally decide the best policy for each enumerator.\n"
         "+ none\n"
         "  Do not use actively-generated sygus enumerators.\n"
         "+ var-agnostic\n"
         "  Use sygus solver to enumerate terms that are agnostic to variables.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-active-gen: `") +
                        optarg + "'.  Try --sygus-active-gen=help.");
}

std::ostream& operator<<(std::ostream& os, SygusFilterSolMode mode)
{
  switch(mode) {
    case SygusFilterSolMode::STRONG:
      return os << "SygusFilterSolMode::STRONG";
    case SygusFilterSolMode::WEAK:
      return os << "SygusFilterSolMode::WEAK";
    case SygusFilterSolMode::NONE:
      return os << "SygusFilterSolMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

SygusFilterSolMode stringToSygusFilterSolMode(const std::string& optarg)
{
  if (optarg == "strong")
  {
    return SygusFilterSolMode::STRONG;
  }
  else if (optarg == "weak")
  {
    return SygusFilterSolMode::WEAK;
  }
  else if (optarg == "none")
  {
    return SygusFilterSolMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for filtering sygus solutions.\n"
         "Available modes for --sygus-filter-sol are:\n"
         "+ strong\n"
         "  Filter solutions that are logically stronger than others.\n"
         "+ weak\n"
         "  Filter solutions that are logically weaker than others.\n"
         "+ none (default)\n"
         "  Do not filter sygus solutions.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-filter-sol: `") +
                        optarg + "'.  Try --sygus-filter-sol=help.");
}

std::ostream& operator<<(std::ostream& os, SygusGrammarConsMode mode)
{
  switch(mode) {
    case SygusGrammarConsMode::SIMPLE:
      return os << "SygusGrammarConsMode::SIMPLE";
    case SygusGrammarConsMode::ANY_TERM:
      return os << "SygusGrammarConsMode::ANY_TERM";
    case SygusGrammarConsMode::ANY_CONST:
      return os << "SygusGrammarConsMode::ANY_CONST";
    case SygusGrammarConsMode::ANY_TERM_CONCISE:
      return os << "SygusGrammarConsMode::ANY_TERM_CONCISE";
    default:
      Unreachable();
  }
  return os;
}

SygusGrammarConsMode stringToSygusGrammarConsMode(const std::string& optarg)
{
  if (optarg == "simple")
  {
    return SygusGrammarConsMode::SIMPLE;
  }
  else if (optarg == "any-term")
  {
    return SygusGrammarConsMode::ANY_TERM;
  }
  else if (optarg == "any-const")
  {
    return SygusGrammarConsMode::ANY_CONST;
  }
  else if (optarg == "any-term-concise")
  {
    return SygusGrammarConsMode::ANY_TERM_CONCISE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for default SyGuS grammars.\n"
         "Available modes for --sygus-grammar-cons are:\n"
         "+ simple (default)\n"
         "  Use simple grammar construction (no symbolic terms or constants).\n"
         "+ any-term\n"
         "  When applicable, use constructors corresponding to any symbolic term. This\n"
         "  option enables a sum-of-monomials grammar for arithmetic. For all other types,\n"
         "  it enables symbolic constant constructors.\n"
         "+ any-const\n"
         "  Use symoblic constant constructors.\n"
         "+ any-term-concise\n"
         "  When applicable, use constructors corresponding to any symbolic term, favoring\n"
         "  conciseness over generality. This option is equivalent to any-term but enables\n"
         "  a polynomial grammar for arithmetic when not in a combined theory.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-grammar-cons: `") +
                        optarg + "'.  Try --sygus-grammar-cons=help.");
}

std::ostream& operator<<(std::ostream& os, SygusInstMode mode)
{
  switch(mode) {
    case SygusInstMode::PRIORITY_INST:
      return os << "SygusInstMode::PRIORITY_INST";
    case SygusInstMode::INTERLEAVE:
      return os << "SygusInstMode::INTERLEAVE";
    case SygusInstMode::PRIORITY_EVAL:
      return os << "SygusInstMode::PRIORITY_EVAL";
    default:
      Unreachable();
  }
  return os;
}

SygusInstMode stringToSygusInstMode(const std::string& optarg)
{
  if (optarg == "priority-inst")
  {
    return SygusInstMode::PRIORITY_INST;
  }
  else if (optarg == "interleave")
  {
    return SygusInstMode::INTERLEAVE;
  }
  else if (optarg == "priority-eval")
  {
    return SygusInstMode::PRIORITY_EVAL;
  }
  else if (optarg == "help")
  {
    std::cerr << "SyGuS instantiation lemma modes.\n"
         "Available modes for --sygus-inst-mode are:\n"
         "+ priority-inst (default)\n"
         "  add instantiation lemmas first, add evaluation unfolding if instantiation\n"
         "  fails.\n"
         "+ interleave\n"
         "  add instantiation and evaluation unfolding lemmas in the same step.\n"
         "+ priority-eval\n"
         "  add evaluation unfolding lemma first, add instantiation lemma if unfolding\n"
         "  lemmas already added.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-inst-mode: `") +
                        optarg + "'.  Try --sygus-inst-mode=help.");
}

std::ostream& operator<<(std::ostream& os, SygusInstScope mode)
{
  switch(mode) {
    case SygusInstScope::OUT:
      return os << "SygusInstScope::OUT";
    case SygusInstScope::BOTH:
      return os << "SygusInstScope::BOTH";
    case SygusInstScope::IN:
      return os << "SygusInstScope::IN";
    default:
      Unreachable();
  }
  return os;
}

SygusInstScope stringToSygusInstScope(const std::string& optarg)
{
  if (optarg == "out")
  {
    return SygusInstScope::OUT;
  }
  else if (optarg == "both")
  {
    return SygusInstScope::BOTH;
  }
  else if (optarg == "in")
  {
    return SygusInstScope::IN;
  }
  else if (optarg == "help")
  {
    std::cerr << "scope for collecting ground terms for the grammar.\n"
         "Available modes for --sygus-inst-scope are:\n"
         "+ out\n"
         "  use ground terms outside of quantified formulas only.\n"
         "+ both\n"
         "  combines inside and outside.\n"
         "+ in (default)\n"
         "  use ground terms inside given quantified formula only.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-inst-scope: `") +
                        optarg + "'.  Try --sygus-inst-scope=help.");
}

std::ostream& operator<<(std::ostream& os, SygusInstTermSelMode mode)
{
  switch(mode) {
    case SygusInstTermSelMode::BOTH:
      return os << "SygusInstTermSelMode::BOTH";
    case SygusInstTermSelMode::MIN:
      return os << "SygusInstTermSelMode::MIN";
    case SygusInstTermSelMode::MAX:
      return os << "SygusInstTermSelMode::MAX";
    default:
      Unreachable();
  }
  return os;
}

SygusInstTermSelMode stringToSygusInstTermSelMode(const std::string& optarg)
{
  if (optarg == "both")
  {
    return SygusInstTermSelMode::BOTH;
  }
  else if (optarg == "min")
  {
    return SygusInstTermSelMode::MIN;
  }
  else if (optarg == "max")
  {
    return SygusInstTermSelMode::MAX;
  }
  else if (optarg == "help")
  {
    std::cerr << "Ground term selection modes.\n"
         "Available modes for --sygus-inst-term-sel are:\n"
         "+ both\n"
         "  combines minimal and maximal .\n"
         "+ min (default)\n"
         "  collect minimal ground terms only.\n"
         "+ max\n"
         "  collect maximal ground terms only.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-inst-term-sel: `") +
                        optarg + "'.  Try --sygus-inst-term-sel=help.");
}

std::ostream& operator<<(std::ostream& os, SygusInvTemplMode mode)
{
  switch(mode) {
    case SygusInvTemplMode::POST:
      return os << "SygusInvTemplMode::POST";
    case SygusInvTemplMode::PRE:
      return os << "SygusInvTemplMode::PRE";
    case SygusInvTemplMode::NONE:
      return os << "SygusInvTemplMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

SygusInvTemplMode stringToSygusInvTemplMode(const std::string& optarg)
{
  if (optarg == "post")
  {
    return SygusInvTemplMode::POST;
  }
  else if (optarg == "pre")
  {
    return SygusInvTemplMode::PRE;
  }
  else if (optarg == "none")
  {
    return SygusInvTemplMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Template modes for sygus invariant synthesis.\n"
         "Available modes for --sygus-inv-templ are:\n"
         "+ post (default)\n"
         "  Synthesize invariant based on strengthening of postcondition.\n"
         "+ pre\n"
         "  Synthesize invariant based on weakening of precondition.\n"
         "+ none\n"
         "  Synthesize invariant directly.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
                        optarg + "'.  Try --sygus-inv-templ=help.");
}

std::ostream& operator<<(std::ostream& os, SygusQueryDumpFilesMode mode)
{
  switch(mode) {
    case SygusQueryDumpFilesMode::UNSOLVED:
      return os << "SygusQueryDumpFilesMode::UNSOLVED";
    case SygusQueryDumpFilesMode::ALL:
      return os << "SygusQueryDumpFilesMode::ALL";
    case SygusQueryDumpFilesMode::NONE:
      return os << "SygusQueryDumpFilesMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode(const std::string& optarg)
{
  if (optarg == "unsolved")
  {
    return SygusQueryDumpFilesMode::UNSOLVED;
  }
  else if (optarg == "all")
  {
    return SygusQueryDumpFilesMode::ALL;
  }
  else if (optarg == "none")
  {
    return SygusQueryDumpFilesMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Query file options.\n"
         "Available modes for --sygus-query-gen-dump-files are:\n"
         "+ unsolved\n"
         "  Dump query files that the subsolver did not solve.\n"
         "+ all\n"
         "  Dump all query files.\n"
         "+ none (default)\n"
         "  Do not dump query files when using --sygus-query-gen.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-query-gen-dump-files: `") +
                        optarg + "'.  Try --sygus-query-gen-dump-files=help.");
}

std::ostream& operator<<(std::ostream& os, CegqiSingleInvRconsMode mode)
{
  switch(mode) {
    case CegqiSingleInvRconsMode::ALL_LIMIT:
      return os << "CegqiSingleInvRconsMode::ALL_LIMIT";
    case CegqiSingleInvRconsMode::TRY:
      return os << "CegqiSingleInvRconsMode::TRY";
    case CegqiSingleInvRconsMode::NONE:
      return os << "CegqiSingleInvRconsMode::NONE";
    case CegqiSingleInvRconsMode::ALL:
      return os << "CegqiSingleInvRconsMode::ALL";
    default:
      Unreachable();
  }
  return os;
}

CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode(const std::string& optarg)
{
  if (optarg == "all-limit")
  {
    return CegqiSingleInvRconsMode::ALL_LIMIT;
  }
  else if (optarg == "try")
  {
    return CegqiSingleInvRconsMode::TRY;
  }
  else if (optarg == "none")
  {
    return CegqiSingleInvRconsMode::NONE;
  }
  else if (optarg == "all")
  {
    return CegqiSingleInvRconsMode::ALL;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for reconstruction solutions while using single invocation techniques.\n"
         "Available modes for --sygus-si-rcons are:\n"
         "+ all-limit (default)\n"
         "  Try to reconstruct solutions in the original grammar, but termintate if a\n"
         "  maximum number of rounds for reconstruction is exceeded.\n"
         "+ try\n"
         "  Try to reconstruct solutions in the original grammar when using single\n"
         "  invocation techniques in an incomplete (fail-fast) manner.\n"
         "+ none\n"
         "  Do not try to reconstruct solutions in the original (user-provided) grammar\n"
         "  when using single invocation techniques. In this mode, solutions produced by\n"
         "  cvc5 may violate grammar restrictions.\n"
         "+ all\n"
         "  Try to reconstruct solutions in the original grammar. In this mode, we do not\n"
         "  terminate until a solution is successfully reconstructed.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-si-rcons: `") +
                        optarg + "'.  Try --sygus-si-rcons=help.");
}

std::ostream& operator<<(std::ostream& os, CegqiSingleInvMode mode)
{
  switch(mode) {
    case CegqiSingleInvMode::ALL:
      return os << "CegqiSingleInvMode::ALL";
    case CegqiSingleInvMode::USE:
      return os << "CegqiSingleInvMode::USE";
    case CegqiSingleInvMode::NONE:
      return os << "CegqiSingleInvMode::NONE";
    default:
      Unreachable();
  }
  return os;
}

CegqiSingleInvMode stringToCegqiSingleInvMode(const std::string& optarg)
{
  if (optarg == "all")
  {
    return CegqiSingleInvMode::ALL;
  }
  else if (optarg == "use")
  {
    return CegqiSingleInvMode::USE;
  }
  else if (optarg == "none")
  {
    return CegqiSingleInvMode::NONE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for single invocation techniques.\n"
         "Available modes for --sygus-si are:\n"
         "+ all\n"
         "  Always use single invocation techniques.\n"
         "+ use\n"
         "  Use single invocation techniques only if grammar is not restrictive.\n"
         "+ none (default)\n"
         "  Do not use single invocation techniques.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-si: `") +
                        optarg + "'.  Try --sygus-si=help.");
}

std::ostream& operator<<(std::ostream& os, SygusUnifPiMode mode)
{
  switch(mode) {
    case SygusUnifPiMode::COMPLETE:
      return os << "SygusUnifPiMode::COMPLETE";
    case SygusUnifPiMode::CENUM_IGAIN:
      return os << "SygusUnifPiMode::CENUM_IGAIN";
    case SygusUnifPiMode::NONE:
      return os << "SygusUnifPiMode::NONE";
    case SygusUnifPiMode::CENUM:
      return os << "SygusUnifPiMode::CENUM";
    default:
      Unreachable();
  }
  return os;
}

SygusUnifPiMode stringToSygusUnifPiMode(const std::string& optarg)
{
  if (optarg == "complete")
  {
    return SygusUnifPiMode::COMPLETE;
  }
  else if (optarg == "cond-enum-igain")
  {
    return SygusUnifPiMode::CENUM_IGAIN;
  }
  else if (optarg == "none")
  {
    return SygusUnifPiMode::NONE;
  }
  else if (optarg == "cond-enum")
  {
    return SygusUnifPiMode::CENUM;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for piecewise-independent unification.\n"
         "Available modes for --sygus-unif-pi are:\n"
         "+ complete\n"
         "  Use complete approach for piecewise-independent unification (see Section 3 of\n"
         "  Barbosa et al FMCAD 2019)\n"
         "+ cond-enum-igain\n"
         "  Same as cond-enum, but additionally uses an information gain heuristic when\n"
         "  doing decision tree learning.\n"
         "+ none (default)\n"
         "  Do not use piecewise-independent unification.\n"
         "+ cond-enum\n"
         "  Use unconstrained condition enumeration for piecewise-independent unification\n"
         "  (see Section 4 of Barbosa et al FMCAD 2019).\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-unif-pi: `") +
                        optarg + "'.  Try --sygus-unif-pi=help.");
}

std::ostream& operator<<(std::ostream& os, TermDbMode mode)
{
  switch(mode) {
    case TermDbMode::ALL:
      return os << "TermDbMode::ALL";
    case TermDbMode::RELEVANT:
      return os << "TermDbMode::RELEVANT";
    default:
      Unreachable();
  }
  return os;
}

TermDbMode stringToTermDbMode(const std::string& optarg)
{
  if (optarg == "all")
  {
    return TermDbMode::ALL;
  }
  else if (optarg == "relevant")
  {
    return TermDbMode::RELEVANT;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for terms included in the quantifiers term database.\n"
         "Available modes for --term-db-mode are:\n"
         "+ all (default)\n"
         "  Quantifiers module considers all ground terms.\n"
         "+ relevant\n"
         "  Quantifiers module considers only ground terms connected to current\n"
         "  assertions.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --term-db-mode: `") +
                        optarg + "'.  Try --term-db-mode=help.");
}

std::ostream& operator<<(std::ostream& os, TriggerActiveSelMode mode)
{
  switch(mode) {
    case TriggerActiveSelMode::ALL:
      return os << "TriggerActiveSelMode::ALL";
    case TriggerActiveSelMode::MIN:
      return os << "TriggerActiveSelMode::MIN";
    case TriggerActiveSelMode::MAX:
      return os << "TriggerActiveSelMode::MAX";
    default:
      Unreachable();
  }
  return os;
}

TriggerActiveSelMode stringToTriggerActiveSelMode(const std::string& optarg)
{
  if (optarg == "all")
  {
    return TriggerActiveSelMode::ALL;
  }
  else if (optarg == "min")
  {
    return TriggerActiveSelMode::MIN;
  }
  else if (optarg == "max")
  {
    return TriggerActiveSelMode::MAX;
  }
  else if (optarg == "help")
  {
    std::cerr << "Trigger active selection modes.\n"
         "Available modes for --trigger-active-sel are:\n"
         "+ all (default)\n"
         "  Make all triggers active.\n"
         "+ min\n"
         "  Activate triggers with minimal ground terms.\n"
         "+ max\n"
         "  Activate triggers with maximal ground terms.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --trigger-active-sel: `") +
                        optarg + "'.  Try --trigger-active-sel=help.");
}

std::ostream& operator<<(std::ostream& os, TriggerSelMode mode)
{
  switch(mode) {
    case TriggerSelMode::MIN_SINGLE_ALL:
      return os << "TriggerSelMode::MIN_SINGLE_ALL";
    case TriggerSelMode::MIN:
      return os << "TriggerSelMode::MIN";
    case TriggerSelMode::MIN_SINGLE_MAX:
      return os << "TriggerSelMode::MIN_SINGLE_MAX";
    case TriggerSelMode::MAX:
      return os << "TriggerSelMode::MAX";
    case TriggerSelMode::ALL:
      return os << "TriggerSelMode::ALL";
    default:
      Unreachable();
  }
  return os;
}

TriggerSelMode stringToTriggerSelMode(const std::string& optarg)
{
  if (optarg == "min-s-all")
  {
    return TriggerSelMode::MIN_SINGLE_ALL;
  }
  else if (optarg == "min")
  {
    return TriggerSelMode::MIN;
  }
  else if (optarg == "min-s-max")
  {
    return TriggerSelMode::MIN_SINGLE_MAX;
  }
  else if (optarg == "max")
  {
    return TriggerSelMode::MAX;
  }
  else if (optarg == "all")
  {
    return TriggerSelMode::ALL;
  }
  else if (optarg == "help")
  {
    std::cerr << "Trigger selection modes.\n"
         "Available modes for --trigger-sel are:\n"
         "+ min-s-all\n"
         "  Consider only minimal subterms that meet criteria for single triggers, all\n"
         "  otherwise.\n"
         "+ min (default)\n"
         "  Consider only minimal subterms that meet criteria for triggers.\n"
         "+ min-s-max\n"
         "  Consider only minimal subterms that meet criteria for single triggers, maximal\n"
         "  otherwise.\n"
         "+ max\n"
         "  Consider only maximal subterms that meet criteria for triggers.\n"
         "+ all\n"
         "  Consider all subterms that meet criteria for triggers.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --trigger-sel: `") +
                        optarg + "'.  Try --trigger-sel=help.");
}

std::ostream& operator<<(std::ostream& os, UserPatMode mode)
{
  switch(mode) {
    case UserPatMode::IGNORE:
      return os << "UserPatMode::IGNORE";
    case UserPatMode::TRUST:
      return os << "UserPatMode::TRUST";
    case UserPatMode::RESORT:
      return os << "UserPatMode::RESORT";
    case UserPatMode::INTERLEAVE:
      return os << "UserPatMode::INTERLEAVE";
    case UserPatMode::USE:
      return os << "UserPatMode::USE";
    default:
      Unreachable();
  }
  return os;
}

UserPatMode stringToUserPatMode(const std::string& optarg)
{
  if (optarg == "ignore")
  {
    return UserPatMode::IGNORE;
  }
  else if (optarg == "trust")
  {
    return UserPatMode::TRUST;
  }
  else if (optarg == "resort")
  {
    return UserPatMode::RESORT;
  }
  else if (optarg == "interleave")
  {
    return UserPatMode::INTERLEAVE;
  }
  else if (optarg == "use")
  {
    return UserPatMode::USE;
  }
  else if (optarg == "help")
  {
    std::cerr << "These modes determine how user provided patterns (triggers) are used during\n"
         "E-matching. The modes vary on when instantiation based on user-provided\n"
         "triggers is combined with instantiation based on automatically selected\n"
         "triggers.\n"
         "Available modes for --user-pat are:\n"
         "+ ignore\n"
         "  Ignore user-provided patterns.\n"
         "+ trust (default)\n"
         "  When provided, use only user-provided patterns for a quantified formula.\n"
         "+ resort\n"
         "  Use user-provided patterns only after auto-generated patterns saturate.\n"
         "+ interleave\n"
         "  Alternate between use/resort.\n"
         "+ use\n"
         "  Use both user-provided and auto-generated patterns when patterns are provided\n"
         "  for a quantified formula.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --user-pat: `") +
                        optarg + "'.  Try --user-pat=help.");
}



namespace quantifiers
{
// clang-format off
void setDefaultAggressiveMiniscopeQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.aggressiveMiniscopeQuantWasSetByUser) {
        opts.quantifiers.aggressiveMiniscopeQuant = value;
    }
}
void setDefaultCegisSample(Options& opts, CegisSampleMode value)
{
    if (!opts.quantifiers.cegisSampleWasSetByUser) {
        opts.quantifiers.cegisSample = value;
    }
}
void setDefaultCegqi(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiWasSetByUser) {
        opts.quantifiers.cegqi = value;
    }
}
void setDefaultCegqiAll(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiAllWasSetByUser) {
        opts.quantifiers.cegqiAll = value;
    }
}
void setDefaultCegqiBv(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiBvWasSetByUser) {
        opts.quantifiers.cegqiBv = value;
    }
}
void setDefaultCegqiBvConcInv(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiBvConcInvWasSetByUser) {
        opts.quantifiers.cegqiBvConcInv = value;
    }
}
void setDefaultCegqiBvIneqMode(Options& opts, CegqiBvIneqMode value)
{
    if (!opts.quantifiers.cegqiBvIneqModeWasSetByUser) {
        opts.quantifiers.cegqiBvIneqMode = value;
    }
}
void setDefaultCegqiBvInterleaveValue(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiBvInterleaveValueWasSetByUser) {
        opts.quantifiers.cegqiBvInterleaveValue = value;
    }
}
void setDefaultCegqiBvLinearize(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiBvLinearizeWasSetByUser) {
        opts.quantifiers.cegqiBvLinearize = value;
    }
}
void setDefaultCegqiBvRmExtract(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiBvRmExtractWasSetByUser) {
        opts.quantifiers.cegqiBvRmExtract = value;
    }
}
void setDefaultCegqiBvSolveNl(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiBvSolveNlWasSetByUser) {
        opts.quantifiers.cegqiBvSolveNl = value;
    }
}
void setDefaultCegqiFullEffort(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiFullEffortWasSetByUser) {
        opts.quantifiers.cegqiFullEffort = value;
    }
}
void setDefaultCegqiInnermost(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiInnermostWasSetByUser) {
        opts.quantifiers.cegqiInnermost = value;
    }
}
void setDefaultCegqiMidpoint(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiMidpointWasSetByUser) {
        opts.quantifiers.cegqiMidpoint = value;
    }
}
void setDefaultCegqiMinBounds(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiMinBoundsWasSetByUser) {
        opts.quantifiers.cegqiMinBounds = value;
    }
}
void setDefaultCegqiModel(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiModelWasSetByUser) {
        opts.quantifiers.cegqiModel = value;
    }
}
void setDefaultCegqiMultiInst(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiMultiInstWasSetByUser) {
        opts.quantifiers.cegqiMultiInst = value;
    }
}
void setDefaultCegqiNestedQE(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiNestedQEWasSetByUser) {
        opts.quantifiers.cegqiNestedQE = value;
    }
}
void setDefaultCegqiNopt(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiNoptWasSetByUser) {
        opts.quantifiers.cegqiNopt = value;
    }
}
void setDefaultCegqiRepeatLit(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiRepeatLitWasSetByUser) {
        opts.quantifiers.cegqiRepeatLit = value;
    }
}
void setDefaultCegqiRoundUpLowerLia(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiRoundUpLowerLiaWasSetByUser) {
        opts.quantifiers.cegqiRoundUpLowerLia = value;
    }
}
void setDefaultCegqiSat(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiSatWasSetByUser) {
        opts.quantifiers.cegqiSat = value;
    }
}
void setDefaultCegqiUseInfInt(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiUseInfIntWasSetByUser) {
        opts.quantifiers.cegqiUseInfInt = value;
    }
}
void setDefaultCegqiUseInfReal(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiUseInfRealWasSetByUser) {
        opts.quantifiers.cegqiUseInfReal = value;
    }
}
void setDefaultCondVarSplitQuantAgg(Options& opts, bool value)
{
    if (!opts.quantifiers.condVarSplitQuantAggWasSetByUser) {
        opts.quantifiers.condVarSplitQuantAgg = value;
    }
}
void setDefaultCondVarSplitQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.condVarSplitQuantWasSetByUser) {
        opts.quantifiers.condVarSplitQuant = value;
    }
}
void setDefaultConjectureFilterActiveTerms(Options& opts, bool value)
{
    if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser) {
        opts.quantifiers.conjectureFilterActiveTerms = value;
    }
}
void setDefaultConjectureFilterCanonical(Options& opts, bool value)
{
    if (!opts.quantifiers.conjectureFilterCanonicalWasSetByUser) {
        opts.quantifiers.conjectureFilterCanonical = value;
    }
}
void setDefaultConjectureFilterModel(Options& opts, bool value)
{
    if (!opts.quantifiers.conjectureFilterModelWasSetByUser) {
        opts.quantifiers.conjectureFilterModel = value;
    }
}
void setDefaultConjectureGen(Options& opts, bool value)
{
    if (!opts.quantifiers.conjectureGenWasSetByUser) {
        opts.quantifiers.conjectureGen = value;
    }
}
void setDefaultConjectureGenGtEnum(Options& opts, int value)
{
    if (!opts.quantifiers.conjectureGenGtEnumWasSetByUser) {
        opts.quantifiers.conjectureGenGtEnum = value;
    }
}
void setDefaultConjectureGenMaxDepth(Options& opts, int value)
{
    if (!opts.quantifiers.conjectureGenMaxDepthWasSetByUser) {
        opts.quantifiers.conjectureGenMaxDepth = value;
    }
}
void setDefaultConjectureGenPerRound(Options& opts, int value)
{
    if (!opts.quantifiers.conjectureGenPerRoundWasSetByUser) {
        opts.quantifiers.conjectureGenPerRound = value;
    }
}
void setDefaultConjectureUeeIntro(Options& opts, bool value)
{
    if (!opts.quantifiers.conjectureUeeIntroWasSetByUser) {
        opts.quantifiers.conjectureUeeIntro = value;
    }
}
void setDefaultConjectureNoFilter(Options& opts, bool value)
{
    if (!opts.quantifiers.conjectureNoFilterWasSetByUser) {
        opts.quantifiers.conjectureNoFilter = value;
    }
}
void setDefaultDtStcInduction(Options& opts, bool value)
{
    if (!opts.quantifiers.dtStcInductionWasSetByUser) {
        opts.quantifiers.dtStcInduction = value;
    }
}
void setDefaultDtVarExpandQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.dtVarExpandQuantWasSetByUser) {
        opts.quantifiers.dtVarExpandQuant = value;
    }
}
void setDefaultEMatching(Options& opts, bool value)
{
    if (!opts.quantifiers.eMatchingWasSetByUser) {
        opts.quantifiers.eMatching = value;
    }
}
void setDefaultElimTautQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.elimTautQuantWasSetByUser) {
        opts.quantifiers.elimTautQuant = value;
    }
}
void setDefaultExtRewriteQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.extRewriteQuantWasSetByUser) {
        opts.quantifiers.extRewriteQuant = value;
    }
}
void setDefaultFiniteModelFind(Options& opts, bool value)
{
    if (!opts.quantifiers.finiteModelFindWasSetByUser) {
        opts.quantifiers.finiteModelFind = value;
    }
}
void setDefaultFmfBound(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfBoundWasSetByUser) {
        opts.quantifiers.fmfBound = value;
    }
}
void setDefaultFmfBoundInt(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfBoundIntWasSetByUser) {
        opts.quantifiers.fmfBoundInt = value;
    }
}
void setDefaultFmfBoundLazy(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfBoundLazyWasSetByUser) {
        opts.quantifiers.fmfBoundLazy = value;
    }
}
void setDefaultFmfFmcSimple(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfFmcSimpleWasSetByUser) {
        opts.quantifiers.fmfFmcSimple = value;
    }
}
void setDefaultFmfFreshDistConst(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfFreshDistConstWasSetByUser) {
        opts.quantifiers.fmfFreshDistConst = value;
    }
}
void setDefaultFmfFunWellDefined(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) {
        opts.quantifiers.fmfFunWellDefined = value;
    }
}
void setDefaultFmfFunWellDefinedRelevant(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfFunWellDefinedRelevantWasSetByUser) {
        opts.quantifiers.fmfFunWellDefinedRelevant = value;
    }
}
void setDefaultFmfInstEngine(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfInstEngineWasSetByUser) {
        opts.quantifiers.fmfInstEngine = value;
    }
}
void setDefaultFmfTypeCompletionThresh(Options& opts, int value)
{
    if (!opts.quantifiers.fmfTypeCompletionThreshWasSetByUser) {
        opts.quantifiers.fmfTypeCompletionThresh = value;
    }
}
void setDefaultFullSaturateInterleave(Options& opts, bool value)
{
    if (!opts.quantifiers.fullSaturateInterleaveWasSetByUser) {
        opts.quantifiers.fullSaturateInterleave = value;
    }
}
void setDefaultFullSaturateStratify(Options& opts, bool value)
{
    if (!opts.quantifiers.fullSaturateStratifyWasSetByUser) {
        opts.quantifiers.fullSaturateStratify = value;
    }
}
void setDefaultFullSaturateSum(Options& opts, bool value)
{
    if (!opts.quantifiers.fullSaturateSumWasSetByUser) {
        opts.quantifiers.fullSaturateSum = value;
    }
}
void setDefaultFullSaturateQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.fullSaturateQuantWasSetByUser) {
        opts.quantifiers.fullSaturateQuant = value;
    }
}
void setDefaultFullSaturateLimit(Options& opts, int value)
{
    if (!opts.quantifiers.fullSaturateLimitWasSetByUser) {
        opts.quantifiers.fullSaturateLimit = value;
    }
}
void setDefaultFullSaturateQuantRd(Options& opts, bool value)
{
    if (!opts.quantifiers.fullSaturateQuantRdWasSetByUser) {
        opts.quantifiers.fullSaturateQuantRd = value;
    }
}
void setDefaultGlobalNegate(Options& opts, bool value)
{
    if (!opts.quantifiers.globalNegateWasSetByUser) {
        opts.quantifiers.globalNegate = value;
    }
}
void setDefaultHoElim(Options& opts, bool value)
{
    if (!opts.quantifiers.hoElimWasSetByUser) {
        opts.quantifiers.hoElim = value;
    }
}
void setDefaultHoElimStoreAx(Options& opts, bool value)
{
    if (!opts.quantifiers.hoElimStoreAxWasSetByUser) {
        opts.quantifiers.hoElimStoreAx = value;
    }
}
void setDefaultHoMatching(Options& opts, bool value)
{
    if (!opts.quantifiers.hoMatchingWasSetByUser) {
        opts.quantifiers.hoMatching = value;
    }
}
void setDefaultHoMatchingVarArgPriority(Options& opts, bool value)
{
    if (!opts.quantifiers.hoMatchingVarArgPriorityWasSetByUser) {
        opts.quantifiers.hoMatchingVarArgPriority = value;
    }
}
void setDefaultHoMergeTermDb(Options& opts, bool value)
{
    if (!opts.quantifiers.hoMergeTermDbWasSetByUser) {
        opts.quantifiers.hoMergeTermDb = value;
    }
}
void setDefaultIncrementTriggers(Options& opts, bool value)
{
    if (!opts.quantifiers.incrementTriggersWasSetByUser) {
        opts.quantifiers.incrementTriggers = value;
    }
}
void setDefaultInstLevelInputOnly(Options& opts, bool value)
{
    if (!opts.quantifiers.instLevelInputOnlyWasSetByUser) {
        opts.quantifiers.instLevelInputOnly = value;
    }
}
void setDefaultInstMaxLevel(Options& opts, int value)
{
    if (!opts.quantifiers.instMaxLevelWasSetByUser) {
        opts.quantifiers.instMaxLevel = value;
    }
}
void setDefaultInstMaxRounds(Options& opts, int value)
{
    if (!opts.quantifiers.instMaxRoundsWasSetByUser) {
        opts.quantifiers.instMaxRounds = value;
    }
}
void setDefaultInstNoEntail(Options& opts, bool value)
{
    if (!opts.quantifiers.instNoEntailWasSetByUser) {
        opts.quantifiers.instNoEntail = value;
    }
}
void setDefaultInstWhenPhase(Options& opts, int value)
{
    if (!opts.quantifiers.instWhenPhaseWasSetByUser) {
        opts.quantifiers.instWhenPhase = value;
    }
}
void setDefaultInstWhenStrictInterleave(Options& opts, bool value)
{
    if (!opts.quantifiers.instWhenStrictInterleaveWasSetByUser) {
        opts.quantifiers.instWhenStrictInterleave = value;
    }
}
void setDefaultInstWhenTcFirst(Options& opts, bool value)
{
    if (!opts.quantifiers.instWhenTcFirstWasSetByUser) {
        opts.quantifiers.instWhenTcFirst = value;
    }
}
void setDefaultInstWhenMode(Options& opts, InstWhenMode value)
{
    if (!opts.quantifiers.instWhenModeWasSetByUser) {
        opts.quantifiers.instWhenMode = value;
    }
}
void setDefaultIntWfInduction(Options& opts, bool value)
{
    if (!opts.quantifiers.intWfInductionWasSetByUser) {
        opts.quantifiers.intWfInduction = value;
    }
}
void setDefaultIteDtTesterSplitQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser) {
        opts.quantifiers.iteDtTesterSplitQuant = value;
    }
}
void setDefaultIteLiftQuant(Options& opts, IteLiftQuantMode value)
{
    if (!opts.quantifiers.iteLiftQuantWasSetByUser) {
        opts.quantifiers.iteLiftQuant = value;
    }
}
void setDefaultLiteralMatchMode(Options& opts, LiteralMatchMode value)
{
    if (!opts.quantifiers.literalMatchModeWasSetByUser) {
        opts.quantifiers.literalMatchMode = value;
    }
}
void setDefaultMacrosQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.macrosQuantWasSetByUser) {
        opts.quantifiers.macrosQuant = value;
    }
}
void setDefaultMacrosQuantMode(Options& opts, MacrosQuantMode value)
{
    if (!opts.quantifiers.macrosQuantModeWasSetByUser) {
        opts.quantifiers.macrosQuantMode = value;
    }
}
void setDefaultMbqiInterleave(Options& opts, bool value)
{
    if (!opts.quantifiers.mbqiInterleaveWasSetByUser) {
        opts.quantifiers.mbqiInterleave = value;
    }
}
void setDefaultFmfOneInstPerRound(Options& opts, bool value)
{
    if (!opts.quantifiers.fmfOneInstPerRoundWasSetByUser) {
        opts.quantifiers.fmfOneInstPerRound = value;
    }
}
void setDefaultMbqiMode(Options& opts, MbqiMode value)
{
    if (!opts.quantifiers.mbqiModeWasSetByUser) {
        opts.quantifiers.mbqiMode = value;
    }
}
void setDefaultMiniscopeQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.miniscopeQuantWasSetByUser) {
        opts.quantifiers.miniscopeQuant = value;
    }
}
void setDefaultMiniscopeQuantFreeVar(Options& opts, bool value)
{
    if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) {
        opts.quantifiers.miniscopeQuantFreeVar = value;
    }
}
void setDefaultMultiTriggerCache(Options& opts, bool value)
{
    if (!opts.quantifiers.multiTriggerCacheWasSetByUser) {
        opts.quantifiers.multiTriggerCache = value;
    }
}
void setDefaultMultiTriggerLinear(Options& opts, bool value)
{
    if (!opts.quantifiers.multiTriggerLinearWasSetByUser) {
        opts.quantifiers.multiTriggerLinear = value;
    }
}
void setDefaultMultiTriggerPriority(Options& opts, bool value)
{
    if (!opts.quantifiers.multiTriggerPriorityWasSetByUser) {
        opts.quantifiers.multiTriggerPriority = value;
    }
}
void setDefaultMultiTriggerWhenSingle(Options& opts, bool value)
{
    if (!opts.quantifiers.multiTriggerWhenSingleWasSetByUser) {
        opts.quantifiers.multiTriggerWhenSingle = value;
    }
}
void setDefaultPartialTriggers(Options& opts, bool value)
{
    if (!opts.quantifiers.partialTriggersWasSetByUser) {
        opts.quantifiers.partialTriggers = value;
    }
}
void setDefaultPoolInst(Options& opts, bool value)
{
    if (!opts.quantifiers.poolInstWasSetByUser) {
        opts.quantifiers.poolInst = value;
    }
}
void setDefaultPreSkolemQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.preSkolemQuantWasSetByUser) {
        opts.quantifiers.preSkolemQuant = value;
    }
}
void setDefaultPreSkolemQuantAgg(Options& opts, bool value)
{
    if (!opts.quantifiers.preSkolemQuantAggWasSetByUser) {
        opts.quantifiers.preSkolemQuantAgg = value;
    }
}
void setDefaultPreSkolemQuantNested(Options& opts, bool value)
{
    if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) {
        opts.quantifiers.preSkolemQuantNested = value;
    }
}
void setDefaultPrenexQuantUser(Options& opts, bool value)
{
    if (!opts.quantifiers.prenexQuantUserWasSetByUser) {
        opts.quantifiers.prenexQuantUser = value;
    }
}
void setDefaultPrenexQuant(Options& opts, PrenexQuantMode value)
{
    if (!opts.quantifiers.prenexQuantWasSetByUser) {
        opts.quantifiers.prenexQuant = value;
    }
}
void setDefaultPurifyTriggers(Options& opts, bool value)
{
    if (!opts.quantifiers.purifyTriggersWasSetByUser) {
        opts.quantifiers.purifyTriggers = value;
    }
}
void setDefaultQcfAllConflict(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfAllConflictWasSetByUser) {
        opts.quantifiers.qcfAllConflict = value;
    }
}
void setDefaultQcfEagerCheckRd(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfEagerCheckRdWasSetByUser) {
        opts.quantifiers.qcfEagerCheckRd = value;
    }
}
void setDefaultQcfEagerTest(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfEagerTestWasSetByUser) {
        opts.quantifiers.qcfEagerTest = value;
    }
}
void setDefaultQcfNestedConflict(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfNestedConflictWasSetByUser) {
        opts.quantifiers.qcfNestedConflict = value;
    }
}
void setDefaultQcfSkipRd(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfSkipRdWasSetByUser) {
        opts.quantifiers.qcfSkipRd = value;
    }
}
void setDefaultQcfTConstraint(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfTConstraintWasSetByUser) {
        opts.quantifiers.qcfTConstraint = value;
    }
}
void setDefaultQcfVoExp(Options& opts, bool value)
{
    if (!opts.quantifiers.qcfVoExpWasSetByUser) {
        opts.quantifiers.qcfVoExp = value;
    }
}
void setDefaultQuantAlphaEquiv(Options& opts, bool value)
{
    if (!opts.quantifiers.quantAlphaEquivWasSetByUser) {
        opts.quantifiers.quantAlphaEquiv = value;
    }
}
void setDefaultQuantConflictFind(Options& opts, bool value)
{
    if (!opts.quantifiers.quantConflictFindWasSetByUser) {
        opts.quantifiers.quantConflictFind = value;
    }
}
void setDefaultQcfMode(Options& opts, QcfMode value)
{
    if (!opts.quantifiers.qcfModeWasSetByUser) {
        opts.quantifiers.qcfMode = value;
    }
}
void setDefaultQcfWhenMode(Options& opts, QcfWhenMode value)
{
    if (!opts.quantifiers.qcfWhenModeWasSetByUser) {
        opts.quantifiers.qcfWhenMode = value;
    }
}
void setDefaultQuantDynamicSplit(Options& opts, QuantDSplitMode value)
{
    if (!opts.quantifiers.quantDynamicSplitWasSetByUser) {
        opts.quantifiers.quantDynamicSplit = value;
    }
}
void setDefaultQuantFunWellDefined(Options& opts, bool value)
{
    if (!opts.quantifiers.quantFunWellDefinedWasSetByUser) {
        opts.quantifiers.quantFunWellDefined = value;
    }
}
void setDefaultQuantInduction(Options& opts, bool value)
{
    if (!opts.quantifiers.quantInductionWasSetByUser) {
        opts.quantifiers.quantInduction = value;
    }
}
void setDefaultQuantRepMode(Options& opts, QuantRepMode value)
{
    if (!opts.quantifiers.quantRepModeWasSetByUser) {
        opts.quantifiers.quantRepMode = value;
    }
}
void setDefaultQuantSplit(Options& opts, bool value)
{
    if (!opts.quantifiers.quantSplitWasSetByUser) {
        opts.quantifiers.quantSplit = value;
    }
}
void setDefaultRegisterQuantBodyTerms(Options& opts, bool value)
{
    if (!opts.quantifiers.registerQuantBodyTermsWasSetByUser) {
        opts.quantifiers.registerQuantBodyTerms = value;
    }
}
void setDefaultRelationalTriggers(Options& opts, bool value)
{
    if (!opts.quantifiers.relationalTriggersWasSetByUser) {
        opts.quantifiers.relationalTriggers = value;
    }
}
void setDefaultRelevantTriggers(Options& opts, bool value)
{
    if (!opts.quantifiers.relevantTriggersWasSetByUser) {
        opts.quantifiers.relevantTriggers = value;
    }
}
void setDefaultStrictTriggers(Options& opts, bool value)
{
    if (!opts.quantifiers.strictTriggersWasSetByUser) {
        opts.quantifiers.strictTriggers = value;
    }
}
void setDefaultSygus(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusWasSetByUser) {
        opts.quantifiers.sygus = value;
    }
}
void setDefaultSygusActiveGenEnumConsts(Options& opts, unsigned long value)
{
    if (!opts.quantifiers.sygusActiveGenEnumConstsWasSetByUser) {
        opts.quantifiers.sygusActiveGenEnumConsts = value;
    }
}
void setDefaultSygusActiveGenMode(Options& opts, SygusActiveGenMode value)
{
    if (!opts.quantifiers.sygusActiveGenModeWasSetByUser) {
        opts.quantifiers.sygusActiveGenMode = value;
    }
}
void setDefaultSygusAddConstGrammar(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusAddConstGrammarWasSetByUser) {
        opts.quantifiers.sygusAddConstGrammar = value;
    }
}
void setDefaultSygusArgRelevant(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusArgRelevantWasSetByUser) {
        opts.quantifiers.sygusArgRelevant = value;
    }
}
void setDefaultSygusInvAutoUnfold(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusInvAutoUnfoldWasSetByUser) {
        opts.quantifiers.sygusInvAutoUnfold = value;
    }
}
void setDefaultSygusBoolIteReturnConst(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusBoolIteReturnConstWasSetByUser) {
        opts.quantifiers.sygusBoolIteReturnConst = value;
    }
}
void setDefaultSygusCoreConnective(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusCoreConnectiveWasSetByUser) {
        opts.quantifiers.sygusCoreConnective = value;
    }
}
void setDefaultSygusConstRepairAbort(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusConstRepairAbortWasSetByUser) {
        opts.quantifiers.sygusConstRepairAbort = value;
    }
}
void setDefaultSygusEvalOpt(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusEvalOptWasSetByUser) {
        opts.quantifiers.sygusEvalOpt = value;
    }
}
void setDefaultSygusEvalUnfold(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusEvalUnfoldWasSetByUser) {
        opts.quantifiers.sygusEvalUnfold = value;
    }
}
void setDefaultSygusEvalUnfoldBool(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusEvalUnfoldBoolWasSetByUser) {
        opts.quantifiers.sygusEvalUnfoldBool = value;
    }
}
void setDefaultSygusExprMinerCheckTimeout(Options& opts, unsigned long value)
{
    if (!opts.quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) {
        opts.quantifiers.sygusExprMinerCheckTimeout = value;
    }
}
void setDefaultSygusExtRew(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusExtRewWasSetByUser) {
        opts.quantifiers.sygusExtRew = value;
    }
}
void setDefaultSygusFilterSolRevSubsume(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusFilterSolRevSubsumeWasSetByUser) {
        opts.quantifiers.sygusFilterSolRevSubsume = value;
    }
}
void setDefaultSygusFilterSolMode(Options& opts, SygusFilterSolMode value)
{
    if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) {
        opts.quantifiers.sygusFilterSolMode = value;
    }
}
void setDefaultSygusGrammarConsMode(Options& opts, SygusGrammarConsMode value)
{
    if (!opts.quantifiers.sygusGrammarConsModeWasSetByUser) {
        opts.quantifiers.sygusGrammarConsMode = value;
    }
}
void setDefaultSygusGrammarNorm(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusGrammarNormWasSetByUser) {
        opts.quantifiers.sygusGrammarNorm = value;
    }
}
void setDefaultSygusInference(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusInferenceWasSetByUser) {
        opts.quantifiers.sygusInference = value;
    }
}
void setDefaultSygusInst(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusInstWasSetByUser) {
        opts.quantifiers.sygusInst = value;
    }
}
void setDefaultSygusInstMode(Options& opts, SygusInstMode value)
{
    if (!opts.quantifiers.sygusInstModeWasSetByUser) {
        opts.quantifiers.sygusInstMode = value;
    }
}
void setDefaultSygusInstScope(Options& opts, SygusInstScope value)
{
    if (!opts.quantifiers.sygusInstScopeWasSetByUser) {
        opts.quantifiers.sygusInstScope = value;
    }
}
void setDefaultSygusInstTermSel(Options& opts, SygusInstTermSelMode value)
{
    if (!opts.quantifiers.sygusInstTermSelWasSetByUser) {
        opts.quantifiers.sygusInstTermSel = value;
    }
}
void setDefaultSygusInvTemplWhenSyntax(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusInvTemplWhenSyntaxWasSetByUser) {
        opts.quantifiers.sygusInvTemplWhenSyntax = value;
    }
}
void setDefaultSygusInvTemplMode(Options& opts, SygusInvTemplMode value)
{
    if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) {
        opts.quantifiers.sygusInvTemplMode = value;
    }
}
void setDefaultSygusMinGrammar(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusMinGrammarWasSetByUser) {
        opts.quantifiers.sygusMinGrammar = value;
    }
}
void setDefaultSygusUnifPbe(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusUnifPbeWasSetByUser) {
        opts.quantifiers.sygusUnifPbe = value;
    }
}
void setDefaultSygusPbeMultiFair(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusPbeMultiFairWasSetByUser) {
        opts.quantifiers.sygusPbeMultiFair = value;
    }
}
void setDefaultSygusPbeMultiFairDiff(Options& opts, int value)
{
    if (!opts.quantifiers.sygusPbeMultiFairDiffWasSetByUser) {
        opts.quantifiers.sygusPbeMultiFairDiff = value;
    }
}
void setDefaultSygusQePreproc(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusQePreprocWasSetByUser) {
        opts.quantifiers.sygusQePreproc = value;
    }
}
void setDefaultSygusQueryGen(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusQueryGenWasSetByUser) {
        opts.quantifiers.sygusQueryGen = value;
    }
}
void setDefaultSygusQueryGenCheck(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusQueryGenCheckWasSetByUser) {
        opts.quantifiers.sygusQueryGenCheck = value;
    }
}
void setDefaultSygusQueryGenDumpFiles(Options& opts, SygusQueryDumpFilesMode value)
{
    if (!opts.quantifiers.sygusQueryGenDumpFilesWasSetByUser) {
        opts.quantifiers.sygusQueryGenDumpFiles = value;
    }
}
void setDefaultSygusQueryGenThresh(Options& opts, unsigned value)
{
    if (!opts.quantifiers.sygusQueryGenThreshWasSetByUser) {
        opts.quantifiers.sygusQueryGenThresh = value;
    }
}
void setDefaultSygusRecFun(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRecFunWasSetByUser) {
        opts.quantifiers.sygusRecFun = value;
    }
}
void setDefaultSygusRecFunEvalLimit(Options& opts, unsigned value)
{
    if (!opts.quantifiers.sygusRecFunEvalLimitWasSetByUser) {
        opts.quantifiers.sygusRecFunEvalLimit = value;
    }
}
void setDefaultSygusRepairConst(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRepairConstWasSetByUser) {
        opts.quantifiers.sygusRepairConst = value;
    }
}
void setDefaultSygusRepairConstTimeout(Options& opts, unsigned long value)
{
    if (!opts.quantifiers.sygusRepairConstTimeoutWasSetByUser) {
        opts.quantifiers.sygusRepairConstTimeout = value;
    }
}
void setDefaultSygusRew(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewWasSetByUser) {
        opts.quantifiers.sygusRew = value;
    }
}
void setDefaultSygusRewSynth(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthWasSetByUser) {
        opts.quantifiers.sygusRewSynth = value;
    }
}
void setDefaultSygusRewSynthAccel(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthAccelWasSetByUser) {
        opts.quantifiers.sygusRewSynthAccel = value;
    }
}
void setDefaultSygusRewSynthCheck(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthCheckWasSetByUser) {
        opts.quantifiers.sygusRewSynthCheck = value;
    }
}
void setDefaultSygusRewSynthFilterCong(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthFilterCongWasSetByUser) {
        opts.quantifiers.sygusRewSynthFilterCong = value;
    }
}
void setDefaultSygusRewSynthFilterMatch(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthFilterMatchWasSetByUser) {
        opts.quantifiers.sygusRewSynthFilterMatch = value;
    }
}
void setDefaultSygusRewSynthFilterNonLinear(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthFilterNonLinearWasSetByUser) {
        opts.quantifiers.sygusRewSynthFilterNonLinear = value;
    }
}
void setDefaultSygusRewSynthFilterOrder(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthFilterOrderWasSetByUser) {
        opts.quantifiers.sygusRewSynthFilterOrder = value;
    }
}
void setDefaultSygusRewSynthInput(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthInputWasSetByUser) {
        opts.quantifiers.sygusRewSynthInput = value;
    }
}
void setDefaultSygusRewSynthInputNVars(Options& opts, int value)
{
    if (!opts.quantifiers.sygusRewSynthInputNVarsWasSetByUser) {
        opts.quantifiers.sygusRewSynthInputNVars = value;
    }
}
void setDefaultSygusRewSynthInputUseBool(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthInputUseBoolWasSetByUser) {
        opts.quantifiers.sygusRewSynthInputUseBool = value;
    }
}
void setDefaultSygusRewSynthRec(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewSynthRecWasSetByUser) {
        opts.quantifiers.sygusRewSynthRec = value;
    }
}
void setDefaultSygusRewVerify(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewVerifyWasSetByUser) {
        opts.quantifiers.sygusRewVerify = value;
    }
}
void setDefaultSygusRewVerifyAbort(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusRewVerifyAbortWasSetByUser) {
        opts.quantifiers.sygusRewVerifyAbort = value;
    }
}
void setDefaultSygusSampleFpUniform(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusSampleFpUniformWasSetByUser) {
        opts.quantifiers.sygusSampleFpUniform = value;
    }
}
void setDefaultSygusSampleGrammar(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusSampleGrammarWasSetByUser) {
        opts.quantifiers.sygusSampleGrammar = value;
    }
}
void setDefaultSygusSamples(Options& opts, int value)
{
    if (!opts.quantifiers.sygusSamplesWasSetByUser) {
        opts.quantifiers.sygusSamples = value;
    }
}
void setDefaultCegqiSingleInvAbort(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiSingleInvAbortWasSetByUser) {
        opts.quantifiers.cegqiSingleInvAbort = value;
    }
}
void setDefaultCegqiSingleInvPartial(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiSingleInvPartialWasSetByUser) {
        opts.quantifiers.cegqiSingleInvPartial = value;
    }
}
void setDefaultCegqiSingleInvReconstructLimit(Options& opts, int value)
{
    if (!opts.quantifiers.cegqiSingleInvReconstructLimitWasSetByUser) {
        opts.quantifiers.cegqiSingleInvReconstructLimit = value;
    }
}
void setDefaultCegqiSingleInvReconstruct(Options& opts, CegqiSingleInvRconsMode value)
{
    if (!opts.quantifiers.cegqiSingleInvReconstructWasSetByUser) {
        opts.quantifiers.cegqiSingleInvReconstruct = value;
    }
}
void setDefaultCegqiSingleInvReconstructConst(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiSingleInvReconstructConstWasSetByUser) {
        opts.quantifiers.cegqiSingleInvReconstructConst = value;
    }
}
void setDefaultCegqiSingleInvMode(Options& opts, CegqiSingleInvMode value)
{
    if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) {
        opts.quantifiers.cegqiSingleInvMode = value;
    }
}
void setDefaultSygusStream(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusStreamWasSetByUser) {
        opts.quantifiers.sygusStream = value;
    }
}
void setDefaultSygusTemplEmbedGrammar(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusTemplEmbedGrammarWasSetByUser) {
        opts.quantifiers.sygusTemplEmbedGrammar = value;
    }
}
void setDefaultSygusUnifCondIndNoRepeatSol(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusUnifCondIndNoRepeatSolWasSetByUser) {
        opts.quantifiers.sygusUnifCondIndNoRepeatSol = value;
    }
}
void setDefaultSygusUnifPi(Options& opts, SygusUnifPiMode value)
{
    if (!opts.quantifiers.sygusUnifPiWasSetByUser) {
        opts.quantifiers.sygusUnifPi = value;
    }
}
void setDefaultSygusUnifShuffleCond(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusUnifShuffleCondWasSetByUser) {
        opts.quantifiers.sygusUnifShuffleCond = value;
    }
}
void setDefaultSygusVerifyInstMaxRounds(Options& opts, int value)
{
    if (!opts.quantifiers.sygusVerifyInstMaxRoundsWasSetByUser) {
        opts.quantifiers.sygusVerifyInstMaxRounds = value;
    }
}
void setDefaultTermDbCd(Options& opts, bool value)
{
    if (!opts.quantifiers.termDbCdWasSetByUser) {
        opts.quantifiers.termDbCd = value;
    }
}
void setDefaultTermDbMode(Options& opts, TermDbMode value)
{
    if (!opts.quantifiers.termDbModeWasSetByUser) {
        opts.quantifiers.termDbMode = value;
    }
}
void setDefaultTriggerActiveSelMode(Options& opts, TriggerActiveSelMode value)
{
    if (!opts.quantifiers.triggerActiveSelModeWasSetByUser) {
        opts.quantifiers.triggerActiveSelMode = value;
    }
}
void setDefaultTriggerSelMode(Options& opts, TriggerSelMode value)
{
    if (!opts.quantifiers.triggerSelModeWasSetByUser) {
        opts.quantifiers.triggerSelMode = value;
    }
}
void setDefaultUserPatternsQuant(Options& opts, UserPatMode value)
{
    if (!opts.quantifiers.userPatternsQuantWasSetByUser) {
        opts.quantifiers.userPatternsQuant = value;
    }
}
void setDefaultVarElimQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.varElimQuantWasSetByUser) {
        opts.quantifiers.varElimQuant = value;
    }
}
void setDefaultVarIneqElimQuant(Options& opts, bool value)
{
    if (!opts.quantifiers.varIneqElimQuantWasSetByUser) {
        opts.quantifiers.varIneqElimQuant = value;
    }
}
// clang-format on
}

}  // namespace options
}  // namespace cvc5
// clang-format on

Generated by: GCOVR (Version 3.2)