Fix a few minor issues in options processing, improving usability, consistency, error...

[cvc5.git] / src / options / base_options_handlers.h

diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 6cb74c6378ca2c2a528fee6a94945f9230ee4dc7..76ba9e2954af0c01bf841019948763fd89d3f512 100644 (file)
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -127,6 +127,7 @@ class comparator {
   bool d_hasLbound;
 
 public:
+  comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
   comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
   comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
 
@@ -142,26 +143,31 @@ public:
 };/* class comparator */
 
 struct greater : public comparator<std::greater> {
+  greater(int i) throw() : comparator<std::greater>(i) {}
   greater(long l) throw() : comparator<std::greater>(l) {}
   greater(double d) throw() : comparator<std::greater>(d) {}
 };/* struct greater */
 
 struct greater_equal : public comparator<std::greater_equal> {
+  greater_equal(int i) throw() : comparator<std::greater_equal>(i) {}
   greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
   greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
 };/* struct greater_equal */
 
 struct less : public comparator<std::less> {
+  less(int i) throw() : comparator<std::less>(i) {}
   less(long l) throw() : comparator<std::less>(l) {}
   less(double d) throw() : comparator<std::less>(d) {}
 };/* struct less */
 
 struct less_equal : public comparator<std::less_equal> {
+  less_equal(int i) throw() : comparator<std::less_equal>(i) {}
   less_equal(long l) throw() : comparator<std::less_equal>(l) {}
   less_equal(double d) throw() : comparator<std::less_equal>(d) {}
 };/* struct less_equal */
 
 struct not_equal : public comparator<std::not_equal_to> {
+  not_equal(int i) throw() : comparator<std::not_equal_to>(i) {}
   not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
   not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
 };/* struct not_equal_to */