From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 29 Apr 2021 16:20:36 +0000 (+0200)
Subject: Simplify generated code for getOption() and setOption() (#6462)
X-Git-Tag: cvc5-1.0.0~1811
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13499235189b644fc194680afd5b37378d794c09;p=cvc5.git

Simplify generated code for getOption() and setOption() (#6462)

This PR simplifies the generated code for Options::getOption() and Options::setOption(). It now uses less string streams, less temporary vectors and the new options[...] syntax (instead of options::...().
---

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 13df7b8bd..e2c138490 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -746,15 +746,17 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                         'if ({}) {{'.format(cond))
                     if option.type == 'bool':
                         getoption_handlers.append(
-                            'return options::{}() ? "true" : "false";'.format(
-                                option.name))
+                            'return (*this)[options::{}] ? "true" : "false";'.format(option.name))
+                    elif option.type == 'std::string':
+                        getoption_handlers.append(
+                            'return (*this)[options::{}];'.format(option.name))
+                    elif is_numeric_cpp_type(option.type):
+                        getoption_handlers.append(
+                            'return std::to_string((*this)[options::{}]);'.format(option.name))
                     else:
                         getoption_handlers.append('std::stringstream ss;')
-                        if is_numeric_cpp_type(option.type):
-                            getoption_handlers.append(
-                                'ss << std::fixed << std::setprecision(8);')
-                        getoption_handlers.append('ss << options::{}();'.format(
-                            option.name))
+                        getoption_handlers.append(
+                            'ss << (*this)[options::{}];'.format(option.name))
                         getoption_handlers.append('return ss.str();')
                     getoption_handlers.append('}')
 
@@ -788,21 +790,14 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
                     options_smt.append('"{}",'.format(optname))
 
                     if option.type == 'bool':
-                        s = '{ std::vector<std::string> v; '
-                        s += 'v.push_back("{}"); '.format(optname)
-                        s += 'v.push_back(std::string('
-                        s += 'd_holder->{}'.format(option.name)
-                        s += ' ? "true" : "false")); '
-                        s += 'opts.push_back(v); }'
+                        s = 'opts.push_back({{"{}", d_holder->{} ? "true" : "false"}});'.format(
+                            optname, option.name)
+                    elif is_numeric_cpp_type(option.type):
+                        s = 'opts.push_back({{"{}", std::to_string(d_holder->{})}});'.format(
+                            optname, option.name)
                     else:
-                        s = '{ std::stringstream ss; '
-                        if is_numeric_cpp_type(option.type):
-                            s += 'ss << std::fixed << std::setprecision(8); '
-                        s += 'ss << d_holder->{}; '.format(option.name)
-                        s += 'std::vector<std::string> v; '
-                        s += 'v.push_back("{}"); '.format(optname)
-                        s += 'v.push_back(ss.str()); '
-                        s += 'opts.push_back(v); }'
+                        s = '{{ std::stringstream ss; ss << d_holder->{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
+                            option.name, optname)
                     options_getoptions.append(s)