cvc4-1.4
CVC4::Options Class Reference

#include <options.h>

Public Member Functions

 Options ()
 
 Options (const Options &options)
 
 ~Options ()
 
template<class T >
void set (T, const typename T::type &)
 Set the value of the given option. More...
 
template<class T >
const T::type & operator[] (T) const
 Get the value of the given option. More...
 
template<class T >
bool wasSetByUser (T) const
 Returns true iff the value of the given option was set by the user via a command-line option or SmtEngine::setOption(). More...
 
std::string getDescription () const
 Get a description of the command-line flags accepted by parseOptions. More...
 
std::vector< std::string > parseOptions (int argc, char *argv[]) throw (OptionException)
 Initialize the options based on the given command-line arguments. More...
 
SExpr getOptions () const throw ()
 Get the setting for all options. More...
 
template<>
void set (options::binary_name__option_t, const options::binary_name__option_t::type &x)
 
template<>
const options::binary_name__option_t::typeoperator[] (options::binary_name__option_t) const
 
template<>
bool wasSetByUser (options::binary_name__option_t) const
 
template<>
void assign (options::binary_name__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::in__option_t, const options::in__option_t::type &x)
 
template<>
const options::in__option_t::typeoperator[] (options::in__option_t) const
 
template<>
bool wasSetByUser (options::in__option_t) const
 
template<>
void assign (options::in__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::out__option_t, const options::out__option_t::type &x)
 
template<>
const options::out__option_t::typeoperator[] (options::out__option_t) const
 
template<>
bool wasSetByUser (options::out__option_t) const
 
template<>
void assign (options::out__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::err__option_t, const options::err__option_t::type &x)
 
template<>
const options::err__option_t::typeoperator[] (options::err__option_t) const
 
template<>
bool wasSetByUser (options::err__option_t) const
 
template<>
void assign (options::err__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::inputLanguage__option_t, const options::inputLanguage__option_t::type &x)
 
template<>
const options::inputLanguage__option_t::typeoperator[] (options::inputLanguage__option_t) const
 
template<>
bool wasSetByUser (options::inputLanguage__option_t) const
 
template<>
void assign (options::inputLanguage__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::outputLanguage__option_t, const options::outputLanguage__option_t::type &x)
 
template<>
const options::outputLanguage__option_t::typeoperator[] (options::outputLanguage__option_t) const
 
template<>
bool wasSetByUser (options::outputLanguage__option_t) const
 
template<>
void assign (options::outputLanguage__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::languageHelp__option_t, const options::languageHelp__option_t::type &x)
 
template<>
const options::languageHelp__option_t::typeoperator[] (options::languageHelp__option_t) const
 
template<>
bool wasSetByUser (options::languageHelp__option_t) const
 
template<>
void assignBool (options::languageHelp__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::verbosity__option_t, const options::verbosity__option_t::type &x)
 
template<>
const options::verbosity__option_t::typeoperator[] (options::verbosity__option_t) const
 
template<>
bool wasSetByUser (options::verbosity__option_t) const
 
