diff options
author | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
commit | 5eabda0f55cee3be81aa7ae126269c32e818322f (patch) | |
tree | b873e4cb8e5d37ff3bb70596494bc5964aaef135 /src/options | |
parent | b717513e2a1d956c4456d13e0625957fc84c2449 (diff) |
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options.h | 3 | ||||
-rw-r--r-- | src/options/options_handler_interface.cpp | 4 | ||||
-rw-r--r-- | src/options/options_handler_interface.h | 3 | ||||
-rw-r--r-- | src/options/options_template.cpp | 2 | ||||
-rw-r--r-- | src/options/smt_options | 10 |
5 files changed, 1 insertions, 21 deletions
diff --git a/src/options/options.h b/src/options/options.h index a83de9acb..8e1ca2b65 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -34,9 +34,6 @@ namespace options { class OptionsHandler; }/* CVC4::options namespace */ -// Forward declaration for smt_options -class ExprStream; - class CVC4_PUBLIC Options { /** The struct that holds all option values. */ options::OptionsHolder* d_holder; diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp index bce3643aa..2cf19a611 100644 --- a/src/options/options_handler_interface.cpp +++ b/src/options/options_handler_interface.cpp @@ -323,10 +323,6 @@ std::string checkReplayFilename(std::string option, std::string optarg, OptionsH return handler->checkReplayFilename(option, optarg); } -std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->checkReplayLogFilename(option, optarg); -} // ensure we are a stats-enabled build of CVC4 void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { diff --git a/src/options/options_handler_interface.h b/src/options/options_handler_interface.h index 98575a313..e9e91ef0b 100644 --- a/src/options/options_handler_interface.h +++ b/src/options/options_handler_interface.h @@ -131,7 +131,6 @@ public: virtual void setRegularOutputChannel(std::string option, std::string optarg) = 0; virtual void setDiagnosticOutputChannel(std::string option, std::string optarg) = 0; virtual std::string checkReplayFilename(std::string option, std::string optarg) = 0; - virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg) = 0; virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException) = 0; virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0; virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0; @@ -255,8 +254,6 @@ void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsH std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler); -std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler); - // ensure we are a stats-enabled build of CVC4 void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index ecf42ac58..231e5de90 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -14,8 +14,6 @@ ** Contains code for handling command-line options **/ -#warning "TODO: Remove ExprStream forward declaration from options.h." - #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) // force use of optreset; mingw32 croaks on argv-switching otherwise # include "cvc4autoconfig.h" diff --git a/src/options/smt_options b/src/options/smt_options index d531eefbe..b99a8a83b 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -148,15 +148,7 @@ expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-cons # --replay is currently broken; don't document it for 1.0 undocumented-option replayFilename --replay=FILE std::string :handler CVC4::options::checkReplayFilename :handler-include "options/options_handler_interface.h" replay decisions from file -undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::options::checkReplayLogFilename :handler-include "options/options_handler_interface.h" - log decisions and propagations to file -option replayStream ExprStream* - -# portfolio options -option lemmaInputChannel LemmaInputChannel* :default NULL :include "base/lemma_input_channel_forward.h" - The input channel to receive notfication events for new lemmas -option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "base/lemma_output_channel_forward.h" - The output channel to receive notfication events for new lemmas + option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false Force no CPU limit when dumping models and proofs |