/********************* */
/*! \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-2019 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 "cvc4_public.h"
-#ifndef __CVC4__OPTIONS__OPTIONS_H
-#define __CVC4__OPTIONS__OPTIONS_H
+#ifndef CVC4__OPTIONS__OPTIONS_H
+#define CVC4__OPTIONS__OPTIONS_H
#include <fstream>
#include <ostream>
#include "base/listener.h"
#include "base/modal_exception.h"
-#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 {
+namespace api {
+class Solver;
+}
namespace options {
struct OptionsHolder;
class OptionsHandler;
}/* CVC4::options namespace */
class CVC4_PUBLIC Options {
+ friend api::Solver;
/** The struct that holds all option values. */
options::OptionsHolder* d_holder;
options::OptionsHandler* d_handler;
/** The current Options in effect */
- static CVC4_THREADLOCAL(Options*) s_current;
-
- /** Listeners for options::forceLogicString being set. */
- ListenerCollection d_forceLogicListeners;
+ static thread_local Options* s_current;
/** Listeners for notifyBeforeSearch. */
ListenerCollection d_beforeSearchListeners;
* Options cannot be copied as they are given an explicit list of
* Listeners to respond to.
*/
- Options(const Options& options) CVC4_UNDEFINED;
+ Options(const Options& options) = delete;
/**
* Options cannot be assigned as they are given an explicit list of
* Listeners to respond to.
*/
- Options& operator=(const Options& options) CVC4_UNDEFINED;
+ Options& operator=(const Options& options) = delete;
static std::string formatThreadOptionException(const std::string& option);
/**
* Set the value of the given option by key.
+ *
+ * Throws OptionException or ModalException on failures.
*/
- void setOption(const std::string& key, const std::string& optionarg)
- throw(OptionException, ModalException);
-
+ void setOption(const std::string& key, const std::string& optionarg);
/** Get the value of the given option. Const access only. */
template <class T>
/**
* Gets the value of the given option by key and returns value as a string.
+ *
+ * Throws OptionException on failures, such as key not being the name of an
+ * option.
*/
- std::string getOption(const std::string& key) const
- throw(OptionException);
+ std::string getOption(const std::string& key) const;
// Get accessor functions.
InputLanguage getInputLanguage() const;
InstFormatMode getInstFormatMode() const;
OutputLanguage getOutputLanguage() const;
+ bool getUfHo() const;
bool getCheckProofs() const;
- bool getContinuedExecution() const;
bool getDumpInstantiations() const;
bool getDumpModels() const;
bool getDumpProofs() const;
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;
- const std::vector<std::string>& getThreadArgv() const;
- int getSharingFilterByLength() const;
- int getThreadId() const;
int getVerbosity() const;
std::istream* getIn() const;
std::ostream* getErr();
std::string getBinaryName() const;
std::string getReplayInputFilename() const;
unsigned getParseStep() const;
- unsigned getThreadStackSize() const;
- unsigned getThreads() const;
-
// TODO: Document these.
- void setCeGuidedInst(bool);
- void setDumpSynth(bool);
void setInputLanguage(InputLanguage);
void setInteractive(bool);
void setOut(std::ostream*);
void setOutputLanguage(OutputLanguage);
- void setSharingFilterByLength(int length);
- void setThreadId(int);
bool wasSetByUserCeGuidedInst() const;
bool wasSetByUserDumpSynth() const;
bool wasSetByUserForceLogicString() const;
bool wasSetByUserIncrementalSolving() const;
bool wasSetByUserInteractive() const;
- bool wasSetByUserThreadStackSize() const;
- bool wasSetByUserThreads() const;
// Static accessor functions.
// TODO: Document these.
- static int currentGetSharingFilterByLength();
- static int currentGetThreadId();
static std::ostream* currentGetOut();
/**
* 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
*
* This function uses getopt_long() and is not thread safe.
*
+ * Throws OptionException on failures.
+ *
* Preconditions: options and argv must be non-null.
*/
static std::vector<std::string> parseOptions(Options* options,
- int argc, char* argv[])
- throw(OptionException);
+ int argc,
+ char* argv[]);
/**
* 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.
ListenerCollection::Registration* registerBeforeSearchListener(
Listener* listener);
-
- /**
- * Registers a listener for options::forceLogic being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerForceLogicListener(
- Listener* listener, bool notifyIfSet);
-
/**
* Registers a listener for options::tlimit being set.
*
void flushOut();
private:
-
/**
* Internal procedure for implementing the parseOptions function.
* Initializes the options object based on the given command-line
*
* This is not thread safe.
*
+ * Throws OptionException on failures.
+ *
* Preconditions: options, extender and nonoptions are non-null.
*/
static void parseOptionsRecursive(Options* options,
options::ArgumentExtender* extender,
- std::vector<std::string>* nonoptions)
- throw(OptionException);
+ std::vector<std::string>* nonoptions);
};/* class Options */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__OPTIONS_H */
+#endif /* CVC4__OPTIONS__OPTIONS_H */
projects / cvc5.git / blobdiff