Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

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 (Native.Z3_get_param_value(nCtx, id, out res) == 0)
-            if (r == (int)Z3_lbool.Z3_L_FALSE)
                 return null;
             else
                 return Marshal.PtrToStringAnsi(res);

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
+{
+    /// <summary>
+    /// Global functions for Z3. 
+    /// </summary>
+    /// <remarks>
+    /// This (static) class contains functions that effect the behaviour of Z3
+    /// globally across contexts, etc. 
+    /// </remarks>
+    public static class Global
+    {
+        /// <summary>
+        /// Set a global (or module) parameter, which is shared by all Z3 contexts.
+        /// </summary>
+        /// <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.Z3_global_param_set(id, value);
+        }
+
+        /// <summary>
+        /// Get a global (or module) parameter.
+        /// </summary>
+        /// <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)
+        {
+            IntPtr t;
+            if (Native.Z3_global_param_get(id, out t) == 0)
+                return null;
+            else
+                return Marshal.PtrToStringAnsi(t);
+        }    
+
+
+        /// <summary>
+        /// Restore the value of all global (and module) parameters.
+        /// </summary>
+        /// <remarks>
+        /// This command will not affect already created objects (such as tactics and solvers)
+        /// </remarks>
+        /// <seealso cref="SetParameter"/>
+        public static void ResetParameters()
+        {
+            Native.Z3_global_param_reset_all();
+        }   
+    }
+}

src/api/dotnet/Microsoft.Z3.csproj

@@ -341,6 +341,7 @@
     <Compile Include="ConstructorList.cs" />
     <Compile Include="DatatypeExpr.cs" />
     <Compile Include="DatatypeSort.cs" />
+    <Compile Include="Global.cs" />
     <Compile Include="IDecRefQueue.cs" />
     <Compile Include="Enumerations.cs" />
     <Compile Include="EnumSort.cs" />

src/api/java/Global.java

@@ -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();
+    }   
+}

src/ast/ast_smt_pp.cpp

@@ -401,7 +401,12 @@ class smt_printer {
         if (m_autil.is_numeral(n, val, is_int)) {
             if (val.is_neg()) {
                 val.neg();
-                m_out << "(~ ";
+                if (m_is_smt2) {
+                    m_out << "(- ";
+                }
+                else {
+                    m_out << "(~ ";
+                }
                 display_rational(val, is_int);
                 m_out << ")";
             }