Merge branch 'master' of https://github.com/Z3Prover/z3

examples/dotnet/Program.cs

@@ -2159,6 +2159,8 @@ namespace test_mapi
                 Console.WriteLine(Microsoft.Z3.Version.Major.ToString());
                 Console.Write("Z3 Full Version: ");
                 Console.WriteLine(Microsoft.Z3.Version.ToString());
+                Console.Write("Z3 Full Version String: ");
+                Console.WriteLine(Microsoft.Z3.Version.FullVersion);
 
 
                 SimpleExample();

examples/java/JavaExample.java

@@ -2291,6 +2291,8 @@ class JavaExample
             System.out.println(Version.getMajor());
             System.out.print("Z3 Full Version: ");
             System.out.println(Version.getString());
+            System.out.print("Z3 Full Version String: ");
+            System.out.println(Version.getFullVersion());
 
             p.simpleExample();
 

examples/ml/ml_example.ml

@@ -323,6 +323,7 @@ let _ =
     else
       (
 	Printf.printf "Running Z3 version %s\n" Version.to_string ;
+	Printf.printf "Z3 full version string: %s\n" Version.full_version ;
 	let cfg = [("model", "true"); ("proof", "false")] in
 	let ctx = (mk_context cfg) in
 	let is = (Symbol.mk_int ctx 42) in

scripts/mk_project.py

@@ -88,7 +88,7 @@ def init_project_def():
                               dll_name='libz3',
                               static=build_static_lib(),
                               export_files=API_files)
-    add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
+    add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk')
     add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest')
     add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
     add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])

scripts/mk_util.py

@@ -82,6 +82,7 @@ Z3PY_SRC_DIR=None
 VS_PROJ = False
 TRACE = False
 DOTNET_ENABLED=False
+DOTNET_KEY_FILE=None
 JAVA_ENABLED=False
 ML_ENABLED=False
 PYTHON_INSTALL_ENABLED=False
@@ -99,6 +100,7 @@ VS_PAR=False
 VS_PAR_NUM=8
 GPROF=False
 GIT_HASH=False
+GIT_DESCRIBE=False
 SLOW_OPTIMIZE=False
 USE_OMP=True
 
@@ -534,11 +536,14 @@ def find_c_compiler():
     raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
 
 def set_version(major, minor, build, revision):
-    global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION
+    global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION, GIT_DESCRIBE
     VER_MAJOR = major
     VER_MINOR = minor
     VER_BUILD = build
     VER_REVISION = revision
+    if GIT_DESCRIBE:
+        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
+        VER_REVISION = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
 
 def get_version():
     return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
@@ -621,6 +626,7 @@ def display_help(exit_code):
     print("  --pypkgdir=<dir>              Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
     print("  -b <subdir>, --build=<subdir>  subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
     print("  --githash=hash                include the given hash in the binaries.")
+    print("  --git-describe                include the output of 'git describe' in the version information.")
     print("  -d, --debug                   compile Z3 in debug mode.")
     print("  -t, --trace                   enable tracing in release mode.")
     if IS_WINDOWS:
@@ -633,6 +639,7 @@ def display_help(exit_code):
     if IS_WINDOWS:
         print("  --optimize                    generate optimized code during linking.")
     print("  --dotnet                      generate .NET bindings.")
+    print("  --dotnet-key=<file>           sign the .NET assembly using the private key in <file>.")
     print("  --java                        generate Java bindings.")
     print("  --ml                          generate OCaml bindings.")
     print("  --python                      generate Python bindings.")
@@ -668,14 +675,14 @@ def display_help(exit_code):
 # Parse configuration option for mk_make script
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
-    global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED
+    global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED
     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
-                                                'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
+                                                'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
-                                                'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin'])
+                                                'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin'])
     except:
         print("ERROR: Invalid command line option")
         display_help(1)
@@ -708,6 +715,8 @@ def parse_options():
             TRACE = True
         elif opt in ('-.net', '--dotnet'):
             DOTNET_ENABLED = True