template<>
void assign (options::verbosity__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::statistics__option_t::typeoperator[] (options::statistics__option_t) const
 
template<>
bool wasSetByUser (options::statistics__option_t) const
 
template<>
void assignBool (options::statistics__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::statsEveryQuery__option_t::typeoperator[] (options::statsEveryQuery__option_t) const
 
template<>
bool wasSetByUser (options::statsEveryQuery__option_t) const
 
template<>
void assignBool (options::statsEveryQuery__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::statsHideZeros__option_t::typeoperator[] (options::statsHideZeros__option_t) const
 
template<>
bool wasSetByUser (options::statsHideZeros__option_t) const
 
template<>
void assignBool (options::statsHideZeros__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::parseOnly__option_t, const options::parseOnly__option_t::type &x)
 
template<>
const options::parseOnly__option_t::typeoperator[] (options::parseOnly__option_t) const
 
template<>
bool wasSetByUser (options::parseOnly__option_t) const
 
template<>
void assignBool (options::parseOnly__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::preprocessOnly__option_t::typeoperator[] (options::preprocessOnly__option_t) const
 
template<>
bool wasSetByUser (options::preprocessOnly__option_t) const
 
template<>
void assignBool (options::preprocessOnly__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::printSuccess__option_t::typeoperator[] (options::printSuccess__option_t) const
 
template<>
bool wasSetByUser (options::printSuccess__option_t) const
 
template<>
void assignBool (options::printSuccess__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::satRandomFreq__option_t::typeoperator[] (options::satRandomFreq__option_t) const
 
template<>
bool wasSetByUser (options::satRandomFreq__option_t) const
 
template<>
void assign (options::satRandomFreq__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::satRandomSeed__option_t, const options::satRandomSeed__option_t::type &x)
 
template<>
const options::satRandomSeed__option_t::typeoperator[] (options::satRandomSeed__option_t) const
 
template<>
bool wasSetByUser (options::satRandomSeed__option_t) const
 
template<>
void assign (options::satRandomSeed__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::satVarDecay__option_t, const options::satVarDecay__option_t::type &x)
 
template<>
const options::satVarDecay__option_t::typeoperator[] (options::satVarDecay__option_t) const
 
template<>
bool wasSetByUser (options::satVarDecay__option_t) const
 
template<>
void assign (options::satVarDecay__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::satClauseDecay__option_t, const options::satClauseDecay__option_t::type &x)
 
template<>
const options::satClauseDecay__option_t::typeoperator[] (options::satClauseDecay__option_t) const
 
template<>
bool wasSetByUser (options::satClauseDecay__option_t) const
 
template<>
void assign (options::satClauseDecay__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::satRestartFirst__option_t::typeoperator[] (options::satRestartFirst__option_t) const
 
template<>
bool wasSetByUser (options::satRestartFirst__option_t) const
 
template<>
void assign (options::satRestartFirst__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::satRestartInc__option_t::typeoperator[] (options::satRestartInc__option_t) const
 
template<>
bool wasSetByUser (options::satRestartInc__option_t) const
 
template<>
void assign (options::satRestartInc__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::sat_refine_conflicts__option_t::typeoperator[] (options::sat_refine_conflicts__option_t) const
 
template<>
bool wasSetByUser (options::sat_refine_conflicts__option_t) const
 
template<>
void assignBool (options::sat_refine_conflicts__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::minisatUseElim__option_t, const options::minisatUseElim__option_t::type &x)
 
template<>
const options::minisatUseElim__option_t::typeoperator[] (options::minisatUseElim__option_t) const
 
template<>
bool wasSetByUser (options::minisatUseElim__option_t) const
 
template<>
void assignBool (options::minisatUseElim__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::minisatDumpDimacs__option_t::typeoperator[] (options::minisatDumpDimacs__option_t) const
 
template<>
bool wasSetByUser (options::minisatDumpDimacs__option_t) const
 
template<>
void assignBool (options::minisatDumpDimacs__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::modelFormatMode__option_t, const options::modelFormatMode__option_t::type &x)
 
template<>
const options::modelFormatMode__option_t::typeoperator[] (options::modelFormatMode__option_t) const
 
template<>
bool wasSetByUser (options::modelFormatMode__option_t) const
 
template<>
void assign (options::modelFormatMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::instFormatMode__option_t, const options::instFormatMode__option_t::type &x)
 
template<>
const options::instFormatMode__option_t::typeoperator[] (options::instFormatMode__option_t) const
 
template<>
bool wasSetByUser (options::instFormatMode__option_t) const
 
template<>
void assign (options::instFormatMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::forceLogic__option_t::typeoperator[] (options::forceLogic__option_t) const
 
template<>
bool wasSetByUser (options::forceLogic__option_t) const
 
template<>
void assign (options::forceLogic__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::simplificationMode__option_t, const options::simplificationMode__option_t::type &x)
 
template<>
const options::simplificationMode__option_t::typeoperator[] (options::simplificationMode__option_t) const
 
template<>
bool wasSetByUser (options::simplificationMode__option_t) const
 
template<>
void assign (options::simplificationMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::doStaticLearning__option_t::typeoperator[] (options::doStaticLearning__option_t) const
 
template<>
bool wasSetByUser (options::doStaticLearning__option_t) const
 
template<>
void assignBool (options::doStaticLearning__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::expandDefinitions__option_t::typeoperator[] (options::expandDefinitions__option_t) const
 
template<>
bool wasSetByUser (options::expandDefinitions__option_t) const
 
template<>
void assignBool (options::expandDefinitions__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::produceModels__option_t::typeoperator[] (options::produceModels__option_t) const
 
template<>
bool wasSetByUser (options::produceModels__option_t) const
 
template<>
void assignBool (options::produceModels__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::checkModels__option_t::typeoperator[] (options::checkModels__option_t) const
 
template<>
bool wasSetByUser (options::checkModels__option_t) const
 
template<>
void assignBool (options::checkModels__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::dumpModels__option_t::typeoperator[] (options::dumpModels__option_t) const
 
template<>
bool wasSetByUser (options::dumpModels__option_t) const
 
template<>
void assignBool (options::dumpModels__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::proof__option_t::typeoperator[] (options::proof__option_t) const
 
template<>
bool wasSetByUser (options::proof__option_t) const
 
template<>
void assignBool (options::proof__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::checkProofs__option_t::typeoperator[] (options::checkProofs__option_t) const
 
template<>
bool wasSetByUser (options::checkProofs__option_t) const
 
template<>
void assignBool (options::checkProofs__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::dumpProofs__option_t::typeoperator[] (options::dumpProofs__option_t) const
 
template<>
bool wasSetByUser (options::dumpProofs__option_t) const
 
template<>
void assignBool (options::dumpProofs__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::dumpInstantiations__option_t::typeoperator[] (options::dumpInstantiations__option_t) const
 
template<>
bool wasSetByUser (options::dumpInstantiations__option_t) const
 
template<>
void assignBool (options::dumpInstantiations__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::unsatCores__option_t::typeoperator[] (options::unsatCores__option_t) const
 
template<>
bool wasSetByUser (options::unsatCores__option_t) const
 
template<>
void assignBool (options::unsatCores__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::produceAssignments__option_t::typeoperator[] (options::produceAssignments__option_t) const
 
template<>
bool wasSetByUser (options::produceAssignments__option_t) const
 
template<>
void assignBool (options::produceAssignments__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::interactive__option_t, const options::interactive__option_t::type &x)
 
template<>
const options::interactive__option_t::typeoperator[] (options::interactive__option_t) const
 
template<>
bool wasSetByUser (options::interactive__option_t) const
 
template<>
void assignBool (options::interactive__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::doITESimp__option_t, const options::doITESimp__option_t::type &x)
 
template<>
const options::doITESimp__option_t::typeoperator[] (options::doITESimp__option_t) const
 
template<>
bool wasSetByUser (options::doITESimp__option_t) const
 
template<>
void assignBool (options::doITESimp__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::doITESimpOnRepeat__option_t, const options::doITESimpOnRepeat__option_t::type &x)
 
template<>
const options::doITESimpOnRepeat__option_t::typeoperator[] (options::doITESimpOnRepeat__option_t) const
 
template<>
bool wasSetByUser (options::doITESimpOnRepeat__option_t) const
 
template<>
void assignBool (options::doITESimpOnRepeat__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::simplifyWithCareEnabled__option_t, const options::simplifyWithCareEnabled__option_t::type &x)
 
template<>
const options::simplifyWithCareEnabled__option_t::typeoperator[] (options::simplifyWithCareEnabled__option_t) const
 
template<>
bool wasSetByUser (options::simplifyWithCareEnabled__option_t) const
 
template<>
void assignBool (options::simplifyWithCareEnabled__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::compressItes__option_t, const options::compressItes__option_t::type &x)
 
template<>
const options::compressItes__option_t::typeoperator[] (options::compressItes__option_t) const
 
template<>
bool wasSetByUser (options::compressItes__option_t) const
 
template<>
void assignBool (options::compressItes__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::unconstrainedSimp__option_t, const options::unconstrainedSimp__option_t::type &x)
 
template<>
const options::unconstrainedSimp__option_t::typeoperator[] (options::unconstrainedSimp__option_t) const
 
template<>
bool wasSetByUser (options::unconstrainedSimp__option_t) const
 
template<>
void assignBool (options::unconstrainedSimp__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::repeatSimp__option_t, const options::repeatSimp__option_t::type &x)
 
template<>
const options::repeatSimp__option_t::typeoperator[] (options::repeatSimp__option_t) const
 
template<>
bool wasSetByUser (options::repeatSimp__option_t) const
 
template<>
void assignBool (options::repeatSimp__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::zombieHuntThreshold__option_t::typeoperator[] (options::zombieHuntThreshold__option_t) const
 
template<>
bool wasSetByUser (options::zombieHuntThreshold__option_t) const
 
template<>
void assign (options::zombieHuntThreshold__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::sortInference__option_t, const options::sortInference__option_t::type &x)
 
template<>
const options::sortInference__option_t::typeoperator[] (options::sortInference__option_t) const
 
template<>
bool wasSetByUser (options::sortInference__option_t) const
 
template<>
void assignBool (options::sortInference__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::incrementalSolving__option_t::typeoperator[] (options::incrementalSolving__option_t) const
 
template<>
bool wasSetByUser (options::incrementalSolving__option_t) const
 
template<>
void assignBool (options::incrementalSolving__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::abstractValues__option_t::typeoperator[] (options::abstractValues__option_t) const
 
template<>
bool wasSetByUser (options::abstractValues__option_t) const
 
template<>
void assignBool (options::abstractValues__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::modelUninterpDtEnum__option_t::typeoperator[] (options::modelUninterpDtEnum__option_t) const
 
template<>
bool wasSetByUser (options::modelUninterpDtEnum__option_t) const
 
template<>
void assignBool (options::modelUninterpDtEnum__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::cumulativeMillisecondLimit__option_t::typeoperator[] (options::cumulativeMillisecondLimit__option_t) const
 
template<>
bool wasSetByUser (options::cumulativeMillisecondLimit__option_t) const
 
template<>
void assign (options::cumulativeMillisecondLimit__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::perCallMillisecondLimit__option_t::typeoperator[] (options::perCallMillisecondLimit__option_t) const
 
template<>
bool wasSetByUser (options::perCallMillisecondLimit__option_t) const
 
template<>
void assign (options::perCallMillisecondLimit__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::cumulativeResourceLimit__option_t::typeoperator[] (options::cumulativeResourceLimit__option_t) const
 
template<>
bool wasSetByUser (options::cumulativeResourceLimit__option_t) const
 
template<>
void assign (options::cumulativeResourceLimit__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::perCallResourceLimit__option_t::typeoperator[] (options::perCallResourceLimit__option_t) const
 
template<>
bool wasSetByUser (options::perCallResourceLimit__option_t) const
 
template<>
void assign (options::perCallResourceLimit__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::rewriteApplyToConst__option_t::typeoperator[] (options::rewriteApplyToConst__option_t) const
 
template<>
bool wasSetByUser (options::rewriteApplyToConst__option_t) const
 
template<>
void assignBool (options::rewriteApplyToConst__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::replayFilename__option_t::typeoperator[] (options::replayFilename__option_t) const
 
template<>
bool wasSetByUser (options::replayFilename__option_t) const
 
template<>
void assign (options::replayFilename__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::replayLog__option_t::typeoperator[] (options::replayLog__option_t) const
 
template<>
bool wasSetByUser (options::replayLog__option_t) const
 
template<>
void assign (options::replayLog__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::replayStream__option_t, const options::replayStream__option_t::type &x)
 
template<>
const options::replayStream__option_t::typeoperator[] (options::replayStream__option_t) const
 
template<>
bool wasSetByUser (options::replayStream__option_t) const
 
template<>
void assign (options::replayStream__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::lemmaInputChannel__option_t, const options::lemmaInputChannel__option_t::type &x)
 
template<>
const options::lemmaInputChannel__option_t::typeoperator[] (options::lemmaInputChannel__option_t) const
 
template<>
bool wasSetByUser (options::lemmaInputChannel__option_t) const
 
template<>
void assign (options::lemmaInputChannel__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::lemmaOutputChannel__option_t, const options::lemmaOutputChannel__option_t::type &x)
 
template<>
const options::lemmaOutputChannel__option_t::typeoperator[] (options::lemmaOutputChannel__option_t) const
 
template<>
bool wasSetByUser (options::lemmaOutputChannel__option_t) const
 
template<>
void assign (options::lemmaOutputChannel__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::forceNoLimitCpuWhileDump__option_t::typeoperator[] (options::forceNoLimitCpuWhileDump__option_t) const
 
template<>
bool wasSetByUser (options::forceNoLimitCpuWhileDump__option_t) const
 
template<>
void assignBool (options::forceNoLimitCpuWhileDump__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::defaultExprDepth__option_t::typeoperator[] (options::defaultExprDepth__option_t) const
 
template<>
bool wasSetByUser (options::defaultExprDepth__option_t) const
 
template<>
void assign (options::defaultExprDepth__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::defaultDagThresh__option_t::typeoperator[] (options::defaultDagThresh__option_t) const
 
template<>
bool wasSetByUser (options::defaultDagThresh__option_t) const
 
template<>
void assign (options::defaultDagThresh__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::earlyTypeChecking__option_t::typeoperator[] (options::earlyTypeChecking__option_t) const
 
template<>
bool wasSetByUser (options::earlyTypeChecking__option_t) const
 
template<>
void assignBool (options::earlyTypeChecking__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::typeChecking__option_t::typeoperator[] (options::typeChecking__option_t) const
 
template<>
bool wasSetByUser (options::typeChecking__option_t) const
 
template<>
void assignBool (options::typeChecking__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::biasedITERemoval__option_t::typeoperator[] (options::biasedITERemoval__option_t) const
 
template<>
bool wasSetByUser (options::biasedITERemoval__option_t) const
 
template<>
void assignBool (options::biasedITERemoval__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::strictParsing__option_t::typeoperator[] (options::strictParsing__option_t) const
 
template<>
bool wasSetByUser (options::strictParsing__option_t) const
 
template<>
void assignBool (options::strictParsing__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::memoryMap__option_t::typeoperator[] (options::memoryMap__option_t) const
 
template<>
bool wasSetByUser (options::memoryMap__option_t) const
 
template<>
void assignBool (options::memoryMap__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::semanticChecks__option_t::typeoperator[] (options::semanticChecks__option_t) const
 
template<>
bool wasSetByUser (options::semanticChecks__option_t) const
 
template<>
void assignBool (options::semanticChecks__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::filesystemAccess__option_t::typeoperator[] (options::filesystemAccess__option_t) const
 
template<>
bool wasSetByUser (options::filesystemAccess__option_t) const
 
template<>
void assignBool (options::filesystemAccess__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bitblastMode__option_t, const options::bitblastMode__option_t::type &x)
 
template<>
const options::bitblastMode__option_t::typeoperator[] (options::bitblastMode__option_t) const
 
template<>
bool wasSetByUser (options::bitblastMode__option_t) const
 
template<>
void assign (options::bitblastMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::bitvectorAig__option_t, const options::bitvectorAig__option_t::type &x)
 
template<>
const options::bitvectorAig__option_t::typeoperator[] (options::bitvectorAig__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorAig__option_t) const
 
template<>
void assignBool (options::bitvectorAig__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bitvectorAigSimplifications__option_t, const options::bitvectorAigSimplifications__option_t::type &x)
 
template<>
const options::bitvectorAigSimplifications__option_t::typeoperator[] (options::bitvectorAigSimplifications__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorAigSimplifications__option_t) const
 
template<>
void assign (options::bitvectorAigSimplifications__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::bitvectorPropagate__option_t, const options::bitvectorPropagate__option_t::type &x)
 
template<>
const options::bitvectorPropagate__option_t::typeoperator[] (options::bitvectorPropagate__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorPropagate__option_t) const
 
template<>
void assignBool (options::bitvectorPropagate__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bitvectorEqualitySolver__option_t, const options::bitvectorEqualitySolver__option_t::type &x)
 
template<>
const options::bitvectorEqualitySolver__option_t::typeoperator[] (options::bitvectorEqualitySolver__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorEqualitySolver__option_t) const
 
template<>
void assignBool (options::bitvectorEqualitySolver__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bitvectorEqualitySlicer__option_t, const options::bitvectorEqualitySlicer__option_t::type &x)
 
template<>
const options::bitvectorEqualitySlicer__option_t::typeoperator[] (options::bitvectorEqualitySlicer__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorEqualitySlicer__option_t) const
 
template<>
void assign (options::bitvectorEqualitySlicer__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::bitvectorInequalitySolver__option_t, const options::bitvectorInequalitySolver__option_t::type &x)
 
template<>
const options::bitvectorInequalitySolver__option_t::typeoperator[] (options::bitvectorInequalitySolver__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorInequalitySolver__option_t) const
 
template<>
void assignBool (options::bitvectorInequalitySolver__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bitvectorAlgebraicSolver__option_t, const options::bitvectorAlgebraicSolver__option_t::type &x)
 
template<>
const options::bitvectorAlgebraicSolver__option_t::typeoperator[] (options::bitvectorAlgebraicSolver__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorAlgebraicSolver__option_t) const
 
template<>
void assignBool (options::bitvectorAlgebraicSolver__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bitvectorAlgebraicBudget__option_t, const options::bitvectorAlgebraicBudget__option_t::type &x)
 
template<>
const options::bitvectorAlgebraicBudget__option_t::typeoperator[] (options::bitvectorAlgebraicBudget__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorAlgebraicBudget__option_t) const
 
template<>
void assign (options::bitvectorAlgebraicBudget__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::bitvectorToBool__option_t, const options::bitvectorToBool__option_t::type &x)
 
template<>
const options::bitvectorToBool__option_t::typeoperator[] (options::bitvectorToBool__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorToBool__option_t) const
 
template<>
void assignBool (options::bitvectorToBool__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::bitvectorDivByZeroConst__option_t::typeoperator[] (options::bitvectorDivByZeroConst__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorDivByZeroConst__option_t) const
 
template<>
void assignBool (options::bitvectorDivByZeroConst__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::bvAbstraction__option_t, const options::bvAbstraction__option_t::type &x)
 
template<>
const options::bvAbstraction__option_t::typeoperator[] (options::bvAbstraction__option_t) const
 
template<>
bool wasSetByUser (options::bvAbstraction__option_t) const
 
template<>
void assignBool (options::bvAbstraction__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::skolemizeArguments__option_t, const options::skolemizeArguments__option_t::type &x)
 
template<>
const options::skolemizeArguments__option_t::typeoperator[] (options::skolemizeArguments__option_t) const
 
template<>
bool wasSetByUser (options::skolemizeArguments__option_t) const
 
template<>
void assignBool (options::skolemizeArguments__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::bvNumFunc__option_t::typeoperator[] (options::bvNumFunc__option_t) const
 
template<>
bool wasSetByUser (options::bvNumFunc__option_t) const
 
template<>
void assign (options::bvNumFunc__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::bvEagerExplanations__option_t, const options::bvEagerExplanations__option_t::type &x)
 
template<>
const options::bvEagerExplanations__option_t::typeoperator[] (options::bvEagerExplanations__option_t) const
 
template<>
bool wasSetByUser (options::bvEagerExplanations__option_t) const
 
template<>
void assignBool (options::bvEagerExplanations__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::bitvectorQuickXplain__option_t::typeoperator[] (options::bitvectorQuickXplain__option_t) const
 
template<>
bool wasSetByUser (options::bitvectorQuickXplain__option_t) const
 
template<>
void assignBool (options::bitvectorQuickXplain__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::bvIntroducePow2__option_t::typeoperator[] (options::bvIntroducePow2__option_t) const
 
template<>
bool wasSetByUser (options::bvIntroducePow2__option_t) const
 
template<>
void assignBool (options::bvIntroducePow2__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::ufSymmetryBreaker__option_t, const options::ufSymmetryBreaker__option_t::type &x)
 
template<>
const options::ufSymmetryBreaker__option_t::typeoperator[] (options::ufSymmetryBreaker__option_t) const
 
template<>
bool wasSetByUser (options::ufSymmetryBreaker__option_t) const
 
template<>
void assignBool (options::ufSymmetryBreaker__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::condenseFunctionValues__option_t::typeoperator[] (options::condenseFunctionValues__option_t) const
 
template<>
bool wasSetByUser (options::condenseFunctionValues__option_t) const
 
template<>
void assignBool (options::condenseFunctionValues__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssRegions__option_t::typeoperator[] (options::ufssRegions__option_t) const
 
template<>
bool wasSetByUser (options::ufssRegions__option_t) const
 
template<>
void assignBool (options::ufssRegions__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssEagerSplits__option_t::typeoperator[] (options::ufssEagerSplits__option_t) const
 
template<>
bool wasSetByUser (options::ufssEagerSplits__option_t) const
 
template<>
void assignBool (options::ufssEagerSplits__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssTotality__option_t::typeoperator[] (options::ufssTotality__option_t) const
 
template<>
bool wasSetByUser (options::ufssTotality__option_t) const
 
template<>
void assignBool (options::ufssTotality__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssTotalityLimited__option_t::typeoperator[] (options::ufssTotalityLimited__option_t) const
 
template<>
bool wasSetByUser (options::ufssTotalityLimited__option_t) const
 
template<>
void assign (options::ufssTotalityLimited__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::ufssTotalitySymBreak__option_t::typeoperator[] (options::ufssTotalitySymBreak__option_t) const
 
template<>
bool wasSetByUser (options::ufssTotalitySymBreak__option_t) const
 
template<>
void assignBool (options::ufssTotalitySymBreak__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssAbortCardinality__option_t::typeoperator[] (options::ufssAbortCardinality__option_t) const
 
template<>
bool wasSetByUser (options::ufssAbortCardinality__option_t) const
 
template<>
void assign (options::ufssAbortCardinality__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::ufssExplainedCliques__option_t::typeoperator[] (options::ufssExplainedCliques__option_t) const
 
template<>
bool wasSetByUser (options::ufssExplainedCliques__option_t) const
 
template<>
void assignBool (options::ufssExplainedCliques__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssSimpleCliques__option_t::typeoperator[] (options::ufssSimpleCliques__option_t) const
 
template<>
bool wasSetByUser (options::ufssSimpleCliques__option_t) const
 
template<>
void assignBool (options::ufssSimpleCliques__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssDiseqPropagation__option_t::typeoperator[] (options::ufssDiseqPropagation__option_t) const
 
template<>
bool wasSetByUser (options::ufssDiseqPropagation__option_t) const
 
template<>
void assignBool (options::ufssDiseqPropagation__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssMinimalModel__option_t::typeoperator[] (options::ufssMinimalModel__option_t) const
 
template<>
bool wasSetByUser (options::ufssMinimalModel__option_t) const
 
template<>
void assignBool (options::ufssMinimalModel__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssCliqueSplits__option_t::typeoperator[] (options::ufssCliqueSplits__option_t) const
 
template<>
bool wasSetByUser (options::ufssCliqueSplits__option_t) const
 
template<>
void assignBool (options::ufssCliqueSplits__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssSymBreak__option_t::typeoperator[] (options::ufssSymBreak__option_t) const
 
template<>
bool wasSetByUser (options::ufssSymBreak__option_t) const
 
template<>
void assignBool (options::ufssSymBreak__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::ufssFairness__option_t::typeoperator[] (options::ufssFairness__option_t) const
 
template<>
bool wasSetByUser (options::ufssFairness__option_t) const
 
template<>
void assignBool (options::ufssFairness__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::stringExp__option_t, const options::stringExp__option_t::type &x)
 
template<>
const options::stringExp__option_t::typeoperator[] (options::stringExp__option_t) const
 
template<>
bool wasSetByUser (options::stringExp__option_t) const
 
template<>
void assignBool (options::stringExp__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::stringLB__option_t::typeoperator[] (options::stringLB__option_t) const
 
template<>
bool wasSetByUser (options::stringLB__option_t) const
 
template<>
void assign (options::stringLB__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::stringFMF__option_t, const options::stringFMF__option_t::type &x)
 
template<>
const options::stringFMF__option_t::typeoperator[] (options::stringFMF__option_t) const
 
template<>
bool wasSetByUser (options::stringFMF__option_t) const
 
template<>
void assignBool (options::stringFMF__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::stringEIT__option_t::typeoperator[] (options::stringEIT__option_t) const
 
template<>
bool wasSetByUser (options::stringEIT__option_t) const
 
template<>
void assignBool (options::stringEIT__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::stringOpt1__option_t::typeoperator[] (options::stringOpt1__option_t) const
 
template<>
bool wasSetByUser (options::stringOpt1__option_t) const
 
template<>
void assignBool (options::stringOpt1__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::stringOpt2__option_t::typeoperator[] (options::stringOpt2__option_t) const
 
template<>
bool wasSetByUser (options::stringOpt2__option_t) const
 
template<>
void assignBool (options::stringOpt2__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::stringCharCardinality__option_t::typeoperator[] (options::stringCharCardinality__option_t) const
 
template<>
bool wasSetByUser (options::stringCharCardinality__option_t) const
 
template<>
void assign (options::stringCharCardinality__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::miniscopeQuant__option_t::typeoperator[] (options::miniscopeQuant__option_t) const
 
template<>
bool wasSetByUser (options::miniscopeQuant__option_t) const
 
template<>
void assignBool (options::miniscopeQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::miniscopeQuantFreeVar__option_t::typeoperator[] (options::miniscopeQuantFreeVar__option_t) const
 
template<>
bool wasSetByUser (options::miniscopeQuantFreeVar__option_t) const
 
template<>
void assignBool (options::miniscopeQuantFreeVar__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::prenexQuant__option_t::typeoperator[] (options::prenexQuant__option_t) const
 
template<>
bool wasSetByUser (options::prenexQuant__option_t) const
 
template<>
void assignBool (options::prenexQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::varElimQuant__option_t::typeoperator[] (options::varElimQuant__option_t) const
 
template<>
bool wasSetByUser (options::varElimQuant__option_t) const
 
template<>
void assignBool (options::varElimQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::simpleIteLiftQuant__option_t::typeoperator[] (options::simpleIteLiftQuant__option_t) const
 
template<>
bool wasSetByUser (options::simpleIteLiftQuant__option_t) const
 
template<>
void assignBool (options::simpleIteLiftQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::cnfQuant__option_t::typeoperator[] (options::cnfQuant__option_t) const
 
template<>
bool wasSetByUser (options::cnfQuant__option_t) const
 
template<>
void assignBool (options::cnfQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::nnfQuant__option_t::typeoperator[] (options::nnfQuant__option_t) const
 
template<>
bool wasSetByUser (options::nnfQuant__option_t) const
 
template<>
void assignBool (options::nnfQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::clauseSplit__option_t::typeoperator[] (options::clauseSplit__option_t) const
 
template<>
bool wasSetByUser (options::clauseSplit__option_t) const
 
template<>
void assignBool (options::clauseSplit__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::preSkolemQuant__option_t, const options::preSkolemQuant__option_t::type &x)
 
template<>
const options::preSkolemQuant__option_t::typeoperator[] (options::preSkolemQuant__option_t) const
 
template<>
bool wasSetByUser (options::preSkolemQuant__option_t) const
 
template<>
void assignBool (options::preSkolemQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::aggressiveMiniscopeQuant__option_t::typeoperator[] (options::aggressiveMiniscopeQuant__option_t) const
 
template<>
bool wasSetByUser (options::aggressiveMiniscopeQuant__option_t) const
 
template<>
void assignBool (options::aggressiveMiniscopeQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::macrosQuant__option_t::typeoperator[] (options::macrosQuant__option_t) const
 
template<>
bool wasSetByUser (options::macrosQuant__option_t) const
 
template<>
void assignBool (options::macrosQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::foPropQuant__option_t::typeoperator[] (options::foPropQuant__option_t) const
 
template<>
bool wasSetByUser (options::foPropQuant__option_t) const
 
template<>
void assignBool (options::foPropQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::smartTriggers__option_t::typeoperator[] (options::smartTriggers__option_t) const
 
template<>
bool wasSetByUser (options::smartTriggers__option_t) const
 
template<>
void assignBool (options::smartTriggers__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::relevantTriggers__option_t::typeoperator[] (options::relevantTriggers__option_t) const
 
template<>
bool wasSetByUser (options::relevantTriggers__option_t) const
 
template<>
void assignBool (options::relevantTriggers__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::relationalTriggers__option_t::typeoperator[] (options::relationalTriggers__option_t) const
 
template<>
bool wasSetByUser (options::relationalTriggers__option_t) const
 
template<>
void assignBool (options::relationalTriggers__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::registerQuantBodyTerms__option_t::typeoperator[] (options::registerQuantBodyTerms__option_t) const
 
template<>
bool wasSetByUser (options::registerQuantBodyTerms__option_t) const
 
template<>
void assignBool (options::registerQuantBodyTerms__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::instWhenMode__option_t, const options::instWhenMode__option_t::type &x)
 
template<>
const options::instWhenMode__option_t::typeoperator[] (options::instWhenMode__option_t) const
 
template<>
bool wasSetByUser (options::instWhenMode__option_t) const
 
template<>
void assign (options::instWhenMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::instMaxLevel__option_t::typeoperator[] (options::instMaxLevel__option_t) const
 
template<>
bool wasSetByUser (options::instMaxLevel__option_t) const
 
template<>
void assign (options::instMaxLevel__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::eagerInstQuant__option_t::typeoperator[] (options::eagerInstQuant__option_t) const
 
template<>
bool wasSetByUser (options::eagerInstQuant__option_t) const
 
template<>
void assignBool (options::eagerInstQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fullSaturateQuant__option_t::typeoperator[] (options::fullSaturateQuant__option_t) const
 
template<>
bool wasSetByUser (options::fullSaturateQuant__option_t) const
 
template<>
void assignBool (options::fullSaturateQuant__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::literalMatchMode__option_t::typeoperator[] (options::literalMatchMode__option_t) const
 
template<>
bool wasSetByUser (options::literalMatchMode__option_t) const
 
template<>
void assign (options::literalMatchMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::cbqi__option_t, const options::cbqi__option_t::type &x)
 
template<>
const options::cbqi__option_t::typeoperator[] (options::cbqi__option_t) const
 
template<>
bool wasSetByUser (options::cbqi__option_t) const
 
template<>
void assignBool (options::cbqi__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::recurseCbqi__option_t::typeoperator[] (options::recurseCbqi__option_t) const
 
template<>
bool wasSetByUser (options::recurseCbqi__option_t) const
 
template<>
void assignBool (options::recurseCbqi__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::userPatternsQuant__option_t::typeoperator[] (options::userPatternsQuant__option_t) const
 
template<>
bool wasSetByUser (options::userPatternsQuant__option_t) const
 
template<>
void assign (options::userPatternsQuant__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::flipDecision__option_t::typeoperator[] (options::flipDecision__option_t) const
 
template<>
bool wasSetByUser (options::flipDecision__option_t) const
 
template<>
void assignBool (options::flipDecision__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::internalReps__option_t::typeoperator[] (options::internalReps__option_t) const
 
template<>
bool wasSetByUser (options::internalReps__option_t) const
 
template<>
void assignBool (options::internalReps__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::finiteModelFind__option_t, const options::finiteModelFind__option_t::type &x)
 
template<>
const options::finiteModelFind__option_t::typeoperator[] (options::finiteModelFind__option_t) const
 
template<>
bool wasSetByUser (options::finiteModelFind__option_t) const
 
template<>
void assignBool (options::finiteModelFind__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::mbqiMode__option_t, const options::mbqiMode__option_t::type &x)
 
template<>
const options::mbqiMode__option_t::typeoperator[] (options::mbqiMode__option_t) const
 
template<>
bool wasSetByUser (options::mbqiMode__option_t) const
 
template<>
void assign (options::mbqiMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::fmfOneInstPerRound__option_t::typeoperator[] (options::fmfOneInstPerRound__option_t) const
 
template<>
bool wasSetByUser (options::fmfOneInstPerRound__option_t) const
 
template<>
void assignBool (options::fmfOneInstPerRound__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fmfOneQuantPerRound__option_t::typeoperator[] (options::fmfOneQuantPerRound__option_t) const
 
template<>
bool wasSetByUser (options::fmfOneQuantPerRound__option_t) const
 
template<>
void assignBool (options::fmfOneQuantPerRound__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fmfInstEngine__option_t::typeoperator[] (options::fmfInstEngine__option_t) const
 
template<>
bool wasSetByUser (options::fmfInstEngine__option_t) const
 
template<>
void assignBool (options::fmfInstEngine__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fmfInstGen__option_t::typeoperator[] (options::fmfInstGen__option_t) const
 
template<>
bool wasSetByUser (options::fmfInstGen__option_t) const
 
template<>
void assignBool (options::fmfInstGen__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fmfInstGenOneQuantPerRound__option_t::typeoperator[] (options::fmfInstGenOneQuantPerRound__option_t) const
 
template<>
bool wasSetByUser (options::fmfInstGenOneQuantPerRound__option_t) const
 
template<>
void assignBool (options::fmfInstGenOneQuantPerRound__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fmfFreshDistConst__option_t::typeoperator[] (options::fmfFreshDistConst__option_t) const
 
template<>
bool wasSetByUser (options::fmfFreshDistConst__option_t) const
 
template<>
void assignBool (options::fmfFreshDistConst__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::fmfFmcSimple__option_t::typeoperator[] (options::fmfFmcSimple__option_t) const
 
template<>
bool wasSetByUser (options::fmfFmcSimple__option_t) const
 
template<>
void assignBool (options::fmfFmcSimple__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::fmfBoundInt__option_t, const options::fmfBoundInt__option_t::type &x)
 
template<>
const options::fmfBoundInt__option_t::typeoperator[] (options::fmfBoundInt__option_t) const
 
template<>
bool wasSetByUser (options::fmfBoundInt__option_t) const
 
template<>
void assignBool (options::fmfBoundInt__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::fmfBoundIntLazy__option_t, const options::fmfBoundIntLazy__option_t::type &x)
 
template<>
const options::fmfBoundIntLazy__option_t::typeoperator[] (options::fmfBoundIntLazy__option_t) const
 
template<>
bool wasSetByUser (options::fmfBoundIntLazy__option_t) const
 
template<>
void assignBool (options::fmfBoundIntLazy__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::axiomInstMode__option_t::typeoperator[] (options::axiomInstMode__option_t) const
 
template<>
bool wasSetByUser (options::axiomInstMode__option_t) const
 
template<>
void assign (options::axiomInstMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::quantConflictFind__option_t, const options::quantConflictFind__option_t::type &x)
 
template<>
const options::quantConflictFind__option_t::typeoperator[] (options::quantConflictFind__option_t) const
 
template<>
bool wasSetByUser (options::quantConflictFind__option_t) const
 
template<>
void assignBool (options::quantConflictFind__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::qcfMode__option_t::typeoperator[] (options::qcfMode__option_t) const
 
template<>
bool wasSetByUser (options::qcfMode__option_t) const
 
template<>
void assign (options::qcfMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::qcfWhenMode__option_t::typeoperator[] (options::qcfWhenMode__option_t) const
 
template<>
bool wasSetByUser (options::qcfWhenMode__option_t) const
 
template<>
void assign (options::qcfWhenMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::qcfTConstraint__option_t, const options::qcfTConstraint__option_t::type &x)
 
template<>
const options::qcfTConstraint__option_t::typeoperator[] (options::qcfTConstraint__option_t) const
 
template<>
bool wasSetByUser (options::qcfTConstraint__option_t) const
 
template<>
void assignBool (options::qcfTConstraint__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::quantRewriteRules__option_t::typeoperator[] (options::quantRewriteRules__option_t) const
 
template<>
bool wasSetByUser (options::quantRewriteRules__option_t) const
 
template<>
void assignBool (options::quantRewriteRules__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::rrOneInstPerRound__option_t::typeoperator[] (options::rrOneInstPerRound__option_t) const
 
template<>
bool wasSetByUser (options::rrOneInstPerRound__option_t) const
 
template<>
void assignBool (options::rrOneInstPerRound__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::dtStcInduction__option_t::typeoperator[] (options::dtStcInduction__option_t) const
 
template<>
bool wasSetByUser (options::dtStcInduction__option_t) const
 
template<>
void assignBool (options::dtStcInduction__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::booleanTermConversionMode__option_t::typeoperator[] (options::booleanTermConversionMode__option_t) const
 
template<>
bool wasSetByUser (options::booleanTermConversionMode__option_t) const
 
template<>
void assign (options::booleanTermConversionMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::setsPropagate__option_t::typeoperator[] (options::setsPropagate__option_t) const
 
template<>
bool wasSetByUser (options::setsPropagate__option_t) const
 
template<>
void assignBool (options::setsPropagate__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::setsEagerLemmas__option_t::typeoperator[] (options::setsEagerLemmas__option_t) const
 
template<>
bool wasSetByUser (options::setsEagerLemmas__option_t) const
 
template<>
void assignBool (options::setsEagerLemmas__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::dtRewriteErrorSel__option_t::typeoperator[] (options::dtRewriteErrorSel__option_t) const
 
template<>
bool wasSetByUser (options::dtRewriteErrorSel__option_t) const
 
template<>
void assignBool (options::dtRewriteErrorSel__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::dtForceAssignment__option_t, const options::dtForceAssignment__option_t::type &x)
 
template<>
const options::dtForceAssignment__option_t::typeoperator[] (options::dtForceAssignment__option_t) const
 
template<>
bool wasSetByUser (options::dtForceAssignment__option_t) const
 
template<>
void assignBool (options::dtForceAssignment__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arraysOptimizeLinear__option_t, const options::arraysOptimizeLinear__option_t::type &x)
 
template<>
const options::arraysOptimizeLinear__option_t::typeoperator[] (options::arraysOptimizeLinear__option_t) const
 
template<>
bool wasSetByUser (options::arraysOptimizeLinear__option_t) const
 
template<>
void assignBool (options::arraysOptimizeLinear__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arraysLazyRIntro1__option_t, const options::arraysLazyRIntro1__option_t::type &x)
 
template<>
const options::arraysLazyRIntro1__option_t::typeoperator[] (options::arraysLazyRIntro1__option_t) const
 
template<>
bool wasSetByUser (options::arraysLazyRIntro1__option_t) const
 
template<>
void assignBool (options::arraysLazyRIntro1__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arraysModelBased__option_t, const options::arraysModelBased__option_t::type &x)
 
template<>
const options::arraysModelBased__option_t::typeoperator[] (options::arraysModelBased__option_t) const
 
template<>
bool wasSetByUser (options::arraysModelBased__option_t) const
 
template<>
void assignBool (options::arraysModelBased__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arraysEagerIndexSplitting__option_t, const options::arraysEagerIndexSplitting__option_t::type &x)
 
template<>
const options::arraysEagerIndexSplitting__option_t::typeoperator[] (options::arraysEagerIndexSplitting__option_t) const
 
template<>
bool wasSetByUser (options::arraysEagerIndexSplitting__option_t) const
 
template<>
void assignBool (options::arraysEagerIndexSplitting__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arraysEagerLemmas__option_t, const options::arraysEagerLemmas__option_t::type &x)
 
template<>
const options::arraysEagerLemmas__option_t::typeoperator[] (options::arraysEagerLemmas__option_t) const
 
template<>
bool wasSetByUser (options::arraysEagerLemmas__option_t) const
 
template<>
void assignBool (options::arraysEagerLemmas__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::idlRewriteEq__option_t, const options::idlRewriteEq__option_t::type &x)
 
template<>
const options::idlRewriteEq__option_t::typeoperator[] (options::idlRewriteEq__option_t) const
 
template<>
bool wasSetByUser (options::idlRewriteEq__option_t) const
 
template<>
void assignBool (options::idlRewriteEq__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::theoryOfMode__option_t, const options::theoryOfMode__option_t::type &x)
 
template<>
const options::theoryOfMode__option_t::typeoperator[] (options::theoryOfMode__option_t) const
 
template<>
bool wasSetByUser (options::theoryOfMode__option_t) const
 
template<>
void assign (options::theoryOfMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::theoryAlternates__option_t, const options::theoryAlternates__option_t::type &x)
 
template<>
const options::theoryAlternates__option_t::typeoperator[] (options::theoryAlternates__option_t) const
 
template<>
bool wasSetByUser (options::theoryAlternates__option_t) const
 
template<>
void assign (options::theoryAlternates__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::arithUnateLemmaMode__option_t::typeoperator[] (options::arithUnateLemmaMode__option_t) const
 
template<>
bool wasSetByUser (options::arithUnateLemmaMode__option_t) const
 
template<>
void assign (options::arithUnateLemmaMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::arithPropagationMode__option_t::typeoperator[] (options::arithPropagationMode__option_t) const
 
template<>
bool wasSetByUser (options::arithPropagationMode__option_t) const
 
template<>
void assign (options::arithPropagationMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::arithHeuristicPivots__option_t, const options::arithHeuristicPivots__option_t::type &x)
 
template<>
const options::arithHeuristicPivots__option_t::typeoperator[] (options::arithHeuristicPivots__option_t) const
 
template<>
bool wasSetByUser (options::arithHeuristicPivots__option_t) const
 
template<>
void assign (options::arithHeuristicPivots__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::arithStandardCheckVarOrderPivots__option_t, const options::arithStandardCheckVarOrderPivots__option_t::type &x)
 
template<>
const options::arithStandardCheckVarOrderPivots__option_t::typeoperator[] (options::arithStandardCheckVarOrderPivots__option_t) const
 
template<>
bool wasSetByUser (options::arithStandardCheckVarOrderPivots__option_t) const
 
template<>
void assign (options::arithStandardCheckVarOrderPivots__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::arithErrorSelectionRule__option_t::typeoperator[] (options::arithErrorSelectionRule__option_t) const
 
template<>
bool wasSetByUser (options::arithErrorSelectionRule__option_t) const
 
template<>
void assign (options::arithErrorSelectionRule__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::arithSimplexCheckPeriod__option_t::typeoperator[] (options::arithSimplexCheckPeriod__option_t) const
 
template<>
bool wasSetByUser (options::arithSimplexCheckPeriod__option_t) const
 
template<>
void assign (options::arithSimplexCheckPeriod__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::arithPivotThreshold__option_t, const options::arithPivotThreshold__option_t::type &x)
 
template<>
const options::arithPivotThreshold__option_t::typeoperator[] (options::arithPivotThreshold__option_t) const
 
template<>
bool wasSetByUser (options::arithPivotThreshold__option_t) const
 
template<>
void assign (options::arithPivotThreshold__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::arithPropagateMaxLength__option_t::typeoperator[] (options::arithPropagateMaxLength__option_t) const
 
template<>
bool wasSetByUser (options::arithPropagateMaxLength__option_t) const
 
template<>
void assign (options::arithPropagateMaxLength__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::arithDioSolver__option_t::typeoperator[] (options::arithDioSolver__option_t) const
 
template<>
bool wasSetByUser (options::arithDioSolver__option_t) const
 
template<>
void assignBool (options::arithDioSolver__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arithRewriteEq__option_t, const options::arithRewriteEq__option_t::type &x)
 
template<>
const options::arithRewriteEq__option_t::typeoperator[] (options::arithRewriteEq__option_t) const
 
template<>
bool wasSetByUser (options::arithRewriteEq__option_t) const
 
template<>
void assignBool (options::arithRewriteEq__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::arithMLTrick__option_t::typeoperator[] (options::arithMLTrick__option_t) const
 
template<>
bool wasSetByUser (options::arithMLTrick__option_t) const
 
template<>
void assignBool (options::arithMLTrick__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::arithMLTrickSubstitutions__option_t::typeoperator[] (options::arithMLTrickSubstitutions__option_t) const
 
template<>
bool wasSetByUser (options::arithMLTrickSubstitutions__option_t) const
 
template<>
void assign (options::arithMLTrickSubstitutions__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::doCutAllBounded__option_t, const options::doCutAllBounded__option_t::type &x)
 
template<>
const options::doCutAllBounded__option_t::typeoperator[] (options::doCutAllBounded__option_t) const
 
template<>
bool wasSetByUser (options::doCutAllBounded__option_t) const
 
template<>
void assignBool (options::doCutAllBounded__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::maxCutsInContext__option_t::typeoperator[] (options::maxCutsInContext__option_t) const
 
template<>
bool wasSetByUser (options::maxCutsInContext__option_t) const
 
template<>
void assign (options::maxCutsInContext__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::revertArithModels__option_t::typeoperator[] (options::revertArithModels__option_t) const
 
template<>
bool wasSetByUser (options::revertArithModels__option_t) const
 
template<>
void assignBool (options::revertArithModels__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::havePenalties__option_t, const options::havePenalties__option_t::type &x)
 
template<>
const options::havePenalties__option_t::typeoperator[] (options::havePenalties__option_t) const
 
template<>
bool wasSetByUser (options::havePenalties__option_t) const
 
template<>
void assignBool (options::havePenalties__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::useFC__option_t, const options::useFC__option_t::type &x)
 
template<>
const options::useFC__option_t::typeoperator[] (options::useFC__option_t) const
 
template<>
bool wasSetByUser (options::useFC__option_t) const
 
template<>
void assignBool (options::useFC__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::useSOI__option_t, const options::useSOI__option_t::type &x)
 
template<>
const options::useSOI__option_t::typeoperator[] (options::useSOI__option_t) const
 
template<>
bool wasSetByUser (options::useSOI__option_t) const
 
template<>
void assignBool (options::useSOI__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::restrictedPivots__option_t, const options::restrictedPivots__option_t::type &x)
 
template<>
const options::restrictedPivots__option_t::typeoperator[] (options::restrictedPivots__option_t) const
 
template<>
bool wasSetByUser (options::restrictedPivots__option_t) const
 
template<>
void assignBool (options::restrictedPivots__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::collectPivots__option_t, const options::collectPivots__option_t::type &x)
 
template<>
const options::collectPivots__option_t::typeoperator[] (options::collectPivots__option_t) const
 
template<>
bool wasSetByUser (options::collectPivots__option_t) const
 
template<>
void assignBool (options::collectPivots__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::useApprox__option_t, const options::useApprox__option_t::type &x)
 
template<>
const options::useApprox__option_t::typeoperator[] (options::useApprox__option_t) const
 
template<>
bool wasSetByUser (options::useApprox__option_t) const
 
template<>
void assignBool (options::useApprox__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::maxApproxDepth__option_t, const options::maxApproxDepth__option_t::type &x)
 
template<>
const options::maxApproxDepth__option_t::typeoperator[] (options::maxApproxDepth__option_t) const
 
template<>
bool wasSetByUser (options::maxApproxDepth__option_t) const
 
template<>
void assign (options::maxApproxDepth__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::exportDioDecompositions__option_t, const options::exportDioDecompositions__option_t::type &x)
 
template<>
const options::exportDioDecompositions__option_t::typeoperator[] (options::exportDioDecompositions__option_t) const
 
template<>
bool wasSetByUser (options::exportDioDecompositions__option_t) const
 
template<>
void assignBool (options::exportDioDecompositions__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::newProp__option_t, const options::newProp__option_t::type &x)
 
template<>
const options::newProp__option_t::typeoperator[] (options::newProp__option_t) const
 
template<>
bool wasSetByUser (options::newProp__option_t) const
 
template<>
void assignBool (options::newProp__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::arithPropAsLemmaLength__option_t, const options::arithPropAsLemmaLength__option_t::type &x)
 
template<>
const options::arithPropAsLemmaLength__option_t::typeoperator[] (options::arithPropAsLemmaLength__option_t) const
 
template<>
bool wasSetByUser (options::arithPropAsLemmaLength__option_t) const
 
template<>
void assign (options::arithPropAsLemmaLength__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::soiQuickExplain__option_t, const options::soiQuickExplain__option_t::type &x)
 
template<>
const options::soiQuickExplain__option_t::typeoperator[] (options::soiQuickExplain__option_t) const
 
template<>
bool wasSetByUser (options::soiQuickExplain__option_t) const
 
template<>
void assignBool (options::soiQuickExplain__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
void set (options::rewriteDivk__option_t, const options::rewriteDivk__option_t::type &x)
 
template<>
const options::rewriteDivk__option_t::typeoperator[] (options::rewriteDivk__option_t) const
 
template<>
bool wasSetByUser (options::rewriteDivk__option_t) const
 
template<>
void assignBool (options::rewriteDivk__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::trySolveIntStandardEffort__option_t::typeoperator[] (options::trySolveIntStandardEffort__option_t) const
 
template<>
bool wasSetByUser (options::trySolveIntStandardEffort__option_t) const
 
template<>
void assignBool (options::trySolveIntStandardEffort__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::replayFailureLemma__option_t::typeoperator[] (options::replayFailureLemma__option_t) const
 
template<>
bool wasSetByUser (options::replayFailureLemma__option_t) const
 
template<>
void assignBool (options::replayFailureLemma__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::dioSolverTurns__option_t::typeoperator[] (options::dioSolverTurns__option_t) const
 
template<>
bool wasSetByUser (options::dioSolverTurns__option_t) const
 
template<>
void assign (options::dioSolverTurns__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::rrTurns__option_t::typeoperator[] (options::rrTurns__option_t) const
 
template<>
bool wasSetByUser (options::rrTurns__option_t) const
 
template<>
void assign (options::rrTurns__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::dioRepeat__option_t::typeoperator[] (options::dioRepeat__option_t) const
 
template<>
bool wasSetByUser (options::dioRepeat__option_t) const
 
template<>
void assignBool (options::dioRepeat__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::replayEarlyCloseDepths__option_t::typeoperator[] (options::replayEarlyCloseDepths__option_t) const
 
template<>
bool wasSetByUser (options::replayEarlyCloseDepths__option_t) const
 
template<>
void assign (options::replayEarlyCloseDepths__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::replayFailurePenalty__option_t::typeoperator[] (options::replayFailurePenalty__option_t) const
 
template<>
bool wasSetByUser (options::replayFailurePenalty__option_t) const
 
template<>
void assign (options::replayFailurePenalty__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::replayNumericFailurePenalty__option_t::typeoperator[] (options::replayNumericFailurePenalty__option_t) const
 
template<>
bool wasSetByUser (options::replayNumericFailurePenalty__option_t) const
 
template<>
void assign (options::replayNumericFailurePenalty__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::replayRejectCutSize__option_t::typeoperator[] (options::replayRejectCutSize__option_t) const
 
template<>
bool wasSetByUser (options::replayRejectCutSize__option_t) const
 
template<>
void assign (options::replayRejectCutSize__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::lemmaRejectCutSize__option_t::typeoperator[] (options::lemmaRejectCutSize__option_t) const
 
template<>
bool wasSetByUser (options::lemmaRejectCutSize__option_t) const
 
template<>
void assign (options::lemmaRejectCutSize__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::soiApproxMajorFailure__option_t::typeoperator[] (options::soiApproxMajorFailure__option_t) const
 
template<>
bool wasSetByUser (options::soiApproxMajorFailure__option_t) const
 
template<>
void assign (options::soiApproxMajorFailure__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::soiApproxMajorFailurePen__option_t::typeoperator[] (options::soiApproxMajorFailurePen__option_t) const
 
template<>
bool wasSetByUser (options::soiApproxMajorFailurePen__option_t) const
 
template<>
void assign (options::soiApproxMajorFailurePen__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::soiApproxMinorFailure__option_t::typeoperator[] (options::soiApproxMinorFailure__option_t) const
 
template<>
bool wasSetByUser (options::soiApproxMinorFailure__option_t) const
 
template<>
void assign (options::soiApproxMinorFailure__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::soiApproxMinorFailurePen__option_t::typeoperator[] (options::soiApproxMinorFailurePen__option_t) const
 
template<>
bool wasSetByUser (options::soiApproxMinorFailurePen__option_t) const
 
template<>
void assign (options::soiApproxMinorFailurePen__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::ppAssertMaxSubSize__option_t::typeoperator[] (options::ppAssertMaxSubSize__option_t) const
 
template<>
bool wasSetByUser (options::ppAssertMaxSubSize__option_t) const
 
template<>
void assign (options::ppAssertMaxSubSize__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::maxReplayTree__option_t::typeoperator[] (options::maxReplayTree__option_t) const
 
template<>
bool wasSetByUser (options::maxReplayTree__option_t) const
 
template<>
void assign (options::maxReplayTree__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::pbRewrites__option_t::typeoperator[] (options::pbRewrites__option_t) const
 
template<>
bool wasSetByUser (options::pbRewrites__option_t) const
 
template<>
void assignBool (options::pbRewrites__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::pbRewriteThreshold__option_t::typeoperator[] (options::pbRewriteThreshold__option_t) const
 
template<>
bool wasSetByUser (options::pbRewriteThreshold__option_t) const
 
template<>
void assign (options::pbRewriteThreshold__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::decisionMode__option_t, const options::decisionMode__option_t::type &x)
 
template<>
const options::decisionMode__option_t::typeoperator[] (options::decisionMode__option_t) const
 
template<>
bool wasSetByUser (options::decisionMode__option_t) const
 
template<>
void assign (options::decisionMode__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::decisionStopOnly__option_t, const options::decisionStopOnly__option_t::type &x)
 
template<>
const options::decisionStopOnly__option_t::typeoperator[] (options::decisionStopOnly__option_t) const
 
template<>
bool wasSetByUser (options::decisionStopOnly__option_t) const
 
template<>
void assignBool (options::decisionStopOnly__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::decisionThreshold__option_t::typeoperator[] (options::decisionThreshold__option_t) const
 
template<>
bool wasSetByUser (options::decisionThreshold__option_t) const
 
template<>
void assign (options::decisionThreshold__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::decisionUseWeight__option_t::typeoperator[] (options::decisionUseWeight__option_t) const
 
template<>
bool wasSetByUser (options::decisionUseWeight__option_t) const
 
template<>
void assignBool (options::decisionUseWeight__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::decisionRandomWeight__option_t::typeoperator[] (options::decisionRandomWeight__option_t) const
 
template<>
bool wasSetByUser (options::decisionRandomWeight__option_t) const
 
template<>
void assign (options::decisionRandomWeight__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::decisionWeightInternal__option_t::typeoperator[] (options::decisionWeightInternal__option_t) const
 
template<>
bool wasSetByUser (options::decisionWeightInternal__option_t) const
 
template<>
void assign (options::decisionWeightInternal__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::version__option_t::typeoperator[] (options::version__option_t) const
 
template<>
bool wasSetByUser (options::version__option_t) const
 
template<>
void assignBool (options::version__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::help__option_t::typeoperator[] (options::help__option_t) const
 
template<>
bool wasSetByUser (options::help__option_t) const
 
template<>
void assignBool (options::help__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::earlyExit__option_t::typeoperator[] (options::earlyExit__option_t) const
 
template<>
bool wasSetByUser (options::earlyExit__option_t) const
 
template<>
void assignBool (options::earlyExit__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::threads__option_t::typeoperator[] (options::threads__option_t) const
 
template<>
bool wasSetByUser (options::threads__option_t) const
 
template<>
void assign (options::threads__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::threadStackSize__option_t::typeoperator[] (options::threadStackSize__option_t) const
 
template<>
bool wasSetByUser (options::threadStackSize__option_t) const
 
template<>
void assign (options::threadStackSize__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::threadArgv__option_t, const options::threadArgv__option_t::type &x)
 
template<>
const options::threadArgv__option_t::typeoperator[] (options::threadArgv__option_t) const
 
template<>
bool wasSetByUser (options::threadArgv__option_t) const
 
template<>
void assign (options::threadArgv__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::thread_id__option_t, const options::thread_id__option_t::type &x)
 
template<>
const options::thread_id__option_t::typeoperator[] (options::thread_id__option_t) const
 
template<>
bool wasSetByUser (options::thread_id__option_t) const
 
template<>
void assign (options::thread_id__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
void set (options::sharingFilterByLength__option_t, const options::sharingFilterByLength__option_t::type &x)
 
template<>
const options::sharingFilterByLength__option_t::typeoperator[] (options::sharingFilterByLength__option_t) const
 
template<>
bool wasSetByUser (options::sharingFilterByLength__option_t) const
 
template<>
void assign (options::sharingFilterByLength__option_t, std::string option, std::string value, SmtEngine *smt)
 
template<>
const options::fallbackSequential__option_t::typeoperator[] (options::fallbackSequential__option_t) const
 
template<>
bool wasSetByUser (options::fallbackSequential__option_t) const
 
template<>
void assignBool (options::fallbackSequential__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::incrementalParallel__option_t::typeoperator[] (options::incrementalParallel__option_t) const
 
template<>
bool wasSetByUser (options::incrementalParallel__option_t) const
 
template<>
void assignBool (options::incrementalParallel__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::interactivePrompt__option_t::typeoperator[] (options::interactivePrompt__option_t) const
 
template<>
bool wasSetByUser (options::interactivePrompt__option_t) const
 
template<>
void assignBool (options::interactivePrompt__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::continuedExecution__option_t::typeoperator[] (options::continuedExecution__option_t) const
 
template<>
bool wasSetByUser (options::continuedExecution__option_t) const
 
template<>
void assignBool (options::continuedExecution__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::segvSpin__option_t::typeoperator[] (options::segvSpin__option_t) const
 
template<>
bool wasSetByUser (options::segvSpin__option_t) const
 
template<>
void assignBool (options::segvSpin__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::tearDownIncremental__option_t::typeoperator[] (options::tearDownIncremental__option_t) const
 
template<>
bool wasSetByUser (options::tearDownIncremental__option_t) const
 
template<>
void assignBool (options::tearDownIncremental__option_t, std::string option, bool value, SmtEngine *smt)
 
template<>
const options::waitToJoin__option_t::typeoperator[] (options::waitToJoin__option_t) const
 
template<>
bool wasSetByUser (options::waitToJoin__option_t) const
 
template<>
void assignBool (options::waitToJoin__option_t, std::string option, bool value, SmtEngine *smt)
 

Static Public Member Functions

static Optionscurrent ()
 Get the current Options in effect. More...
 
static void printUsage (const std::string msg, std::ostream &out)
 Print overall command-line option usage message, prefixed by "msg"—which could be an error message causing the usage output in the first place, e.g. More...
 
static void printShortUsage (const std::string msg, std::ostream &out)
 Print command-line option usage message for only the most-commonly used options. More...
 
static void printLanguageHelp (std::ostream &out)
 Print help for the –lang command line option. More...
 
static std::string suggestCommandLineOptions (const std::string &optionName) throw ()
 Look up long command-line option names that bear some similarity to the given name. More...
 
static std::vector< std::string > suggestSmtOptions (const std::string &optionName) throw ()
 Look up SMT option names that bear some similarity to the given name. More...
 

Friends

class NodeManager
 
class NodeManagerScope
 
class SmtEngine
 

Detailed Description

Definition at line 43 of file options.h.

Constructor & Destructor Documentation

CVC4::Options::Options ( )
CVC4::Options::Options ( const Options options)
CVC4::Options::~Options ( )

Member Function Documentation

template<>
void CVC4::Options::assign ( options::booleanTermConversionMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::modelFormatMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::theoryOfMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::defaultExprDepth__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::theoryAlternates__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::instFormatMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::defaultDagThresh__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::decisionMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::stringLB__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::satRandomFreq__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::satRandomSeed__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::decisionThreshold__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::satVarDecay__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::decisionRandomWeight__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::satClauseDecay__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::decisionWeightInternal__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::satRestartFirst__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::binary_name__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::stringCharCardinality__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::satRestartInc__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::bitblastMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::in__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::threads__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::out__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::threadStackSize__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::bitvectorAigSimplifications__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::ufssTotalityLimited__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::err__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::threadArgv__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::inputLanguage__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::ufssAbortCardinality__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::thread_id__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::outputLanguage__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::sharingFilterByLength__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::bitvectorEqualitySlicer__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::verbosity__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::bitvectorAlgebraicBudget__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::forceLogic__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::simplificationMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::bvNumFunc__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithUnateLemmaMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithPropagationMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithHeuristicPivots__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithStandardCheckVarOrderPivots__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithErrorSelectionRule__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithSimplexCheckPeriod__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithPivotThreshold__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithPropagateMaxLength__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithMLTrickSubstitutions__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::maxCutsInContext__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::zombieHuntThreshold__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::instWhenMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::instMaxLevel__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::literalMatchMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::cumulativeMillisecondLimit__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::perCallMillisecondLimit__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::cumulativeResourceLimit__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::maxApproxDepth__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::perCallResourceLimit__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::userPatternsQuant__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayFilename__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayLog__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::arithPropAsLemmaLength__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayStream__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::mbqiMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::lemmaInputChannel__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::lemmaOutputChannel__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::dioSolverTurns__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::rrTurns__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayEarlyCloseDepths__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayFailurePenalty__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayNumericFailurePenalty__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::replayRejectCutSize__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::axiomInstMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::lemmaRejectCutSize__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::soiApproxMajorFailure__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::qcfMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::soiApproxMajorFailurePen__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::qcfWhenMode__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::soiApproxMinorFailure__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::soiApproxMinorFailurePen__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::ppAssertMaxSubSize__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::maxReplayTree__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assign ( options::pbRewriteThreshold__option_t  ,
std::string  option,
std::string  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::idlRewriteEq__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::setsPropagate__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dtRewriteErrorSel__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::setsEagerLemmas__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dtForceAssignment__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::strictParsing__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arraysOptimizeLinear__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::memoryMap__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::semanticChecks__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arraysLazyRIntro1__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::stringExp__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::earlyTypeChecking__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::filesystemAccess__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arraysModelBased__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::decisionStopOnly__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::typeChecking__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::stringFMF__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::biasedITERemoval__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arraysEagerIndexSplitting__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::stringEIT__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::decisionUseWeight__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arraysEagerLemmas__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::stringOpt1__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufSymmetryBreaker__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::stringOpt2__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::version__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::condenseFunctionValues__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::help__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssRegions__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::earlyExit__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::sat_refine_conflicts__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssEagerSplits__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorAig__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssTotality__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::minisatUseElim__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::minisatDumpDimacs__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorPropagate__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssTotalitySymBreak__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorEqualitySolver__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssExplainedCliques__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssSimpleCliques__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::languageHelp__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fallbackSequential__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorInequalitySolver__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssDiseqPropagation__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::incrementalParallel__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssMinimalModel__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorAlgebraicSolver__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::statistics__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::interactivePrompt__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssCliqueSplits__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::continuedExecution__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::statsEveryQuery__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssSymBreak__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::segvSpin__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::statsHideZeros__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorToBool__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::ufssFairness__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::tearDownIncremental__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::parseOnly__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorDivByZeroConst__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::waitToJoin__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::preprocessOnly__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bvAbstraction__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::printSuccess__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::doStaticLearning__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::skolemizeArguments__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::expandDefinitions__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::produceModels__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bvEagerExplanations__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::checkModels__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bitvectorQuickXplain__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dumpModels__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::bvIntroducePow2__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::miniscopeQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::proof__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::miniscopeQuantFreeVar__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::checkProofs__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::prenexQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dumpProofs__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::varElimQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dumpInstantiations__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::simpleIteLiftQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::unsatCores__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::cnfQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::produceAssignments__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::nnfQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::interactive__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::clauseSplit__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arithDioSolver__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::doITESimp__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::preSkolemQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arithRewriteEq__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::doITESimpOnRepeat__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::aggressiveMiniscopeQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::arithMLTrick__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::macrosQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::simplifyWithCareEnabled__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::foPropQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::compressItes__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::doCutAllBounded__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::smartTriggers__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::unconstrainedSimp__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::relevantTriggers__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::revertArithModels__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::relationalTriggers__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::repeatSimp__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::registerQuantBodyTerms__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::havePenalties__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::useFC__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::sortInference__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::incrementalSolving__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::useSOI__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::eagerInstQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::abstractValues__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::restrictedPivots__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fullSaturateQuant__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::modelUninterpDtEnum__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::collectPivots__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::cbqi__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::useApprox__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::recurseCbqi__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::exportDioDecompositions__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::rewriteApplyToConst__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::flipDecision__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::internalReps__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::newProp__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::finiteModelFind__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::soiQuickExplain__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfOneInstPerRound__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::rewriteDivk__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfOneQuantPerRound__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::trySolveIntStandardEffort__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfInstEngine__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::forceNoLimitCpuWhileDump__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::replayFailureLemma__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfInstGen__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfInstGenOneQuantPerRound__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfFreshDistConst__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dioRepeat__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfFmcSimple__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfBoundInt__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::fmfBoundIntLazy__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::quantConflictFind__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::qcfTConstraint__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::quantRewriteRules__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::rrOneInstPerRound__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::dtStcInduction__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
template<>
void CVC4::Options::assignBool ( options::pbRewrites__option_t  ,
std::string  option,
bool  value,
SmtEngine smt 
)
static Options& CVC4::Options::current ( )
inlinestatic

Get the current Options in effect.

Definition at line 64 of file options.h.

Referenced by CVC4::expr::ExprDag::getDag(), CVC4::expr::ExprSetDepth::getDepth(), CVC4::expr::ExprSetLanguage::getLanguage(), CVC4::options::idlRewriteEq__option_t::operator()(), CVC4::options::booleanTermConversionMode__option_t::operator()(), CVC4::options::setsPropagate__option_t::operator()(), CVC4::options::dtRewriteErrorSel__option_t::operator()(), CVC4::options::setsEagerLemmas__option_t::operator()(), CVC4::options::dtForceAssignment__option_t::operator()(), CVC4::options::strictParsing__option_t::operator()(), CVC4::options::theoryOfMode__option_t::operator()(), CVC4::options::modelFormatMode__option_t::operator()(), CVC4::options::instFormatMode__option_t::operator()(), CVC4::options::defaultExprDepth__option_t::operator()(), CVC4::options::memoryMap__option_t::operator()(), CVC4::options::arraysOptimizeLinear__option_t::operator()(), CVC4::options::theoryAlternates__option_t::operator()(), CVC4::options::defaultDagThresh__option_t::operator()(), CVC4::options::semanticChecks__option_t::operator()(), CVC4::options::arraysLazyRIntro1__option_t::operator()(), CVC4::options::earlyTypeChecking__option_t::operator()(), CVC4::options::filesystemAccess__option_t::operator()(), CVC4::options::arraysModelBased__option_t::operator()(), CVC4::options::stringExp__option_t::operator()(), CVC4::options::typeChecking__option_t::operator()(), CVC4::options::arraysEagerIndexSplitting__option_t::operator()(), CVC4::options::stringLB__option_t::operator()(), CVC4::options::decisionMode__option_t::operator()(), CVC4::options::satRandomFreq__option_t::operator()(), CVC4::options::biasedITERemoval__option_t::operator()(), CVC4::options::arraysEagerLemmas__option_t::operator()(), CVC4::options::stringFMF__option_t::operator()(), CVC4::options::decisionStopOnly__option_t::operator()(), CVC4::options::stringEIT__option_t::operator()(), CVC4::options::decisionThreshold__option_t::operator()(), CVC4::options::satRandomSeed__option_t::operator()(), CVC4::options::stringOpt1__option_t::operator()(), CVC4::options::decisionUseWeight__option_t::operator()(), CVC4::options::satVarDecay__option_t::operator()(), CVC4::options::stringOpt2__option_t::operator()(), CVC4::options::decisionRandomWeight__option_t::operator()(), CVC4::options::satClauseDecay__option_t::operator()(), CVC4::options::decisionWeightInternal__option_t::operator()(), CVC4::options::stringCharCardinality__option_t::operator()(), CVC4::options::satRestartFirst__option_t::operator()(), CVC4::options::satRestartInc__option_t::operator()(), CVC4::options::ufSymmetryBreaker__option_t::operator()(), CVC4::options::sat_refine_conflicts__option_t::operator()(), CVC4::options::condenseFunctionValues__option_t::operator()(), CVC4::options::minisatUseElim__option_t::operator()(), CVC4::options::version__option_t::operator()(), CVC4::options::ufssRegions__option_t::operator()(), CVC4::options::minisatDumpDimacs__option_t::operator()(), CVC4::options::help__option_t::operator()(), CVC4::options::ufssEagerSplits__option_t::operator()(), CVC4::options::binary_name__option_t::operator()(), CVC4::options::earlyExit__option_t::operator()(), CVC4::options::bitblastMode__option_t::operator()(), CVC4::options::ufssTotality__option_t::operator()(), CVC4::options::threads__option_t::operator()(), CVC4::options::bitvectorAig__option_t::operator()(), CVC4::options::ufssTotalityLimited__option_t::operator()(), CVC4::options::in__option_t::operator()(), CVC4::options::threadStackSize__option_t::operator()(), CVC4::options::out__option_t::operator()(), CVC4::options::bitvectorAigSimplifications__option_t::operator()(), CVC4::options::ufssTotalitySymBreak__option_t::operator()(), CVC4::options::threadArgv__option_t::operator()(), CVC4::options::bitvectorPropagate__option_t::operator()(), CVC4::options::err__option_t::operator()(), CVC4::options::ufssAbortCardinality__option_t::operator()(), CVC4::options::inputLanguage__option_t::operator()(), CVC4::options::thread_id__option_t::operator()(), CVC4::options::bitvectorEqualitySolver__option_t::operator()(), CVC4::options::ufssExplainedCliques__option_t::operator()(), CVC4::options::sharingFilterByLength__option_t::operator()(), CVC4::options::outputLanguage__option_t::operator()(), CVC4::options::bitvectorEqualitySlicer__option_t::operator()(), CVC4::options::ufssSimpleCliques__option_t::operator()(), CVC4::options::fallbackSequential__option_t::operator()(), CVC4::options::languageHelp__option_t::operator()(), CVC4::options::bitvectorInequalitySolver__option_t::operator()(), CVC4::options::ufssDiseqPropagation__option_t::operator()(), CVC4::options::incrementalParallel__option_t::operator()(), CVC4::options::verbosity__option_t::operator()(), CVC4::options::bitvectorAlgebraicSolver__option_t::operator()(), CVC4::options::ufssMinimalModel__option_t::operator()(), CVC4::options::interactivePrompt__option_t::operator()(), CVC4::options::bitvectorAlgebraicBudget__option_t::operator()(), CVC4::options::statistics__option_t::operator()(), CVC4::options::ufssCliqueSplits__option_t::operator()(), CVC4::options::continuedExecution__option_t::operator()(), CVC4::options::bitvectorToBool__option_t::operator()(), CVC4::options::statsEveryQuery__option_t::operator()(), CVC4::options::ufssSymBreak__option_t::operator()(), CVC4::options::statsHideZeros__option_t::operator()(), CVC4::options::segvSpin__option_t::operator()(), CVC4::options::bitvectorDivByZeroConst__option_t::operator()(), CVC4::options::ufssFairness__option_t::operator()(), CVC4::options::parseOnly__option_t::operator()(), CVC4::options::tearDownIncremental__option_t::operator()(), CVC4::options::bvAbstraction__option_t::operator()(), CVC4::options::waitToJoin__option_t::operator()(), CVC4::options::preprocessOnly__option_t::operator()(), CVC4::options::skolemizeArguments__option_t::operator()(), CVC4::options::printSuccess__option_t::operator()(), CVC4::options::bvNumFunc__option_t::operator()(), CVC4::options::bvEagerExplanations__option_t::operator()(), CVC4::options::bitvectorQuickXplain__option_t::operator()(), CVC4::options::bvIntroducePow2__option_t::operator()(), CVC4::options::forceLogic__option_t::operator()(), CVC4::options::simplificationMode__option_t::operator()(), CVC4::options::doStaticLearning__option_t::operator()(), CVC4::options::expandDefinitions__option_t::operator()(), CVC4::options::produceModels__option_t::operator()(), CVC4::options::checkModels__option_t::operator()(), CVC4::options::dumpModels__option_t::operator()(), CVC4::options::proof__option_t::operator()(), CVC4::options::checkProofs__option_t::operator()(), CVC4::options::arithUnateLemmaMode__option_t::operator()(), CVC4::options::dumpProofs__option_t::operator()(), CVC4::options::arithPropagationMode__option_t::operator()(), CVC4::options::dumpInstantiations__option_t::operator()(), CVC4::options::arithHeuristicPivots__option_t::operator()(), CVC4::options::unsatCores__option_t::operator()(), CVC4::options::arithStandardCheckVarOrderPivots__option_t::operator()(), CVC4::options::miniscopeQuant__option_t::operator()(), CVC4::options::produceAssignments__option_t::operator()(), CVC4::options::arithErrorSelectionRule__option_t::operator()(), CVC4::options::miniscopeQuantFreeVar__option_t::operator()(), CVC4::options::interactive__option_t::operator()(), CVC4::options::arithSimplexCheckPeriod__option_t::operator()(), CVC4::options::prenexQuant__option_t::operator()(), CVC4::options::doITESimp__option_t::operator()(), CVC4::options::arithPivotThreshold__option_t::operator()(), CVC4::options::varElimQuant__option_t::operator()(), CVC4::options::doITESimpOnRepeat__option_t::operator()(), CVC4::options::arithPropagateMaxLength__option_t::operator()(), CVC4::options::simpleIteLiftQuant__option_t::operator()(), CVC4::options::arithDioSolver__option_t::operator()(), CVC4::options::simplifyWithCareEnabled__option_t::operator()(), CVC4::options::cnfQuant__option_t::operator()(), CVC4::options::arithRewriteEq__option_t::operator()(), CVC4::options::compressItes__option_t::operator()(), CVC4::options::nnfQuant__option_t::operator()(), CVC4::options::arithMLTrick__option_t::operator()(), CVC4::options::unconstrainedSimp__option_t::operator()(), CVC4::options::clauseSplit__option_t::operator()(), CVC4::options::arithMLTrickSubstitutions__option_t::operator()(), CVC4::options::repeatSimp__option_t::operator()(), CVC4::options::preSkolemQuant__option_t::operator()(), CVC4::options::doCutAllBounded__option_t::operator()(), CVC4::options::zombieHuntThreshold__option_t::operator()(), CVC4::options::aggressiveMiniscopeQuant__option_t::operator()(), CVC4::options::maxCutsInContext__option_t::operator()(), CVC4::options::sortInference__option_t::operator()(), CVC4::options::macrosQuant__option_t::operator()(), CVC4::options::revertArithModels__option_t::operator()(), CVC4::options::incrementalSolving__option_t::operator()(), CVC4::options::foPropQuant__option_t::operator()(), CVC4::options::havePenalties__option_t::operator()(), CVC4::options::abstractValues__option_t::operator()(), CVC4::options::smartTriggers__option_t::operator()(), CVC4::options::useFC__option_t::operator()(), CVC4::options::modelUninterpDtEnum__option_t::operator()(), CVC4::options::cumulativeMillisecondLimit__option_t::operator()(), CVC4::options::relevantTriggers__option_t::operator()(), CVC4::options::useSOI__option_t::operator()(), CVC4::options::perCallMillisecondLimit__option_t::operator()(), CVC4::options::relationalTriggers__option_t::operator()(), CVC4::options::restrictedPivots__option_t::operator()(), CVC4::options::cumulativeResourceLimit__option_t::operator()(), CVC4::options::registerQuantBodyTerms__option_t::operator()(), CVC4::options::collectPivots__option_t::operator()(), CVC4::options::perCallResourceLimit__option_t::operator()(), CVC4::options::instWhenMode__option_t::operator()(), CVC4::options::useApprox__option_t::operator()(), CVC4::options::rewriteApplyToConst__option_t::operator()(), CVC4::options::instMaxLevel__option_t::operator()(), CVC4::options::maxApproxDepth__option_t::operator()(), CVC4::options::replayFilename__option_t::operator()(), CVC4::options::eagerInstQuant__option_t::operator()(), CVC4::options::exportDioDecompositions__option_t::operator()(), CVC4::options::replayLog__option_t::operator()(), CVC4::options::fullSaturateQuant__option_t::operator()(), CVC4::options::newProp__option_t::operator()(), CVC4::options::replayStream__option_t::operator()(), CVC4::options::literalMatchMode__option_t::operator()(), CVC4::options::arithPropAsLemmaLength__option_t::operator()(), CVC4::options::lemmaInputChannel__option_t::operator()(), CVC4::options::cbqi__option_t::operator()(), CVC4::options::soiQuickExplain__option_t::operator()(), CVC4::options::lemmaOutputChannel__option_t::operator()(), CVC4::options::recurseCbqi__option_t::operator()(), CVC4::options::rewriteDivk__option_t::operator()(), CVC4::options::forceNoLimitCpuWhileDump__option_t::operator()(), CVC4::options::userPatternsQuant__option_t::operator()(), CVC4::options::trySolveIntStandardEffort__option_t::operator()(), CVC4::options::flipDecision__option_t::operator()(), CVC4::options::replayFailureLemma__option_t::operator()(), CVC4::options::internalReps__option_t::operator()(), CVC4::options::dioSolverTurns__option_t::operator()(), CVC4::options::finiteModelFind__option_t::operator()(), CVC4::options::rrTurns__option_t::operator()(), CVC4::options::mbqiMode__option_t::operator()(), CVC4::options::dioRepeat__option_t::operator()(), CVC4::options::fmfOneInstPerRound__option_t::operator()(), CVC4::options::replayEarlyCloseDepths__option_t::operator()(), CVC4::options::fmfOneQuantPerRound__option_t::operator()(), CVC4::options::replayFailurePenalty__option_t::operator()(), CVC4::options::fmfInstEngine__option_t::operator()(), CVC4::options::replayNumericFailurePenalty__option_t::operator()(), CVC4::options::fmfInstGen__option_t::operator()(), CVC4::options::replayRejectCutSize__option_t::operator()(), CVC4::options::fmfInstGenOneQuantPerRound__option_t::operator()(), CVC4::options::lemmaRejectCutSize__option_t::operator()(), CVC4::options::fmfFreshDistConst__option_t::operator()(), CVC4::options::soiApproxMajorFailure__option_t::operator()(), CVC4::options::fmfFmcSimple__option_t::operator()(), CVC4::options::soiApproxMajorFailurePen__option_t::operator()(), CVC4::options::fmfBoundInt__option_t::operator()(), CVC4::options::soiApproxMinorFailure__option_t::operator()(), CVC4::options::fmfBoundIntLazy__option_t::operator()(), CVC4::options::soiApproxMinorFailurePen__option_t::operator()(), CVC4::options::axiomInstMode__option_t::operator()(), CVC4::options::ppAssertMaxSubSize__option_t::operator()(), CVC4::options::quantConflictFind__option_t::operator()(), CVC4::options::maxReplayTree__option_t::operator()(), CVC4::options::qcfMode__option_t::operator()(), CVC4::options::pbRewrites__option_t::operator()(), CVC4::options::qcfWhenMode__option_t::operator()(), CVC4::options::pbRewriteThreshold__option_t::operator()(), CVC4::options::qcfTConstraint__option_t::operator()(), CVC4::options::quantRewriteRules__option_t::operator()(), CVC4::options::rrOneInstPerRound__option_t::operator()(), CVC4::options::dtStcInduction__option_t::operator()(), CVC4::options::idlRewriteEq__option_t::set(), CVC4::options::dtForceAssignment__option_t::set(), CVC4::options::modelFormatMode__option_t::set(), CVC4::options::theoryOfMode__option_t::set(), CVC4::options::instFormatMode__option_t::set(), CVC4::options::arraysOptimizeLinear__option_t::set(), CVC4::options::theoryAlternates__option_t::set(), CVC4::options::arraysLazyRIntro1__option_t::set(), CVC4::options::arraysModelBased__option_t::set(), CVC4::options::stringExp__option_t::set(), CVC4::options::arraysEagerIndexSplitting__option_t::set(), CVC4::options::decisionMode__option_t::set(), CVC4::options::stringFMF__option_t::set(), CVC4::options::arraysEagerLemmas__option_t::set(), CVC4::options::decisionStopOnly__option_t::set(), CVC4::options::satRandomSeed__option_t::set(), CVC4::options::satVarDecay__option_t::set(), CVC4::options::satClauseDecay__option_t::set(), CVC4::options::ufSymmetryBreaker__option_t::set(), CVC4::options::minisatUseElim__option_t::set(), CVC4::options::bitblastMode__option_t::set(), CVC4::options::binary_name__option_t::set(), CVC4::options::in__option_t::set(), CVC4::options::bitvectorAig__option_t::set(), CVC4::options::bitvectorAigSimplifications__option_t::set(), CVC4::options::out__option_t::set(), CVC4::options::threadArgv__option_t::set(), CVC4::options::bitvectorPropagate__option_t::set(), CVC4::options::err__option_t::set(), CVC4::options::thread_id__option_t::set(), CVC4::options::inputLanguage__option_t::set(), CVC4::options::bitvectorEqualitySolver__option_t::set(), CVC4::options::outputLanguage__option_t::set(), CVC4::options::sharingFilterByLength__option_t::set(), CVC4::options::bitvectorEqualitySlicer__option_t::set(), CVC4::options::bitvectorInequalitySolver__option_t::set(), CVC4::options::languageHelp__option_t::set(), CVC4::options::bitvectorAlgebraicSolver__option_t::set(), CVC4::options::verbosity__option_t::set(), CVC4::options::bitvectorAlgebraicBudget__option_t::set(), CVC4::options::bitvectorToBool__option_t::set(), CVC4::options::parseOnly__option_t::set(), CVC4::options::bvAbstraction__option_t::set(), CVC4::options::skolemizeArguments__option_t::set(), CVC4::options::bvEagerExplanations__option_t::set(), CVC4::options::simplificationMode__option_t::set(), CVC4::options::arithHeuristicPivots__option_t::set(), CVC4::options::arithStandardCheckVarOrderPivots__option_t::set(), CVC4::options::interactive__option_t::set(), CVC4::options::doITESimp__option_t::set(), CVC4::options::arithPivotThreshold__option_t::set(), CVC4::options::doITESimpOnRepeat__option_t::set(), CVC4::options::simplifyWithCareEnabled__option_t::set(), CVC4::options::arithRewriteEq__option_t::set(), CVC4::options::compressItes__option_t::set(), CVC4::options::unconstrainedSimp__option_t::set(), CVC4::options::repeatSimp__option_t::set(), CVC4::options::preSkolemQuant__option_t::set(), CVC4::options::doCutAllBounded__option_t::set(), CVC4::options::sortInference__option_t::set(), CVC4::options::havePenalties__option_t::set(), CVC4::options::useFC__option_t::set(), CVC4::options::useSOI__option_t::set(), CVC4::options::restrictedPivots__option_t::set(), CVC4::options::collectPivots__option_t::set(), CVC4::options::instWhenMode__option_t::set(), CVC4::options::useApprox__option_t::set(), CVC4::options::maxApproxDepth__option_t::set(), CVC4::options::exportDioDecompositions__option_t::set(), CVC4::options::newProp__option_t::set(), CVC4::options::replayStream__option_t::set(), CVC4::options::arithPropAsLemmaLength__option_t::set(), CVC4::options::lemmaInputChannel__option_t::set(), CVC4::options::cbqi__option_t::set(), CVC4::options::soiQuickExplain__option_t::set(), CVC4::options::lemmaOutputChannel__option_t::set(), CVC4::options::rewriteDivk__option_t::set(), CVC4::options::finiteModelFind__option_t::set(), CVC4::options::mbqiMode__option_t::set(), CVC4::options::fmfBoundInt__option_t::set(), CVC4::options::fmfBoundIntLazy__option_t::set(), CVC4::options::quantConflictFind__option_t::set(), CVC4::options::qcfTConstraint__option_t::set(), CVC4::options::idlRewriteEq__option_t::wasSetByUser(), CVC4::options::setsPropagate__option_t::wasSetByUser(), CVC4::options::booleanTermConversionMode__option_t::wasSetByUser(), CVC4::options::dtRewriteErrorSel__option_t::wasSetByUser(), CVC4::options::setsEagerLemmas__option_t::wasSetByUser(), CVC4::options::dtForceAssignment__option_t::wasSetByUser(), CVC4::options::theoryOfMode__option_t::wasSetByUser(), CVC4::options::strictParsing__option_t::wasSetByUser(), CVC4::options::modelFormatMode__option_t::wasSetByUser(), CVC4::options::instFormatMode__option_t::wasSetByUser(), CVC4::options::defaultExprDepth__option_t::wasSetByUser(), CVC4::options::memoryMap__option_t::wasSetByUser(), CVC4::options::arraysOptimizeLinear__option_t::wasSetByUser(), CVC4::options::theoryAlternates__option_t::wasSetByUser(), CVC4::options::defaultDagThresh__option_t::wasSetByUser(), CVC4::options::semanticChecks__option_t::wasSetByUser(), CVC4::options::arraysLazyRIntro1__option_t::wasSetByUser(), CVC4::options::earlyTypeChecking__option_t::wasSetByUser(), CVC4::options::arraysModelBased__option_t::wasSetByUser(), CVC4::options::stringExp__option_t::wasSetByUser(), CVC4::options::filesystemAccess__option_t::wasSetByUser(), CVC4::options::typeChecking__option_t::wasSetByUser(), CVC4::options::arraysEagerIndexSplitting__option_t::wasSetByUser(), CVC4::options::decisionMode__option_t::wasSetByUser(), CVC4::options::stringLB__option_t::wasSetByUser(), CVC4::options::decisionStopOnly__option_t::wasSetByUser(), CVC4::options::stringFMF__option_t::wasSetByUser(), CVC4::options::biasedITERemoval__option_t::wasSetByUser(), CVC4::options::satRandomFreq__option_t::wasSetByUser(), CVC4::options::arraysEagerLemmas__option_t::wasSetByUser(), CVC4::options::decisionThreshold__option_t::wasSetByUser(), CVC4::options::stringEIT__option_t::wasSetByUser(), CVC4::options::satRandomSeed__option_t::wasSetByUser(), CVC4::options::decisionUseWeight__option_t::wasSetByUser(), CVC4::options::satVarDecay__option_t::wasSetByUser(), CVC4::options::stringOpt1__option_t::wasSetByUser(), CVC4::options::decisionRandomWeight__option_t::wasSetByUser(), CVC4::options::stringOpt2__option_t::wasSetByUser(), CVC4::options::satClauseDecay__option_t::wasSetByUser(), CVC4::options::satRestartFirst__option_t::wasSetByUser(), CVC4::options::stringCharCardinality__option_t::wasSetByUser(), CVC4::options::decisionWeightInternal__option_t::wasSetByUser(), CVC4::options::satRestartInc__option_t::wasSetByUser(), CVC4::options::sat_refine_conflicts__option_t::wasSetByUser(), CVC4::options::ufSymmetryBreaker__option_t::wasSetByUser(), CVC4::options::minisatUseElim__option_t::wasSetByUser(), CVC4::options::condenseFunctionValues__option_t::wasSetByUser(), CVC4::options::ufssRegions__option_t::wasSetByUser(), CVC4::options::version__option_t::wasSetByUser(), CVC4::options::minisatDumpDimacs__option_t::wasSetByUser(), CVC4::options::ufssEagerSplits__option_t::wasSetByUser(), CVC4::options::help__option_t::wasSetByUser(), CVC4::options::bitblastMode__option_t::wasSetByUser(), CVC4::options::binary_name__option_t::wasSetByUser(), CVC4::options::earlyExit__option_t::wasSetByUser(), CVC4::options::ufssTotality__option_t::wasSetByUser(), CVC4::options::in__option_t::wasSetByUser(), CVC4::options::ufssTotalityLimited__option_t::wasSetByUser(), CVC4::options::threads__option_t::wasSetByUser(), CVC4::options::bitvectorAig__option_t::wasSetByUser(), CVC4::options::ufssTotalitySymBreak__option_t::wasSetByUser(), CVC4::options::out__option_t::wasSetByUser(), CVC4::options::bitvectorAigSimplifications__option_t::wasSetByUser(), CVC4::options::threadStackSize__option_t::wasSetByUser(), CVC4::options::threadArgv__option_t::wasSetByUser(), CVC4::options::bitvectorPropagate__option_t::wasSetByUser(), CVC4::options::ufssAbortCardinality__option_t::wasSetByUser(), CVC4::options::err__option_t::wasSetByUser(), CVC4::options::inputLanguage__option_t::wasSetByUser(), CVC4::options::thread_id__option_t::wasSetByUser(), CVC4::options::bitvectorEqualitySolver__option_t::wasSetByUser(), CVC4::options::ufssExplainedCliques__option_t::wasSetByUser(), CVC4::options::bitvectorEqualitySlicer__option_t::wasSetByUser(), CVC4::options::ufssSimpleCliques__option_t::wasSetByUser(), CVC4::options::outputLanguage__option_t::wasSetByUser(), CVC4::options::sharingFilterByLength__option_t::wasSetByUser(), CVC4::options::ufssDiseqPropagation__option_t::wasSetByUser(), CVC4::options::bitvectorInequalitySolver__option_t::wasSetByUser(), CVC4::options::fallbackSequential__option_t::wasSetByUser(), CVC4::options::languageHelp__option_t::wasSetByUser(), CVC4::options::incrementalParallel__option_t::wasSetByUser(), CVC4::options::verbosity__option_t::wasSetByUser(), CVC4::options::bitvectorAlgebraicSolver__option_t::wasSetByUser(), CVC4::options::ufssMinimalModel__option_t::wasSetByUser(), CVC4::options::ufssCliqueSplits__option_t::wasSetByUser(), CVC4::options::interactivePrompt__option_t::wasSetByUser(), CVC4::options::bitvectorAlgebraicBudget__option_t::wasSetByUser(), CVC4::options::statistics__option_t::wasSetByUser(), CVC4::options::statsEveryQuery__option_t::wasSetByUser(), CVC4::options::ufssSymBreak__option_t::wasSetByUser(), CVC4::options::continuedExecution__option_t::wasSetByUser(), CVC4::options::bitvectorToBool__option_t::wasSetByUser(), CVC4::options::ufssFairness__option_t::wasSetByUser(), CVC4::options::statsHideZeros__option_t::wasSetByUser(), CVC4::options::segvSpin__option_t::wasSetByUser(), CVC4::options::bitvectorDivByZeroConst__option_t::wasSetByUser(), CVC4::options::parseOnly__option_t::wasSetByUser(), CVC4::options::bvAbstraction__option_t::wasSetByUser(), CVC4::options::tearDownIncremental__option_t::wasSetByUser(), CVC4::options::preprocessOnly__option_t::wasSetByUser(), CVC4::options::skolemizeArguments__option_t::wasSetByUser(), CVC4::options::waitToJoin__option_t::wasSetByUser(), CVC4::options::bvNumFunc__option_t::wasSetByUser(), CVC4::options::printSuccess__option_t::wasSetByUser(), CVC4::options::bvEagerExplanations__option_t::wasSetByUser(), CVC4::options::bitvectorQuickXplain__option_t::wasSetByUser(), CVC4::options::bvIntroducePow2__option_t::wasSetByUser(), CVC4::options::forceLogic__option_t::wasSetByUser(), CVC4::options::simplificationMode__option_t::wasSetByUser(), CVC4::options::doStaticLearning__option_t::wasSetByUser(), CVC4::options::expandDefinitions__option_t::wasSetByUser(), CVC4::options::produceModels__option_t::wasSetByUser(), CVC4::options::checkModels__option_t::wasSetByUser(), CVC4::options::dumpModels__option_t::wasSetByUser(), CVC4::options::proof__option_t::wasSetByUser(), CVC4::options::arithUnateLemmaMode__option_t::wasSetByUser(), CVC4::options::checkProofs__option_t::wasSetByUser(), CVC4::options::dumpProofs__option_t::wasSetByUser(), CVC4::options::arithPropagationMode__option_t::wasSetByUser(), CVC4::options::dumpInstantiations__option_t::wasSetByUser(), CVC4::options::arithHeuristicPivots__option_t::wasSetByUser(), CVC4::options::unsatCores__option_t::wasSetByUser(), CVC4::options::arithStandardCheckVarOrderPivots__option_t::wasSetByUser(), CVC4::options::miniscopeQuant__option_t::wasSetByUser(), CVC4::options::produceAssignments__option_t::wasSetByUser(), CVC4::options::arithErrorSelectionRule__option_t::wasSetByUser(), CVC4::options::interactive__option_t::wasSetByUser(), CVC4::options::miniscopeQuantFreeVar__option_t::wasSetByUser(), CVC4::options::arithSimplexCheckPeriod__option_t::wasSetByUser(), CVC4::options::doITESimp__option_t::wasSetByUser(), CVC4::options::arithPivotThreshold__option_t::wasSetByUser(), CVC4::options::prenexQuant__option_t::wasSetByUser(), CVC4::options::doITESimpOnRepeat__option_t::wasSetByUser(), CVC4::options::arithPropagateMaxLength__option_t::wasSetByUser(), CVC4::options::varElimQuant__option_t::wasSetByUser(), CVC4::options::arithDioSolver__option_t::wasSetByUser(), CVC4::options::simpleIteLiftQuant__option_t::wasSetByUser(), CVC4::options::simplifyWithCareEnabled__option_t::wasSetByUser(), CVC4::options::compressItes__option_t::wasSetByUser(), CVC4::options::cnfQuant__option_t::wasSetByUser(), CVC4::options::arithRewriteEq__option_t::wasSetByUser(), CVC4::options::arithMLTrick__option_t::wasSetByUser(), CVC4::options::nnfQuant__option_t::wasSetByUser(), CVC4::options::unconstrainedSimp__option_t::wasSetByUser(), CVC4::options::clauseSplit__option_t::wasSetByUser(), CVC4::options::arithMLTrickSubstitutions__option_t::wasSetByUser(), CVC4::options::repeatSimp__option_t::wasSetByUser(), CVC4::options::preSkolemQuant__option_t::wasSetByUser(), CVC4::options::doCutAllBounded__option_t::wasSetByUser(), CVC4::options::zombieHuntThreshold__option_t::wasSetByUser(), CVC4::options::sortInference__option_t::wasSetByUser(), CVC4::options::maxCutsInContext__option_t::wasSetByUser(), CVC4::options::aggressiveMiniscopeQuant__option_t::wasSetByUser(), CVC4::options::incrementalSolving__option_t::wasSetByUser(), CVC4::options::macrosQuant__option_t::wasSetByUser(), CVC4::options::revertArithModels__option_t::wasSetByUser(), CVC4::options::foPropQuant__option_t::wasSetByUser(), CVC4::options::havePenalties__option_t::wasSetByUser(), CVC4::options::abstractValues__option_t::wasSetByUser(), CVC4::options::useFC__option_t::wasSetByUser(), CVC4::options::smartTriggers__option_t::wasSetByUser(), CVC4::options::modelUninterpDtEnum__option_t::wasSetByUser(), CVC4::options::useSOI__option_t::wasSetByUser(), CVC4::options::relevantTriggers__option_t::wasSetByUser(), CVC4::options::cumulativeMillisecondLimit__option_t::wasSetByUser(), CVC4::options::restrictedPivots__option_t::wasSetByUser(), CVC4::options::perCallMillisecondLimit__option_t::wasSetByUser(), CVC4::options::relationalTriggers__option_t::wasSetByUser(), CVC4::options::collectPivots__option_t::wasSetByUser(), CVC4::options::registerQuantBodyTerms__option_t::wasSetByUser(), CVC4::options::cumulativeResourceLimit__option_t::wasSetByUser(), CVC4::options::useApprox__option_t::wasSetByUser(), CVC4::options::perCallResourceLimit__option_t::wasSetByUser(), CVC4::options::instWhenMode__option_t::wasSetByUser(), CVC4::options::instMaxLevel__option_t::wasSetByUser(), CVC4::options::rewriteApplyToConst__option_t::wasSetByUser(), CVC4::options::maxApproxDepth__option_t::wasSetByUser(), CVC4::options::replayFilename__option_t::wasSetByUser(), CVC4::options::exportDioDecompositions__option_t::wasSetByUser(), CVC4::options::eagerInstQuant__option_t::wasSetByUser(), CVC4::options::newProp__option_t::wasSetByUser(), CVC4::options::replayLog__option_t::wasSetByUser(), CVC4::options::fullSaturateQuant__option_t::wasSetByUser(), CVC4::options::replayStream__option_t::wasSetByUser(), CVC4::options::arithPropAsLemmaLength__option_t::wasSetByUser(), CVC4::options::literalMatchMode__option_t::wasSetByUser(), CVC4::options::lemmaInputChannel__option_t::wasSetByUser(), CVC4::options::soiQuickExplain__option_t::wasSetByUser(), CVC4::options::cbqi__option_t::wasSetByUser(), CVC4::options::lemmaOutputChannel__option_t::wasSetByUser(), CVC4::options::recurseCbqi__option_t::wasSetByUser(), CVC4::options::rewriteDivk__option_t::wasSetByUser(), CVC4::options::forceNoLimitCpuWhileDump__option_t::wasSetByUser(), CVC4::options::trySolveIntStandardEffort__option_t::wasSetByUser(), CVC4::options::userPatternsQuant__option_t::wasSetByUser(), CVC4::options::replayFailureLemma__option_t::wasSetByUser(), CVC4::options::flipDecision__option_t::wasSetByUser(), CVC4::options::dioSolverTurns__option_t::wasSetByUser(), CVC4::options::internalReps__option_t::wasSetByUser(), CVC4::options::rrTurns__option_t::wasSetByUser(), CVC4::options::finiteModelFind__option_t::wasSetByUser(), CVC4::options::dioRepeat__option_t::wasSetByUser(), CVC4::options::mbqiMode__option_t::wasSetByUser(), CVC4::options::replayEarlyCloseDepths__option_t::wasSetByUser(), CVC4::options::fmfOneInstPerRound__option_t::wasSetByUser(), CVC4::options::replayFailurePenalty__option_t::wasSetByUser(), CVC4::options::fmfOneQuantPerRound__option_t::wasSetByUser(), CVC4::options::fmfInstEngine__option_t::wasSetByUser(), CVC4::options::replayNumericFailurePenalty__option_t::wasSetByUser(), CVC4::options::fmfInstGen__option_t::wasSetByUser(), CVC4::options::replayRejectCutSize__option_t::wasSetByUser(), CVC4::options::lemmaRejectCutSize__option_t::wasSetByUser(), CVC4::options::fmfInstGenOneQuantPerRound__option_t::wasSetByUser(), CVC4::options::soiApproxMajorFailure__option_t::wasSetByUser(), CVC4::options::fmfFreshDistConst__option_t::wasSetByUser(), CVC4::options::soiApproxMajorFailurePen__option_t::wasSetByUser(), CVC4::options::fmfFmcSimple__option_t::wasSetByUser(), CVC4::options::fmfBoundInt__option_t::wasSetByUser(), CVC4::options::soiApproxMinorFailure__option_t::wasSetByUser(), CVC4::options::soiApproxMinorFailurePen__option_t::wasSetByUser(), CVC4::options::fmfBoundIntLazy__option_t::wasSetByUser(), CVC4::options::ppAssertMaxSubSize__option_t::wasSetByUser(), CVC4::options::axiomInstMode__option_t::wasSetByUser(), CVC4::options::quantConflictFind__option_t::wasSetByUser(), CVC4::options::maxReplayTree__option_t::wasSetByUser(), CVC4::options::qcfMode__option_t::wasSetByUser(), CVC4::options::pbRewrites__option_t::wasSetByUser(), CVC4::options::qcfWhenMode__option_t::wasSetByUser(), CVC4::options::pbRewriteThreshold__option_t::wasSetByUser(), CVC4::options::qcfTConstraint__option_t::wasSetByUser(), CVC4::options::quantRewriteRules__option_t::wasSetByUser(), CVC4::options::rrOneInstPerRound__option_t::wasSetByUser(), and CVC4::options::dtStcInduction__option_t::wasSetByUser().

std::string CVC4::Options::getDescription ( ) const

Get a description of the command-line flags accepted by parseOptions.

The returned string will be escaped so that it is suitable as an argument to printf.

SExpr CVC4::Options::getOptions ( ) const
throw (
)

Get the setting for all options.

template<>
const options::idlRewriteEq__option_t::type& CVC4::Options::operator[] ( options::idlRewriteEq__option_t  ) const
template<>
const options::setsPropagate__option_t::type& CVC4::Options::operator[] ( options::setsPropagate__option_t  ) const
template<>
const options::dtRewriteErrorSel__option_t::type& CVC4::Options::operator[] ( options::dtRewriteErrorSel__option_t  ) const
template<>
const options::setsEagerLemmas__option_t::type& CVC4::Options::operator[] ( options::setsEagerLemmas__option_t  ) const
template<>
const options::theoryOfMode__option_t::type& CVC4::Options::operator[] ( options::theoryOfMode__option_t  ) const
template<>
const options::modelFormatMode__option_t::type& CVC4::Options::operator[] ( options::modelFormatMode__option_t  ) const
template<class T >
const T::type& CVC4::Options::operator[] ( ) const

Get the value of the given option.

Const access only.

template<>
const options::dtForceAssignment__option_t::type& CVC4::Options::operator[] ( options::dtForceAssignment__option_t  ) const
template<>
const options::strictParsing__option_t::type& CVC4::Options::operator[] ( options::strictParsing__option_t  ) const
template<>
const options::defaultExprDepth__option_t::type& CVC4::Options::operator[] ( options::defaultExprDepth__option_t  ) const
template<>
const options::arraysOptimizeLinear__option_t::type& CVC4::Options::operator[] ( options::arraysOptimizeLinear__option_t  ) const
template<>
const options::theoryAlternates__option_t::type& CVC4::Options::operator[] ( options::theoryAlternates__option_t  ) const
template<>
const options::instFormatMode__option_t::type& CVC4::Options::operator[] ( options::instFormatMode__option_t  ) const
template<>
const options::memoryMap__option_t::type& CVC4::Options::operator[] ( options::memoryMap__option_t  ) const
template<>
const options::defaultDagThresh__option_t::type& CVC4::Options::operator[] ( options::defaultDagThresh__option_t  ) const
template<>
const options::semanticChecks__option_t::type& CVC4::Options::operator[] ( options::semanticChecks__option_t  ) const
template<>
const options::arraysLazyRIntro1__option_t::type& CVC4::Options::operator[] ( options::arraysLazyRIntro1__option_t  ) const
template<>
const options::stringExp__option_t::type& CVC4::Options::operator[] ( options::stringExp__option_t  ) const
template<>
const options::decisionMode__option_t::type& CVC4::Options::operator[] ( options::decisionMode__option_t  ) const
template<>
const options::earlyTypeChecking__option_t::type& CVC4::Options::operator[] ( options::earlyTypeChecking__option_t  ) const
template<>
const options::filesystemAccess__option_t::type& CVC4::Options::operator[] ( options::filesystemAccess__option_t  ) const
template<>
const options::satRandomFreq__option_t::type& CVC4::Options::operator[] ( options::satRandomFreq__option_t  ) const
template<>
const options::stringLB__option_t::type& CVC4::Options::operator[] ( options::stringLB__option_t  ) const
template<>
const options::arraysModelBased__option_t::type& CVC4::Options::operator[] ( options::arraysModelBased__option_t  ) const
template<>
const options::decisionStopOnly__option_t::type& CVC4::Options::operator[] ( options::decisionStopOnly__option_t  ) const
template<>
const options::typeChecking__option_t::type& CVC4::Options::operator[] ( options::typeChecking__option_t  ) const
template<>
const options::satRandomSeed__option_t::type& CVC4::Options::operator[] ( options::satRandomSeed__option_t  ) const
template<>
const options::decisionThreshold__option_t::type& CVC4::Options::operator[] ( options::decisionThreshold__option_t  ) const
template<>
const options::stringFMF__option_t::type& CVC4::Options::operator[] ( options::stringFMF__option_t  ) const
template<>
const options::biasedITERemoval__option_t::type& CVC4::Options::operator[] ( options::biasedITERemoval__option_t  ) const
template<>
const options::decisionUseWeight__option_t::type& CVC4::Options::operator[] ( options::decisionUseWeight__option_t  ) const
template<>
const options::stringEIT__option_t::type& CVC4::Options::operator[] ( options::stringEIT__option_t  ) const
template<>
const options::satVarDecay__option_t::type& CVC4::Options::operator[] ( options::satVarDecay__option_t  ) const
template<>
const options::arraysEagerLemmas__option_t::type& CVC4::Options::operator[] ( options::arraysEagerLemmas__option_t  ) const
template<>
const options::decisionRandomWeight__option_t::type& CVC4::Options::operator[] ( options::decisionRandomWeight__option_t  ) const
template<>
const options::stringOpt1__option_t::type& CVC4::Options::operator[] ( options::stringOpt1__option_t  ) const
template<>
const options::satClauseDecay__option_t::type& CVC4::Options::operator[] ( options::satClauseDecay__option_t  ) const
template<>
const options::stringOpt2__option_t::type& CVC4::Options::operator[] ( options::stringOpt2__option_t  ) const
template<>
const options::ufSymmetryBreaker__option_t::type& CVC4::Options::operator[] ( options::ufSymmetryBreaker__option_t  ) const
template<>
const options::decisionWeightInternal__option_t::type& CVC4::Options::operator[] ( options::decisionWeightInternal__option_t  ) const
template<>
const options::version__option_t::type& CVC4::Options::operator[] ( options::version__option_t  ) const
template<>
const options::satRestartFirst__option_t::type& CVC4::Options::operator[] ( options::satRestartFirst__option_t  ) const
template<>
const options::condenseFunctionValues__option_t::type& CVC4::Options::operator[] ( options::condenseFunctionValues__option_t  ) const
template<>
const options::stringCharCardinality__option_t::type& CVC4::Options::operator[] ( options::stringCharCardinality__option_t  ) const
template<>
const options::binary_name__option_t::type& CVC4::Options::operator[] ( options::binary_name__option_t  ) const
template<>
const options::help__option_t::type& CVC4::Options::operator[] ( options::help__option_t  ) const
template<>
const options::satRestartInc__option_t::type& CVC4::Options::operator[] ( options::satRestartInc__option_t  ) const
template<>
const options::ufssRegions__option_t::type& CVC4::Options::operator[] ( options::ufssRegions__option_t  ) const
template<>
const options::bitblastMode__option_t::type& CVC4::Options::operator[] ( options::bitblastMode__option_t  ) const
template<>
const options::in__option_t::type& CVC4::Options::operator[] ( options::in__option_t  ) const
template<>
const options::earlyExit__option_t::type& CVC4::Options::operator[] ( options::earlyExit__option_t  ) const
template<>
const options::sat_refine_conflicts__option_t::type& CVC4::Options::operator[] ( options::sat_refine_conflicts__option_t  ) const
template<>
const options::ufssEagerSplits__option_t::type& CVC4::Options::operator[] ( options::ufssEagerSplits__option_t  ) const
template<>
const options::threads__option_t::type& CVC4::Options::operator[] ( options::threads__option_t  ) const
template<>
const options::bitvectorAig__option_t::type& CVC4::Options::operator[] ( options::bitvectorAig__option_t  ) const
template<>
const options::out__option_t::type& CVC4::Options::operator[] ( options::out__option_t  ) const
template<>
const options::ufssTotality__option_t::type& CVC4::Options::operator[] ( options::ufssTotality__option_t  ) const
template<>
const options::minisatUseElim__option_t::type& CVC4::Options::operator[] ( options::minisatUseElim__option_t  ) const
template<>
const options::threadStackSize__option_t::type& CVC4::Options::operator[] ( options::threadStackSize__option_t  ) const
template<>
const options::ufssTotalityLimited__option_t::type& CVC4::Options::operator[] ( options::ufssTotalityLimited__option_t  ) const
template<>
const options::minisatDumpDimacs__option_t::type& CVC4::Options::operator[] ( options::minisatDumpDimacs__option_t  ) const
template<>
const options::err__option_t::type& CVC4::Options::operator[] ( options::err__option_t  ) const
template<>
const options::threadArgv__option_t::type& CVC4::Options::operator[] ( options::threadArgv__option_t  ) const
template<>
const options::bitvectorPropagate__option_t::type& CVC4::Options::operator[] ( options::bitvectorPropagate__option_t  ) const
template<>
const options::ufssTotalitySymBreak__option_t::type& CVC4::Options::operator[] ( options::ufssTotalitySymBreak__option_t  ) const
template<>
const options::inputLanguage__option_t::type& CVC4::Options::operator[] ( options::inputLanguage__option_t  ) const
template<>
const options::ufssAbortCardinality__option_t::type& CVC4::Options::operator[] ( options::ufssAbortCardinality__option_t  ) const
template<>
const options::thread_id__option_t::type& CVC4::Options::operator[] ( options::thread_id__option_t  ) const
template<>
const options::outputLanguage__option_t::type& CVC4::Options::operator[] ( options::outputLanguage__option_t  ) const
template<>
const options::ufssExplainedCliques__option_t::type& CVC4::Options::operator[] ( options::ufssExplainedCliques__option_t  ) const
template<>
const options::sharingFilterByLength__option_t::type& CVC4::Options::operator[] ( options::sharingFilterByLength__option_t  ) const
template<>
const options::languageHelp__option_t::type& CVC4::Options::operator[] ( options::languageHelp__option_t  ) const
template<>
const options::ufssSimpleCliques__option_t::type& CVC4::Options::operator[] ( options::ufssSimpleCliques__option_t  ) const
template<>
const options::fallbackSequential__option_t::type& CVC4::Options::operator[] ( options::fallbackSequential__option_t  ) const
template<>
const options::ufssDiseqPropagation__option_t::type& CVC4::Options::operator[] ( options::ufssDiseqPropagation__option_t  ) const
template<>
const options::incrementalParallel__option_t::type& CVC4::Options::operator[] ( options::incrementalParallel__option_t  ) const
template<>
const options::verbosity__option_t::type& CVC4::Options::operator[] ( options::verbosity__option_t  ) const
template<>
const options::ufssMinimalModel__option_t::type& CVC4::Options::operator[] ( options::ufssMinimalModel__option_t  ) const
template<>
const options::interactivePrompt__option_t::type& CVC4::Options::operator[] ( options::interactivePrompt__option_t  ) const
template<>
const options::statistics__option_t::type& CVC4::Options::operator[] ( options::statistics__option_t  ) const
template<>
const options::ufssCliqueSplits__option_t::type& CVC4::Options::operator[] ( options::ufssCliqueSplits__option_t  ) const
template<>
const options::statsEveryQuery__option_t::type& CVC4::Options::operator[] ( options::statsEveryQuery__option_t  ) const
template<>
const options::continuedExecution__option_t::type& CVC4::Options::operator[] ( options::continuedExecution__option_t  ) const
template<>
const options::ufssSymBreak__option_t::type& CVC4::Options::operator[] ( options::ufssSymBreak__option_t  ) const
template<>
const options::segvSpin__option_t::type& CVC4::Options::operator[] ( options::segvSpin__option_t  ) const
template<>
const options::statsHideZeros__option_t::type& CVC4::Options::operator[] ( options::statsHideZeros__option_t  ) const
template<>
const options::bitvectorToBool__option_t::type& CVC4::Options::operator[] ( options::bitvectorToBool__option_t  ) const
template<>
const options::ufssFairness__option_t::type& CVC4::Options::operator[] ( options::ufssFairness__option_t  ) const
template<>
const options::tearDownIncremental__option_t::type& CVC4::Options::operator[] ( options::tearDownIncremental__option_t  ) const
template<>
const options::parseOnly__option_t::type& CVC4::Options::operator[] ( options::parseOnly__option_t  ) const
template<>
const options::forceLogic__option_t::type& CVC4::Options::operator[] ( options::forceLogic__option_t  ) const
template<>
const options::waitToJoin__option_t::type& CVC4::Options::operator[] ( options::waitToJoin__option_t  ) const
template<>
const options::preprocessOnly__option_t::type& CVC4::Options::operator[] ( options::preprocessOnly__option_t  ) const
template<>
const options::bvAbstraction__option_t::type& CVC4::Options::operator[] ( options::bvAbstraction__option_t  ) const
template<>
const options::simplificationMode__option_t::type& CVC4::Options::operator[] ( options::simplificationMode__option_t  ) const
template<>
const options::printSuccess__option_t::type& CVC4::Options::operator[] ( options::printSuccess__option_t  ) const
template<>
const options::doStaticLearning__option_t::type& CVC4::Options::operator[] ( options::doStaticLearning__option_t  ) const
template<>
const options::skolemizeArguments__option_t::type& CVC4::Options::operator[] ( options::skolemizeArguments__option_t  ) const
template<>
const options::expandDefinitions__option_t::type& CVC4::Options::operator[] ( options::expandDefinitions__option_t  ) const
template<>
const options::bvNumFunc__option_t::type& CVC4::Options::operator[] ( options::bvNumFunc__option_t  ) const
template<>
const options::produceModels__option_t::type& CVC4::Options::operator[] ( options::produceModels__option_t  ) const
template<>
const options::bvEagerExplanations__option_t::type& CVC4::Options::operator[] ( options::bvEagerExplanations__option_t  ) const
template<>
const options::checkModels__option_t::type& CVC4::Options::operator[] ( options::checkModels__option_t  ) const
template<>
const options::arithUnateLemmaMode__option_t::type& CVC4::Options::operator[] ( options::arithUnateLemmaMode__option_t  ) const
template<>
const options::bitvectorQuickXplain__option_t::type& CVC4::Options::operator[] ( options::bitvectorQuickXplain__option_t  ) const
template<>
const options::dumpModels__option_t::type& CVC4::Options::operator[] ( options::dumpModels__option_t  ) const
template<>
const options::arithPropagationMode__option_t::type& CVC4::Options::operator[] ( options::arithPropagationMode__option_t  ) const
template<>
const options::bvIntroducePow2__option_t::type& CVC4::Options::operator[] ( options::bvIntroducePow2__option_t  ) const
template<>
const options::miniscopeQuant__option_t::type& CVC4::Options::operator[] ( options::miniscopeQuant__option_t  ) const
template<>
const options::proof__option_t::type& CVC4::Options::operator[] ( options::proof__option_t  ) const
template<>
const options::arithHeuristicPivots__option_t::type& CVC4::Options::operator[] ( options::arithHeuristicPivots__option_t  ) const
template<>
const options::miniscopeQuantFreeVar__option_t::type& CVC4::Options::operator[] ( options::miniscopeQuantFreeVar__option_t  ) const
template<>
const options::checkProofs__option_t::type& CVC4::Options::operator[] ( options::checkProofs__option_t  ) const
template<>
const options::prenexQuant__option_t::type& CVC4::Options::operator[] ( options::prenexQuant__option_t  ) const
template<>
const options::dumpProofs__option_t::type& CVC4::Options::operator[] ( options::dumpProofs__option_t  ) const
template<>
const options::varElimQuant__option_t::type& CVC4::Options::operator[] ( options::varElimQuant__option_t  ) const
template<>
const options::dumpInstantiations__option_t::type& CVC4::Options::operator[] ( options::dumpInstantiations__option_t  ) const
template<>
const options::simpleIteLiftQuant__option_t::type& CVC4::Options::operator[] ( options::simpleIteLiftQuant__option_t  ) const
template<>
const options::unsatCores__option_t::type& CVC4::Options::operator[] ( options::unsatCores__option_t  ) const
template<>
const options::cnfQuant__option_t::type& CVC4::Options::operator[] ( options::cnfQuant__option_t  ) const
template<>
const options::produceAssignments__option_t::type& CVC4::Options::operator[] ( options::produceAssignments__option_t  ) const
template<>
const options::arithPivotThreshold__option_t::type& CVC4::Options::operator[] ( options::arithPivotThreshold__option_t  ) const
template<>
const options::nnfQuant__option_t::type& CVC4::Options::operator[] ( options::nnfQuant__option_t  ) const
template<>
const options::interactive__option_t::type& CVC4::Options::operator[] ( options::interactive__option_t  ) const
template<>
const options::clauseSplit__option_t::type& CVC4::Options::operator[] ( options::clauseSplit__option_t  ) const
template<>
const options::arithDioSolver__option_t::type& CVC4::Options::operator[] ( options::arithDioSolver__option_t  ) const
template<>
const options::doITESimp__option_t::type& CVC4::Options::operator[] ( options::doITESimp__option_t  ) const
template<>
const options::preSkolemQuant__option_t::type& CVC4::Options::operator[] ( options::preSkolemQuant__option_t  ) const
template<>
const options::arithRewriteEq__option_t::type& CVC4::Options::operator[] ( options::arithRewriteEq__option_t  ) const
template<>
const options::doITESimpOnRepeat__option_t::type& CVC4::Options::operator[] ( options::doITESimpOnRepeat__option_t  ) const
template<>
const options::arithMLTrick__option_t::type& CVC4::Options::operator[] ( options::arithMLTrick__option_t  ) const
template<>
const options::macrosQuant__option_t::type& CVC4::Options::operator[] ( options::macrosQuant__option_t  ) const
template<>
const options::foPropQuant__option_t::type& CVC4::Options::operator[] ( options::foPropQuant__option_t  ) const
template<>
const options::compressItes__option_t::type& CVC4::Options::operator[] ( options::compressItes__option_t  ) const
template<>
const options::doCutAllBounded__option_t::type& CVC4::Options::operator[] ( options::doCutAllBounded__option_t  ) const
template<>
const options::smartTriggers__option_t::type& CVC4::Options::operator[] ( options::smartTriggers__option_t  ) const
template<>
const options::maxCutsInContext__option_t::type& CVC4::Options::operator[] ( options::maxCutsInContext__option_t  ) const
template<>
const options::unconstrainedSimp__option_t::type& CVC4::Options::operator[] ( options::unconstrainedSimp__option_t  ) const
template<>
const options::relevantTriggers__option_t::type& CVC4::Options::operator[] ( options::relevantTriggers__option_t  ) const
template<>
const options::revertArithModels__option_t::type& CVC4::Options::operator[] ( options::revertArithModels__option_t  ) const
template<>
const options::relationalTriggers__option_t::type& CVC4::Options::operator[] ( options::relationalTriggers__option_t  ) const
template<>
const options::repeatSimp__option_t::type& CVC4::Options::operator[] ( options::repeatSimp__option_t  ) const
template<>
const options::registerQuantBodyTerms__option_t::type& CVC4::Options::operator[] ( options::registerQuantBodyTerms__option_t  ) const
template<>
const options::havePenalties__option_t::type& CVC4::Options::operator[] ( options::havePenalties__option_t  ) const
template<>
const options::zombieHuntThreshold__option_t::type& CVC4::Options::operator[] ( options::zombieHuntThreshold__option_t  ) const
template<>
const options::instWhenMode__option_t::type& CVC4::Options::operator[] ( options::instWhenMode__option_t  ) const
template<>
const options::useFC__option_t::type& CVC4::Options::operator[] ( options::useFC__option_t  ) const
template<>
const options::sortInference__option_t::type& CVC4::Options::operator[] ( options::sortInference__option_t  ) const
template<>
const options::instMaxLevel__option_t::type& CVC4::Options::operator[] ( options::instMaxLevel__option_t  ) const
template<>
const options::incrementalSolving__option_t::type& CVC4::Options::operator[] ( options::incrementalSolving__option_t  ) const
template<>
const options::useSOI__option_t::type& CVC4::Options::operator[] ( options::useSOI__option_t  ) const
template<>
const options::eagerInstQuant__option_t::type& CVC4::Options::operator[] ( options::eagerInstQuant__option_t  ) const
template<>
const options::abstractValues__option_t::type& CVC4::Options::operator[] ( options::abstractValues__option_t  ) const
template<>
const options::restrictedPivots__option_t::type& CVC4::Options::operator[] ( options::restrictedPivots__option_t  ) const
template<>
const options::fullSaturateQuant__option_t::type& CVC4::Options::operator[] ( options::fullSaturateQuant__option_t  ) const
template<>
const options::modelUninterpDtEnum__option_t::type& CVC4::Options::operator[] ( options::modelUninterpDtEnum__option_t  ) const
template<>
const options::literalMatchMode__option_t::type& CVC4::Options::operator[] ( options::literalMatchMode__option_t  ) const
template<>
const options::collectPivots__option_t::type& CVC4::Options::operator[] ( options::collectPivots__option_t  ) const
template<>
const options::cbqi__option_t::type& CVC4::Options::operator[] ( options::cbqi__option_t  ) const
template<>
const options::useApprox__option_t::type& CVC4::Options::operator[] ( options::useApprox__option_t  ) const
template<>
const options::recurseCbqi__option_t::type& CVC4::Options::operator[] ( options::recurseCbqi__option_t  ) const
template<>
const options::maxApproxDepth__option_t::type& CVC4::Options::operator[] ( options::maxApproxDepth__option_t  ) const
template<>
const options::perCallResourceLimit__option_t::type& CVC4::Options::operator[] ( options::perCallResourceLimit__option_t  ) const
template<>
const options::userPatternsQuant__option_t::type& CVC4::Options::operator[] ( options::userPatternsQuant__option_t  ) const
template<>
const options::rewriteApplyToConst__option_t::type& CVC4::Options::operator[] ( options::rewriteApplyToConst__option_t  ) const
template<>
const options::flipDecision__option_t::type& CVC4::Options::operator[] ( options::flipDecision__option_t  ) const
template<>
const options::replayFilename__option_t::type& CVC4::Options::operator[] ( options::replayFilename__option_t  ) const
template<>
const options::internalReps__option_t::type& CVC4::Options::operator[] ( options::internalReps__option_t  ) const
template<>
const options::newProp__option_t::type& CVC4::Options::operator[] ( options::newProp__option_t  ) const
template<>
const options::replayLog__option_t::type& CVC4::Options::operator[] ( options::replayLog__option_t  ) const
template<>
const options::finiteModelFind__option_t::type& CVC4::Options::operator[] ( options::finiteModelFind__option_t  ) const
template<>
const options::arithPropAsLemmaLength__option_t::type& CVC4::Options::operator[] ( options::arithPropAsLemmaLength__option_t  ) const
template<>
const options::replayStream__option_t::type& CVC4::Options::operator[] ( options::replayStream__option_t  ) const
template<>
const options::mbqiMode__option_t::type& CVC4::Options::operator[] ( options::mbqiMode__option_t  ) const
template<>
const options::soiQuickExplain__option_t::type& CVC4::Options::operator[] ( options::soiQuickExplain__option_t  ) const
template<>
const options::lemmaInputChannel__option_t::type& CVC4::Options::operator[] ( options::lemmaInputChannel__option_t  ) const
template<>
const options::fmfOneInstPerRound__option_t::type& CVC4::Options::operator[] ( options::fmfOneInstPerRound__option_t  ) const
template<>
const options::rewriteDivk__option_t::type& CVC4::Options::operator[] ( options::rewriteDivk__option_t  ) const
template<>
const options::fmfOneQuantPerRound__option_t::type& CVC4::Options::operator[] ( options::fmfOneQuantPerRound__option_t  ) const
template<>
const options::lemmaOutputChannel__option_t::type& CVC4::Options::operator[] ( options::lemmaOutputChannel__option_t  ) const
template<>
const options::fmfInstEngine__option_t::type& CVC4::Options::operator[] ( options::fmfInstEngine__option_t  ) const
template<>
const options::replayFailureLemma__option_t::type& CVC4::Options::operator[] ( options::replayFailureLemma__option_t  ) const
template<>
const options::fmfInstGen__option_t::type& CVC4::Options::operator[] ( options::fmfInstGen__option_t  ) const
template<>
const options::dioSolverTurns__option_t::type& CVC4::Options::operator[] ( options::dioSolverTurns__option_t  ) const
template<>
const options::rrTurns__option_t::type& CVC4::Options::operator[] ( options::rrTurns__option_t  ) const
template<>
const options::fmfFreshDistConst__option_t::type& CVC4::Options::operator[] ( options::fmfFreshDistConst__option_t  ) const
template<>
const options::dioRepeat__option_t::type& CVC4::Options::operator[] ( options::dioRepeat__option_t  ) const
template<>
const options::fmfFmcSimple__option_t::type& CVC4::Options::operator[] ( options::fmfFmcSimple__option_t  ) const
template<>
const options::replayEarlyCloseDepths__option_t::type& CVC4::Options::operator[] ( options::replayEarlyCloseDepths__option_t  ) const
template<>
const options::fmfBoundInt__option_t::type& CVC4::Options::operator[] ( options::fmfBoundInt__option_t  ) const
template<>
const options::replayFailurePenalty__option_t::type& CVC4::Options::operator[] ( options::replayFailurePenalty__option_t  ) const
template<>
const options::fmfBoundIntLazy__option_t::type& CVC4::Options::operator[] ( options::fmfBoundIntLazy__option_t  ) const
template<>
const options::replayRejectCutSize__option_t::type& CVC4::Options::operator[] ( options::replayRejectCutSize__option_t  ) const
template<>
const options::axiomInstMode__option_t::type& CVC4::Options::operator[] ( options::axiomInstMode__option_t  ) const
template<>
const options::lemmaRejectCutSize__option_t::type& CVC4::Options::operator[] ( options::lemmaRejectCutSize__option_t  ) const
template<>
const options::quantConflictFind__option_t::type& CVC4::Options::operator[] ( options::quantConflictFind__option_t  ) const
template<>
const options::soiApproxMajorFailure__option_t::type& CVC4::Options::operator[] ( options::soiApproxMajorFailure__option_t  ) const
template<>
const options::qcfMode__option_t::type& CVC4::Options::operator[] ( options::qcfMode__option_t  ) const
template<>
const options::qcfWhenMode__option_t::type& CVC4::Options::operator[] ( options::qcfWhenMode__option_t  ) const
template<>
const options::soiApproxMinorFailure__option_t::type& CVC4::Options::operator[] ( options::soiApproxMinorFailure__option_t  ) const
template<>
const options::qcfTConstraint__option_t::type& CVC4::Options::operator[] ( options::qcfTConstraint__option_t  ) const
template<>
const options::quantRewriteRules__option_t::type& CVC4::Options::operator[] ( options::quantRewriteRules__option_t  ) const
template<>
const options::ppAssertMaxSubSize__option_t::type& CVC4::Options::operator[] ( options::ppAssertMaxSubSize__option_t  ) const
template<>
const options::rrOneInstPerRound__option_t::type& CVC4::Options::operator[] ( options::rrOneInstPerRound__option_t  ) const
template<>
const options::maxReplayTree__option_t::type& CVC4::Options::operator[] ( options::maxReplayTree__option_t  ) const
template<>
const options::dtStcInduction__option_t::type& CVC4::Options::operator[] ( options::dtStcInduction__option_t  ) const
template<>
const options::pbRewrites__option_t::type& CVC4::Options::operator[] ( options::pbRewrites__option_t  ) const
template<>
const options::pbRewriteThreshold__option_t::type& CVC4::Options::operator[] ( options::pbRewriteThreshold__option_t  ) const
std::vector<std::string> CVC4::Options::parseOptions ( int  argc,
char *  argv[] 
)
throw (OptionException
)

Initialize the options based on the given command-line arguments.

The return value is what's left of the command line (that is, the non-option arguments).

static void CVC4::Options::printLanguageHelp ( std::ostream &  out)
static

Print help for the –lang command line option.

static void CVC4::Options::printShortUsage ( const std::string  msg,
std::ostream &  out 
)
static

Print command-line option usage message for only the most-commonly used options.

The message is prefixed by "msg"—which could be an error message causing the usage output in the first place, e.g. "no such option --foo"

static void CVC4::Options::printUsage ( const std::string  msg,
std::ostream &  out 
)
static

Print overall command-line option usage message, prefixed by "msg"—which could be an error message causing the usage output in the first place, e.g.

"no such option --foo"

template<>
void CVC4::Options::set ( options::idlRewriteEq__option_t  ,
const options::idlRewriteEq__option_t::type x 
)
template<class T >
void CVC4::Options::set ( ,
const typename T::type &   
)
inline

Set the value of the given option.

Use of this default implementation causes a compile-time error; write-able options specialize this template with a real implementation.

Definition at line 78 of file options.h.

Referenced by CVC4::options::idlRewriteEq__option_t::set(), CVC4::options::dtForceAssignment__option_t::set(), CVC4::options::modelFormatMode__option_t::set(), CVC4::options::theoryOfMode__option_t::set(), CVC4::options::instFormatMode__option_t::set(), CVC4::options::arraysOptimizeLinear__option_t::set(), CVC4::options::theoryAlternates__option_t::set(), CVC4::options::arraysLazyRIntro1__option_t::set(), CVC4::options::stringExp__option_t::set(), CVC4::options::arraysModelBased__option_t::set(), CVC4::options::decisionMode__option_t::set(), CVC4::options::arraysEagerIndexSplitting__option_t::set(), CVC4::options::stringFMF__option_t::set(), CVC4::options::decisionStopOnly__option_t::set(), CVC4::options::arraysEagerLemmas__option_t::set(), CVC4::options::satRandomSeed__option_t::set(), CVC4::options::satVarDecay__option_t::set(), CVC4::options::satClauseDecay__option_t::set(), CVC4::options::ufSymmetryBreaker__option_t::set(), CVC4::options::minisatUseElim__option_t::set(), CVC4::options::binary_name__option_t::set(), CVC4::options::bitblastMode__option_t::set(), CVC4::options::in__option_t::set(), CVC4::options::bitvectorAig__option_t::set(), CVC4::options::out__option_t::set(), CVC4::options::bitvectorAigSimplifications__option_t::set(), CVC4::options::err__option_t::set(), CVC4::options::threadArgv__option_t::set(), CVC4::options::bitvectorPropagate__option_t::set(), CVC4::options::bitvectorEqualitySolver__option_t::set(), CVC4::options::thread_id__option_t::set(), CVC4::options::inputLanguage__option_t::set(), CVC4::options::bitvectorEqualitySlicer__option_t::set(), CVC4::options::outputLanguage__option_t::set(), CVC4::options::sharingFilterByLength__option_t::set(), CVC4::options::bitvectorInequalitySolver__option_t::set(), CVC4::options::languageHelp__option_t::set(), CVC4::options::verbosity__option_t::set(), CVC4::options::bitvectorAlgebraicSolver__option_t::set(), CVC4::options::bitvectorAlgebraicBudget__option_t::set(), CVC4::options::bitvectorToBool__option_t::set(), CVC4::options::parseOnly__option_t::set(), CVC4::options::bvAbstraction__option_t::set(), CVC4::options::skolemizeArguments__option_t::set(), CVC4::options::bvEagerExplanations__option_t::set(), CVC4::options::simplificationMode__option_t::set(), CVC4::options::arithHeuristicPivots__option_t::set(), CVC4::options::arithStandardCheckVarOrderPivots__option_t::set(), CVC4::options::interactive__option_t::set(), CVC4::options::doITESimp__option_t::set(), CVC4::options::arithPivotThreshold__option_t::set(), CVC4::options::doITESimpOnRepeat__option_t::set(), CVC4::options::simplifyWithCareEnabled__option_t::set(), CVC4::options::compressItes__option_t::set(), CVC4::options::arithRewriteEq__option_t::set(), CVC4::options::unconstrainedSimp__option_t::set(), CVC4::options::repeatSimp__option_t::set(), CVC4::options::preSkolemQuant__option_t::set(), CVC4::options::doCutAllBounded__option_t::set(), CVC4::options::sortInference__option_t::set(), CVC4::options::havePenalties__option_t::set(), CVC4::options::useFC__option_t::set(), CVC4::options::useSOI__option_t::set(), CVC4::options::restrictedPivots__option_t::set(), CVC4::options::collectPivots__option_t::set(), CVC4::options::useApprox__option_t::set(), CVC4::options::instWhenMode__option_t::set(), CVC4::options::maxApproxDepth__option_t::set(), CVC4::options::exportDioDecompositions__option_t::set(), CVC4::options::newProp__option_t::set(), CVC4::options::arithPropAsLemmaLength__option_t::set(), CVC4::options::replayStream__option_t::set(), CVC4::options::cbqi__option_t::set(), CVC4::options::lemmaInputChannel__option_t::set(), CVC4::options::soiQuickExplain__option_t::set(), CVC4::options::rewriteDivk__option_t::set(), CVC4::options::lemmaOutputChannel__option_t::set(), CVC4::options::finiteModelFind__option_t::set(), CVC4::options::mbqiMode__option_t::set(), CVC4::options::fmfBoundInt__option_t::set(), CVC4::options::fmfBoundIntLazy__option_t::set(), CVC4::options::quantConflictFind__option_t::set(), and CVC4::options::qcfTConstraint__option_t::set().

template<>
void CVC4::Options::set ( options::theoryOfMode__option_t  ,
const options::theoryOfMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::modelFormatMode__option_t  ,
const options::modelFormatMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::dtForceAssignment__option_t  ,
const options::dtForceAssignment__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arraysOptimizeLinear__option_t  ,
const options::arraysOptimizeLinear__option_t::type x 
)
template<>
void CVC4::Options::set ( options::theoryAlternates__option_t  ,
const options::theoryAlternates__option_t::type x 
)
template<>
void CVC4::Options::set ( options::instFormatMode__option_t  ,
const options::instFormatMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arraysLazyRIntro1__option_t  ,
const options::arraysLazyRIntro1__option_t::type x 
)
template<>
void CVC4::Options::set ( options::stringExp__option_t  ,
const options::stringExp__option_t::type x 
)
template<>
void CVC4::Options::set ( options::decisionMode__option_t  ,
const options::decisionMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arraysModelBased__option_t  ,
const options::arraysModelBased__option_t::type x 
)
template<>
void CVC4::Options::set ( options::decisionStopOnly__option_t  ,
const options::decisionStopOnly__option_t::type x 
)
template<>
void CVC4::Options::set ( options::stringFMF__option_t  ,
const options::stringFMF__option_t::type x 
)
template<>
void CVC4::Options::set ( options::satRandomSeed__option_t  ,
const options::satRandomSeed__option_t::type x 
)
template<>
void CVC4::Options::set ( options::satVarDecay__option_t  ,
const options::satVarDecay__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arraysEagerLemmas__option_t  ,
const options::arraysEagerLemmas__option_t::type x 
)
template<>
void CVC4::Options::set ( options::satClauseDecay__option_t  ,
const options::satClauseDecay__option_t::type x 
)
template<>
void CVC4::Options::set ( options::ufSymmetryBreaker__option_t  ,
const options::ufSymmetryBreaker__option_t::type x 
)
template<>
void CVC4::Options::set ( options::binary_name__option_t  ,
const options::binary_name__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bitblastMode__option_t  ,
const options::bitblastMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::in__option_t  ,
const options::in__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bitvectorAig__option_t  ,
const options::bitvectorAig__option_t::type x 
)
template<>
void CVC4::Options::set ( options::out__option_t  ,
const options::out__option_t::type x 
)
template<>
void CVC4::Options::set ( options::minisatUseElim__option_t  ,
const options::minisatUseElim__option_t::type x 
)
template<>
void CVC4::Options::set ( options::err__option_t  ,
const options::err__option_t::type x 
)
template<>
void CVC4::Options::set ( options::threadArgv__option_t  ,
const options::threadArgv__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bitvectorPropagate__option_t  ,
const options::bitvectorPropagate__option_t::type x 
)
template<>
void CVC4::Options::set ( options::inputLanguage__option_t  ,
const options::inputLanguage__option_t::type x 
)
template<>
void CVC4::Options::set ( options::thread_id__option_t  ,
const options::thread_id__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bitvectorEqualitySolver__option_t  ,
const options::bitvectorEqualitySolver__option_t::type x 
)
template<>
void CVC4::Options::set ( options::outputLanguage__option_t  ,
const options::outputLanguage__option_t::type x 
)
template<>
void CVC4::Options::set ( options::sharingFilterByLength__option_t  ,
const options::sharingFilterByLength__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bitvectorEqualitySlicer__option_t  ,
const options::bitvectorEqualitySlicer__option_t::type x 
)
template<>
void CVC4::Options::set ( options::languageHelp__option_t  ,
const options::languageHelp__option_t::type x 
)
template<>
void CVC4::Options::set ( options::verbosity__option_t  ,
const options::verbosity__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bitvectorToBool__option_t  ,
const options::bitvectorToBool__option_t::type x 
)
template<>
void CVC4::Options::set ( options::parseOnly__option_t  ,
const options::parseOnly__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bvAbstraction__option_t  ,
const options::bvAbstraction__option_t::type x 
)
template<>
void CVC4::Options::set ( options::simplificationMode__option_t  ,
const options::simplificationMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::skolemizeArguments__option_t  ,
const options::skolemizeArguments__option_t::type x 
)
template<>
void CVC4::Options::set ( options::bvEagerExplanations__option_t  ,
const options::bvEagerExplanations__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arithHeuristicPivots__option_t  ,
const options::arithHeuristicPivots__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arithPivotThreshold__option_t  ,
const options::arithPivotThreshold__option_t::type x 
)
template<>
void CVC4::Options::set ( options::interactive__option_t  ,
const options::interactive__option_t::type x 
)
template<>
void CVC4::Options::set ( options::doITESimp__option_t  ,
const options::doITESimp__option_t::type x 
)
template<>
void CVC4::Options::set ( options::preSkolemQuant__option_t  ,
const options::preSkolemQuant__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arithRewriteEq__option_t  ,
const options::arithRewriteEq__option_t::type x 
)
template<>
void CVC4::Options::set ( options::doITESimpOnRepeat__option_t  ,
const options::doITESimpOnRepeat__option_t::type x 
)
template<>
void CVC4::Options::set ( options::simplifyWithCareEnabled__option_t  ,
const options::simplifyWithCareEnabled__option_t::type x 
)
template<>
void CVC4::Options::set ( options::compressItes__option_t  ,
const options::compressItes__option_t::type x 
)
template<>
void CVC4::Options::set ( options::doCutAllBounded__option_t  ,
const options::doCutAllBounded__option_t::type x 
)
template<>
void CVC4::Options::set ( options::unconstrainedSimp__option_t  ,
const options::unconstrainedSimp__option_t::type x 
)
template<>
void CVC4::Options::set ( options::repeatSimp__option_t  ,
const options::repeatSimp__option_t::type x 
)
template<>
void CVC4::Options::set ( options::havePenalties__option_t  ,
const options::havePenalties__option_t::type x 
)
template<>
void CVC4::Options::set ( options::instWhenMode__option_t  ,
const options::instWhenMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::useFC__option_t  ,
const options::useFC__option_t::type x 
)
template<>
void CVC4::Options::set ( options::sortInference__option_t  ,
const options::sortInference__option_t::type x 
)
template<>
void CVC4::Options::set ( options::useSOI__option_t  ,
const options::useSOI__option_t::type x 
)
template<>
void CVC4::Options::set ( options::restrictedPivots__option_t  ,
const options::restrictedPivots__option_t::type x 
)
template<>
void CVC4::Options::set ( options::collectPivots__option_t  ,
const options::collectPivots__option_t::type x 
)
template<>
void CVC4::Options::set ( options::cbqi__option_t  ,
const options::cbqi__option_t::type x 
)
template<>
void CVC4::Options::set ( options::useApprox__option_t  ,
const options::useApprox__option_t::type x 
)
template<>
void CVC4::Options::set ( options::maxApproxDepth__option_t  ,
const options::maxApproxDepth__option_t::type x 
)
template<>
void CVC4::Options::set ( options::exportDioDecompositions__option_t  ,
const options::exportDioDecompositions__option_t::type x 
)
template<>
void CVC4::Options::set ( options::newProp__option_t  ,
const options::newProp__option_t::type x 
)
template<>
void CVC4::Options::set ( options::finiteModelFind__option_t  ,
const options::finiteModelFind__option_t::type x 
)
template<>
void CVC4::Options::set ( options::arithPropAsLemmaLength__option_t  ,
const options::arithPropAsLemmaLength__option_t::type x 
)
template<>
void CVC4::Options::set ( options::replayStream__option_t  ,
const options::replayStream__option_t::type x 
)
template<>
void CVC4::Options::set ( options::mbqiMode__option_t  ,
const options::mbqiMode__option_t::type x 
)
template<>
void CVC4::Options::set ( options::soiQuickExplain__option_t  ,
const options::soiQuickExplain__option_t::type x 
)
template<>
void CVC4::Options::set ( options::lemmaInputChannel__option_t  ,
const options::lemmaInputChannel__option_t::type x 
)
template<>
void CVC4::Options::set ( options::rewriteDivk__option_t  ,
const options::rewriteDivk__option_t::type x 
)
template<>
void CVC4::Options::set ( options::lemmaOutputChannel__option_t  ,
const options::lemmaOutputChannel__option_t::type x 
)
template<>
void CVC4::Options::set ( options::fmfBoundInt__option_t  ,
const options::fmfBoundInt__option_t::type x 
)
template<>
void CVC4::Options::set ( options::fmfBoundIntLazy__option_t  ,
const options::fmfBoundIntLazy__option_t::type x 
)
template<>
void CVC4::Options::set ( options::quantConflictFind__option_t  ,
const options::quantConflictFind__option_t::type x 
)
template<>
void CVC4::Options::set ( options::qcfTConstraint__option_t  ,
const options::qcfTConstraint__option_t::type x 
)
static std::string CVC4::Options::suggestCommandLineOptions ( const std::string &  optionName)
throw (
)
static

Look up long command-line option names that bear some similarity to the given name.

Returns an empty string if there are no suggestions.

static std::vector<std::string> CVC4::Options::suggestSmtOptions ( const std::string &  optionName)
throw (
)
static

Look up SMT option names that bear some similarity to the given name.

Don't include the initial ":". This might be useful in case of typos. Can return an empty vector if there are no suggestions.

template<>
bool CVC4::Options::wasSetByUser ( options::booleanTermConversionMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::idlRewriteEq__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::setsPropagate__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dtRewriteErrorSel__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::setsEagerLemmas__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::theoryOfMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::modelFormatMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dtForceAssignment__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::strictParsing__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::defaultExprDepth__option_t  ) const
template<class T >
bool CVC4::Options::wasSetByUser ( ) const

Returns true iff the value of the given option was set by the user via a command-line option or SmtEngine::setOption().

(Options::set() is low-level and doesn't count.) Returns false otherwise.

Referenced by CVC4::options::idlRewriteEq__option_t::wasSetByUser(), CVC4::options::booleanTermConversionMode__option_t::wasSetByUser(), CVC4::options::dtRewriteErrorSel__option_t::wasSetByUser(), CVC4::options::setsPropagate__option_t::wasSetByUser(), CVC4::options::setsEagerLemmas__option_t::wasSetByUser(), CVC4::options::dtForceAssignment__option_t::wasSetByUser(), CVC4::options::modelFormatMode__option_t::wasSetByUser(), CVC4::options::strictParsing__option_t::wasSetByUser(), CVC4::options::theoryOfMode__option_t::wasSetByUser(), CVC4::options::memoryMap__option_t::wasSetByUser(), CVC4::options::arraysOptimizeLinear__option_t::wasSetByUser(), CVC4::options::theoryAlternates__option_t::wasSetByUser(), CVC4::options::instFormatMode__option_t::wasSetByUser(), CVC4::options::defaultExprDepth__option_t::wasSetByUser(), CVC4::options::semanticChecks__option_t::wasSetByUser(), CVC4::options::arraysLazyRIntro1__option_t::wasSetByUser(), CVC4::options::defaultDagThresh__option_t::wasSetByUser(), CVC4::options::earlyTypeChecking__option_t::wasSetByUser(), CVC4::options::filesystemAccess__option_t::wasSetByUser(), CVC4::options::arraysModelBased__option_t::wasSetByUser(), CVC4::options::stringExp__option_t::wasSetByUser(), CVC4::options::typeChecking__option_t::wasSetByUser(), CVC4::options::arraysEagerIndexSplitting__option_t::wasSetByUser(), CVC4::options::stringLB__option_t::wasSetByUser(), CVC4::options::decisionMode__option_t::wasSetByUser(), CVC4::options::biasedITERemoval__option_t::wasSetByUser(), CVC4::options::arraysEagerLemmas__option_t::wasSetByUser(), CVC4::options::satRandomFreq__option_t::wasSetByUser(), CVC4::options::stringFMF__option_t::wasSetByUser(), CVC4::options::decisionStopOnly__option_t::wasSetByUser(), CVC4::options::satRandomSeed__option_t::wasSetByUser(), CVC4::options::stringEIT__option_t::wasSetByUser(), CVC4::options::decisionThreshold__option_t::wasSetByUser(), CVC4::options::satVarDecay__option_t::wasSetByUser(), CVC4::options::stringOpt1__option_t::wasSetByUser(), CVC4::options::decisionUseWeight__option_t::wasSetByUser(), CVC4::options::satClauseDecay__option_t::wasSetByUser(), CVC4::options::stringOpt2__option_t::wasSetByUser(), CVC4::options::decisionRandomWeight__option_t::wasSetByUser(), CVC4::options::stringCharCardinality__option_t::wasSetByUser(), CVC4::options::satRestartFirst__option_t::wasSetByUser(), CVC4::options::decisionWeightInternal__option_t::wasSetByUser(), CVC4::options::satRestartInc__option_t::wasSetByUser(), CVC4::options::sat_refine_conflicts__option_t::wasSetByUser(), CVC4::options::ufSymmetryBreaker__option_t::wasSetByUser(), CVC4::options::minisatUseElim__option_t::wasSetByUser(), CVC4::options::condenseFunctionValues__option_t::wasSetByUser(), CVC4::options::version__option_t::wasSetByUser(), CVC4::options::ufssRegions__option_t::wasSetByUser(), CVC4::options::minisatDumpDimacs__option_t::wasSetByUser(), CVC4::options::ufssEagerSplits__option_t::wasSetByUser(), CVC4::options::help__option_t::wasSetByUser(), CVC4::options::bitblastMode__option_t::wasSetByUser(), CVC4::options::ufssTotality__option_t::wasSetByUser(), CVC4::options::binary_name__option_t::wasSetByUser(), CVC4::options::earlyExit__option_t::wasSetByUser(), CVC4::options::in__option_t::wasSetByUser(), CVC4::options::bitvectorAig__option_t::wasSetByUser(), CVC4::options::ufssTotalityLimited__option_t::wasSetByUser(), CVC4::options::threads__option_t::wasSetByUser(), CVC4::options::threadStackSize__option_t::wasSetByUser(), CVC4::options::bitvectorAigSimplifications__option_t::wasSetByUser(), CVC4::options::ufssTotalitySymBreak__option_t::wasSetByUser(), CVC4::options::out__option_t::wasSetByUser(), CVC4::options::err__option_t::wasSetByUser(), CVC4::options::bitvectorPropagate__option_t::wasSetByUser(), CVC4::options::ufssAbortCardinality__option_t::wasSetByUser(), CVC4::options::threadArgv__option_t::wasSetByUser(), CVC4::options::bitvectorEqualitySolver__option_t::wasSetByUser(), CVC4::options::inputLanguage__option_t::wasSetByUser(), CVC4::options::ufssExplainedCliques__option_t::wasSetByUser(), CVC4::options::thread_id__option_t::wasSetByUser(), CVC4::options::bitvectorEqualitySlicer__option_t::wasSetByUser(), CVC4::options::ufssSimpleCliques__option_t::wasSetByUser(), CVC4::options::outputLanguage__option_t::wasSetByUser(), CVC4::options::sharingFilterByLength__option_t::wasSetByUser(), CVC4::options::bitvectorInequalitySolver__option_t::wasSetByUser(), CVC4::options::ufssDiseqPropagation__option_t::wasSetByUser(), CVC4::options::fallbackSequential__option_t::wasSetByUser(), CVC4::options::languageHelp__option_t::wasSetByUser(), CVC4::options::verbosity__option_t::wasSetByUser(), CVC4::options::bitvectorAlgebraicSolver__option_t::wasSetByUser(), CVC4::options::ufssMinimalModel__option_t::wasSetByUser(), CVC4::options::incrementalParallel__option_t::wasSetByUser(), CVC4::options::statistics__option_t::wasSetByUser(), CVC4::options::bitvectorAlgebraicBudget__option_t::wasSetByUser(), CVC4::options::ufssCliqueSplits__option_t::wasSetByUser(), CVC4::options::interactivePrompt__option_t::wasSetByUser(), CVC4::options::statsEveryQuery__option_t::wasSetByUser(), CVC4::options::bitvectorToBool__option_t::wasSetByUser(), CVC4::options::ufssSymBreak__option_t::wasSetByUser(), CVC4::options::continuedExecution__option_t::wasSetByUser(), CVC4::options::segvSpin__option_t::wasSetByUser(), CVC4::options::bitvectorDivByZeroConst__option_t::wasSetByUser(), CVC4::options::statsHideZeros__option_t::wasSetByUser(), CVC4::options::ufssFairness__option_t::wasSetByUser(), CVC4::options::bvAbstraction__option_t::wasSetByUser(), CVC4::options::parseOnly__option_t::wasSetByUser(), CVC4::options::tearDownIncremental__option_t::wasSetByUser(), CVC4::options::skolemizeArguments__option_t::wasSetByUser(), CVC4::options::preprocessOnly__option_t::wasSetByUser(), CVC4::options::waitToJoin__option_t::wasSetByUser(), CVC4::options::printSuccess__option_t::wasSetByUser(), CVC4::options::bvNumFunc__option_t::wasSetByUser(), CVC4::options::bvEagerExplanations__option_t::wasSetByUser(), CVC4::options::bitvectorQuickXplain__option_t::wasSetByUser(), CVC4::options::bvIntroducePow2__option_t::wasSetByUser(), CVC4::options::forceLogic__option_t::wasSetByUser(), CVC4::options::simplificationMode__option_t::wasSetByUser(), CVC4::options::doStaticLearning__option_t::wasSetByUser(), CVC4::options::expandDefinitions__option_t::wasSetByUser(), CVC4::options::produceModels__option_t::wasSetByUser(), CVC4::options::checkModels__option_t::wasSetByUser(), CVC4::options::dumpModels__option_t::wasSetByUser(), CVC4::options::proof__option_t::wasSetByUser(), CVC4::options::checkProofs__option_t::wasSetByUser(), CVC4::options::arithUnateLemmaMode__option_t::wasSetByUser(), CVC4::options::dumpProofs__option_t::wasSetByUser(), CVC4::options::arithPropagationMode__option_t::wasSetByUser(), CVC4::options::dumpInstantiations__option_t::wasSetByUser(), CVC4::options::arithHeuristicPivots__option_t::wasSetByUser(), CVC4::options::unsatCores__option_t::wasSetByUser(), CVC4::options::arithStandardCheckVarOrderPivots__option_t::wasSetByUser(), CVC4::options::produceAssignments__option_t::wasSetByUser(), CVC4::options::arithErrorSelectionRule__option_t::wasSetByUser(), CVC4::options::miniscopeQuant__option_t::wasSetByUser(), CVC4::options::interactive__option_t::wasSetByUser(), CVC4::options::arithSimplexCheckPeriod__option_t::wasSetByUser(), CVC4::options::miniscopeQuantFreeVar__option_t::wasSetByUser(), CVC4::options::arithPivotThreshold__option_t::wasSetByUser(), CVC4::options::doITESimp__option_t::wasSetByUser(), CVC4::options::prenexQuant__option_t::wasSetByUser(), CVC4::options::varElimQuant__option_t::wasSetByUser(), CVC4::options::arithPropagateMaxLength__option_t::wasSetByUser(), CVC4::options::doITESimpOnRepeat__option_t::wasSetByUser(), CVC4::options::simplifyWithCareEnabled__option_t::wasSetByUser(), CVC4::options::arithDioSolver__option_t::wasSetByUser(), CVC4::options::simpleIteLiftQuant__option_t::wasSetByUser(), CVC4::options::compressItes__option_t::wasSetByUser(), CVC4::options::arithRewriteEq__option_t::wasSetByUser(), CVC4::options::cnfQuant__option_t::wasSetByUser(), CVC4::options::unconstrainedSimp__option_t::wasSetByUser(), CVC4::options::arithMLTrick__option_t::wasSetByUser(), CVC4::options::nnfQuant__option_t::wasSetByUser(), CVC4::options::repeatSimp__option_t::wasSetByUser(), CVC4::options::arithMLTrickSubstitutions__option_t::wasSetByUser(), CVC4::options::clauseSplit__option_t::wasSetByUser(), CVC4::options::doCutAllBounded__option_t::wasSetByUser(), CVC4::options::zombieHuntThreshold__option_t::wasSetByUser(), CVC4::options::preSkolemQuant__option_t::wasSetByUser(), CVC4::options::maxCutsInContext__option_t::wasSetByUser(), CVC4::options::aggressiveMiniscopeQuant__option_t::wasSetByUser(), CVC4::options::sortInference__option_t::wasSetByUser(), CVC4::options::revertArithModels__option_t::wasSetByUser(), CVC4::options::incrementalSolving__option_t::wasSetByUser(), CVC4::options::macrosQuant__option_t::wasSetByUser(), CVC4::options::foPropQuant__option_t::wasSetByUser(), CVC4::options::abstractValues__option_t::wasSetByUser(), CVC4::options::havePenalties__option_t::wasSetByUser(), CVC4::options::useFC__option_t::wasSetByUser(), CVC4::options::modelUninterpDtEnum__option_t::wasSetByUser(), CVC4::options::smartTriggers__option_t::wasSetByUser(), CVC4::options::useSOI__option_t::wasSetByUser(), CVC4::options::relevantTriggers__option_t::wasSetByUser(), CVC4::options::cumulativeMillisecondLimit__option_t::wasSetByUser(), CVC4::options::restrictedPivots__option_t::wasSetByUser(), CVC4::options::perCallMillisecondLimit__option_t::wasSetByUser(), CVC4::options::relationalTriggers__option_t::wasSetByUser(), CVC4::options::collectPivots__option_t::wasSetByUser(), CVC4::options::cumulativeResourceLimit__option_t::wasSetByUser(), CVC4::options::registerQuantBodyTerms__option_t::wasSetByUser(), CVC4::options::perCallResourceLimit__option_t::wasSetByUser(), CVC4::options::useApprox__option_t::wasSetByUser(), CVC4::options::instWhenMode__option_t::wasSetByUser(), CVC4::options::maxApproxDepth__option_t::wasSetByUser(), CVC4::options::rewriteApplyToConst__option_t::wasSetByUser(), CVC4::options::instMaxLevel__option_t::wasSetByUser(), CVC4::options::eagerInstQuant__option_t::wasSetByUser(), CVC4::options::replayFilename__option_t::wasSetByUser(), CVC4::options::exportDioDecompositions__option_t::wasSetByUser(), CVC4::options::replayLog__option_t::wasSetByUser(), CVC4::options::fullSaturateQuant__option_t::wasSetByUser(), CVC4::options::newProp__option_t::wasSetByUser(), CVC4::options::literalMatchMode__option_t::wasSetByUser(), CVC4::options::replayStream__option_t::wasSetByUser(), CVC4::options::arithPropAsLemmaLength__option_t::wasSetByUser(), CVC4::options::lemmaInputChannel__option_t::wasSetByUser(), CVC4::options::cbqi__option_t::wasSetByUser(), CVC4::options::soiQuickExplain__option_t::wasSetByUser(), CVC4::options::recurseCbqi__option_t::wasSetByUser(), CVC4::options::rewriteDivk__option_t::wasSetByUser(), CVC4::options::lemmaOutputChannel__option_t::wasSetByUser(), CVC4::options::trySolveIntStandardEffort__option_t::wasSetByUser(), CVC4::options::userPatternsQuant__option_t::wasSetByUser(), CVC4::options::forceNoLimitCpuWhileDump__option_t::wasSetByUser(), CVC4::options::flipDecision__option_t::wasSetByUser(), CVC4::options::replayFailureLemma__option_t::wasSetByUser(), CVC4::options::internalReps__option_t::wasSetByUser(), CVC4::options::dioSolverTurns__option_t::wasSetByUser(), CVC4::options::rrTurns__option_t::wasSetByUser(), CVC4::options::finiteModelFind__option_t::wasSetByUser(), CVC4::options::dioRepeat__option_t::wasSetByUser(), CVC4::options::mbqiMode__option_t::wasSetByUser(), CVC4::options::replayEarlyCloseDepths__option_t::wasSetByUser(), CVC4::options::fmfOneInstPerRound__option_t::wasSetByUser(), CVC4::options::replayFailurePenalty__option_t::wasSetByUser(), CVC4::options::fmfOneQuantPerRound__option_t::wasSetByUser(), CVC4::options::fmfInstEngine__option_t::wasSetByUser(), CVC4::options::replayNumericFailurePenalty__option_t::wasSetByUser(), CVC4::options::replayRejectCutSize__option_t::wasSetByUser(), CVC4::options::fmfInstGen__option_t::wasSetByUser(), CVC4::options::lemmaRejectCutSize__option_t::wasSetByUser(), CVC4::options::fmfInstGenOneQuantPerRound__option_t::wasSetByUser(), CVC4::options::soiApproxMajorFailure__option_t::wasSetByUser(), CVC4::options::fmfFreshDistConst__option_t::wasSetByUser(), CVC4::options::fmfFmcSimple__option_t::wasSetByUser(), CVC4::options::soiApproxMajorFailurePen__option_t::wasSetByUser(), CVC4::options::fmfBoundInt__option_t::wasSetByUser(), CVC4::options::soiApproxMinorFailure__option_t::wasSetByUser(), CVC4::options::soiApproxMinorFailurePen__option_t::wasSetByUser(), CVC4::options::fmfBoundIntLazy__option_t::wasSetByUser(), CVC4::options::axiomInstMode__option_t::wasSetByUser(), CVC4::options::ppAssertMaxSubSize__option_t::wasSetByUser(), CVC4::options::quantConflictFind__option_t::wasSetByUser(), CVC4::options::maxReplayTree__option_t::wasSetByUser(), CVC4::options::qcfMode__option_t::wasSetByUser(), CVC4::options::pbRewrites__option_t::wasSetByUser(), CVC4::options::pbRewriteThreshold__option_t::wasSetByUser(), CVC4::options::qcfWhenMode__option_t::wasSetByUser(), CVC4::options::qcfTConstraint__option_t::wasSetByUser(), CVC4::options::quantRewriteRules__option_t::wasSetByUser(), CVC4::options::rrOneInstPerRound__option_t::wasSetByUser(), and CVC4::options::dtStcInduction__option_t::wasSetByUser().

template<>
bool CVC4::Options::wasSetByUser ( options::arraysOptimizeLinear__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::memoryMap__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::instFormatMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::theoryAlternates__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::defaultDagThresh__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::semanticChecks__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringExp__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arraysLazyRIntro1__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::decisionMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::earlyTypeChecking__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::filesystemAccess__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::satRandomFreq__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringLB__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arraysModelBased__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::typeChecking__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::decisionStopOnly__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::satRandomSeed__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringFMF__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::decisionThreshold__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::biasedITERemoval__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arraysEagerIndexSplitting__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringEIT__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::decisionUseWeight__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::satVarDecay__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arraysEagerLemmas__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::decisionRandomWeight__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringOpt1__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::satClauseDecay__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufSymmetryBreaker__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::decisionWeightInternal__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringOpt2__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::version__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::satRestartFirst__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::stringCharCardinality__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::condenseFunctionValues__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::binary_name__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::help__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::satRestartInc__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssRegions__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitblastMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::earlyExit__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::in__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::sat_refine_conflicts__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssEagerSplits__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::threads__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorAig__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::out__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::minisatUseElim__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssTotality__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::threadStackSize__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorAigSimplifications__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::err__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::minisatDumpDimacs__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssTotalityLimited__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::threadArgv__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorPropagate__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssTotalitySymBreak__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::inputLanguage__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::thread_id__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssAbortCardinality__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorEqualitySolver__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::outputLanguage__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssExplainedCliques__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::sharingFilterByLength__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorEqualitySlicer__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssSimpleCliques__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::languageHelp__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fallbackSequential__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorInequalitySolver__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssDiseqPropagation__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::incrementalParallel__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::verbosity__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssMinimalModel__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::statistics__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::interactivePrompt__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorAlgebraicSolver__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssCliqueSplits__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::statsEveryQuery__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::continuedExecution__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorAlgebraicBudget__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssSymBreak__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::segvSpin__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::statsHideZeros__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ufssFairness__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorToBool__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::tearDownIncremental__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::parseOnly__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorDivByZeroConst__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::forceLogic__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::waitToJoin__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::preprocessOnly__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bvAbstraction__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::simplificationMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::printSuccess__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::doStaticLearning__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::skolemizeArguments__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::expandDefinitions__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bvNumFunc__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::produceModels__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bvEagerExplanations__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::checkModels__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithUnateLemmaMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bitvectorQuickXplain__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dumpModels__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithPropagationMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::bvIntroducePow2__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::miniscopeQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::proof__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithHeuristicPivots__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::miniscopeQuantFreeVar__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::checkProofs__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::prenexQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dumpProofs__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithStandardCheckVarOrderPivots__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::varElimQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dumpInstantiations__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithErrorSelectionRule__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::simpleIteLiftQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithSimplexCheckPeriod__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::unsatCores__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::cnfQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::produceAssignments__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithPivotThreshold__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::nnfQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithPropagateMaxLength__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::interactive__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::clauseSplit__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithDioSolver__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::doITESimp__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::preSkolemQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithRewriteEq__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::aggressiveMiniscopeQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::doITESimpOnRepeat__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithMLTrick__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::macrosQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::simplifyWithCareEnabled__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithMLTrickSubstitutions__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::foPropQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::compressItes__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::smartTriggers__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::doCutAllBounded__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::maxCutsInContext__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::relevantTriggers__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::unconstrainedSimp__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::revertArithModels__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::relationalTriggers__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::repeatSimp__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::registerQuantBodyTerms__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::zombieHuntThreshold__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::havePenalties__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::instWhenMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::sortInference__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::useFC__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::instMaxLevel__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::incrementalSolving__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::useSOI__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::eagerInstQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::abstractValues__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fullSaturateQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::restrictedPivots__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::modelUninterpDtEnum__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::literalMatchMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::collectPivots__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::cumulativeMillisecondLimit__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::perCallMillisecondLimit__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::cbqi__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::useApprox__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::recurseCbqi__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::cumulativeResourceLimit__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::maxApproxDepth__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::userPatternsQuant__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::perCallResourceLimit__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::flipDecision__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::rewriteApplyToConst__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::exportDioDecompositions__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayFilename__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::internalReps__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::newProp__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayLog__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::finiteModelFind__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::arithPropAsLemmaLength__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayStream__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::mbqiMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::soiQuickExplain__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfOneInstPerRound__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::lemmaInputChannel__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::rewriteDivk__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfOneQuantPerRound__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::lemmaOutputChannel__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::trySolveIntStandardEffort__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfInstEngine__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::forceNoLimitCpuWhileDump__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayFailureLemma__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfInstGen__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dioSolverTurns__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfInstGenOneQuantPerRound__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::rrTurns__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfFreshDistConst__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dioRepeat__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfFmcSimple__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayEarlyCloseDepths__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfBoundInt__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayFailurePenalty__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayNumericFailurePenalty__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::fmfBoundIntLazy__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::replayRejectCutSize__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::axiomInstMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::lemmaRejectCutSize__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::quantConflictFind__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::soiApproxMajorFailure__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::qcfMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::soiApproxMajorFailurePen__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::qcfWhenMode__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::soiApproxMinorFailure__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::qcfTConstraint__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::soiApproxMinorFailurePen__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::quantRewriteRules__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::ppAssertMaxSubSize__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::rrOneInstPerRound__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::maxReplayTree__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::dtStcInduction__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::pbRewrites__option_t  ) const
template<>
bool CVC4::Options::wasSetByUser ( options::pbRewriteThreshold__option_t  ) const

Friends And Related Function Documentation

friend class NodeManager
friend

Definition at line 57 of file options.h.

friend class NodeManagerScope
friend

Definition at line 58 of file options.h.

friend class SmtEngine
friend

Definition at line 59 of file options.h.


The documentation for this class was generated from the following files: