Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/options/options_handler.cpp	Lines:	134	300	44.7 %
Date:	2021-09-09	Branches:	140	586	23.9 %


/******************************************************************************
 * 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 "expr/expr_iomanip.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/set_language.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/command.h"
#include "smt/dump.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;
    }
  }
}

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::setDefaultExprDepth(const std::string& option,
                                         const std::string& flag,
                                         int depth)
{
  Debug.getStream() << expr::ExprSetDepth(depth);
  Trace.getStream() << expr::ExprSetDepth(depth);
  Notice.getStream() << expr::ExprSetDepth(depth);
  Chat.getStream() << expr::ExprSetDepth(depth);
  CVC5Message.getStream() << expr::ExprSetDepth(depth);
  Warning.getStream() << expr::ExprSetDepth(depth);
}

void OptionsHandler::setDefaultDagThresh(const std::string& option,
                                         const std::string& flag,
                                         int dag)
{
  Debug.getStream() << expr::ExprDag(dag);
  Trace.getStream() << expr::ExprDag(dag);
  Notice.getStream() << expr::ExprDag(dag);
  Chat.getStream() << expr::ExprDag(dag);
  CVC5Message.getStream() << expr::ExprDag(dag);
  Warning.getStream() << expr::ExprDag(dag);
  Dump.getStream() << expr::ExprDag(dag);
}

// 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)));
}

Language OptionsHandler::stringToLanguage(const std::string& option,
                                          const std::string& flag,
                                          const std::string& optarg)
{
  if(optarg == "help") {
    d_options->base.languageHelp = true;
    return Language::LANG_AUTO;
  }

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

  Unreachable();
}

void OptionsHandler::applyOutputLanguage(const std::string& option,
                                         const std::string& flag,
                                         Language lang)
{
  d_options->base.out << language::SetLanguage(lang);
}

void OptionsHandler::languageIsNotAST(const std::string& option,
                                      const std::string& flag,
                                      Language lang)
{
  if (lang == Language::LANG_AST)
  {
    throw OptionException("Language LANG_AST is not allowed for " + flag);
  }
}

void OptionsHandler::setDumpStream(const std::string& option,
                                   const std::string& flag,
                                   const ManagedOut& mo)
{
#ifdef CVC5_DUMPING
  Dump.setStream(mo);
#else  /* CVC5_DUMPING */
  throw OptionException(
      "The dumping feature was disabled in this build of cvc5.");
#endif /* CVC5_DUMPING */
}
void OptionsHandler::setErrStream(const std::string& option,
                                  const std::string& flag,
                                  const ManagedErr& me)
{
  Debug.setStream(me);
  Warning.setStream(me);
  CVC5Message.setStream(me);
  Notice.setStream(me);
  Chat.setStream(me);
  Trace.setStream(me);
}
void OptionsHandler::setInStream(const std::string& option,
                                 const std::string& flag,
                                 const ManagedIn& mi)
{
}
void OptionsHandler::setOutStream(const std::string& option,
                                  const std::string& flag,
                                  const ManagedOut& mo)
{
}

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

void OptionsHandler::setDumpMode(const std::string& option,
                                 const std::string& flag,
                                 const std::string& optarg)
{
  Dump.setDumpFromString(optarg);
}

void OptionsHandler::setPrintSuccess(const std::string& option,
                                     const std::string& flag,
                                     bool value)
{
  Debug.getStream() << Command::printsuccess(value);
  Trace.getStream() << Command::printsuccess(value);
  Notice.getStream() << Command::printsuccess(value);
  Chat.getStream() << Command::printsuccess(value);
  CVC5Message.getStream() << Command::printsuccess(value);
  Warning.getStream() << Command::printsuccess(value);
  *d_options->base.out << Command::printsuccess(value);
}

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