Z3 |

Static Public Member Functions
Global Class Reference

## Static Public Member Functions
static void | setParameter (String id, String value)
static String | getParameter (String id)
static void | resetParameters ()
static void | ToggleWarningMessages (boolean enabled)
static void | enableTrace (String tag)
static void | disableTrace (String tag)

## Detailed Description

Global functions for Z3. Remarks: This (static) class contains functions that effect the behaviour of Z3 globally across contexts, etc.

Definition at line 27 of file Global.java.

## Member Function Documentation

## ◆ disableTrace()

static void disableTrace | ( | String | tag | ) |
| inline static

Disable tracing messages tagged as ‘tag’ when Z3 is compiled in debug mode.

Remarks: It is a NOOP otherwise.

Definition at line 105 of file Global.java.

106 {
107 Native.disableTrace(tag);
108 }

## ◆ enableTrace()

static void enableTrace | ( | String | tag | ) |
| inline static

Enable tracing messages tagged as ‘tag’ when Z3 is compiled in debug mode.

Remarks: It is a NOOP otherwise.

Definition at line 95 of file Global.java.

96 {
97 Native.enableTrace(tag);
98 }

## ◆ getParameter()

static String getParameter | ( | String | id | ) |
| inline static

Get a global (or module) parameter.
Remarks:
This function cannot be invoked simultaneously from different threads without synchronization. The result string stored in param_value is stored in a shared location.

Returns
  null if the parameter `id` does not exist.

Definition at line 57 of file Global.java.

58 {
59 Native.StringPtr res = new Native.StringPtr();
60 if (!Native.globalParamGet(id, res)) {
61 return null;
62 } else {
63 return res.value;
64 }
65 }

## ◆ resetParameters()

static void resetParameters | ( |  | ) |
| inline static

Restore the value of all global (and module) parameters. Remarks: This command will not affect already created objects (such as tactics and solvers)

See also
  setParameter

Definition at line 73 of file Global.java.

74 {
75 Native.globalParamResetAll();
76 }

## ◆ setParameter()

static void setParameter | ( | String | id,
|  | String | value
| ) |  |
| inline static

Set a global (or module) parameter, which is shared by all Z3 contexts. Remarks: When a Z3 module is initialized it will use the value of these parameters when Z3_params objects are not provided. The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. The character '.' is a delimiter (more later). The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". This function can be used to set parameters for a specific Z3 module. This can be done by using <module-name>.<parameter-name>. For example: Z3_global_param_set('pp.decimal', 'true') will set the parameter "decimal" in the module "pp" to true.

Definition at line 45 of file Global.java.

46 {
47 Native.globalParamSet(id, value);
48 }

## ◆ ToggleWarningMessages()

static void ToggleWarningMessages | ( | boolean | enabled | ) |
| inline static

Enable/disable printing of warning messages to the console. Remarks: Note that this function is static and effects the behaviour of all contexts globally.

Definition at line 84 of file Global.java.

86 {
87 Native.toggleWarningMessages((enabled));
88 }