Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/options/options_handler.cpp	Lines:	108	280	38.6 %
Date:	2021-05-24	Branches:	143	676	21.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Tim King, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Interface for custom handlers and predicates options.
 */

#include "options/options_handler.h"

#include <cerrno>
#include <ostream>
#include <string>

#include "base/check.h"
#include "base/configuration.h"
#include "base/configuration_private.h"
#include "base/cvc5config.h"
#include "base/exception.h"
#include "base/modal_exception.h"
#include "base/output.h"
#include "lib/strtok_r.h"
#include "options/base_options.h"
#include "options/bv_options.h"
#include "options/decision_options.h"
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/option_exception.h"
#include "options/resource_manager_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"

namespace cvc5 {
namespace options {

// helper functions
namespace {

void throwLazyBBUnsupported(options::SatSolverMode m)
{
  std::string sat_solver;
  if (m == options::SatSolverMode::CADICAL)
  {
    sat_solver = "CaDiCaL";
  }
  else if (m == options::SatSolverMode::KISSAT)
  {
    sat_solver = "Kissat";
  }
  else
  {
    Assert(m == options::SatSolverMode::CRYPTOMINISAT);
    sat_solver = "CryptoMiniSat";
  }
  std::string indent(25, ' ');
  throw OptionException(sat_solver + " does not support lazy bit-blasting.\n"
                        + indent + "Try --bv-sat-solver=minisat");
}

}  // namespace

OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }

unsigned long OptionsHandler::limitHandler(std::string option,
                                           std::string optarg)
{
  unsigned long ms;
  std::istringstream convert(optarg);
  if (!(convert >> ms))
  {
    throw OptionException("option `" + option
                          + "` requires a number as an argument");
  }
  return ms;
}

void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
{
  d_options->resman().resourceWeightHolder.emplace_back(optarg);
}

// theory/quantifiers/options_handlers.h

void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
{
  if (mode == InstWhenMode::PRE_FULL)
  {
    throw OptionException(std::string("Mode pre-full for ") + option
                          + " is not supported in this release.");
  }
}

// theory/bv/options_handlers.h
void OptionsHandler::abcEnabledBuild(std::string option, bool value)
{
#ifndef CVC5_USE_ABC
  if(value) {
    std::stringstream ss;
    ss << "option `" << option
       << "' requires an abc-enabled build of cvc5; this binary was not built "
          "with abc support";
    throw OptionException(ss.str());
  }
#endif /* CVC5_USE_ABC */
}

void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
{
#ifndef CVC5_USE_ABC
  if(!value.empty()) {
    std::stringstream ss;
    ss << "option `" << option
       << "' requires an abc-enabled build of cvc5; this binary was not built "
          "with abc support";
    throw OptionException(ss.str());
  }
#endif /* CVC5_USE_ABC */
}

void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
{
  if (m == SatSolverMode::CRYPTOMINISAT
      && !Configuration::isBuiltWithCryptominisat())
  {
    std::stringstream ss;
    ss << "option `" << option
       << "' requires a CryptoMiniSat build of cvc5; this binary was not built "
          "with CryptoMiniSat support";
    throw OptionException(ss.str());
  }

  if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
  {
    std::stringstream ss;
    ss << "option `" << option
       << "' requires a CaDiCaL build of cvc5; this binary was not built with "
          "CaDiCaL support";
    throw OptionException(ss.str());
  }

  if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
  {
    std::stringstream ss;
    ss << "option `" << option
       << "' requires a Kissat build of cvc5; this binary was not built with "
          "Kissat support";
    throw OptionException(ss.str());
  }

  if (options::bvSolver() != options::BVSolver::BITBLAST
      && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
          || m == SatSolverMode::KISSAT))
  {
    if (options::bitblastMode() == options::BitblastMode::LAZY
        && Options::current().wasSetByUser(options::bitblastMode))
    {
      throwLazyBBUnsupported(m);
    }
    Options::current().setDefault(options::bitvectorToBool, true);
  }
}

