Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/options/options_handler.cpp	Lines:	127	232	54.7 %
Date:	2021-11-05	Branches:	121	506	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 <iostream>
#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/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 "util/didyoumean.h"

namespace cvc5 {
namespace options {

// helper functions
namespace {

static void printTags(const std::vector<std::string>& tags)
{
  std::cout << "available tags:";
  for (const auto& t : tags)
  {
    std::cout << "  " << t << std::endl;
  }
  std::cout << std::endl;
}

std::string suggestTags(const std::vector<std::string>& validTags,
                        std::string inputTag,
                        const std::vector<std::string>& additionalTags)
{
  DidYouMean didYouMean;
  didYouMean.addWords(validTags);
  didYouMean.addWords(additionalTags);
  return didYouMean.getMatchAsString(inputTag);
}

}  // namespace

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

void OptionsHandler::setErrStream(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);
}

Language OptionsHandler::stringToLanguage(const std::string& flag,
                                          const std::string& optarg)
{
  if (optarg == "help")
  {
    *d_options->base.out << R"FOOBAR(
Languages currently supported as arguments to the -L / --lang option:
  auto                           attempt to automatically determine language
  smt | smtlib | smt2 |
  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard
  tptp                           TPTP format (cnf, fof and tff)
  sygus | sygus2                 SyGuS version 2.0

Languages currently supported as arguments to the --output-lang option:
  auto                           match output language to input language
  smt | smtlib | smt2 |
  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard
  tptp                           TPTP format
  ast                            internal format (simple syntax trees)
)FOOBAR" << std::endl;
    std::exit(1);
    return Language::LANG_AUTO;
  }

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

  Unreachable();
}

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

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

void OptionsHandler::setVerbosity(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::decreaseVerbosity(const std::string& flag)
{
  d_options->base.verbosity -= 1;
  setVerbosity(flag, d_options->base.verbosity);
}

void OptionsHandler::increaseVerbosity(const std::string& flag)
{
  d_options->base.verbosity += 1;
  setVerbosity(flag, d_options->base.verbosity);
}

void OptionsHandler::setStats(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 */
  if (!value)
  {
    d_options->base.statisticsAll = false;
    d_options->base.statisticsEveryQuery = false;
    d_options->base.statisticsExpert = false;
  }
}

void OptionsHandler::setStatsDetail(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 */
  if (value)
  {
    d_options->base.statistics = true;
  }
}

void OptionsHandler::enableTraceTag(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::getTraceTags());
      std::exit(0);
    }

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

void OptionsHandler::enableDebugTag(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::getDebugTags());
      std::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& flag,
                                     const std::string& optarg)
{
  size_t tagid = static_cast<size_t>(stringToOutputTag(optarg));
  Assert(d_options->base.outputTagHolder.size() > tagid)
      << "Output tag is larger than the bitset that holds it.";
  d_options->base.outputTagHolder.set(tagid);
}

void OptionsHandler::setPrintSuccess(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);
}

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

void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m)
{
  if (m == SatSolverMode::CRYPTOMINISAT
      && !Configuration::isBuiltWithCryptominisat())
  {
    std::stringstream ss;
    ss << "option `" << flag
       << "' 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 `" << flag
       << "' 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)
    {
      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";
      }
      throw OptionException(sat_solver
                            + " does not support lazy bit-blasting.\n"
                            + "Try --bv-sat-solver=minisat");
    }
    if (!d_options->bv.bitvectorToBoolWasSetByUser)
    {
      d_options->bv.bitvectorToBool = true;
    }
  }
}

void OptionsHandler::setBitblastAig(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 {
      d_options->bv.bitblastMode = options::BitblastMode::EAGER;
    }
  }
}

void OptionsHandler::setDefaultExprDepth(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& 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);
}

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::showConfiguration(const std::string& flag)
{
  std::cout << Configuration::about() << std::endl;

  print_config("version", Configuration::getVersionString());
  if (Configuration::isGitBuild())
  {
    print_config("scm", Configuration::getGitInfo());
  }
  else
  {
    print_config_cond("scm", false);
  }

  std::cout << std::endl;

  std::stringstream ss;
  ss << Configuration::getVersionString();
  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("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());

  std::exit(0);
}

void OptionsHandler::showCopyright(const std::string& flag)
{
  std::cout << Configuration::copyright() << std::endl;
  std::exit(0);
}

void OptionsHandler::showVersion(const std::string& flag)
{
  d_options->base.out << Configuration::about() << std::endl;
  std::exit(0);
}

void OptionsHandler::showDebugTags(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::getDebugTags());
  std::exit(0);
}

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

}  // 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 <iostream>
20		#include <ostream>
21		#include <string>
22
23		#include "base/check.h"
24		#include "base/configuration.h"
25		#include "base/configuration_private.h"
26		#include "base/cvc5config.h"
27		#include "base/exception.h"
28		#include "base/modal_exception.h"
29		#include "base/output.h"
30		#include "expr/expr_iomanip.h"
31		#include "lib/strtok_r.h"
32		#include "options/base_options.h"
33		#include "options/bv_options.h"
34		#include "options/decision_options.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 "util/didyoumean.h"
42
43		namespace cvc5 {
44		namespace options {
45
46		// helper functions
47		namespace {
48
49		static void printTags(const std::vector<std::string>& tags)
50		{
51		std::cout << "available tags:";
52		for (const auto& t : tags)
53		{
54		std::cout << " " << t << std::endl;
55		}
56		std::cout << std::endl;
57		}
58
59		std::string suggestTags(const std::vector<std::string>& validTags,
60		std::string inputTag,
61		const std::vector<std::string>& additionalTags)
62		{
63		DidYouMean didYouMean;
64		didYouMean.addWords(validTags);
65		didYouMean.addWords(additionalTags);
66		return didYouMean.getMatchAsString(inputTag);
67		}
68
69		} // namespace
70
71	30741	OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
72
73	1	void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me)
74		{
75	1	Debug.setStream(me);
76	1	Warning.setStream(me);
77	1	CVC5Message.setStream(me);
78	1	Notice.setStream(me);
79	1	Chat.setStream(me);
80	1	Trace.setStream(me);
81	1	}
82
83	17631	Language OptionsHandler::stringToLanguage(const std::string& flag,
84		const std::string& optarg)
85		{
86	17631	if (optarg == "help")
87		{
88		*d_options->base.out << R"FOOBAR(
89		Languages currently supported as arguments to the -L / --lang option:
90		auto attempt to automatically determine language
91		smt \| smtlib \| smt2 \|
92		smt2.6 \| smtlib2.6 SMT-LIB format 2.6 with support for the strings standard
93		tptp TPTP format (cnf, fof and tff)
94		sygus \| sygus2 SyGuS version 2.0
95
96		Languages currently supported as arguments to the --output-lang option:
97		auto match output language to input language
98		smt \| smtlib \| smt2 \|
99		smt2.6 \| smtlib2.6 SMT-LIB format 2.6 with support for the strings standard
100		tptp TPTP format
101		ast internal format (simple syntax trees)
102		)FOOBAR" << std::endl;
103		std::exit(1);
104		return Language::LANG_AUTO;
105		}
106
107		try
108		{
109	17631	return language::toLanguage(optarg);
110		}
111		catch (OptionException& oe)
112		{
113		throw OptionException("Error in " + flag + ": " + oe.getMessage()
114		+ "\nTry --lang help");
115		}
116
117		Unreachable();
118		}
119
120	11030	void OptionsHandler::languageIsNotAST(const std::string& flag, Language lang)
121		{
122	11030	if (lang == Language::LANG_AST)
123		{
124		throw OptionException("Language LANG_AST is not allowed for " + flag);
125		}
126	11030	}
127
128	6601	void OptionsHandler::applyOutputLanguage(const std::string& flag, Language lang)
129		{
130	6601	d_options->base.out << language::SetLanguage(lang);
131	6601	}
132
133	217	void OptionsHandler::setVerbosity(const std::string& flag, int value)
134		{
135	217	if(Configuration::isMuzzledBuild()) {
136		DebugChannel.setStream(&cvc5::null_os);
137		TraceChannel.setStream(&cvc5::null_os);
138		NoticeChannel.setStream(&cvc5::null_os);
139		ChatChannel.setStream(&cvc5::null_os);
140		MessageChannel.setStream(&cvc5::null_os);
141		WarningChannel.setStream(&cvc5::null_os);
142		} else {
143	217	if(value < 2) {
144	215	ChatChannel.setStream(&cvc5::null_os);
145		} else {
146	2	ChatChannel.setStream(&std::cout);
147		}
148	217	if(value < 1) {
149	212	NoticeChannel.setStream(&cvc5::null_os);
150		} else {
151	5	NoticeChannel.setStream(&std::cout);
152		}
153	217	if(value < 0) {
154	208	MessageChannel.setStream(&cvc5::null_os);
155	208	WarningChannel.setStream(&cvc5::null_os);
156		} else {
157	9	MessageChannel.setStream(&std::cout);
158	9	WarningChannel.setStream(&std::cerr);
159		}
160		}
161	217	}
162
163	208	void OptionsHandler::decreaseVerbosity(const std::string& flag)
164		{
165	208	d_options->base.verbosity -= 1;
166	208	setVerbosity(flag, d_options->base.verbosity);
167	208	}
168
169	3	void OptionsHandler::increaseVerbosity(const std::string& flag)
170		{
171	3	d_options->base.verbosity += 1;
172	3	setVerbosity(flag, d_options->base.verbosity);
173	3	}
174
175	2	void OptionsHandler::setStats(const std::string& flag, bool value)
176		{
177		#ifndef CVC5_STATISTICS_ON
178		if (value)
179		{
180		std::stringstream ss;
181		ss << "option `" << flag
182		<< "' requires a statistics-enabled build of cvc5; this binary was not "
183		"built with statistics support";
184		throw OptionException(ss.str());
185		}
186		#endif /* CVC5_STATISTICS_ON */
187	2	if (!value)
188		{
189	2	d_options->base.statisticsAll = false;
190	2	d_options->base.statisticsEveryQuery = false;
191	2	d_options->base.statisticsExpert = false;
192		}
193	2	}
194
195	2	void OptionsHandler::setStatsDetail(const std::string& flag, bool value)
196		{
197		#ifndef CVC5_STATISTICS_ON
198		if (value)
199		{
200		std::stringstream ss;
201		ss << "option `" << flag
202		<< "' requires a statistics-enabled build of cvc5; this binary was not "
203		"built with statistics support";
204		throw OptionException(ss.str());
205		}
206		#endif /* CVC5_STATISTICS_ON */
207	2	if (value)
208		{
209	2	d_options->base.statistics = true;
210		}
211	2	}
212
213	1	void OptionsHandler::enableTraceTag(const std::string& flag,
214		const std::string& optarg)
215		{
216	1	if(!Configuration::isTracingBuild())
217		{
218		throw OptionException("trace tags not available in non-tracing builds");
219		}
220	1	else if(!Configuration::isTraceTag(optarg.c_str()))
221		{
222		if (optarg == "help")
223		{
224		printTags(Configuration::getTraceTags());
225		std::exit(0);
226		}
227
228		throw OptionException(
229		std::string("trace tag ") + optarg + std::string(" not available.")
230		+ suggestTags(Configuration::getTraceTags(), optarg, {}));
231		}
232	1	Trace.on(optarg);
233	1	}
234
235		void OptionsHandler::enableDebugTag(const std::string& flag,
236		const std::string& optarg)
237		{
238		if (!Configuration::isDebugBuild())
239		{
240		throw OptionException("debug tags not available in non-debug builds");
241		}
242		else if (!Configuration::isTracingBuild())
243		{
244		throw OptionException("debug tags not available in non-tracing builds");
245		}
246
247		if (!Configuration::isDebugTag(optarg.c_str())
248		&& !Configuration::isTraceTag(optarg.c_str()))
249		{
250		if (optarg == "help")
251		{
252		printTags(Configuration::getDebugTags());
253		std::exit(0);
254		}
255
256		throw OptionException(std::string("debug tag ") + optarg
257		+ std::string(" not available.")
258		+ suggestTags(Configuration::getDebugTags(),
259		optarg,
260		Configuration::getTraceTags()));
261		}
262		Debug.on(optarg);
263		Trace.on(optarg);
264		}
265
266	11	void OptionsHandler::enableOutputTag(const std::string& flag,
267		const std::string& optarg)
268		{
269	11	size_t tagid = static_cast<size_t>(stringToOutputTag(optarg));
270	11	Assert(d_options->base.outputTagHolder.size() > tagid)
271		<< "Output tag is larger than the bitset that holds it.";
272	11	d_options->base.outputTagHolder.set(tagid);
273	11	}
274
275	30	void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
276		{
277	30	Debug.getStream() << Command::printsuccess(value);
278	30	Trace.getStream() << Command::printsuccess(value);
279	30	Notice.getStream() << Command::printsuccess(value);
280	30	Chat.getStream() << Command::printsuccess(value);
281	30	CVC5Message.getStream() << Command::printsuccess(value);
282	30	Warning.getStream() << Command::printsuccess(value);
283	30	*d_options->base.out << Command::printsuccess(value);
284	30	}
285
286		void OptionsHandler::setResourceWeight(const std::string& flag,
287		const std::string& optarg)
288		{
289		d_options->base.resourceWeightHolder.emplace_back(optarg);
290		}
291
292	16	void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m)
293		{
294	16	if (m == SatSolverMode::CRYPTOMINISAT
295	16	&& !Configuration::isBuiltWithCryptominisat())
296		{
297		std::stringstream ss;
298		ss << "option `" << flag
299		<< "' requires a CryptoMiniSat build of cvc5; this binary was not built "
300		"with CryptoMiniSat support";
301		throw OptionException(ss.str());
302		}
303
304	16	if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
305		{
306		std::stringstream ss;
307		ss << "option `" << flag
308		<< "' requires a Kissat build of cvc5; this binary was not built with "
309		"Kissat support";
310		throw OptionException(ss.str());
311		}
312
313	16	if (d_options->bv.bvSolver != options::BVSolver::BITBLAST
314		&& (m == SatSolverMode::CRYPTOMINISAT \|\| m == SatSolverMode::CADICAL
315		\|\| m == SatSolverMode::KISSAT))
316		{
317		if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
318		&& d_options->bv.bitblastModeWasSetByUser)
319		{
320		std::string sat_solver;
321		if (m == options::SatSolverMode::CADICAL)
322		{
323		sat_solver = "CaDiCaL";
324		}
325		else if (m == options::SatSolverMode::KISSAT)
326		{
327		sat_solver = "Kissat";
328		}
329		else
330		{
331		Assert(m == options::SatSolverMode::CRYPTOMINISAT);
332		sat_solver = "CryptoMiniSat";
333		}
334		throw OptionException(sat_solver
335		+ " does not support lazy bit-blasting.\n"
336		+ "Try --bv-sat-solver=minisat");
337		}
338		if (!d_options->bv.bitvectorToBoolWasSetByUser)
339		{
340		d_options->bv.bitvectorToBool = true;
341		}
342		}
343	16	}
344
345		void OptionsHandler::setBitblastAig(const std::string& flag, bool arg)
346		{
347		if(arg) {
348		if (d_options->bv.bitblastModeWasSetByUser) {
349		if (d_options->bv.bitblastMode != options::BitblastMode::EAGER)
350		{
351		throw OptionException("bitblast-aig must be used with eager bitblaster");
352		}
353		} else {
354		d_options->bv.bitblastMode = options::BitblastMode::EAGER;
355		}
356		}
357		}
358
359		void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth)
360		{
361		Debug.getStream() << expr::ExprSetDepth(depth);
362		Trace.getStream() << expr::ExprSetDepth(depth);
363		Notice.getStream() << expr::ExprSetDepth(depth);
364		Chat.getStream() << expr::ExprSetDepth(depth);
365		CVC5Message.getStream() << expr::ExprSetDepth(depth);
366		Warning.getStream() << expr::ExprSetDepth(depth);
367		}
368
369	3	void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
370		{
371	3	Debug.getStream() << expr::ExprDag(dag);
372	3	Trace.getStream() << expr::ExprDag(dag);
373	3	Notice.getStream() << expr::ExprDag(dag);
374	3	Chat.getStream() << expr::ExprDag(dag);
375	3	CVC5Message.getStream() << expr::ExprDag(dag);
376	3	Warning.getStream() << expr::ExprDag(dag);
377	3	}
378
379	59972	static void print_config(const char* str, std::string config)
380		{
381	119944	std::string s(str);
382	59972	unsigned sz = 14;
383	59972	if (s.size() < sz) s.resize(sz, ' ');
384	59972	std::cout << s << ": " << config << std::endl;
385	59972	}
386
387	51794	static void print_config_cond(const char* str, bool cond = false)
388		{
389	51794	print_config(str, cond ? "yes" : "no");
390	51794	}
391
392	2726	void OptionsHandler::showConfiguration(const std::string& flag)
393		{
394	2726	std::cout << Configuration::about() << std::endl;
395
396	2726	print_config("version", Configuration::getVersionString());
397	2726	if (Configuration::isGitBuild())
398		{
399	2726	print_config("scm", Configuration::getGitInfo());
400		}
401		else
402		{
403		print_config_cond("scm", false);
404		}
405
406	2726	std::cout << std::endl;
407
408	2726	std::stringstream ss;
409	2726	ss << Configuration::getVersionString();
410	2726	print_config("library", ss.str());
411
412	2726	std::cout << std::endl;
413
414	2726	print_config_cond("debug code", Configuration::isDebugBuild());
415	2726	print_config_cond("statistics", Configuration::isStatisticsBuild());
416	2726	print_config_cond("tracing", Configuration::isTracingBuild());
417	2726	print_config_cond("dumping", Configuration::isDumpingBuild());
418	2726	print_config_cond("muzzled", Configuration::isMuzzledBuild());
419	2726	print_config_cond("assertions", Configuration::isAssertionBuild());
420	2726	print_config_cond("coverage", Configuration::isCoverageBuild());
421	2726	print_config_cond("profiling", Configuration::isProfilingBuild());
422	2726	print_config_cond("asan", Configuration::isAsanBuild());
423	2726	print_config_cond("ubsan", Configuration::isUbsanBuild());
424	2726	print_config_cond("tsan", Configuration::isTsanBuild());
425	2726	print_config_cond("competition", Configuration::isCompetitionBuild());
426
427	2726	std::cout << std::endl;
428
429	2726	print_config_cond("cln", Configuration::isBuiltWithCln());
430	2726	print_config_cond("glpk", Configuration::isBuiltWithGlpk());
431	2726	print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
432	2726	print_config_cond("gmp", Configuration::isBuiltWithGmp());
433	2726	print_config_cond("kissat", Configuration::isBuiltWithKissat());
434	2726	print_config_cond("poly", Configuration::isBuiltWithPoly());
435	2726	print_config_cond("editline", Configuration::isBuiltWithEditline());
436
437	2726	std::exit(0);
438		}
439
440		void OptionsHandler::showCopyright(const std::string& flag)
441		{
442		std::cout << Configuration::copyright() << std::endl;
443		std::exit(0);
444		}
445
446	1	void OptionsHandler::showVersion(const std::string& flag)
447		{
448	1	d_options->base.out << Configuration::about() << std::endl;
449	1	std::exit(0);
450		}
451
452		void OptionsHandler::showDebugTags(const std::string& flag)
453		{
454		if (!Configuration::isDebugBuild())
455		{
456		throw OptionException("debug tags not available in non-debug builds");
457		}
458		else if (!Configuration::isTracingBuild())
459		{
460		throw OptionException("debug tags not available in non-tracing builds");
461		}
462		printTags(Configuration::getDebugTags());
463		std::exit(0);
464		}
465
466		void OptionsHandler::showTraceTags(const std::string& flag)
467		{
468		if (!Configuration::isTracingBuild())
469		{
470		throw OptionException("trace tags not available in non-tracing build");
471		}
472		printTags(Configuration::getTraceTags());
473		std::exit(0);
474		}
475
476		} // namespace options
477	31125	} // namespace cvc5