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