Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/quantifiers_options.cpp	Lines:	46	447	10.3 %
Date:	2021-11-07	Branches:	44	715	6.2 %

/******************************************************************************
 * 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::USE: return os << "use";
    case CegisSampleMode::NONE: return os << "none";
    case CegisSampleMode::TRUST: return os << "trust";
    default: Unreachable();
  }
  return os;
}
CegisSampleMode stringToCegisSampleMode(const std::string& optarg)
{
  if (optarg == "use") return CegisSampleMode::USE;
  else if (optarg == "none") return CegisSampleMode::NONE;
  else if (optarg == "trust") return CegisSampleMode::TRUST;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for sampling with counterexample-guided inductive synthesis (CEGIS).
Available modes for --cegis-sample are:
+ use
  Use sampling to accelerate CEGIS. This will rule out solutions for a
  conjecture when they are not satisfied by a sample point.
+ none (default)
  Do not use sampling with CEGIS.
+ 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.
)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 << "keep";
    case CegqiBvIneqMode::EQ_BOUNDARY: return os << "eq-boundary";
    case CegqiBvIneqMode::EQ_SLACK: return os << "eq-slack";
    default: Unreachable();
  }
  return os;
}
CegqiBvIneqMode stringToCegqiBvIneqMode(const std::string& optarg)
{
  if (optarg == "keep") return CegqiBvIneqMode::KEEP;
  else if (optarg == "eq-boundary") return CegqiBvIneqMode::EQ_BOUNDARY;
  else if (optarg == "eq-slack") return CegqiBvIneqMode::EQ_SLACK;
  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-boundary (default)
  Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1.
+ eq-slack
  Solve for the inequality using the slack value in the model, e.g., t > s
  becomes t = s + ( t-s )^M.
)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::LAST_CALL: return os << "last-call";
    case InstWhenMode::FULL_LAST_CALL: return os << "full-last-call";
    case InstWhenMode::FULL_DELAY: return os << "full-delay";
    case InstWhenMode::FULL: return os << "full";
    case InstWhenMode::FULL_DELAY_LAST_CALL: return os << "full-delay-last-call";
    default: Unreachable();
  }
  return os;
}
InstWhenMode stringToInstWhenMode(const std::string& optarg)
{
  if (optarg == "last-call") return InstWhenMode::LAST_CALL;
  else if (optarg == "full-last-call") return InstWhenMode::FULL_LAST_CALL;
  else if (optarg == "full-delay") return InstWhenMode::FULL_DELAY;
  else if (optarg == "full") return InstWhenMode::FULL;
  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:
+ last-call
  Run instantiation at last call effort, after theory combination and and
  theories report sat.
+ 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.
+ full
  Run instantiation round at full effort, before theory combination.
+ 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 << "simple";
    case IteLiftQuantMode::ALL: return os << "all";
    case IteLiftQuantMode::NONE: return os << "none";
    default: Unreachable();
  }
  return os;
}
IteLiftQuantMode stringToIteLiftQuantMode(const std::string& optarg)
{
  if (optarg == "simple") return IteLiftQuantMode::SIMPLE;
  else if (optarg == "all") return IteLiftQuantMode::ALL;
  else if (optarg == "none") return IteLiftQuantMode::NONE;
  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.
+ all
  Lift if-then-else in quantified formulas.
+ none
  Do not 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_PREDICATE: return os << "agg-predicate";
    case LiteralMatchMode::USE: return os << "use";
    case LiteralMatchMode::NONE: return os << "none";
    case LiteralMatchMode::AGG: return os << "agg";
    default: Unreachable();
  }
  return os;
}
LiteralMatchMode stringToLiteralMatchMode(const std::string& optarg)
{
  if (optarg == "agg-predicate") return LiteralMatchMode::AGG_PREDICATE;
  else if (optarg == "use") return LiteralMatchMode::USE;
  else if (optarg == "none") return LiteralMatchMode::NONE;
  else if (optarg == "agg") return LiteralMatchMode::AGG;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Literal match modes.
Available modes for --literal-matching are:
+ 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.
+ 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.
+ none
  Do not use literal matching.
+ agg
  Consider the phase requirements aggressively for all triggers.
)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 << "ground-uf";
    case MacrosQuantMode::ALL: return os << "all";
    case MacrosQuantMode::GROUND: return os << "ground";
    default: Unreachable();
  }
  return os;
}
MacrosQuantMode stringToMacrosQuantMode(const std::string& optarg)
{
  if (optarg == "ground-uf") return MacrosQuantMode::GROUND_UF;
  else if (optarg == "all") return MacrosQuantMode::ALL;
  else if (optarg == "ground") return MacrosQuantMode::GROUND;
  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.
+ all
  Infer definitions for functions, including those containing quantified
  formulas.
+ ground
  Only infer ground definitions for functions.
)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::FMC: return os << "fmc";
    case MbqiMode::NONE: return os << "none";
    case MbqiMode::TRUST: return os << "trust";
    default: Unreachable();
  }
  return os;
}
MbqiMode stringToMbqiMode(const std::string& optarg)
{
  if (optarg == "fmc") return MbqiMode::FMC;
  else if (optarg == "none") return MbqiMode::NONE;
  else if (optarg == "trust") return MbqiMode::TRUST;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Model-based quantifier instantiation modes.
Available modes for --mbqi are:
+ fmc (default)
  Use algorithm from Section 5.4.2 of thesis Finite Model Finding in
  Satisfiability Modulo Theories.
+ none
  Disable model-based quantifier instantiation.
+ trust
  Do not instantiate quantified formulas (incomplete technique).
)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::SIMPLE: return os << "simple";
    case PrenexQuantMode::NORMAL: return os << "norm";
    case PrenexQuantMode::NONE: return os << "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 << R"FOOBAR(
  Prenex quantifiers modes.
Available modes for --prenex-quant are:
+ simple (default)
  Do simple prenexing of same sign quantifiers.
+ norm
  Prenex to prenex normal form.
+ 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::CONFLICT_ONLY: return os << "conflict";
    case QcfMode::PARTIAL: return os << "partial";
    case QcfMode::PROP_EQ: return os << "prop-eq";
    default: Unreachable();
  }
  return os;
}
QcfMode stringToQcfMode(const std::string& optarg)
{
  if (optarg == "conflict") return QcfMode::CONFLICT_ONLY;
  else if (optarg == "partial") return QcfMode::PARTIAL;
  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:
+ conflict
  Apply QCF algorithm to find conflicts only.
+ partial
  Use QCF for conflicts, propagations and heuristic instantiations.
+ 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::LAST_CALL: return os << "last-call";
    case QcfWhenMode::STD: return os << "std";
    case QcfWhenMode::STD_H: return os << "std-h";
    case QcfWhenMode::DEFAULT: return os << "default";
    default: Unreachable();
  }
  return os;
}
QcfWhenMode stringToQcfWhenMode(const std::string& optarg)
{
  if (optarg == "last-call") return QcfWhenMode::LAST_CALL;
  else 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 == "help")
  {
    std::cerr << R"FOOBAR(
  Quantifier conflict find modes.
Available modes for --quant-cf-when are:
+ last-call
  Apply conflict finding at last call, after theory combination and and all
  theories report sat.
+ std
  Apply conflict finding at standard effort.
+ std-h
  Apply conflict finding at standard effort when heuristic says to.
+ 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 << "agg";
    case QuantDSplitMode::NONE: return os << "none";
    case QuantDSplitMode::DEFAULT: return os << "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::FIRST: return os << "first";
    case QuantRepMode::DEPTH: return os << "depth";
    case QuantRepMode::EE: return os << "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 << R"FOOBAR(
  Modes for quantifiers representative selection.
Available modes for --quant-rep-mode are:
+ first (default)
  Choose terms that appear first.
+ depth
  Choose terms that are of minimal depth.
+ ee
  Let equality engine choose representatives.
)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::ENUM_BASIC: return os << "basic";
    case SygusActiveGenMode::VAR_AGNOSTIC: return os << "var-agnostic";
    case SygusActiveGenMode::AUTO: return os << "auto";
    case SygusActiveGenMode::NONE: return os << "none";
    case SygusActiveGenMode::ENUM: return os << "enum";
    default: Unreachable();
  }
  return os;
}
SygusActiveGenMode stringToSygusActiveGenMode(const std::string& optarg)
{
  if (optarg == "basic") return SygusActiveGenMode::ENUM_BASIC;
  else if (optarg == "var-agnostic") return SygusActiveGenMode::VAR_AGNOSTIC;
  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:
+ basic
  Use basic type enumerator for actively-generated sygus enumerators.
+ var-agnostic
  Use sygus solver to enumerate terms that are agnostic to variables.
+ 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::STRONG: return os << "strong";
    case SygusFilterSolMode::NONE: return os << "none";
    case SygusFilterSolMode::WEAK: return os << "weak";
    default: Unreachable();
  }
  return os;
}
SygusFilterSolMode stringToSygusFilterSolMode(const std::string& optarg)
{
  if (optarg == "strong") return SygusFilterSolMode::STRONG;
  else if (optarg == "none") return SygusFilterSolMode::NONE;
  else if (optarg == "weak") return SygusFilterSolMode::WEAK;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for filtering sygus solutions.
Available modes for --sygus-filter-sol are:
+ strong
  Filter solutions that are logically stronger than others.
+ none (default)
  Do not filter sygus solutions.
+ weak
  Filter solutions that are logically weaker than others.
)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 << "any-term-concise";
    case SygusGrammarConsMode::SIMPLE: return os << "simple";
    case SygusGrammarConsMode::ANY_CONST: return os << "any-const";
    case SygusGrammarConsMode::ANY_TERM: return os << "any-term";
    default: Unreachable();
  }
  return os;
}
SygusGrammarConsMode stringToSygusGrammarConsMode(const std::string& optarg)
{
  if (optarg == "any-term-concise") return SygusGrammarConsMode::ANY_TERM_CONCISE;
  else if (optarg == "simple") return SygusGrammarConsMode::SIMPLE;
  else if (optarg == "any-const") return SygusGrammarConsMode::ANY_CONST;
  else if (optarg == "any-term") return SygusGrammarConsMode::ANY_TERM;
  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.
+ simple (default)
  Use simple grammar construction (no symbolic terms or constants).
+ any-const
  Use symoblic constant constructors.
+ 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.
)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::INTERLEAVE: return os << "interleave";
    case SygusInstMode::PRIORITY_EVAL: return os << "priority-eval";
    case SygusInstMode::PRIORITY_INST: return os << "priority-inst";
    default: Unreachable();
  }
  return os;
}
SygusInstMode stringToSygusInstMode(const std::string& optarg)
{
  if (optarg == "interleave") return SygusInstMode::INTERLEAVE;
  else if (optarg == "priority-eval") return SygusInstMode::PRIORITY_EVAL;
  else if (optarg == "priority-inst") return SygusInstMode::PRIORITY_INST;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  SyGuS instantiation lemma modes.
Available modes for --sygus-inst-mode are:
+ interleave
  add instantiation and evaluation unfolding lemmas in the same step.
+ priority-eval
  add evaluation unfolding lemma first, add instantiation lemma if unfolding
  lemmas already added.
+ priority-inst (default)
  add instantiation lemmas first, add evaluation unfolding if instantiation
  fails.
)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 << "in";
    case SygusInstScope::OUT: return os << "out";
    case SygusInstScope::BOTH: return os << "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::BOTH: return os << "both";
    case SygusInstTermSelMode::MIN: return os << "min";
    case SygusInstTermSelMode::MAX: return os << "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 << R"FOOBAR(
  Ground term selection modes.
Available modes for --sygus-inst-term-sel are:
+ both
  combines minimal and maximal .
+ min (default)
  collect minimal ground terms only.
+ max
  collect maximal 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 << "post";
    case SygusInvTemplMode::PRE: return os << "pre";
    case SygusInvTemplMode::NONE: return os << "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 << R"FOOBAR(
  Template modes for sygus invariant synthesis.
Available modes for --sygus-inv-templ are:
+ post (default)
  Synthesize invariant based on strengthening of postcondition.
+ pre
  Synthesize invariant based on weakening of precondition.
+ none
  Synthesize invariant directly.
)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, SygusQueryGenMode mode)
{
  switch(mode)
  {
    case SygusQueryGenMode::NONE: return os << "none";
    case SygusQueryGenMode::UNSAT: return os << "unsat";
    case SygusQueryGenMode::SAT: return os << "sat";
    default: Unreachable();
  }
  return os;
}
SygusQueryGenMode stringToSygusQueryGenMode(const std::string& optarg)
{
  if (optarg == "none") return SygusQueryGenMode::NONE;
  else if (optarg == "unsat") return SygusQueryGenMode::UNSAT;
  else if (optarg == "sat") return SygusQueryGenMode::SAT;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for generating interesting satisfiability queries using SyGuS.
Available modes for --sygus-query-gen are:
+ none (default)
  Do not generate queries with SyGuS.
+ unsat
  Generate interesting UNSAT queries, for e.g. proof testing.
+ sat
  Generate interesting SAT queries, for e.g. soundness testing.
)FOOBAR";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-query-gen: `") +
                        optarg + "'.  Try --sygus-query-gen=help.");
}
std::ostream& operator<<(std::ostream& os, SygusQueryDumpFilesMode mode)
{
  switch(mode)
  {
    case SygusQueryDumpFilesMode::UNSOLVED: return os << "unsolved";
    case SygusQueryDumpFilesMode::ALL: return os << "all";
    case SygusQueryDumpFilesMode::NONE: return os << "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 << R"FOOBAR(
  Query file options.
Available modes for --sygus-query-gen-dump-files are:
+ unsolved
  Dump query files that the subsolver did not solve.
+ all
  Dump all query files.
+ none (default)
  Do not dump query files when using --sygus-query-gen.
)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::USE: return os << "use";
    case CegqiSingleInvMode::ALL: return os << "all";
    case CegqiSingleInvMode::NONE: return os << "none";
    default: Unreachable();
  }
  return os;
}
CegqiSingleInvMode stringToCegqiSingleInvMode(const std::string& optarg)
{
  if (optarg == "use") return CegqiSingleInvMode::USE;
  else if (optarg == "all") return CegqiSingleInvMode::ALL;
  else if (optarg == "none") return CegqiSingleInvMode::NONE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for single invocation techniques.
Available modes for --sygus-si are:
+ use
  Use single invocation techniques only if grammar is not restrictive.
+ all
  Always use single invocation techniques.
+ none (default)
  Do not 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::ALL_LIMIT: return os << "all-limit";
    case CegqiSingleInvRconsMode::TRY: return os << "try";
    case CegqiSingleInvRconsMode::NONE: return os << "none";
    case CegqiSingleInvRconsMode::ALL: return os << "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 << R"FOOBAR(
  Modes for reconstruction solutions while using single invocation techniques.
Available modes for --sygus-si-rcons are:
+ all-limit (default)
  Try to reconstruct solutions in the original grammar, but termintate if a
  maximum number of rounds for reconstruction is exceeded.
+ try
  Try to reconstruct solutions in the original grammar when using single
  invocation techniques in an incomplete (fail-fast) manner.
+ 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
  Try to reconstruct solutions in the original grammar. In this mode, we do not
  terminate until a solution is successfully reconstructed.
)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_IGAIN: return os << "cond-enum-igain";
    case SygusUnifPiMode::CENUM: return os << "cond-enum";
    case SygusUnifPiMode::COMPLETE: return os << "complete";
    case SygusUnifPiMode::NONE: return os << "none";
    default: Unreachable();
  }
  return os;
}
SygusUnifPiMode stringToSygusUnifPiMode(const std::string& optarg)
{
  if (optarg == "cond-enum-igain") return SygusUnifPiMode::CENUM_IGAIN;
  else if (optarg == "cond-enum") return SygusUnifPiMode::CENUM;
  else if (optarg == "complete") return SygusUnifPiMode::COMPLETE;
  else if (optarg == "none") return SygusUnifPiMode::NONE;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Modes for piecewise-independent unification.
Available modes for --sygus-unif-pi are:
+ cond-enum-igain
  Same as cond-enum, but additionally uses an information gain heuristic when
  doing decision tree learning.
+ cond-enum
  Use unconstrained condition enumeration for piecewise-independent unification
  (see Section 4 of Barbosa et al FMCAD 2019).
+ complete
  Use complete approach for piecewise-independent unification (see Section 3 of
  Barbosa et al FMCAD 2019)
+ none (default)
  Do not use piecewise-independent unification.
)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::ALL: return os << "all";
    case TermDbMode::RELEVANT: return os << "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 << R"FOOBAR(
  Modes for terms included in the quantifiers term database.
Available modes for --term-db-mode are:
+ all (default)
  Quantifiers module considers all ground terms.
+ relevant
  Quantifiers module considers only ground terms connected to current
  assertions.
)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::MIN: return os << "min";
    case TriggerActiveSelMode::ALL: return os << "all";
    case TriggerActiveSelMode::MAX: return os << "max";
    default: Unreachable();
  }
  return os;
}
TriggerActiveSelMode stringToTriggerActiveSelMode(const std::string& optarg)
{
  if (optarg == "min") return TriggerActiveSelMode::MIN;
  else if (optarg == "all") return TriggerActiveSelMode::ALL;
  else if (optarg == "max") return TriggerActiveSelMode::MAX;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Trigger active selection modes.
Available modes for --trigger-active-sel are:
+ min
  Activate triggers with minimal ground terms.
+ all (default)
  Make all triggers active.
+ max
  Activate triggers with maximal ground terms.
)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_MAX: return os << "min-s-max";
    case TriggerSelMode::MIN: return os << "min";
    case TriggerSelMode::MAX: return os << "max";
    case TriggerSelMode::ALL: return os << "all";
    case TriggerSelMode::MIN_SINGLE_ALL: return os << "min-s-all";
    default: Unreachable();
  }
  return os;
}
TriggerSelMode stringToTriggerSelMode(const std::string& optarg)
{
  if (optarg == "min-s-max") return TriggerSelMode::MIN_SINGLE_MAX;
  else if (optarg == "min") return TriggerSelMode::MIN;
  else if (optarg == "max") return TriggerSelMode::MAX;
  else if (optarg == "all") return TriggerSelMode::ALL;
  else if (optarg == "min-s-all") return TriggerSelMode::MIN_SINGLE_ALL;
  else if (optarg == "help")
  {
    std::cerr << R"FOOBAR(
  Trigger selection modes.
Available modes for --trigger-sel are:
+ min-s-max
  Consider only minimal subterms that meet criteria for single triggers, maximal
  otherwise.
+ min (default)
  Consider only minimal subterms that meet criteria for triggers.
+ max
  Consider only maximal subterms that meet criteria for triggers.
+ all
  Consider all subterms that meet criteria for triggers.
+ min-s-all
  Consider only minimal subterms that meet criteria for single triggers, all
  otherwise.
)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::RESORT: return os << "resort";
    case UserPatMode::STRICT: return os << "strict";
    case UserPatMode::USE: return os << "use";
    case UserPatMode::INTERLEAVE: return os << "interleave";
    case UserPatMode::IGNORE: return os << "ignore";
    case UserPatMode::TRUST: return os << "trust";
    default: Unreachable();
  }
  return os;
}
UserPatMode stringToUserPatMode(const std::string& optarg)
{
  if (optarg == "resort") return UserPatMode::RESORT;
  else if (optarg == "strict") return UserPatMode::STRICT;
  else if (optarg == "use") return UserPatMode::USE;
  else if (optarg == "interleave") return UserPatMode::INTERLEAVE;
  else if (optarg == "ignore") return UserPatMode::IGNORE;
  else if (optarg == "trust") return UserPatMode::TRUST;
  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:
+ resort
  Use user-provided patterns only after auto-generated patterns saturate.
+ strict
  When provided, use only user-provided patterns for a quantified formula, and
  do not use any other instantiation techniques.
+ use
  Use both user-provided and auto-generated patterns when patterns are provided
  for a quantified formula.
+ interleave
  Alternate between use/resort.
+ ignore
  Ignore user-provided patterns.
+ trust (default)
  When provided, use only user-provided patterns 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 cvc5::options

Generated by: GCOVR (Version 3.2)