1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     gparams.h
7 
8 Abstract:
9 
10     Global parameter management.
11 
12 Author:
13 
14     Leonardo (leonardo) 2012-11-29
15 
16 Notes:
17 
18 --*/
19 #pragma once
20 
21 #include "util/params.h"
22 
23 class gparams {
24     struct imp;
25     static imp * g_imp;
26 public:
27     typedef default_exception exception;
28 
29     /**
30        \brief Reset all global and module parameters.
31     */
32     static void reset();
33 
34     /**
35        \brief Set a global parameter \c name with \c value.
36 
37        The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'.
38        The character '.' is a delimiter (more later).
39 
40        The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
41        Thus, the following parameter names are considered equivalent: "auto-config"  and "AUTO_CONFIG".
42 
43        This function can be used to set parameters for a specific Z3 module.
44        This can be done by using <module-name>.<parameter-name>.
45        For example:
46        set_global_param('pp.decimal', 'true')
47        will set the parameter "decimal" in the module "pp" to true.
48 
49        An exception is thrown if the parameter name is unknown, or if the value is incorrect.
50     */
51     static void set(char const * name, char const * value);
52     static void set(symbol const & name, char const * value);
53 
54     /**
55        \brief Auxiliary method used to implement get-option in SMT 2.0 front-end.
56 
57        If the parameter is not set, then it just returns 'default'.
58 
59        An exception is thrown if the parameter name is unknown.
60     */
61     static std::string get_value(char const * name);
62     static std::string get_value(symbol const & name);
63 
64     /**
65        \brief Register additional global parameters
66 
67        This is an auxiliary function used by our automatic code generator.
68        Example: the directive REG_PARAMS('collect_param_descrs')
69        "tells" the automatic code generator how to register the additional global parameters.
70     */
71     static void register_global(param_descrs & d);
72 
73     /**
74        \brief Register parameter descriptions for a Z3 module.
75        The parameters of a given Z3 module can only be set using #set_global_param if
76        they are registered in this module using this function.
77 
78        This is an auxiliary function used by our automatic code generator.
79        Each module will contain directives (in comments) such as
80        Example: the directive REG_MODULE_PARAMS('nlsat', 'nlsat::solver::collect_param_descrs')
81        "tells" the automatic code generator how to register the parameters for the given
82        module.
83     */
84 
85     typedef std::function<param_descrs*(void)> lazy_descrs_t;
86     static void register_module(char const* module_name, lazy_descrs_t& get_descrs);
87 
88     /**
89        \brief Add a (small) description to the given module.
90     */
91     static void register_module_descr(char const * module_name, char const * descr);
92 
93     /**
94        \brief Retrieves the parameters associated with the given module.
95 
96        Example:
97        // The following command sets the parameter "decimal" in the module "pp" to true.
98        set_global_param("pp.decimal", "true");
99        ...
100        // The following command will return  the global parameters that were set for the module "pp".
101        // In this example "p" will contain "decimal" -> true after executing this function.
102        params_ref const & p = get_module_params("pp")
103     */
104     static params_ref get_module(char const * module_name);
105     /**
106        \brief Return the global parameter set (i.e., parameters that are not associated with any particular module).
107     */
108 
109     static params_ref const& get_ref();
110 
111     /**
112        \brief Dump information about available parameters in the given output stream.
113     */
114     static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true);
115 
116     // Auxiliary APIs for better command line support
117     static void display_modules(std::ostream & out);
118     static void display_module(std::ostream & out, char const * module_name);
119     static void display_parameter(std::ostream & out, char const * name);
120 
121     /**
122        \brief Initialize the global parameter management module.
123 
124        Remark: I set a priority in the initialization, because this module must be initialized
125        after the core modules such as symbol.
126        ADD_INITIALIZER('gparams::init();', 1)
127     */
128     static void init();
129 
130     /**
131        \brief Finalize the global parameter management module.
132 
133        ADD_FINALIZER('gparams::finalize();');
134     */
135     static void finalize();
136 };
137 
138 
139 
140