Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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 ()

Detailed Description

Global functions for Z3.

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

static String getParameter ( String  id) [inline, static]

Get a global (or module) parameter.

Returns null if the parameter

Parameters:
idparameter id

does not exist. This function cannot be invoked simultaneously from different threads without synchronization. The result string stored in param_value is stored in a shared location.

Definition at line 58 of file Global.java.

    {
        Native.StringPtr res = new Native.StringPtr();
        if (!Native.globalParamGet(id, res))
            return null;
        else
            return res.value;
    }    
static void resetParameters ( ) [inline, static]

Restore the value of all global (and module) parameters.

This command will not affect already created objects (such as tactics and solvers)

See also:
SetParameter

Definition at line 74 of file Global.java.

    {
        Native.globalParamResetAll();
    }   
static void setParameter ( String  id,
String  value 
) [inline, static]

Set a global (or module) parameter, which is shared by all Z3 contexts.

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);
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines