diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/options/options_public_functions.cpp | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
Diffstat (limited to 'src/options/options_public_functions.cpp')
-rw-r--r-- | src/options/options_public_functions.cpp | 322 |
1 files changed, 322 insertions, 0 deletions
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp new file mode 100644 index 000000000..2e86c732e --- /dev/null +++ b/src/options/options_public_functions.cpp @@ -0,0 +1,322 @@ +/********************* */ +/*! \file options_public_functions.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal + ** 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 + ** + ** \brief Definitions of public facing interface functions for Options. + ** + ** Definitions of public facing interface functions for Options. These are + ** all 1 line wrappers for Options::get<T>, Options::set<T>, and + ** Options::wasSetByUser<T> for different option types T. + **/ + +#include "options.h" + +#include <fstream> +#include <ostream> +#include <string> +#include <vector> + +#include "base/listener.h" +#include "base/modal_exception.h" +#include "base/tls.h" +#include "options/base_options.h" +#include "options/language.h" +#include "options/main_options.h" +#include "options/parser_options.h" +#include "options/printer_modes.h" +#include "options/printer_options.h" +#include "options/option_exception.h" +#include "options/smt_options.h" +#include "options/quantifiers_options.h" + +namespace CVC4 { + +// Get accessor functions. +InputLanguage Options::getInputLanguage() const { + return (*this)[options::inputLanguage]; +} + +InstFormatMode Options::getInstFormatMode() const { + return (*this)[options::instFormatMode]; +} + +OutputLanguage Options::getOutputLanguage() const { + return (*this)[options::outputLanguage]; +} + +bool Options::getCheckProofs() const{ + return (*this)[options::checkProofs]; +} + +bool Options::getContinuedExecution() const{ + return (*this)[options::continuedExecution]; +} + +bool Options::getDumpInstantiations() const{ + return (*this)[options::dumpInstantiations]; +} + +bool Options::getDumpModels() const{ + return (*this)[options::dumpModels]; +} + +bool Options::getDumpProofs() const{ + return (*this)[options::dumpProofs]; +} + +bool Options::getDumpSynth() const{ + return (*this)[options::dumpSynth]; +} + +bool Options::getDumpUnsatCores() const{ + return (*this)[options::dumpUnsatCores]; +} + +bool Options::getEarlyExit() const{ + return (*this)[options::earlyExit]; +} + +bool Options::getFallbackSequential() const{ + return (*this)[options::fallbackSequential]; +} + +bool Options::getFilesystemAccess() const{ + return (*this)[options::filesystemAccess]; +} + +bool Options::getForceNoLimitCpuWhileDump() const{ + return (*this)[options::forceNoLimitCpuWhileDump]; +} + +bool Options::getHelp() const{ + return (*this)[options::help]; +} + +bool Options::getIncrementalParallel() const{ + return (*this)[options::incrementalParallel]; +} + +bool Options::getIncrementalSolving() const{ + return (*this)[options::incrementalSolving]; +} + +bool Options::getInteractive() const{ + return (*this)[options::interactive]; +} + +bool Options::getInteractivePrompt() const{ + return (*this)[options::interactivePrompt]; +} + +bool Options::getLanguageHelp() const{ + return (*this)[options::languageHelp]; +} + +bool Options::getMemoryMap() const{ + return (*this)[options::memoryMap]; +} + +bool Options::getParseOnly() const{ + return (*this)[options::parseOnly]; +} + +bool Options::getProduceModels() const{ + return (*this)[options::produceModels]; +} + +bool Options::getProof() const{ + return (*this)[options::proof]; +} + +bool Options::getSegvSpin() const{ + return (*this)[options::segvSpin]; +} + +bool Options::getSemanticChecks() const{ + return (*this)[options::semanticChecks]; +} + +bool Options::getStatistics() const{ + return (*this)[options::statistics]; +} + +bool Options::getStatsEveryQuery() const{ + return (*this)[options::statsEveryQuery]; +} + +bool Options::getStatsHideZeros() const{ + return (*this)[options::statsHideZeros]; +} + +bool Options::getStrictParsing() const{ + return (*this)[options::strictParsing]; +} + +bool Options::getTearDownIncremental() const{ + return (*this)[options::tearDownIncremental]; +} + +bool Options::getVersion() const{ + return (*this)[options::version]; +} + +bool Options::getWaitToJoin() const{ + return (*this)[options::waitToJoin]; +} + +const std::string& Options::getForceLogicString() const{ + return (*this)[options::forceLogicString]; +} + +const std::vector<std::string>& Options::getThreadArgv() const{ + return (*this)[options::threadArgv]; +} + +int Options::getSharingFilterByLength() const{ + return (*this)[options::sharingFilterByLength]; +} + +int Options::getThreadId() const{ + return (*this)[options::thread_id]; +} + +int Options::getVerbosity() const{ + return (*this)[options::verbosity]; +} + +std::istream* Options::getIn() const{ + return (*this)[options::in]; +} + +std::ostream* Options::getErr(){ + return (*this)[options::err]; +} + +std::ostream* Options::getOut(){ + return (*this)[options::out]; +} + +std::ostream* Options::getOutConst() const{ +#warning "Remove Options::getOutConst" + return (*this)[options::out]; +} + +std::string Options::getBinaryName() const{ + return (*this)[options::binary_name]; +} + +std::string Options::getReplayInputFilename() const{ + return (*this)[options::replayInputFilename]; +} + +unsigned Options::getParseStep() const{ + return (*this)[options::parseStep]; +} + +unsigned Options::getThreadStackSize() const{ + return (*this)[options::threadStackSize]; +} + +unsigned Options::getThreads() const{ + return (*this)[options::threads]; +} + +int Options::currentGetSharingFilterByLength() { + return current()->getSharingFilterByLength(); +} + +int Options::currentGetThreadId() { + return current()->getThreadId(); +} + +std::ostream* Options::currentGetOut() { + return current()->getOut(); +} + + +// TODO: Document these. +void Options::setCeGuidedInst(bool value) { + set(options::ceGuidedInst, value); +} + +void Options::setDumpSynth(bool value) { + set(options::dumpSynth, value); +} + +void Options::setInputLanguage(InputLanguage value) { + set(options::inputLanguage, value); +} + +void Options::setInteractive(bool value) { + set(options::interactive, value); +} + +void Options::setOut(std::ostream* value) { + set(options::out, value); +} + +void Options::setOutputLanguage(OutputLanguage value) { + set(options::outputLanguage, value); +} + +void Options::setSharingFilterByLength(int length) { + set(options::sharingFilterByLength, length); +} + +void Options::setThreadId(int value) { + set(options::thread_id, value); +} + +bool Options::wasSetByUserCeGuidedInst() const { + return wasSetByUser(options::ceGuidedInst); +} + +bool Options::wasSetByUserDumpSynth() const { + return wasSetByUser(options::dumpSynth); +} + +bool Options::wasSetByUserEarlyExit() const { + return wasSetByUser(options::earlyExit); +} + +bool Options::wasSetByUserForceLogicString() const { + return wasSetByUser(options::forceLogicString); +} + +bool Options::wasSetByUserIncrementalSolving() const { + return wasSetByUser(options::incrementalSolving); +} + +bool Options::wasSetByUserInteractive() const { + return wasSetByUser(options::interactive); +} + +bool Options::wasSetByUserThreadStackSize() const { + return wasSetByUser(options::threadStackSize); +} + +bool Options::wasSetByUserThreads() const { + return wasSetByUser(options::threads); +} + + +void Options::flushErr() { + if(getErr() != NULL) { + *(getErr()) << std::flush; + } +} + +void Options::flushOut() { + if(getOut() != NULL) { + *(getOut()) << std::flush; + } +} + +}/* CVC4 namespace */ |