From 37801c1da918ad1c4de97e8a64ca7d1177b61de4 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 8 Jul 2020 06:38:26 -0700
Subject: [PATCH] Add getName() method to options. (#4704)

getName() returns the long option name if it exists and an empty string otherwise.
---
 src/options/mkoptions.py | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index d9bc1a0bd..3f00204fb 100755
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -164,6 +164,7 @@ TPL_OPTION_STRUCT_RW = \
   type operator()() const;
   bool wasSetByUser() const;
   void set(const type& v);
+  const char* getName() const;
 }} {name} CVC4_PUBLIC;"""
 
 TPL_OPTION_STRUCT_RO = \
@@ -172,6 +173,7 @@ TPL_OPTION_STRUCT_RO = \
   typedef {type} type;
   type operator()() const;
   bool wasSetByUser() const;
+  const char* getName() const;
 }} {name} CVC4_PUBLIC;"""
 
 
@@ -207,7 +209,6 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
   return d_holder->{name}__setByUser__;
 }}"""
 
-
 # Option specific methods
 
 TPL_IMPL_OPTION_SET = \
@@ -228,6 +229,14 @@ TPL_IMPL_OPTION_WAS_SET_BY_USER = \
   return Options::current()->wasSetByUser(*this);
 }}"""
 
+TPL_IMPL_GET_NAME = \
+"""inline const char* {name}__option_t::getName() const
+{{
+  return "{long_name}";
+}}"""
+
+
+
 # Mode templates
 TPL_DECL_MODE_ENUM = \
 """
@@ -593,6 +602,12 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         inls.append(TPL_IMPL_OPTION_WAS_SET_BY_USER.format(name=option.name))
         if not option.read_only:
             inls.append(TPL_IMPL_OPTION_SET.format(name=option.name))
+        if option.long:
+            long_name = option.long.split('=')[0]
+        else:
+            long_name = ""
+        inls.append(TPL_IMPL_GET_NAME.format(
+                        name=option.name, long_name=long_name))
 
 
         ### Generate code for {module.name}_options.cpp
-- 
2.30.2