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 )

inlinestatic

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.

    {
        Native.disableTrace(tag);
    }

enableTrace()

static void enableTrace ( String  tag )

inlinestatic

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.

    {
        Native.enableTrace(tag);
    }

getParameter()

static String getParameter ( String  id )

inlinestatic

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.

    {
        Native.StringPtr res = new Native.StringPtr();
        if (!Native.globalParamGet(id, res)) {
            return null;
        } else {
            return res.value;
        }
    }    

resetParameters()

static void resetParameters ( )

inlinestatic

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.

    {
        Native.globalParamResetAll();
    }

setParameter()

static void setParameter ( String  id, String  value  )

inlinestatic

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.

    {
        Native.globalParamSet(id, value);
    }

ToggleWarningMessages()

static void ToggleWarningMessages ( boolean  enabled )

inlinestatic

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.

    {
        Native.toggleWarningMessages((enabled));
    }