+        elif opt in ('--dotnet-key'):
+            DOTNET_KEY_FILE = arg
         elif opt in ('--staticlib'):
             STATIC_LIB = True
         elif opt in ('--staticbin'):
@@ -732,6 +741,8 @@ def parse_options():
             GPROF = True
         elif opt == '--githash':
             GIT_HASH=arg
+        elif opt == '--git-describe':
+            GIT_DESCRIBE = True
         elif opt in ('', '--ml'):
             ML_ENABLED = True
         elif opt in ('', '--noomp'):
@@ -1491,7 +1502,7 @@ class PythonInstallComponent(Component):
         return
 
 class DotNetDLLComponent(Component):
-    def __init__(self, name, dll_name, path, deps, assembly_info_dir):
+    def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file):
         Component.__init__(self, name, path, deps)
         if dll_name is None:
             dll_name = name
@@ -1499,6 +1510,7 @@ class DotNetDLLComponent(Component):
             assembly_info_dir = "."
         self.dll_name          = dll_name
         self.assembly_info_dir = assembly_info_dir
+        self.key_file = default_key_file
 
     def mk_pkg_config_file(self):
         """
@@ -1524,6 +1536,8 @@ class DotNetDLLComponent(Component):
         configure_file(pkg_config_template, pkg_config_output, substitutions)
 
     def mk_makefile(self, out):
+        global DOTNET_KEY_FILE
+        
         if not is_dotnet_enabled():
             return
         cs_fp_files = []
@@ -1554,17 +1568,24 @@ class DotNetDLLComponent(Component):
                                 '/linkresource:{}.dll'.format(get_component(Z3_DLL_COMPONENT).dll_name),
                                ]
                              )
-            pathToSnk = os.path.join(self.to_src_dir, 'z3.snk')
+
-            snkFile   = os.path.join(self.src_dir, 'z3.snk')
+        # We need to give the assembly a strong name so that it
-        else:
+        # can be installed into the GAC with ``make install``
-            # We need to give the assembly a strong name so that it
+        if not DOTNET_KEY_FILE is None:
-            # can be installed into the GAC with ``make install``
+            self.key_file = DOTNET_KEY_FILE
-            pathToSnk = os.path.join(self.to_src_dir, 'Microsoft.Z3.mono.snk')
+
-            snkFile  = os.path.join(self.src_dir, 'Microsoft.Z3.mono.snk')
+        if not self.key_file is None:
-        if os.path.isfile(snkFile):
+            if os.path.isfile(self.key_file):
-            cscCmdLine.append('/keyfile:{}'.format(pathToSnk))
+                self.key_file = os.path.abspath(self.key_file)
-        else:
+            elif os.path.isfile(os.path.join(self.src_dir, self.key_file)):
-            print("Keyfile is not configured: %s" % snkFile)
+                self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file))
+            else:
+                print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.dll_name, self.key_file))
+                self.key_file = None
+                
+        if not self.key_file is None:
+            print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
+            cscCmdLine.append('/keyfile:{}'.format(self.key_file))
 
         cscCmdLine.extend( ['/unsafe+',
                             '/nowarn:1701,1702',
@@ -1588,6 +1609,7 @@ class DotNetDLLComponent(Component):
                              )
         else:
             cscCmdLine.extend(['/optimize+'])
+            
         if IS_WINDOWS:
             if VS_X64:
                 cscCmdLine.extend(['/platform:x64'])
@@ -2172,8 +2194,8 @@ def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=
     reg_component(name, c)
     return c
 
-def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None):
+def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None):
-    c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir)
+    c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file)
     reg_component(name, c)
 
 def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None):
@@ -2593,6 +2615,16 @@ def update_version():
         mk_all_assembly_infos(major, minor, build, revision)
         mk_def_files()
 
+def get_full_version_string(major, minor, build, revision):
+    global GIT_HASH, GIT_DESCRIBE
+    res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision)
+    if GIT_HASH:
+        res += " " + GIT_HASH
+    if GIT_DESCRIBE:
+        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long'])
+        res += " master " + check_output(['git', 'describe'])
+    return '"' + res + '"'
+        
 # Update files with the version number
 def mk_version_dot_h(major, minor, build, revision):
     c = get_component(UTIL_COMPONENT)
@@ -2606,6 +2638,7 @@ def mk_version_dot_h(major, minor, build, revision):
           'Z3_VERSION_MINOR': str(minor),
           'Z3_VERSION_PATCH': str(build),
           'Z3_VERSION_TWEAK': str(revision),
+          'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision)
         }
     )
     if VERBOSE:

src/api/api_context.cpp

@@ -430,6 +430,11 @@ extern "C" {
         *revision_number = Z3_REVISION_NUMBER;
     }
 
+    Z3_string Z3_API Z3_get_full_version(void) {
+        LOG_Z3_get_full_version();
+        return Z3_FULL_VERSION;
+    }
+
     void Z3_API Z3_enable_trace(Z3_string tag) {
         memory::initialize(UINT_MAX);
         LOG_Z3_enable_trace(tag);

src/api/dotnet/InterpolationContext.cs

@@ -30,7 +30,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Constructor.
         /// </summary>
-        /// <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
+        /// <remarks><seealso cref="Context"/></remarks>
         public InterpolationContext(Dictionary<string, string> settings) : base(settings) { }
 
         #region Terms

src/api/dotnet/Version.cs

@@ -83,6 +83,17 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// A full version string
+        /// </summary>
+        public static string FullVersion
+        {
+            get
+            {
+                return Native.Z3_get_full_version();
+            }
+        }
+
         /// <summary>
         /// A string representation of the version information.
         /// </summary>

src/api/java/Version.java

@@ -63,6 +63,14 @@ public class Version
         return revision.value;
     }
 
+    /**
+     * A full version string
+     **/
+    public static String getFullVersion()
+    {
+        return Native.getFullVersion();
+    }
+
     /**
      * A string representation of the version information.
      **/

src/api/ml/z3.ml

@@ -25,6 +25,8 @@ module Version =
 struct
   let (major, minor, build, revision) = Z3native.get_version ()
 
+  let full_version : string = Z3native.get_full_version()
+                                                             
   let to_string =
     string_of_int major ^ "." ^
     string_of_int minor ^ "." ^

src/api/ml/z3.mli

@@ -80,6 +80,9 @@ sig
   (** The revision. *)
   val revision : int
 
+  (** A full version string. *)
+  val full_version : string
+
   (** A string representation of the version information. *)
   val to_string : string
 end

src/api/python/z3.py

@@ -79,6 +79,9 @@ def get_version():
   Z3_get_version(major, minor, build, rev)
   return (major.value, minor.value, build.value, rev.value)
 
+def get_full_version():
+  return Z3_get_full_version()
+
 # We use _z3_assert instead of the assert command because we want to
 # produce nice error messages in Z3Py at rise4fun.com
 def _z3_assert(cond, msg):

src/api/z3_api.h

@@ -5139,6 +5139,13 @@ extern "C" {
     */
     void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
 
+    /**
+        \brief Return a string that fully describes the version of Z3 in use.
+
+        def_API('Z3_get_full_version', STRING, ())
+    */
+    Z3_string Z3_API Z3_get_full_version(void);
+
     /**
        \brief Enable tracing messages tagged as \c tag when Z3 is compiled in debug mode.
        It is a NOOP otherwise

src/util/version.h.in

@@ -3,3 +3,5 @@
 #define Z3_MINOR_VERSION   @Z3_VERSION_MINOR@
 #define Z3_BUILD_NUMBER    @Z3_VERSION_PATCH@
 #define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@
+
+#define Z3_FULL_VERSION    @Z3_FULL_VERSION@