Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/quantifiers_options.cpp	Lines:	40	989	4.0 %
Date:	2021-09-16	Branches:	40	1064	3.8 %

/******************************************************************************
 * 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"

namespace cvc5::options {

// clang-format off
std::ostream& operator<<(std::ostream& os, CegisSampleMode mode)
{
  switch(mode)
  {
    case CegisSampleMode::TRUST: return os << "CegisSampleMode::TRUST";
    case CegisSampleMode::NONE: return os << "CegisSampleMode::NONE";
    case CegisSampleMode::USE: return os << "CegisSampleMode::USE";
    default: Unreachable();
  }
  return os;
}
CegisSampleMode stringToCegisSampleMode(const std::string& optarg)
{
  if (optarg == "trust") return CegisSampleMode::TRUST;
  else if (optarg == "none") return CegisSampleMode::NONE;
  else if (optarg == "use") return CegisSampleMode::USE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for sampling with counterexample-guided inductive synthesis (CEGIS).
Available modes for --cegis-sample are:
+ trust
  Trust that when a solution for a conjecture is always true under sampling,
  then it is indeed a solution. Note this option may print out spurious
  solutions for synthesis conjectures.
+ none (default)
  Do not use sampling with CEGIS.
+ use
  Use sampling to accelerate CEGIS. This will rule out solutions for a
  conjecture when they are not satisfied by a sample point.
)FOOBAR";
    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::KEEP: return os << "CegqiBvIneqMode::KEEP";
    case CegqiBvIneqMode::EQ_SLACK: return os << "CegqiBvIneqMode::EQ_SLACK";
    case CegqiBvIneqMode::EQ_BOUNDARY: return os << "CegqiBvIneqMode::EQ_BOUNDARY";
    default: Unreachable();
  }
  return os;
}
CegqiBvIneqMode stringToCegqiBvIneqMode(const std::string& optarg)
{
  if (optarg == "keep") return CegqiBvIneqMode::KEEP;
  else if (optarg == "eq-slack") return CegqiBvIneqMode::EQ_SLACK;
  else if (optarg == "eq-boundary") return CegqiBvIneqMode::EQ_BOUNDARY;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for handling bit-vector inequalities in counterexample-guided
  instantiation.
Available modes for --cegqi-bv-ineq are:
+ keep
  Solve for the inequality directly using side conditions for invertibility.
+ eq-slack
  Solve for the inequality using the slack value in the model, e.g., t > s
  becomes t = s + ( t-s )^M.
+ eq-boundary (default)
  Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1.
)FOOBAR";
    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_LAST_CALL: return os << "InstWhenMode::FULL_LAST_CALL";
    case InstWhenMode::FULL_DELAY: return os << "InstWhenMode::FULL_DELAY";
    case InstWhenMode::PRE_FULL: return os << "InstWhenMode::PRE_FULL";
    case InstWhenMode::FULL: return os << "InstWhenMode::FULL";
    case InstWhenMode::LAST_CALL: return os << "InstWhenMode::LAST_CALL";
    case InstWhenMode::FULL_DELAY_LAST_CALL: return os << "InstWhenMode::FULL_DELAY_LAST_CALL";
    default: Unreachable();
  }
  return os;
}
InstWhenMode stringToInstWhenMode(const std::string& optarg)
{
  if (optarg == "full-last-call") return InstWhenMode::FULL_LAST_CALL;
  else if (optarg == "full-delay") return InstWhenMode::FULL_DELAY;
  else if (optarg == "pre-full") return InstWhenMode::PRE_FULL;
  else if (optarg == "full") return InstWhenMode::FULL;
  else if (optarg == "last-call") return InstWhenMode::LAST_CALL;
  else if (optarg == "full-delay-last-call") return InstWhenMode::FULL_DELAY_LAST_CALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Instantiation modes.
Available modes for --inst-when are:
+ full-last-call (default)
  Alternate running instantiation rounds at full effort and last call.  In other
  words, interleave instantiation and theory combination.
+ full-delay
  Run instantiation round at full effort, before theory combination, after all
  other theories have finished.
+ pre-full
  Run instantiation round before full effort (possibly at standard effort).
+ full
  Run instantiation round at full effort, before theory combination.
+ last-call
  Run instantiation at last call effort, after theory combination and and
  theories report sat.
+ full-delay-last-call
  Alternate running instantiation rounds at full effort after all other theories
  have finished, and last call.
)FOOBAR";
    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 << R"FOOBAR(
  ITE lifting modes for quantified formulas.
Available modes for --ite-lift-quant are:
+ simple (default)
  Lift if-then-else in quantified formulas if results in smaller term size.
+ none
  Do not lift if-then-else in quantified formulas.
+ all
  Lift if-then-else in quantified formulas.
)FOOBAR";
    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::NONE: return os << "LiteralMatchMode::NONE";
    case LiteralMatchMode::USE: return os << "LiteralMatchMode::USE";
    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 == "none") return LiteralMatchMode::NONE;
  else if (optarg == "use") return LiteralMatchMode::USE;
  else if (optarg == "agg-predicate") return LiteralMatchMode::AGG_PREDICATE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Literal match modes.
Available modes for --literal-matching are:
+ agg
  Consider the phase requirements aggressively for all triggers.
+ none
  Do not use literal matching.
+ use (default)
  Consider phase requirements of triggers conservatively. For example, the
  trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with
  terms in the equivalence class of true, and likewise Q( x ) will not be
  matched terms in the equivalence class of false. Extends to equality.
+ agg-predicate
  Consider phase requirements aggressively for predicates. In the above example,
  only match P( x ) with terms that are in the equivalence class of false.
)FOOBAR";
    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_UF: return os << "MacrosQuantMode::GROUND_UF";
    case MacrosQuantMode::GROUND: return os << "MacrosQuantMode::GROUND";
    case MacrosQuantMode::ALL: return os << "MacrosQuantMode::ALL";
    default: Unreachable();
  }
  return os;
}
MacrosQuantMode stringToMacrosQuantMode(const std::string& optarg)
{
  if (optarg == "ground-uf") return MacrosQuantMode::GROUND_UF;
  else if (optarg == "ground") return MacrosQuantMode::GROUND;
  else if (optarg == "all") return MacrosQuantMode::ALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for quantifiers macro expansion.
Available modes for --macros-quant-mode are:
+ ground-uf (default)
  Only infer ground definitions for functions that result in triggers for all
  free variables.
+ ground
  Only infer ground definitions for functions.
+ all
  Infer definitions for functions, including those containing quantified
  formulas.
)FOOBAR";
    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::TRUST: return os << "MbqiMode::TRUST";
    case MbqiMode::FMC: return os << "MbqiMode::FMC";
    case MbqiMode::NONE: return os << "MbqiMode::NONE";
    default: Unreachable();
  }
  return os;
}
MbqiMode stringToMbqiMode(const std::string& optarg)
{
  if (optarg == "trust") return MbqiMode::TRUST;
  else if (optarg == "fmc") return MbqiMode::FMC;
  else if (optarg == "none") return MbqiMode::NONE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Model-based quantifier instantiation modes.
Available modes for --mbqi are:
+ trust
  Do not instantiate quantified formulas (incomplete technique).
+ fmc (default)
  Use algorithm from Section 5.4.2 of thesis Finite Model Finding in
  Satisfiability Modulo Theories.
+ none
  Disable model-based quantifier instantiation.
)FOOBAR";
    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::NORMAL: return os << "PrenexQuantMode::NORMAL";
    case PrenexQuantMode::SIMPLE: return os << "PrenexQuantMode::SIMPLE";
    case PrenexQuantMode::NONE: return os << "PrenexQuantMode::NONE";
    default: Unreachable();
  }
  return os;
}
PrenexQuantMode stringToPrenexQuantMode(const std::string& optarg)
{
  if (optarg == "norm") return PrenexQuantMode::NORMAL;
  else if (optarg == "simple") return PrenexQuantMode::SIMPLE;
  else if (optarg == "none") return PrenexQuantMode::NONE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Prenex quantifiers modes.
Available modes for --prenex-quant are:
+ norm
  Prenex to prenex normal form.
+ simple (default)
  Do simple prenexing of same sign quantifiers.
+ none
  Do no prenex nested quantifiers.
)FOOBAR";
    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::CONFLICT_ONLY: return os << "QcfMode::CONFLICT_ONLY";
    case QcfMode::PROP_EQ: return os << "QcfMode::PROP_EQ";
    default: Unreachable();
  }
  return os;
}
QcfMode stringToQcfMode(const std::string& optarg)
{
  if (optarg == "partial") return QcfMode::PARTIAL;
  else if (optarg == "conflict") return QcfMode::CONFLICT_ONLY;
  else if (optarg == "prop-eq") return QcfMode::PROP_EQ;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Quantifier conflict find modes.
Available modes for --quant-cf-mode are:
+ partial
  Use QCF for conflicts, propagations and heuristic instantiations.
+ conflict
  Apply QCF algorithm to find conflicts only.
+ prop-eq (default)
  Apply QCF algorithm to propagate equalities as well as conflicts.
)FOOBAR";
    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_H: return os << "QcfWhenMode::STD_H";
    case QcfWhenMode::STD: return os << "QcfWhenMode::STD";
    case QcfWhenMode::LAST_CALL: return os << "QcfWhenMode::LAST_CALL";
    case QcfWhenMode::DEFAULT: return os << "QcfWhenMode::DEFAULT";
    default: Unreachable();
  }
  return os;
}
QcfWhenMode stringToQcfWhenMode(const std::string& optarg)
{
  if (optarg == "std-h") return QcfWhenMode::STD_H;
  else if (optarg == "std") return QcfWhenMode::STD;
  else if (optarg == "last-call") return QcfWhenMode::LAST_CALL;
  else if (optarg == "default") return QcfWhenMode::DEFAULT;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Quantifier conflict find modes.
Available modes for --quant-cf-when are:
+ std-h
  Apply conflict finding at standard effort when heuristic says to.
+ std
  Apply conflict finding at standard effort.
+ last-call
  Apply conflict finding at last call, after theory combination and and all
  theories report sat.
+ default
  Default, apply conflict finding at full effort.
)FOOBAR";
    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::NONE: return os << "QuantDSplitMode::NONE";
    case QuantDSplitMode::DEFAULT: return os << "QuantDSplitMode::DEFAULT";
    default: Unreachable();
  }
  return os;
}
QuantDSplitMode stringToQuantDSplitMode(const std::string& optarg)
{
  if (optarg == "agg") return QuantDSplitMode::AGG;
  else if (optarg == "none") return QuantDSplitMode::NONE;
  else if (optarg == "default") return QuantDSplitMode::DEFAULT;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for quantifiers splitting.
Available modes for --quant-dsplit-mode are:
+ agg
  Aggressively split quantified formulas.
+ none
  Never split quantified formulas.
+ default
  Split quantified formulas over some finite datatypes when finite model finding
  is enabled.
)FOOBAR";
    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::EE: return os << "QuantRepMode::EE";
    case QuantRepMode::FIRST: return os << "QuantRepMode::FIRST";
    case QuantRepMode::DEPTH: return os << "QuantRepMode::DEPTH";
    default: Unreachable();
  }
  return os;
}
QuantRepMode stringToQuantRepMode(const std::string& optarg)
{
  if (optarg == "ee") return QuantRepMode::EE;
  else if (optarg == "first") return QuantRepMode::FIRST;
  else if (optarg == "depth") return QuantRepMode::DEPTH;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for quantifiers representative selection.
Available modes for --quant-rep-mode are:
+ ee
  Let equality engine choose representatives.
+ first (default)
  Choose terms that appear first.
+ depth
  Choose terms that are of minimal depth.
)FOOBAR";
    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::VAR_AGNOSTIC: return os << "SygusActiveGenMode::VAR_AGNOSTIC";
    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::ENUM: return os << "SygusActiveGenMode::ENUM";
    default: Unreachable();
  }
  return os;
}
SygusActiveGenMode stringToSygusActiveGenMode(const std::string& optarg)
{
  if (optarg == "var-agnostic") return SygusActiveGenMode::VAR_AGNOSTIC;
  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 == "enum") return SygusActiveGenMode::ENUM;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for actively-generated sygus enumerators.
Available modes for --sygus-active-gen are:
+ var-agnostic
  Use sygus solver to enumerate terms that are agnostic to variables.
+ basic
  Use basic type enumerator for actively-generated sygus enumerators.
+ auto (default)
  Internally decide the best policy for each enumerator.
+ none
  Do not use actively-generated sygus enumerators.
+ enum
  Use optimized enumerator for actively-generated sygus enumerators.
)FOOBAR";
    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::WEAK: return os << "SygusFilterSolMode::WEAK";
    case SygusFilterSolMode::STRONG: return os << "SygusFilterSolMode::STRONG";
    case SygusFilterSolMode::NONE: return os << "SygusFilterSolMode::NONE";
    default: Unreachable();
  }
  return os;
}
SygusFilterSolMode stringToSygusFilterSolMode(const std::string& optarg)
{
  if (optarg == "weak") return SygusFilterSolMode::WEAK;
  else if (optarg == "strong") return SygusFilterSolMode::STRONG;
  else if (optarg == "none") return SygusFilterSolMode::NONE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for filtering sygus solutions.
Available modes for --sygus-filter-sol are:
+ weak
  Filter solutions that are logically weaker than others.
+ strong
  Filter solutions that are logically stronger than others.
+ none (default)
  Do not filter sygus solutions.
)FOOBAR";
    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::ANY_TERM_CONCISE: return os << "SygusGrammarConsMode::ANY_TERM_CONCISE";
    case SygusGrammarConsMode::ANY_TERM: return os << "SygusGrammarConsMode::ANY_TERM";
    case SygusGrammarConsMode::SIMPLE: return os << "SygusGrammarConsMode::SIMPLE";
    case SygusGrammarConsMode::ANY_CONST: return os << "SygusGrammarConsMode::ANY_CONST";
    default: Unreachable();
  }
  return os;
}
SygusGrammarConsMode stringToSygusGrammarConsMode(const std::string& optarg)
{
  if (optarg == "any-term-concise") return SygusGrammarConsMode::ANY_TERM_CONCISE;
  else if (optarg == "any-term") return SygusGrammarConsMode::ANY_TERM;
  else if (optarg == "simple") return SygusGrammarConsMode::SIMPLE;
  else if (optarg == "any-const") return SygusGrammarConsMode::ANY_CONST;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for default SyGuS grammars.
Available modes for --sygus-grammar-cons are:
+ any-term-concise
  When applicable, use constructors corresponding to any symbolic term, favoring
  conciseness over generality. This option is equivalent to any-term but enables
  a polynomial grammar for arithmetic when not in a combined theory.
+ any-term
  When applicable, use constructors corresponding to any symbolic term. This
  option enables a sum-of-monomials grammar for arithmetic. For all other types,
  it enables symbolic constant constructors.
+ simple (default)
  Use simple grammar construction (no symbolic terms or constants).
+ any-const
  Use symoblic constant constructors.
)FOOBAR";
    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::PRIORITY_EVAL: return os << "SygusInstMode::PRIORITY_EVAL";
    case SygusInstMode::INTERLEAVE: return os << "SygusInstMode::INTERLEAVE";
    default: Unreachable();
  }
  return os;
}
SygusInstMode stringToSygusInstMode(const std::string& optarg)
{
  if (optarg == "priority-inst") return SygusInstMode::PRIORITY_INST;
  else if (optarg == "priority-eval") return SygusInstMode::PRIORITY_EVAL;
  else if (optarg == "interleave") return SygusInstMode::INTERLEAVE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  SyGuS instantiation lemma modes.
Available modes for --sygus-inst-mode are:
+ priority-inst (default)
  add instantiation lemmas first, add evaluation unfolding if instantiation
  fails.
+ priority-eval
  add evaluation unfolding lemma first, add instantiation lemma if unfolding
  lemmas already added.
+ interleave
  add instantiation and evaluation unfolding lemmas in the same step.
)FOOBAR";
    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::IN: return os << "SygusInstScope::IN";
    case SygusInstScope::OUT: return os << "SygusInstScope::OUT";
    case SygusInstScope::BOTH: return os << "SygusInstScope::BOTH";
    default: Unreachable();
  }
  return os;
}
SygusInstScope stringToSygusInstScope(const std::string& optarg)
{
  if (optarg == "in") return SygusInstScope::IN;
  else if (optarg == "out") return SygusInstScope::OUT;
  else if (optarg == "both") return SygusInstScope::BOTH;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  scope for collecting ground terms for the grammar.
Available modes for --sygus-inst-scope are:
+ in (default)
  use ground terms inside given quantified formula only.
+ out
  use ground terms outside of quantified formulas only.
+ both
  combines inside and outside.
)FOOBAR";
    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::MAX: return os << "SygusInstTermSelMode::MAX";
    case SygusInstTermSelMode::BOTH: return os << "SygusInstTermSelMode::BOTH";
    case SygusInstTermSelMode::MIN: return os << "SygusInstTermSelMode::MIN";
    default: Unreachable();
  }
  return os;
}
SygusInstTermSelMode stringToSygusInstTermSelMode(const std::string& optarg)
{
  if (optarg == "max") return SygusInstTermSelMode::MAX;
  else if (optarg == "both") return SygusInstTermSelMode::BOTH;
  else if (optarg == "min") return SygusInstTermSelMode::MIN;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Ground term selection modes.
Available modes for --sygus-inst-term-sel are:
+ max
  collect maximal ground terms only.
+ both
  combines minimal and maximal .
+ min (default)
  collect minimal ground terms only.
)FOOBAR";
    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::NONE: return os << "SygusInvTemplMode::NONE";
    case SygusInvTemplMode::PRE: return os << "SygusInvTemplMode::PRE";
    default: Unreachable();
  }
  return os;
}
SygusInvTemplMode stringToSygusInvTemplMode(const std::string& optarg)
{
  if (optarg == "post") return SygusInvTemplMode::POST;
  else if (optarg == "none") return SygusInvTemplMode::NONE;
  else if (optarg == "pre") return SygusInvTemplMode::PRE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Template modes for sygus invariant synthesis.
Available modes for --sygus-inv-templ are:
+ post (default)
  Synthesize invariant based on strengthening of postcondition.
+ none
  Synthesize invariant directly.
+ pre
  Synthesize invariant based on weakening of precondition.
)FOOBAR";
    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::NONE: return os << "SygusQueryDumpFilesMode::NONE";
    case SygusQueryDumpFilesMode::UNSOLVED: return os << "SygusQueryDumpFilesMode::UNSOLVED";
    case SygusQueryDumpFilesMode::ALL: return os << "SygusQueryDumpFilesMode::ALL";
    default: Unreachable();
  }
  return os;
}
SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode(const std::string& optarg)
{
  if (optarg == "none") return SygusQueryDumpFilesMode::NONE;
  else if (optarg == "unsolved") return SygusQueryDumpFilesMode::UNSOLVED;
  else if (optarg == "all") return SygusQueryDumpFilesMode::ALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Query file options.
Available modes for --sygus-query-gen-dump-files are:
+ none (default)
  Do not dump query files when using --sygus-query-gen.
+ unsolved
  Dump query files that the subsolver did not solve.
+ all
  Dump all query files.
)FOOBAR";
    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, CegqiSingleInvMode mode)
{
  switch(mode)
  {
    case CegqiSingleInvMode::NONE: return os << "CegqiSingleInvMode::NONE";
    case CegqiSingleInvMode::USE: return os << "CegqiSingleInvMode::USE";
    case CegqiSingleInvMode::ALL: return os << "CegqiSingleInvMode::ALL";
    default: Unreachable();
  }
  return os;
}
CegqiSingleInvMode stringToCegqiSingleInvMode(const std::string& optarg)
{
  if (optarg == "none") return CegqiSingleInvMode::NONE;
  else if (optarg == "use") return CegqiSingleInvMode::USE;
  else if (optarg == "all") return CegqiSingleInvMode::ALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for single invocation techniques.
Available modes for --sygus-si are:
+ none (default)
  Do not use single invocation techniques.
+ use
  Use single invocation techniques only if grammar is not restrictive.
+ all
  Always use single invocation techniques.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-si: `") +
                        optarg + "'.  Try --sygus-si=help.");
}
std::ostream& operator<<(std::ostream& os, CegqiSingleInvRconsMode mode)
{
  switch(mode)
  {
    case CegqiSingleInvRconsMode::TRY: return os << "CegqiSingleInvRconsMode::TRY";
    case CegqiSingleInvRconsMode::ALL: return os << "CegqiSingleInvRconsMode::ALL";
    case CegqiSingleInvRconsMode::NONE: return os << "CegqiSingleInvRconsMode::NONE";
    case CegqiSingleInvRconsMode::ALL_LIMIT: return os << "CegqiSingleInvRconsMode::ALL_LIMIT";
    default: Unreachable();
  }
  return os;
}
CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode(const std::string& optarg)
{
  if (optarg == "try") return CegqiSingleInvRconsMode::TRY;
  else if (optarg == "all") return CegqiSingleInvRconsMode::ALL;
  else if (optarg == "none") return CegqiSingleInvRconsMode::NONE;
  else if (optarg == "all-limit") return CegqiSingleInvRconsMode::ALL_LIMIT;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for reconstruction solutions while using single invocation techniques.
Available modes for --sygus-si-rcons are:
+ try
  Try to reconstruct solutions in the original grammar when using single
  invocation techniques in an incomplete (fail-fast) manner.
+ all
  Try to reconstruct solutions in the original grammar. In this mode, we do not
  terminate until a solution is successfully reconstructed.
+ none
  Do not try to reconstruct solutions in the original (user-provided) grammar
  when using single invocation techniques. In this mode, solutions produced by
  cvc5 may violate grammar restrictions.
+ all-limit (default)
  Try to reconstruct solutions in the original grammar, but termintate if a
  maximum number of rounds for reconstruction is exceeded.
)FOOBAR";
    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, SygusUnifPiMode mode)
{
  switch(mode)
  {
    case SygusUnifPiMode::CENUM: return os << "SygusUnifPiMode::CENUM";
    case SygusUnifPiMode::NONE: return os << "SygusUnifPiMode::NONE";
    case SygusUnifPiMode::COMPLETE: return os << "SygusUnifPiMode::COMPLETE";
    case SygusUnifPiMode::CENUM_IGAIN: return os << "SygusUnifPiMode::CENUM_IGAIN";
    default: Unreachable();
  }
  return os;
}
SygusUnifPiMode stringToSygusUnifPiMode(const std::string& optarg)
{
  if (optarg == "cond-enum") return SygusUnifPiMode::CENUM;
  else if (optarg == "none") return SygusUnifPiMode::NONE;
  else if (optarg == "complete") return SygusUnifPiMode::COMPLETE;
  else if (optarg == "cond-enum-igain") return SygusUnifPiMode::CENUM_IGAIN;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for piecewise-independent unification.
Available modes for --sygus-unif-pi are:
+ cond-enum
  Use unconstrained condition enumeration for piecewise-independent unification
  (see Section 4 of Barbosa et al FMCAD 2019).
+ none (default)
  Do not use piecewise-independent unification.
+ complete
  Use complete approach for piecewise-independent unification (see Section 3 of
  Barbosa et al FMCAD 2019)
+ cond-enum-igain
  Same as cond-enum, but additionally uses an information gain heuristic when
  doing decision tree learning.
)FOOBAR";
    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::RELEVANT: return os << "TermDbMode::RELEVANT";
    case TermDbMode::ALL: return os << "TermDbMode::ALL";
    default: Unreachable();
  }
  return os;
}
TermDbMode stringToTermDbMode(const std::string& optarg)
{
  if (optarg == "relevant") return TermDbMode::RELEVANT;
  else if (optarg == "all") return TermDbMode::ALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for terms included in the quantifiers term database.
Available modes for --term-db-mode are:
+ relevant
  Quantifiers module considers only ground terms connected to current
  assertions.
+ all (default)
  Quantifiers module considers all ground terms.
)FOOBAR";
    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::MAX: return os << "TriggerActiveSelMode::MAX";
    case TriggerActiveSelMode::MIN: return os << "TriggerActiveSelMode::MIN";
    case TriggerActiveSelMode::ALL: return os << "TriggerActiveSelMode::ALL";
    default: Unreachable();
  }
  return os;
}
TriggerActiveSelMode stringToTriggerActiveSelMode(const std::string& optarg)
{
  if (optarg == "max") return TriggerActiveSelMode::MAX;
  else if (optarg == "min") return TriggerActiveSelMode::MIN;
  else if (optarg == "all") return TriggerActiveSelMode::ALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Trigger active selection modes.
Available modes for --trigger-active-sel are:
+ max
  Activate triggers with maximal ground terms.
+ min
  Activate triggers with minimal ground terms.
+ all (default)
  Make all triggers active.
)FOOBAR";
    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::MAX: return os << "TriggerSelMode::MAX";
    case TriggerSelMode::MIN_SINGLE_MAX: return os << "TriggerSelMode::MIN_SINGLE_MAX";
    case TriggerSelMode::ALL: return os << "TriggerSelMode::ALL";
    case TriggerSelMode::MIN: return os << "TriggerSelMode::MIN";
    default: Unreachable();
  }
  return os;
}
TriggerSelMode stringToTriggerSelMode(const std::string& optarg)
{
  if (optarg == "min-s-all") return TriggerSelMode::MIN_SINGLE_ALL;
  else if (optarg == "max") return TriggerSelMode::MAX;
  else if (optarg == "min-s-max") return TriggerSelMode::MIN_SINGLE_MAX;
  else if (optarg == "all") return TriggerSelMode::ALL;
  else if (optarg == "min") return TriggerSelMode::MIN;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Trigger selection modes.
Available modes for --trigger-sel are:
+ min-s-all
  Consider only minimal subterms that meet criteria for single triggers, all
  otherwise.
+ max
  Consider only maximal subterms that meet criteria for triggers.
+ min-s-max
  Consider only minimal subterms that meet criteria for single triggers, maximal
  otherwise.
+ all
  Consider all subterms that meet criteria for triggers.
+ min (default)
  Consider only minimal subterms that meet criteria for triggers.
)FOOBAR";
    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::STRICT: return os << "UserPatMode::STRICT";
    case UserPatMode::RESORT: return os << "UserPatMode::RESORT";
    case UserPatMode::TRUST: return os << "UserPatMode::TRUST";
    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 == "strict") return UserPatMode::STRICT;
  else if (optarg == "resort") return UserPatMode::RESORT;
  else if (optarg == "trust") return UserPatMode::TRUST;
  else if (optarg == "interleave") return UserPatMode::INTERLEAVE;
  else if (optarg == "use") return UserPatMode::USE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  These modes determine how user provided patterns (triggers) are used during
  E-matching. The modes vary on when instantiation based on user-provided
  triggers is combined with instantiation based on automatically selected
  triggers.
Available modes for --user-pat are:
+ ignore
  Ignore user-provided patterns.
+ strict
  When provided, use only user-provided patterns for a quantified formula, and
  do not use any other instantiation techniques.
+ resort
  Use user-provided patterns only after auto-generated patterns saturate.
+ trust (default)
  When provided, use only user-provided patterns for a quantified formula.
+ interleave
  Alternate between use/resort.
+ use
  Use both user-provided and auto-generated patterns when patterns are provided
  for a quantified formula.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --user-pat: `") +
                        optarg + "'.  Try --user-pat=help.");
}
// clang-format on

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, int64_t value)
{
    if (!opts.quantifiers.conjectureGenGtEnumWasSetByUser) opts.quantifiers.conjectureGenGtEnum = value;
}
void setDefaultConjectureGenMaxDepth(Options& opts, int64_t value)
{
    if (!opts.quantifiers.conjectureGenMaxDepthWasSetByUser) opts.quantifiers.conjectureGenMaxDepth = value;
}
void setDefaultConjectureGenPerRound(Options& opts, int64_t 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, int64_t 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, int64_t 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, int64_t value)
{
    if (!opts.quantifiers.instMaxLevelWasSetByUser) opts.quantifiers.instMaxLevel = value;
}
void setDefaultInstMaxRounds(Options& opts, int64_t value)
{
    if (!opts.quantifiers.instMaxRoundsWasSetByUser) opts.quantifiers.instMaxRounds = value;
}
void setDefaultInstNoEntail(Options& opts, bool value)
{
    if (!opts.quantifiers.instNoEntailWasSetByUser) opts.quantifiers.instNoEntail = value;
}
void setDefaultInstWhenMode(Options& opts, InstWhenMode value)
{
    if (!opts.quantifiers.instWhenModeWasSetByUser) opts.quantifiers.instWhenMode = value;
}
void setDefaultInstWhenPhase(Options& opts, int64_t 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 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 setDefaultMbqiMode(Options& opts, MbqiMode value)
{
    if (!opts.quantifiers.mbqiModeWasSetByUser) opts.quantifiers.mbqiMode = 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 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 setDefaultPrenexQuant(Options& opts, PrenexQuantMode value)
{
    if (!opts.quantifiers.prenexQuantWasSetByUser) opts.quantifiers.prenexQuant = value;
}
void setDefaultPrenexQuantUser(Options& opts, bool value)
{
    if (!opts.quantifiers.prenexQuantUserWasSetByUser) opts.quantifiers.prenexQuantUser = 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 setDefaultSygus(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusWasSetByUser) opts.quantifiers.sygus = value;
}
void setDefaultSygusActiveGenMode(Options& opts, SygusActiveGenMode value)
{
    if (!opts.quantifiers.sygusActiveGenModeWasSetByUser) opts.quantifiers.sygusActiveGenMode = value;
}
void setDefaultSygusActiveGenEnumConsts(Options& opts, uint64_t value)
{
    if (!opts.quantifiers.sygusActiveGenEnumConstsWasSetByUser) opts.quantifiers.sygusActiveGenEnumConsts = 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, uint64_t value)
{
    if (!opts.quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) opts.quantifiers.sygusExprMinerCheckTimeout = value;
}
void setDefaultSygusExtRew(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusExtRewWasSetByUser) opts.quantifiers.sygusExtRew = value;
}
void setDefaultSygusFilterSolMode(Options& opts, SygusFilterSolMode value)
{
    if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) opts.quantifiers.sygusFilterSolMode = value;
}
void setDefaultSygusFilterSolRevSubsume(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusFilterSolRevSubsumeWasSetByUser) opts.quantifiers.sygusFilterSolRevSubsume = 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 setDefaultSygusInvTemplMode(Options& opts, SygusInvTemplMode value)
{
    if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) opts.quantifiers.sygusInvTemplMode = value;
}
void setDefaultSygusInvTemplWhenSyntax(Options& opts, bool value)
{
    if (!opts.quantifiers.sygusInvTemplWhenSyntaxWasSetByUser) opts.quantifiers.sygusInvTemplWhenSyntax = 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, int64_t 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, uint64_t 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, uint64_t 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, uint64_t 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, int64_t 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, int64_t value)
{
    if (!opts.quantifiers.sygusSamplesWasSetByUser) opts.quantifiers.sygusSamples = value;
}
void setDefaultCegqiSingleInvMode(Options& opts, CegqiSingleInvMode value)
{
    if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) opts.quantifiers.cegqiSingleInvMode = value;
}
void setDefaultCegqiSingleInvAbort(Options& opts, bool value)
{
    if (!opts.quantifiers.cegqiSingleInvAbortWasSetByUser) opts.quantifiers.cegqiSingleInvAbort = value;
}
void setDefaultCegqiSingleInvReconstruct(Options& opts, CegqiSingleInvRconsMode value)
{
    if (!opts.quantifiers.cegqiSingleInvReconstructWasSetByUser) opts.quantifiers.cegqiSingleInvReconstruct = value;
}
void setDefaultCegqiSingleInvReconstructLimit(Options& opts, int64_t value)
{
    if (!opts.quantifiers.cegqiSingleInvReconstructLimitWasSetByUser) opts.quantifiers.cegqiSingleInvReconstructLimit = 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, int64_t 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 cvc5::options

Generated by: GCOVR (Version 3.2)