diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index aee60c43f..6d322394c 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3518,8 +3518,7 @@ namespace Microsoft.Z3
public string GetParamValue(string id)
{
IntPtr res = IntPtr.Zero;
- int r = Native.Z3_get_param_value(nCtx, id, out res);
- if (r == (int)Z3_lbool.Z3_L_FALSE)
+ if (Native.Z3_get_param_value(nCtx, id, out res) == 0)
return null;
else
return Marshal.PtrToStringAnsi(res);
diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs
new file mode 100644
index 000000000..707264c82
--- /dev/null
+++ b/src/api/dotnet/Global.cs
@@ -0,0 +1,87 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ Global.cs
+
+Abstract:
+
+ Z3 Managed API: Global Functions
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2013-01-15
+
+Notes:
+
+--*/
+
+using System;
+using System.Runtime.InteropServices;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// Global functions for Z3.
+ ///
+ ///
+ /// This (static) class contains functions that effect the behaviour of Z3
+ /// globally across contexts, etc.
+ ///
+ public static class Global
+ {
+ ///
+ /// 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 ..
+ /// For example:
+ /// Z3_global_param_set('pp.decimal', 'true')
+ /// will set the parameter "decimal" in the module "pp" to true.
+ ///
+ public static void SetParameter(string id, string value)
+ {
+ Native.Z3_global_param_set(id, value);
+ }
+
+ ///
+ /// Get a global (or module) parameter.
+ ///
+ ///
+ /// Returns null if the parameter 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.
+ ///
+ public static string GetParameter(string id)
+ {
+ IntPtr t;
+ if (Native.Z3_global_param_get(id, out t) == 0)
+ return null;
+ else
+ return Marshal.PtrToStringAnsi(t);
+ }
+
+
+ ///
+ /// Restore the value of all global (and module) parameters.
+ ///
+ ///
+ /// This command will not affect already created objects (such as tactics and solvers)
+ ///
+ ///
+ public static void ResetParameters()
+ {
+ Native.Z3_global_param_reset_all();
+ }
+ }
+}
diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj
index a1bb868eb..8f6e34517 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj
+++ b/src/api/dotnet/Microsoft.Z3.csproj
@@ -341,6 +341,7 @@
+
diff --git a/src/api/java/Global.java b/src/api/java/Global.java
new file mode 100644
index 000000000..c08691ded
--- /dev/null
+++ b/src/api/java/Global.java
@@ -0,0 +1,67 @@
+/**
+ * Global.java
+ * @author Christoph M. Wintersteiger (cwinter)
+ **/
+
+package com.microsoft.z3;
+
+/**
+ * Global functions for Z3.
+ *
+ * This (static) class contains functions that effect the behaviour of Z3
+ * globally across contexts, etc.
+ *
+ **/
+public final class Global
+{
+ /**
+ * 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 ..
+ * For example:
+ * Z3_global_param_set('pp.decimal', 'true')
+ * will set the parameter "decimal" in the module "pp" to true.
+ *
+ **/
+ public static void SetParameter(String id, String value)
+ {
+ Native.globalParamSet(id, value);
+ }
+
+ /**
+ * Get a global (or module) parameter.
+ *
+ * Returns null if the parameter 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.
+ *
+ **/
+ 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.
+ *
+ * This command will not affect already created objects (such as tactics and solvers)
+ *
+ * @seealso SetParameter
+ **/
+ public static void ResetParameters()
+ {
+ Native.globalParamResetAll();
+ }
+}