Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/options/options_handler.cpp	Lines:	114	275	41.5 %
Date:	2021-08-04	Branches:	122	540	22.6 %


/******************************************************************************
 * 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/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) { }

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

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

// theory/quantifiers/options_handlers.h

void OptionsHandler::checkInstWhenMode(const std::string& option,
                                       const std::string& flag,
                                       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(const std::string& option,
                                     const std::string& flag,
                                     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(const std::string& option,
                                     const std::string& flag,
                                     const 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(const std::string& option,
                                      const std::string& flag,
                                      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::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 (d_options->bv.bvSolver != options::BVSolver::BITBLAST
      && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
          || m == SatSolverMode::KISSAT))
  {
    if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
        && d_options->bv.bitblastModeWasSetByUser)
    {
      throwLazyBBUnsupported(m);
    }
    options::bv::setDefaultBitvectorToBool(*d_options, true);
  }
}

void OptionsHandler::checkBitblastMode(const std::string& option,
                                       const std::string& flag,
                                       BitblastMode m)
{
  if (m == options::BitblastMode::LAZY)
  {
    options::bv::setDefaultBitvectorPropagate(*d_options, true);
    options::bv::setDefaultBitvectorEqualitySolver(*d_options, true);
    options::bv::setDefaultBitvectorInequalitySolver(*d_options, true);
    options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true);
    if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT)
    {
      throwLazyBBUnsupported(d_options->bv.bvSatSolver);
    }
  }
  else if (m == BitblastMode::EAGER)
  {
    options::bv::setDefaultBitvectorToBool(*d_options, true);
  }
}

void OptionsHandler::setBitblastAig(const std::string& option,
                                    const std::string& flag,
                                    bool arg)
{
  if(arg) {
    if (d_options->bv.bitblastModeWasSetByUser) {
      if (d_options->bv.bitblastMode != options::BitblastMode::EAGER)
      {
        throw OptionException("bitblast-aig must be used with eager bitblaster");
      }
    } else {
      options::BitblastMode mode = stringToBitblastMode("eager");
      d_options->bv.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(const std::string& option,
                                                      const std::string& flag,
                                                      const 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.");
  }
}

void OptionsHandler::setProduceAssertions(const std::string& option,
                                          const std::string& flag,
                                          bool value)
{
  d_options->smt.produceAssertions = value;
  d_options->smt.interactiveMode = value;
}

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

void OptionsHandler::threadN(const std::string& option, const std::string& flag)
{
  throw OptionException(flag + " 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(const std::string& option,
                                                  const std::string& flag,
                                                  int depth)
{
  if(depth < -1) {
    throw OptionException("--expr-depth requires a positive argument, or -1.");
  }
}

void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option,
                                                  const std::string& flag,
                                                  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(const std::string& option,
                               const std::string& flag)
{
  std::cout << Configuration::copyright() << std::endl;
  exit(0);
}

void OptionsHandler::showConfiguration(const std::string& option,
                                       const std::string& flag)
{
  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("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());

  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(const std::string& option,
                                   const std::string& flag)
{
  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(const std::string& option,
                                   const std::string& flag)
{
  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(const std::string& option,
                                    const std::string& flag,
                                    const 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(const std::string& option,
                                    const std::string& flag,
                                    const 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);
}

void OptionsHandler::enableOutputTag(const std::string& option,
                                     const std::string& flag,
                                     const std::string& optarg)
{
  d_options->base.outputTagHolder.set(
      static_cast<size_t>(stringToOutputTag(optarg)));
}

OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option,
                                                      const std::string& flag,
                                                      const std::string& optarg)
{
  if(optarg == "help") {
    d_options->base.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(const std::string& option,
                                                    const std::string& flag,
                                                    const std::string& optarg)
{
  if(optarg == "help") {
    d_options->base.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(const std::string& option,
                                  const std::string& flag,
                                  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(const std::string& option,
                                       const std::string& flag)
{
  d_options->base.verbosity += 1;
  setVerbosity(option, flag, d_options->base.verbosity);
}

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