From 5f0cb28ca39cfa83c4a7d10cf703f126e316ec5f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Jan 2013 17:05:31 +0000 Subject: [PATCH 1/2] .NET and Java APIs: added functions for global parameter management. Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 3 +- src/api/dotnet/Global.cs | 87 ++++++++++++++++++++++++++++++ src/api/dotnet/Microsoft.Z3.csproj | 1 + src/api/java/Global.java | 67 +++++++++++++++++++++++ 4 files changed, 156 insertions(+), 2 deletions(-) create mode 100644 src/api/dotnet/Global.cs create mode 100644 src/api/java/Global.java 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(); + } +} From ca5eb5186d003afe910463b20850a809c24961f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Jan 2013 09:24:12 -0800 Subject: [PATCH 2/2] fix pretty printer for smt2 unary minus Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 66b467b92..3dc94d3b3 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/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 << ")"; }