.NET/Java/ML: Moved toggle_warning_messages to Global, added en/disable_trace.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

examples/dotnet/Program.cs

@@ -1041,7 +1041,7 @@ namespace test_mapi
         {
             Console.WriteLine("LogicTest");
 
-            Context.ToggleWarningMessages(true);
+            Microsoft.Z3.Global.ToggleWarningMessages(true);
 
             BitVecSort bvs = ctx.MkBitVecSort(32);
             Expr x = ctx.MkConst("x", bvs);
@@ -2110,7 +2110,7 @@ namespace test_mapi
         {
             try
             {
-                Context.ToggleWarningMessages(true);
+                Microsoft.Z3.Global.ToggleWarningMessages(true);
                 Log.Open("test.log");
 
                 Console.Write("Z3 Major Version: ");

examples/java/JavaExample.java

@@ -1101,7 +1101,7 @@ class JavaExample
         System.out.println("LogicTest");
         Log.append("LogicTest");
 
-        Context.ToggleWarningMessages(true);
+        com.microsoft.z3.Global.ToggleWarningMessages(true);
 
         BitVecSort bvs = ctx.mkBitVecSort(32);
         Expr x = ctx.mkConst("x", bvs);
@@ -2242,7 +2242,7 @@ class JavaExample
         JavaExample p = new JavaExample();
         try
         {
-            Context.ToggleWarningMessages(true);
+            com.microsoft.z3.Global.ToggleWarningMessages(true);
             Log.open("test.log");
 
             System.out.print("Z3 Major Version: ");

src/api/dotnet/Context.cs

@@ -4288,16 +4288,6 @@ namespace Microsoft.Z3
         {
             get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
         }        
-
-        /// <summary>
-        /// Enable/disable printing of warning messages to the console.
-        /// </summary>
-        /// <remarks>Note that this function is static and effects the behaviour of 
-        /// all contexts globally.</remarks>
-        public static void ToggleWarningMessages(bool enabled)
-        {
-            Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
-        }
         #endregion
 
         #region Error Handling

src/api/dotnet/Global.cs

@@ -83,5 +83,39 @@ namespace Microsoft.Z3
         {
             Native.Z3_global_param_reset_all();
         }
+
+        /// <summary>
+        /// Enable/disable printing of warning messages to the console.
+        /// </summary>
+        /// <remarks>Note that this function is static and effects the behaviour of 
+        /// all contexts globally.</remarks>
+        public static void ToggleWarningMessages(bool enabled)
+        {
+            Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
+        }
+
+        /// <summary>
+        /// Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode.
+        /// </summary>
+        /// <remarks>
+        /// It is a NOOP otherwise. 
+        /// </remarks>
+        /// <param name="tag">trace tag</param>
+        public static void EnableTrace(string tag)
+        {
+            Native.Z3_enable_trace(tag);
+        }
+
+        /// <summary>
+        /// Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode.        
+        /// </summary>
+        /// <remarks>
+        /// It is a NOOP otherwise.
+        /// </remarks>
+        /// <param name="tag">trace tag</param>
+        public static void DisableTrace(string tag)
+        {
+            Native.Z3_disable_trace(tag);
+        }
     }
 }

src/api/java/Context.java

@@ -3607,18 +3607,6 @@ public class Context extends IDisposable
         return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
     }
 
-    /**
-     * Enable/disable printing of warning messages to the console.
-     * Remarks: Note
-     * that this function is static and effects the behaviour of all contexts
-     * globally.
-     **/
-    public static void ToggleWarningMessages(boolean enabled)
-            throws Z3Exception
-    {
-        Native.toggleWarningMessages((enabled) ? true : false);
-    }
-
     /**
      * Update a mutable configuration parameter.
      * Remarks:  The list of all

src/api/java/Global.java

@@ -44,7 +44,7 @@ public final class Global
      **/
     public static void setParameter(String id, String value)
     {
-    Native.globalParamSet(id, value);
+        Native.globalParamSet(id, value);
     }
     
     /**
@@ -71,6 +71,38 @@ public final class Global
      **/
     public static void resetParameters()
     {
-    Native.globalParamResetAll();
+        Native.globalParamResetAll();
+    }
+    
+    /**
+     * Enable/disable printing of warning messages to the console.
+     * Remarks: Note
+     * that this function is static and effects the behaviour of all contexts
+     * globally.
+     **/
+    public static void ToggleWarningMessages(boolean enabled)
+            throws Z3Exception
+    {
+        Native.toggleWarningMessages((enabled) ? true : false);
+    }
+    
+    /** 
+     * Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode.        
+     * 
+     * Remarks: It is a NOOP otherwise.
+     **/
+    public static void enableTrace(String tag)
+    {
+        Native.enableTrace(tag);
+    }
+
+    /** 
+     * Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode.        
+     * 
+     * Remarks: It is a NOOP otherwise.
+     **/
+    public static void disableTrace(String tag)
+    {
+        Native.disableTrace(tag);
     }
 }

src/api/ml/z3.ml

@@ -2943,5 +2943,12 @@ let get_global_param ( id : string ) =
 let global_param_reset_all =
   Z3native.global_param_reset_all
 
-let toggle_warning_messages ( enabled: bool ) =
+let toggle_warning_messages ( enabled : bool ) =
   Z3native.toggle_warning_messages enabled
+
+let enable_trace ( tag : string ) =
+  (Z3native.enable_trace tag)
+
+let disable_trace ( tag : string ) =
+  (Z3native.enable_trace tag)
+

src/api/ml/z3.mli

@@ -3329,3 +3329,17 @@ val global_param_reset_all : unit -> unit
     all contexts globally. *)
 val toggle_warning_messages : bool -> unit
 
+(**
+   Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode.
+   
+   Remarks: It is a NOOP otherwise. 
+*)
+val enable_trace : string -> unit
+
+(**
+   Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode.        
+
+   Remarks: It is a NOOP otherwise.
+*)
+val disable_trace : string -> unit
+