/********************* */
/*! \file options.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Global (command-line, set-option, ...) parameters for SMT.
**
#include "base/tls.h"
#include "options/argument_extender.h"
#include "options/language.h"
-#include "options/printer_modes.h"
#include "options/option_exception.h"
+#include "options/printer_modes.h"
namespace CVC4 {
options::OptionsHandler* d_handler;
/** The current Options in effect */
- static CVC4_THREADLOCAL(Options*) s_current;
+ static CVC4_THREAD_LOCAL Options* s_current;
/** Listeners for options::forceLogicString being set. */
ListenerCollection d_forceLogicListeners;
bool getStatsEveryQuery() const;
bool getStatsHideZeros() const;
bool getStrictParsing() const;
- bool getTearDownIncremental() const;
+ int getTearDownIncremental() const;
bool getVersion() const;
bool getWaitToJoin() const;
const std::string& getForceLogicString() const;
// TODO: Document these.
- void setCeGuidedInst(bool);
- void setDumpSynth(bool);
void setInputLanguage(InputLanguage);
void setInteractive(bool);
void setOut(std::ostream*);
* to the given name. Returns an empty string if there are no
* suggestions.
*/
- static std::string suggestCommandLineOptions(const std::string& optionName) throw();
+ static std::string suggestCommandLineOptions(const std::string& optionName);
/**
* Look up SMT option names that bear some similarity to
* useful in case of typos. Can return an empty vector if there are
* no suggestions.
*/
- static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
+ static std::vector<std::string> suggestSmtOptions(
+ const std::string& optionName);
/**
* Initialize the Options object options based on the given
/**
* Get the setting for all options.
*/
- std::vector< std::vector<std::string> > getOptions() const throw();
-
+ std::vector<std::vector<std::string> > getOptions() const;
/**
* Registers a listener for the notification, notifyBeforeSearch.