mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
.NET and Java APIs: added functions for global parameter management.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
f0737bdf7f
commit
5f0cb28ca3
4 changed files with 156 additions and 2 deletions
67
src/api/java/Global.java
Normal file
67
src/api/java/Global.java
Normal file
|
@ -0,0 +1,67 @@
|
|||
/**
|
||||
* Global.java
|
||||
* @author Christoph M. Wintersteiger (cwinter)
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
||||
/**
|
||||
* Global functions for Z3.
|
||||
* <remarks>
|
||||
* This (static) class contains functions that effect the behaviour of Z3
|
||||
* globally across contexts, etc.
|
||||
* </remarks>
|
||||
**/
|
||||
public final class Global
|
||||
{
|
||||
/**
|
||||
* 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.
|
||||
* </remarks>
|
||||
**/
|
||||
public static void SetParameter(String id, String value)
|
||||
{
|
||||
Native.globalParamSet(id, value);
|
||||
}
|
||||
|
||||
/**
|
||||
* Get a global (or module) parameter.
|
||||
* <remarks>
|
||||
* Returns null if the parameter <param name="id"/> does not exist.
|
||||
* The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
|
||||
* This function cannot be invoked simultaneously from different threads without synchronization.
|
||||
* The result string stored in param_value is stored in a shared location.
|
||||
* </remarks>
|
||||
**/
|
||||
public static String GetParameter(String id)
|
||||
{
|
||||
Native.StringPtr res = new Native.StringPtr();
|
||||
if (!Native.globalParamGet(id, res))
|
||||
return null;
|
||||
else
|
||||
return res.value;
|
||||
}
|
||||
|
||||
/**
|
||||
* Restore the value of all global (and module) parameters.
|
||||
* <remarks>
|
||||
* This command will not affect already created objects (such as tactics and solvers)
|
||||
* </remarks>
|
||||
* @seealso SetParameter
|
||||
**/
|
||||
public static void ResetParameters()
|
||||
{
|
||||
Native.globalParamResetAll();
|
||||
}
|
||||
}
|
Loading…
Add table
Add a link
Reference in a new issue