void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
{
  if (m == options::BitblastMode::LAZY)
  {
    Options::current().setDefault(options::bitvectorPropagate, true);
    Options::current().setDefault(options::bitvectorEqualitySolver, true);
    Options::current().setDefault(options::bitvectorInequalitySolver, true);
    Options::current().setDefault(options::bitvectorAlgebraicSolver, true);
    if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
    {
      throwLazyBBUnsupported(options::bvSatSolver());
    }
  }
  else if (m == BitblastMode::EAGER)
  {
    Options::current().setDefault(options::bitvectorToBool, true);
  }
}

void OptionsHandler::setBitblastAig(std::string option, bool arg)
{
  if(arg) {
    if(Options::current().wasSetByUser(options::bitblastMode)) {
      if (options::bitblastMode() != options::BitblastMode::EAGER)
      {
        throw OptionException("bitblast-aig must be used with eager bitblaster");
      }
    } else {
      options::BitblastMode mode = stringToBitblastMode("eager");
      Options::current().set(options::bitblastMode, mode);
    }
  }
}

// printer/options_handlers.h
const std::string OptionsHandler::s_instFormatHelp = "\
Inst format modes currently supported by the --inst-format option:\n\
\n\
default \n\
+ Print instantiations as a list in the output language format.\n\
\n\
szs\n\
+ Print instantiations as SZS compliant proof.\n\
";

InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
                                                      std::string optarg)
{
  if(optarg == "default") {
    return InstFormatMode::DEFAULT;
  } else if(optarg == "szs") {
    return InstFormatMode::SZS;
  } else if(optarg == "help") {
    puts(s_instFormatHelp.c_str());
    exit(1);
  } else {
    throw OptionException(std::string("unknown option for --inst-format: `") +
                          optarg + "'.  Try --inst-format help.");
  }
}

// decision/options_handlers.h
void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
{
  Options::current().set(options::decisionStopOnly, m == DecisionMode::RELEVANCY);
}

void OptionsHandler::setProduceAssertions(std::string option, bool value)
{
  Options::current().set(options::produceAssertions, value);
  Options::current().set(options::interactiveMode, value);
}

void OptionsHandler::setStats(const std::string& option, bool value)
{
#ifndef CVC5_STATISTICS_ON
  if (value)
  {
    std::stringstream ss;
    ss << "option `" << option
       << "' requires a statistics-enabled build of cvc5; this binary was not "
          "built with statistics support";
    throw OptionException(ss.str());
  }
#endif /* CVC5_STATISTICS_ON */
  Assert(option.substr(0, 2) == "--");
  std::string opt = option.substr(2);
  if (value)
  {
    if (option == options::base::statisticsAll__name)
    {
      d_options->base().statistics = true;
    }
    else if (option == options::base::statisticsEveryQuery__name)
    {
      d_options->base().statistics = true;
    }
    else if (option == options::base::statisticsExpert__name)
    {
      d_options->base().statistics = true;
    }
  }
  else
  {
    if (option == options::base::statistics__name)
    {
      d_options->base().statisticsAll = false;
      d_options->base().statisticsEveryQuery = false;
      d_options->base().statisticsExpert = false;
    }
  }
}

void OptionsHandler::threadN(std::string option) {
  throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
}

// expr/options_handlers.h
void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
  if(depth < -1) {
    throw OptionException("--expr-depth requires a positive argument, or -1.");
  }
}

void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
  if(dag < 0) {
    throw OptionException("--dag-thresh requires a nonnegative argument.");
  }
}

// main/options_handlers.h

static void print_config (const char * str, std::string config) {
  std::string s(str);
  unsigned sz = 14;
  if (s.size() < sz) s.resize(sz, ' ');
  std::cout << s << ": " << config << std::endl;
}

static void print_config_cond (const char * str, bool cond = false) {
  print_config(str, cond ? "yes" : "no");
}

void OptionsHandler::copyright(std::string option) {
  std::cout << Configuration::copyright() << std::endl;
  exit(0);
}

void OptionsHandler::showConfiguration(std::string option) {
  std::cout << Configuration::about() << std::endl;

  print_config ("version", Configuration::getVersionString());

  if(Configuration::isGitBuild()) {
    const char* branchName = Configuration::getGitBranchName();
    if(*branchName == '\0')  { branchName = "-"; }
    std::stringstream ss;
    ss << "git ["
       << branchName << " "
       << std::string(Configuration::getGitCommit()).substr(0, 8)
       << (Configuration::hasGitModifications() ? " (with modifications)" : "")
       << "]";
    print_config("scm", ss.str());
  } else {
    print_config_cond("scm", false);
  }

  std::cout << std::endl;

  std::stringstream ss;
  ss << Configuration::getVersionMajor() << "."
     << Configuration::getVersionMinor() << "."
     << Configuration::getVersionRelease();
  print_config("library", ss.str());

  std::cout << std::endl;

  print_config_cond("debug code", Configuration::isDebugBuild());
  print_config_cond("statistics", Configuration::isStatisticsBuild());
  print_config_cond("tracing", Configuration::isTracingBuild());
  print_config_cond("dumping", Configuration::isDumpingBuild());
  print_config_cond("muzzled", Configuration::isMuzzledBuild());
  print_config_cond("assertions", Configuration::isAssertionBuild());
  print_config_cond("coverage", Configuration::isCoverageBuild());
  print_config_cond("profiling", Configuration::isProfilingBuild());
  print_config_cond("asan", Configuration::isAsanBuild());
  print_config_cond("ubsan", Configuration::isUbsanBuild());
  print_config_cond("tsan", Configuration::isTsanBuild());
  print_config_cond("competition", Configuration::isCompetitionBuild());

  std::cout << std::endl;

  print_config_cond("abc", Configuration::isBuiltWithAbc());
  print_config_cond("cln", Configuration::isBuiltWithCln());
  print_config_cond("glpk", Configuration::isBuiltWithGlpk());
  print_config_cond("cadical", Configuration::isBuiltWithCadical());
  print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
  print_config_cond("gmp", Configuration::isBuiltWithGmp());
  print_config_cond("kissat", Configuration::isBuiltWithKissat());
  print_config_cond("poly", Configuration::isBuiltWithPoly());
  print_config_cond("editline", Configuration::isBuiltWithEditline());
  print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());

  exit(0);
}

static void printTags(unsigned ntags, char const* const* tags)
{
  std::cout << "available tags:";
  for (unsigned i = 0; i < ntags; ++ i)
  {
    std::cout << "  " << tags[i] << std::endl;
  }
  std::cout << std::endl;
}

void OptionsHandler::showDebugTags(std::string option)
{
  if (!Configuration::isDebugBuild())
  {
    throw OptionException("debug tags not available in non-debug builds");
  }
  else if (!Configuration::isTracingBuild())
  {
    throw OptionException("debug tags not available in non-tracing builds");
  }
  printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
  exit(0);
}

void OptionsHandler::showTraceTags(std::string option)
{
  if (!Configuration::isTracingBuild())
  {
    throw OptionException("trace tags not available in non-tracing build");
  }
  printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
  exit(0);
}

static std::string suggestTags(char const* const* validTags,
                               std::string inputTag,
                               char const* const* additionalTags)
{
  DidYouMean didYouMean;

  const char* opt;
  for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
  {
    didYouMean.addWord(validTags[i]);
  }
  if (additionalTags != nullptr)
  {
    for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
    {
      didYouMean.addWord(additionalTags[i]);
    }
  }

  return didYouMean.getMatchAsString(inputTag);
}

void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
{
  if(!Configuration::isTracingBuild())
  {
    throw OptionException("trace tags not available in non-tracing builds");
  }
  else if(!Configuration::isTraceTag(optarg.c_str()))
  {
    if (optarg == "help")
    {
      printTags(
          Configuration::getNumTraceTags(), Configuration::getTraceTags());
      exit(0);
    }

    throw OptionException(
        std::string("trace tag ") + optarg + std::string(" not available.")
        + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
  }
  Trace.on(optarg);
}

void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
{
  if (!Configuration::isDebugBuild())
  {
    throw OptionException("debug tags not available in non-debug builds");
  }
  else if (!Configuration::isTracingBuild())
  {
    throw OptionException("debug tags not available in non-tracing builds");
  }

  if (!Configuration::isDebugTag(optarg.c_str())
      && !Configuration::isTraceTag(optarg.c_str()))
  {
    if (optarg == "help")
    {
      printTags(
          Configuration::getNumDebugTags(), Configuration::getDebugTags());
      exit(0);
    }

    throw OptionException(std::string("debug tag ") + optarg
                          + std::string(" not available.")
                          + suggestTags(Configuration::getDebugTags(),
                                        optarg,
                                        Configuration::getTraceTags()));
  }
  Debug.on(optarg);
  Trace.on(optarg);
}

OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
                                                      std::string optarg)
{
  if(optarg == "help") {
    Options::current().set(options::languageHelp, true);
    return language::output::LANG_AUTO;
  }

  try {
    return language::toOutputLanguage(optarg);
  } catch(OptionException& oe) {
    throw OptionException("Error in " + option + ": " + oe.getMessage() +
                          "\nTry --output-language help");
  }

  Unreachable();
}

InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
                                                    std::string optarg)
{
  if(optarg == "help") {
    Options::current().set(options::languageHelp, true);
    return language::input::LANG_AUTO;
  }

  try {
    return language::toInputLanguage(optarg);
  } catch(OptionException& oe) {
    throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --lang help");
  }

  Unreachable();
}

/* options/base_options_handlers.h */
void OptionsHandler::setVerbosity(std::string option, int value)
{
  if(Configuration::isMuzzledBuild()) {
    DebugChannel.setStream(&cvc5::null_os);
    TraceChannel.setStream(&cvc5::null_os);
    NoticeChannel.setStream(&cvc5::null_os);
    ChatChannel.setStream(&cvc5::null_os);
    MessageChannel.setStream(&cvc5::null_os);
    WarningChannel.setStream(&cvc5::null_os);
  } else {
    if(value < 2) {
      ChatChannel.setStream(&cvc5::null_os);
    } else {
      ChatChannel.setStream(&std::cout);
    }
    if(value < 1) {
      NoticeChannel.setStream(&cvc5::null_os);
    } else {
      NoticeChannel.setStream(&std::cout);
    }
    if(value < 0) {
      MessageChannel.setStream(&cvc5::null_os);
      WarningChannel.setStream(&cvc5::null_os);
    } else {
      MessageChannel.setStream(&std::cout);
      WarningChannel.setStream(&std::cerr);
    }
  }
}

void OptionsHandler::increaseVerbosity(std::string option) {
  Options::current().set(options::verbosity, options::verbosity() + 1);
  setVerbosity(option, options::verbosity());
}

