From 8ebb053b1c8a43df8b8df21e31ed5a94cf0a53be Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 30 Nov 2012 18:16:59 +0000 Subject: [PATCH] Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentation in base_options. --- src/options/base_options | 2 +- src/smt/options | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/options/base_options b/src/options/base_options index d19c3b812..b4cc473eb 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -31,7 +31,7 @@ # # SPECIFICATIONs take this form: # -# SPECIFICATION ::= (internal-name | -) [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] [smt-option-name] C++-type [ATTRIBUTEs...] +# SPECIFICATION ::= (internal-name | -) [smt-option-name] [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] C++-type [ATTRIBUTEs...] # ATTRIBUTE ::= :include include-files.. # | :default C++-expression # | :handler custom-option-handlers.. diff --git a/src/smt/options b/src/smt/options index a3038cd4e..fc5ccf4c4 100644 --- a/src/smt/options +++ b/src/smt/options @@ -60,13 +60,13 @@ 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=MS "unsigned long" +common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" enable time limiting (give milliseconds) -common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long" +common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit --rlimit=N "unsigned long" +common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" enable resource limiting -common-option perCallResourceLimit --rlimit-per=N "unsigned long" +common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long" enable resource limiting per query # --replay is currently broken; don't document it for 1.0 -- 2.30.2