From: Gereon Kremer <nafur42@gmail.com>
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 <typename T>
-  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 <typename T>
-  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]]