From: Gereon Kremer Date: Wed, 4 Aug 2021 17:49:26 +0000 (-0700) Subject: Replace numeric predicates by explicit minimum and maximum (#6976) X-Git-Tag: cvc5-1.0.0~1412 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d95c17090fb7f67a76a3032c4f778572f003786b;p=cvc5.git Replace numeric predicates by explicit minimum and maximum (#6976) This PR replaces some option predicates by explicit minimum and maximum values. This allows us to export information about an options domain/range in the future. --- diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 04b02e23e..7231106d5 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -56,7 +56,7 @@ OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ 'name', 'short', 'long', 'alias', 'default', 'alternate', 'mode', - 'handler', 'predicates', 'includes', + 'handler', 'predicates', 'includes', 'minimum', 'maximum', 'help', 'help_mode' ] @@ -235,12 +235,17 @@ def get_handler(option): def get_predicates(option): """Render predicate calls for assignment functions""" - if not option.predicates: + if option.type == 'void': return [] optname = option.long_name if option.long else "" assert option.type != 'void' - return ['opts.handler().{}("{}", option, value);'.format(x, optname) + res = ['opts.handler().{}("{}", option, value);'.format(x, optname) for x in option.predicates] + if option.minimum: + res.append('opts.handler().checkMinimum("{}", option, value, {});'.format(optname, option.minimum)) + if option.maximum: + res.append('opts.handler().checkMaximum("{}", option, value, {});'.format(optname, option.maximum)) + return res def get_getall(module, option): diff --git a/src/options/options_handler.h b/src/options/options_handler.h index eed361c0d..a6fc97234 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -45,28 +45,32 @@ public: OptionsHandler(Options* options); template - void geqZero(const std::string& option, - const std::string& flag, - T value) const + void checkMinimum(const std::string& option, + const std::string& flag, + T value, + T minimum) const { - if (value < 0) + if (value < minimum) { std::stringstream ss; - ss << flag << ": " << value << " is not a legal setting, should be " - << value << " >= 0."; + ss << flag << " = " << value + << " is not a legal setting, value should be at least " << minimum + << "."; throw OptionException(ss.str()); } } template - void betweenZeroAndOne(const std::string& option, - const std::string& flag, - T value) const + void checkMaximum(const std::string& option, + const std::string& flag, + T value, + T maximum) const { - if (value < 0 || value > 1) + if (value > maximum) { std::stringstream ss; - ss << flag << ": " << value - << " is not a legal setting, should be 0 <= " << flag << " <= 1."; + ss << flag << " = " << value + << " is not a legal setting, value should be at most " << maximum + << "."; throw OptionException(ss.str()); } } diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 229b6b058..efdc89c3e 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -8,7 +8,8 @@ name = "SAT Layer" long = "random-freq=P" type = "double" default = "0.0" - predicates = ["betweenZeroAndOne"] + minimum = "0.0" + maximum = "1.0" help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)" [[option]] @@ -24,7 +25,8 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.95" - predicates = ["betweenZeroAndOne"] + minimum = "0.0" + maximum = "1.0" help = "variable activity decay factor for Minisat" [[option]] @@ -32,7 +34,8 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.999" - predicates = ["betweenZeroAndOne"] + minimum = "0.0" + maximum = "1.0" help = "clause activity decay factor for Minisat" [[option]] @@ -49,7 +52,7 @@ name = "SAT Layer" long = "restart-int-inc=F" type = "double" default = "3.0" - predicates = ["geqZero"] + minimum = "0.0" help = "sets the restart interval increase factor for the sat solver (F=3.0 by default)" [[option]]