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

doc/mk_api_doc.py

@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation 2015
+
 import os
 import shutil
 import re

examples/c++/example.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<vector>
 #include"z3++.h"
 

examples/c/test_capi.c

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<stdio.h>
 #include<stdlib.h>
 #include<stdarg.h>

examples/interp/iz3.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <iostream>

examples/maxsat/maxsat.c

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 /*
   Simple MAXSAT solver on top of the Z3 API.
 */

examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Collections.Generic;
 using System.Linq;

examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Collections.Generic;
 using System.Linq;

examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Collections.Generic;
 using System.Linq;

examples/msf/SolverFoundation.Plugin.Z3/Utils.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Collections.Generic;
 using System.Linq;

examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Text;
 using Microsoft.SolverFoundation.Services;

examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using Microsoft.SolverFoundation.Services;
 using System;
 

examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Collections.Generic;
 using System.Threading;

examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using Microsoft.SolverFoundation.Services;
 using System;
 

examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using Microsoft.SolverFoundation.Services;
 using System;
 

examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;

examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using Microsoft.SolverFoundation.Services;
 using System;
 

examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using Microsoft.SolverFoundation.Services;
 using System;
 

examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.Threading;
 using System.Globalization;

examples/msf/Validator/Program.cs

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 using System;
 using System.IO;
 using System.Linq;

examples/python/example.py

@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation 2015
+
 from z3 import *
 
 x = Real('x')

examples/tptp/tptp5.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include <string>
 #include <cstring>
 #include <list>

examples/tptp/tptp5.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifndef TPTP5_H_
 #define TPTP5_H_
 

examples/tptp/tptp5.lex.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #line 2 "tptp5.lex.cpp"
 
 #line 4 "tptp5.lex.cpp"

scripts/mk_copyright.py

@@ -0,0 +1,57 @@
+# Copyright (c) 2015 Microsoft Corporation
+
+import os
+import re
+
+cr = re.compile("Copyright")
+aut = re.compile("Automatically generated")
+
+cr_notice = """
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+"""
+
+def has_cr(file):
+    ins = open(file)
+    lines = 0
+    line = ins.readline()
+    while line and lines < 20:
+	m = cr.search(line)
+	if m:
+	    ins.close()
+	    return True
+	m = aut.search(line)
+	if m:
+	    ins.close()
+	    return True
+	line = ins.readline()
+    ins.close()
+    return False
+
+def add_cr(file):
+    tmp = "%s.tmp" % file
+    ins = open(file)
+    ous = open(tmp,'w')
+    ous.write(cr_notice)
+    line = ins.readline()
+    while line:
+	ous.write(line)
+	line = ins.readline()
+    ins.close()
+    ous.close()
+    os.system("move %s %s" % (tmp, file))
+
+def add_missing_cr(dir):
+    for root, dirs, files in os.walk(dir):
+	for f in files:
+	    if f.endswith('.cpp') or f.endswith('.h') or f.endswith('.c') or f.endswith('.cs'):
+		path = "%s\\%s" % (root, f)
+		if not has_cr(path):
+		    print "Missing CR for %s" % path
+		    add_cr(path)
+
+add_missing_cr('src')
+add_missing_cr('examples')

scripts/trackall.sh

@@ -1,7 +1,9 @@
 #!/bin/bash
 
+# Copyright (c) 2015 Microsoft Corporation
 # Script for "cloning" (and tracking) all branches at codeplex.
 # On Windows, this script must be executed in the "git Bash" console.
+
 for branch in `git branch -a | grep remotes | grep -v HEAD | grep -v master`; do
     git branch --track ${branch##*/} $branch
 done

src/api/api_context.cpp

@@ -516,6 +516,11 @@ extern "C" {
         memory::initialize(0);
     }
 
+    void Z3_API Z3_finalize_memory(void) {
+        LOG_Z3_finalize_memory();
+        memory::finalize();
+    }
+
     Z3_error_code Z3_API Z3_get_error_code(Z3_context c) {
         LOG_Z3_get_error_code(c);
         return mk_c(c)->get_error_code();

src/api/api_fpa.cpp

@@ -712,7 +712,7 @@ extern "C" {
 
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {
         Z3_TRY;
-        LOG_Z3_fpa_get_ebits(c, s);
+        LOG_Z3_fpa_get_sbits(c, s);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(s, 0);
         return mk_c(c)->fpautil().get_sbits(to_sort(s));
@@ -765,7 +765,30 @@ extern "C" {
         mpqm.display_decimal(ss, q, sbits);
         return mk_c(c)->mk_external_string(ss.str());
         Z3_CATCH_RETURN("");
+    }
 
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        scoped_mpf val(mpfm);
+        bool r = plugin->is_numeral(to_expr(t), val);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        const mpz & z = mpfm.sig(val);
+        if (!mpzm.is_uint64(z)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *n = mpzm.get_uint64(z);
+        return 1;
+        Z3_CATCH_RETURN(0);
     }
 
     Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
@@ -794,7 +817,7 @@ extern "C" {
 
     Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
         Z3_TRY;
-        LOG_Z3_fpa_get_numeral_exponent_string(c, t);
+        LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();

src/api/dll/dll.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 
 #include<windows.h>

src/api/dotnet/FPNum.cs

@@ -59,6 +59,25 @@ public string Significand
             }
         }
 
+        /// <summary>
+        /// The significand value of a floating-point numeral as a UInt64
+        /// </summary>
+        /// <remarks>
+        /// This function extracts the significand bits, without the 
+        /// hidden bit or normalization. Throws an exception if the
+        /// significand does not fit into a UInt64.
+        /// </remarks>
+        public UInt64 SignificandUInt64
+        {
+            get
+            {
+                UInt64 result = 0;
+                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
+                    throw new Z3Exception("Significand is not a 64 bit unsigned integer");                
+                return result;
+            }
+        }
+
         /// <summary>
         /// Return the exponent value of a floating-point numeral as a string
         /// </summary>