void OptionsHandler::decreaseVerbosity(std::string option) {
  Options::current().set(options::verbosity, options::verbosity() - 1);
  setVerbosity(option, options::verbosity());
}

}  // namespace options
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Tim King, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Interface for custom handlers and predicates options.
14		*/
15
16		#include "options/options_handler.h"
17
18		#include <cerrno>
19		#include <ostream>
20		#include <string>
21
22		#include "base/check.h"
23		#include "base/configuration.h"
24		#include "base/configuration_private.h"
25		#include "base/cvc5config.h"
26		#include "base/exception.h"
27		#include "base/modal_exception.h"
28		#include "base/output.h"
29		#include "lib/strtok_r.h"
30		#include "options/base_options.h"
31		#include "options/bv_options.h"
32		#include "options/decision_options.h"
33		#include "options/didyoumean.h"
34		#include "options/language.h"
35		#include "options/option_exception.h"
36		#include "options/resource_manager_options.h"
37		#include "options/smt_options.h"
38		#include "options/theory_options.h"
39
40		namespace cvc5 {
41		namespace options {
42
43		// helper functions
44		namespace {
45
46		void throwLazyBBUnsupported(options::SatSolverMode m)
47		{
48		std::string sat_solver;
49		if (m == options::SatSolverMode::CADICAL)
50		{
51		sat_solver = "CaDiCaL";
52		}
53		else if (m == options::SatSolverMode::KISSAT)
54		{
55		sat_solver = "Kissat";
56		}
57		else
58		{
59		Assert(m == options::SatSolverMode::CRYPTOMINISAT);
60		sat_solver = "CryptoMiniSat";
61		}
62		std::string indent(25, ' ');
63		throw OptionException(sat_solver + " does not support lazy bit-blasting.\n"
64		+ indent + "Try --bv-sat-solver=minisat");
65		}
66
67		} // namespace
68
69	25265	OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
70
71		unsigned long OptionsHandler::limitHandler(std::string option,
72		std::string optarg)
73		{
74		unsigned long ms;
75		std::istringstream convert(optarg);
76		if (!(convert >> ms))
77		{
78		throw OptionException("option `" + option
79		+ "` requires a number as an argument");
80		}
81		return ms;
82		}
83
84		void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
85		{
86		d_options->resman().resourceWeightHolder.emplace_back(optarg);
87		}
88
89		// theory/quantifiers/options_handlers.h
90
91	3	void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
92		{
93	3	if (mode == InstWhenMode::PRE_FULL)
94		{
95		throw OptionException(std::string("Mode pre-full for ") + option
96		+ " is not supported in this release.");
97		}
98	3	}
99
100		// theory/bv/options_handlers.h
101		void OptionsHandler::abcEnabledBuild(std::string option, bool value)
102		{
103		#ifndef CVC5_USE_ABC
104		if(value) {
105		std::stringstream ss;
106		ss << "option `" << option
107		<< "' requires an abc-enabled build of cvc5; this binary was not built "
108		"with abc support";
109		throw OptionException(ss.str());
110		}
111		#endif /* CVC5_USE_ABC */
112		}
113
114		void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
115		{
116		#ifndef CVC5_USE_ABC
117		if(!value.empty()) {
118		std::stringstream ss;
119		ss << "option `" << option
120		<< "' requires an abc-enabled build of cvc5; this binary was not built "
121		"with abc support";
122		throw OptionException(ss.str());
123		}
124		#endif /* CVC5_USE_ABC */
125		}
126
127	16	void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
128		{
129	16	if (m == SatSolverMode::CRYPTOMINISAT
130	16	&& !Configuration::isBuiltWithCryptominisat())
131		{
132		std::stringstream ss;
133		ss << "option `" << option
134		<< "' requires a CryptoMiniSat build of cvc5; this binary was not built "
135		"with CryptoMiniSat support";
136		throw OptionException(ss.str());
137		}
138
139	16	if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical())
140		{
141		std::stringstream ss;
142		ss << "option `" << option
143		<< "' requires a CaDiCaL build of cvc5; this binary was not built with "
144		"CaDiCaL support";
145		throw OptionException(ss.str());
146		}
147
148	16	if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
149		{
150		std::stringstream ss;
151		ss << "option `" << option
152		<< "' requires a Kissat build of cvc5; this binary was not built with "
153		"Kissat support";
154		throw OptionException(ss.str());
155		}
156
157	32	if (options::bvSolver() != options::BVSolver::BITBLAST
158	30	&& (m == SatSolverMode::CRYPTOMINISAT \|\| m == SatSolverMode::CADICAL
159	2	\|\| m == SatSolverMode::KISSAT))
160		{
161	28	if (options::bitblastMode() == options::BitblastMode::LAZY
162	14	&& Options::current().wasSetByUser(options::bitblastMode))
163		{
164		throwLazyBBUnsupported(m);
165		}
166	14	Options::current().setDefault(options::bitvectorToBool, true);
167		}
168	16	}
169
170		void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
171		{
172		if (m == options::BitblastMode::LAZY)
173		{
174		Options::current().setDefault(options::bitvectorPropagate, true);
175		Options::current().setDefault(options::bitvectorEqualitySolver, true);
176		Options::current().setDefault(options::bitvectorInequalitySolver, true);
177		Options::current().setDefault(options::bitvectorAlgebraicSolver, true);
178		if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
179		{
180		throwLazyBBUnsupported(options::bvSatSolver());
181		}
182		}
183		else if (m == BitblastMode::EAGER)
184		{
185		Options::current().setDefault(options::bitvectorToBool, true);
186		}
187		}
188
189		void OptionsHandler::setBitblastAig(std::string option, bool arg)
190		{
191		if(arg) {
192		if(Options::current().wasSetByUser(options::bitblastMode)) {
193		if (options::bitblastMode() != options::BitblastMode::EAGER)
194		{
195		throw OptionException("bitblast-aig must be used with eager bitblaster");
196		}
197		} else {
198		options::BitblastMode mode = stringToBitblastMode("eager");
199		Options::current().set(options::bitblastMode, mode);
200		}
201		}
202		}
203
204		// printer/options_handlers.h
205	9397	const std::string OptionsHandler::s_instFormatHelp = "\
206		Inst format modes currently supported by the --inst-format option:\n\
207		\n\
208		default \n\
209		+ Print instantiations as a list in the output language format.\n\
210		\n\
211		szs\n\
212		+ Print instantiations as SZS compliant proof.\n\
213		";
214
215		InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
216		std::string optarg)
217		{
218		if(optarg == "default") {
219		return InstFormatMode::DEFAULT;
220		} else if(optarg == "szs") {
221		return InstFormatMode::SZS;
222		} else if(optarg == "help") {
223		puts(s_instFormatHelp.c_str());
224		exit(1);
225		} else {
226		throw OptionException(std::string("unknown option for --inst-format: `") +
227		optarg + "'. Try --inst-format help.");
228		}
229		}
230
231		// decision/options_handlers.h
232	68	void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m)
233		{
234	68	Options::current().set(options::decisionStopOnly, m == DecisionMode::RELEVANCY);
235	68	}
236
237	20	void OptionsHandler::setProduceAssertions(std::string option, bool value)
238		{
239	20	Options::current().set(options::produceAssertions, value);
240	42	Options::current().set(options::interactiveMode, value);
241	20	}
242
243		void OptionsHandler::setStats(const std::string& option, bool value)
244		{
245		#ifndef CVC5_STATISTICS_ON
246		if (value)
247		{
248		std::stringstream ss;
249		ss << "option `" << option
250		<< "' requires a statistics-enabled build of cvc5; this binary was not "
251		"built with statistics support";
252		throw OptionException(ss.str());
253		}
254		#endif /* CVC5_STATISTICS_ON */
255		Assert(option.substr(0, 2) == "--");
256		std::string opt = option.substr(2);
257		if (value)
258		{
259		if (option == options::base::statisticsAll__name)
260		{
261		d_options->base().statistics = true;
262		}
263		else if (option == options::base::statisticsEveryQuery__name)
264		{
265		d_options->base().statistics = true;
266		}
267		else if (option == options::base::statisticsExpert__name)
268		{
269		d_options->base().statistics = true;
270		}
271		}
272		else
273		{
274		if (option == options::base::statistics__name)
275		{
276		d_options->base().statisticsAll = false;
277		d_options->base().statisticsEveryQuery = false;
278		d_options->base().statisticsExpert = false;
279		}
280		}
281		}
282
283		void OptionsHandler::threadN(std::string option) {
284		throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
285		}
286
287		// expr/options_handlers.h
288		void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
289		if(depth < -1) {
290		throw OptionException("--expr-depth requires a positive argument, or -1.");
291		}
292		}
293
294	2	void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
295	2	if(dag < 0) {
296		throw OptionException("--dag-thresh requires a nonnegative argument.");
297		}
298	2	}
299
300		// main/options_handlers.h
301
302	62600	static void print_config (const char * str, std::string config) {
303	125200	std::string s(str);
304	62600	unsigned sz = 14;
305	62600	if (s.size() < sz) s.resize(sz, ' ');
306	62600	std::cout << s << ": " << config << std::endl;
307	62600	}
308
309	55088	static void print_config_cond (const char * str, bool cond = false) {
310	55088	print_config(str, cond ? "yes" : "no");
311	55088	}
312
313		void OptionsHandler::copyright(std::string option) {
314		std::cout << Configuration::copyright() << std::endl;
315		exit(0);
316		}
317
318	2504	void OptionsHandler::showConfiguration(std::string option) {
319	2504	std::cout << Configuration::about() << std::endl;
320
321	2504	print_config ("version", Configuration::getVersionString());
322
323	2504	if(Configuration::isGitBuild()) {
324	2504	const char* branchName = Configuration::getGitBranchName();
325	2504	if(*branchName == '\0') { branchName = "-"; }
326	5008	std::stringstream ss;
327		ss << "git ["
328		<< branchName << " "
329	5008	<< std::string(Configuration::getGitCommit()).substr(0, 8)
330	2504	<< (Configuration::hasGitModifications() ? " (with modifications)" : "")
331	7512	<< "]";
332	2504	print_config("scm", ss.str());
333		} else {
334		print_config_cond("scm", false);
335		}
336
337	2504	std::cout << std::endl;
338
339	2504	std::stringstream ss;
340	2504	ss << Configuration::getVersionMajor() << "."
341	2504	<< Configuration::getVersionMinor() << "."
342	2504	<< Configuration::getVersionRelease();
343	2504	print_config("library", ss.str());
344
345	2504	std::cout << std::endl;
346
347	2504	print_config_cond("debug code", Configuration::isDebugBuild());
348	2504	print_config_cond("statistics", Configuration::isStatisticsBuild());
349	2504	print_config_cond("tracing", Configuration::isTracingBuild());
350	2504	print_config_cond("dumping", Configuration::isDumpingBuild());
351	2504	print_config_cond("muzzled", Configuration::isMuzzledBuild());
352	2504	print_config_cond("assertions", Configuration::isAssertionBuild());
353	2504	print_config_cond("coverage", Configuration::isCoverageBuild());
354	2504	print_config_cond("profiling", Configuration::isProfilingBuild());
355	2504	print_config_cond("asan", Configuration::isAsanBuild());
356	2504	print_config_cond("ubsan", Configuration::isUbsanBuild());
357	2504	print_config_cond("tsan", Configuration::isTsanBuild());
358	2504	print_config_cond("competition", Configuration::isCompetitionBuild());
359
360	2504	std::cout << std::endl;
361
362	2504	print_config_cond("abc", Configuration::isBuiltWithAbc());
363	2504	print_config_cond("cln", Configuration::isBuiltWithCln());
364	2504	print_config_cond("glpk", Configuration::isBuiltWithGlpk());
365	2504	print_config_cond("cadical", Configuration::isBuiltWithCadical());
366	2504	print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
367	2504	print_config_cond("gmp", Configuration::isBuiltWithGmp());
368	2504	print_config_cond("kissat", Configuration::isBuiltWithKissat());
369	2504	print_config_cond("poly", Configuration::isBuiltWithPoly());
370	2504	print_config_cond("editline", Configuration::isBuiltWithEditline());
371	2504	print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
372
373	2504	exit(0);
374		}
375
376		static void printTags(unsigned ntags, char const* const* tags)
377		{
378		std::cout << "available tags:";
379		for (unsigned i = 0; i < ntags; ++ i)
380		{
381		std::cout << " " << tags[i] << std::endl;
382		}
383		std::cout << std::endl;
384		}
385
386		void OptionsHandler::showDebugTags(std::string option)
387		{
388		if (!Configuration::isDebugBuild())
389		{
390		throw OptionException("debug tags not available in non-debug builds");
391		}
392		else if (!Configuration::isTracingBuild())
393		{
394		throw OptionException("debug tags not available in non-tracing builds");
395		}
396		printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
397		exit(0);
398		}
399
400		void OptionsHandler::showTraceTags(std::string option)
401		{
402		if (!Configuration::isTracingBuild())
403		{
404		throw OptionException("trace tags not available in non-tracing build");
405		}
406		printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
407		exit(0);
408		}
409
410		static std::string suggestTags(char const* const* validTags,
411		std::string inputTag,
412		char const* const* additionalTags)
413		{
414		DidYouMean didYouMean;
415
416		const char* opt;
417		for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
418		{
419		didYouMean.addWord(validTags[i]);
420		}
421		if (additionalTags != nullptr)
422		{
423		for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
424		{
425		didYouMean.addWord(additionalTags[i]);
426		}
427		}
428
429		return didYouMean.getMatchAsString(inputTag);
430		}
431
432		void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
433		{
434		if(!Configuration::isTracingBuild())
435		{
436		throw OptionException("trace tags not available in non-tracing builds");
437		}
438		else if(!Configuration::isTraceTag(optarg.c_str()))
439		{
440		if (optarg == "help")
441		{
442		printTags(
443		Configuration::getNumTraceTags(), Configuration::getTraceTags());
444		exit(0);
445		}
446
447		throw OptionException(
448		std::string("trace tag ") + optarg + std::string(" not available.")
449		+ suggestTags(Configuration::getTraceTags(), optarg, nullptr));
450		}
451		Trace.on(optarg);
452		}
453
454		void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
455		{
456		if (!Configuration::isDebugBuild())
457		{
458		throw OptionException("debug tags not available in non-debug builds");
459		}
460		else if (!Configuration::isTracingBuild())
461		{
462		throw OptionException("debug tags not available in non-tracing builds");
463		}
464
465		if (!Configuration::isDebugTag(optarg.c_str())
466		&& !Configuration::isTraceTag(optarg.c_str()))
467		{
468		if (optarg == "help")
469		{
470		printTags(
471		Configuration::getNumDebugTags(), Configuration::getDebugTags());
472		exit(0);
473		}
474
475		throw OptionException(std::string("debug tag ") + optarg
476		+ std::string(" not available.")
477		+ suggestTags(Configuration::getDebugTags(),
478		optarg,
479		Configuration::getTraceTags()));
480		}
481		Debug.on(optarg);
482		Trace.on(optarg);
483		}
484
485	87	OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
486		std::string optarg)
487		{
488	87	if(optarg == "help") {
489	5878	Options::current().set(options::languageHelp, true);
490		return language::output::LANG_AUTO;
491		}
492
493		try {
494	87	return language::toOutputLanguage(optarg);
495		} catch(OptionException& oe) {
496		throw OptionException("Error in " + option + ": " + oe.getMessage() +
497		"\nTry --output-language help");
498		}
499
500		Unreachable();
501		}
502
503	500	InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
504		std::string optarg)
505		{
506	500	if(optarg == "help") {
507		Options::current().set(options::languageHelp, true);
508		return language::input::LANG_AUTO;
509		}
510
511		try {
512	500	return language::toInputLanguage(optarg);
513		} catch(OptionException& oe) {
514		throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --lang help");
515		}
516
517		Unreachable();
518		}
519
520		/* options/base_options_handlers.h */
521	169	void OptionsHandler::setVerbosity(std::string option, int value)
522		{
523	169	if(Configuration::isMuzzledBuild()) {
524		DebugChannel.setStream(&cvc5::null_os);
525		TraceChannel.setStream(&cvc5::null_os);
526		NoticeChannel.setStream(&cvc5::null_os);
527		ChatChannel.setStream(&cvc5::null_os);
528		MessageChannel.setStream(&cvc5::null_os);
529		WarningChannel.setStream(&cvc5::null_os);
530		} else {
531	169	if(value < 2) {
532	167	ChatChannel.setStream(&cvc5::null_os);
533		} else {
534	2	ChatChannel.setStream(&std::cout);
535		}
536	169	if(value < 1) {
537	166	NoticeChannel.setStream(&cvc5::null_os);
538		} else {
539	3	NoticeChannel.setStream(&std::cout);
540		}
541	169	if(value < 0) {
542	166	MessageChannel.setStream(&cvc5::null_os);
543	166	WarningChannel.setStream(&cvc5::null_os);
544		} else {
545	3	MessageChannel.setStream(&std::cout);
546	3	WarningChannel.setStream(&std::cerr);
547		}
548		}
549	169	}
550
551	3	void OptionsHandler::increaseVerbosity(std::string option) {
552	3	Options::current().set(options::verbosity, options::verbosity() + 1);
553	3	setVerbosity(option, options::verbosity());
554	3	}
555
556	166	void OptionsHandler::decreaseVerbosity(std::string option) {
557	166	Options::current().set(options::verbosity, options::verbosity() - 1);
558	166	setVerbosity(option, options::verbosity());
559	166	}
560
561		} // namespace options
562	34091	} // namespace cvc5