Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/options/options_handler.cpp	Lines:	132	311	42.4 %
Date:	2021-08-06	Branches:	143	616	23.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 "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/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;
    }
  }
}

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

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

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