diff options
| author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
| commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
| tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/smt/options | |
| parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) | |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/smt/options')
| -rw-r--r-- | src/smt/options | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/smt/options b/src/smt/options index 0dc416474..20dd5b7d5 100644 --- a/src/smt/options +++ b/src/smt/options @@ -87,14 +87,18 @@ option - regular-output-channel argument :handler CVC4::smt::setRegularOutputCha option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h" set the diagnostic output channel of the solver -common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" +common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::smt::tlimitHandler :handler-include "smt/options_handlers.h" enable time limiting (give milliseconds) -common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" +common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::smt::tlimitPerHandler :handler-include "smt/options_handlers.h" enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" +common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::smt::rlimitHandler :handler-include "smt/options_handlers.h" enable resource limiting (currently, roughly the number of SAT conflicts) -common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" +common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::smt::rlimitPerHandler :handler-include "smt/options_handlers.h" enable resource limiting per query +common-option hardLimit hard-limit --hard-limit bool :default false + the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out) +common-option cpuTime cpu-time --cpu-time bool :default false + measures CPU time if set to true and wall time if false (default false) expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 |