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

scripts/mk_nuget_release.py

@@ -20,19 +20,23 @@ import subprocess
 import mk_util
 import mk_project
 
-data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode())
+release_data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode())
+release_tag_name = release_data['tag_name']
+release_tag_ref_data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/git/refs/tags/%s" % release_tag_name).read().decode())
+release_tag_sha = release_tag_ref_data['object']['sha']
+release_tag_data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/git/tags/%s" % release_tag_sha).read().decode())
 
-version_str = data['tag_name']
-version_num = version_str[3:]
+release_version = release_tag_name[3:]
+release_commit = release_tag_data['object']['sha']
 
-print(version_str)
+print(release_version)
 
 def mk_dir(d):
     if not os.path.exists(d):
         os.makedirs(d)
 
 def download_installs():
-    for asset in data['assets']:
+    for asset in release_data['assets']:
         url = asset['browser_download_url']
         name = asset['name']
         print("Downloading ", url)
@@ -42,7 +46,8 @@ def download_installs():
 os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
            'ubuntu-16' : ('so', 'ubuntu-x64'),
            'x64-win' : ('dll', 'win-x64'),
-           'x86-win' : ('dll', 'win-x86'),
+# Skip x86 as I can't get dotnet build to produce AnyCPU TargetPlatform           
+#          'x86-win' : ('dll', 'win-x86'),
            'osx' : ('dylib', 'macos'),
            'debian' : ('so', 'debian.8-x64') }
 
@@ -82,14 +87,15 @@ def unpack():
                     shutil.move("tmp/%s/bin/%s" % (package_dir, b), "out/lib/netstandard1.4/%s" % b)
 
 def mk_targets():
-    shutil.copy("../src/api/dotnet/Microsoft.Z3.targets.in", "out/Microsoft.Z3.targets")
+    mk_dir("out/build")
+    shutil.copy("../src/api/dotnet/Microsoft.Z3.targets.in", "out/build/Microsoft.Z3.targets")
     
 def create_nuget_spec():
     contents = """<?xml version="1.0" encoding="utf-8"?>
 <package xmlns="http://schemas.microsoft.com/packaging/2010/07/nuspec.xsd">
     <metadata>
-        <id>Microsoft.Z3</id>
-        <version>%s</version>
+        <id>Microsoft.Z3.x64</id>
+        <version>{0}</version>
         <authors>Microsoft</authors>
         <description>
 Z3 is a satisfiability modulo theories solver from Microsoft Research.
@@ -97,19 +103,24 @@ Z3 is a satisfiability modulo theories solver from Microsoft Research.
 Linux Dependencies:
     libgomp.so.1 installed    
         </description>
-        <copyright>Copyright Microsoft Corporation. All rights reserved.</copyright>
+        <copyright>&#169; Microsoft Corporation. All rights reserved.</copyright>
         <tags>smt constraint solver theorem prover</tags>
-        <iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg</iconUrl>
+        <iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/{1}/package/icon.jpg</iconUrl>
         <projectUrl>https://github.com/Z3Prover/z3</projectUrl>
-        <licenseUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt</licenseUrl>
-        <repository type="git" url="https://github.com/Z3Prover/z3.git" />
+        <licenseUrl>https://raw.githubusercontent.com/Z3Prover/z3/{1}/LICENSE.txt</licenseUrl>
+        <repository
+            type="git"
+            url="https://github.com/Z3Prover/z3.git"
+            branch="master"
+            commit="{1}"
+        />
         <requireLicenseAcceptance>true</requireLicenseAcceptance>
         <language>en</language>
     </metadata>
-</package>"""
+</package>""".format(release_version, release_commit)
 
-    with open("out/Microsoft.Z3.nuspec", 'w') as f:
-        f.write(contents % version_num)
+    with open("out/Microsoft.Z3.x64.nuspec", 'w') as f:
+        f.write(contents)
         
 def create_nuget_package():
     subprocess.call(["nuget", "pack"], cwd="out")
@@ -128,8 +139,8 @@ nuget_sign_input = """
     "SignRequestFiles": [
      {
       "CustomerCorrelationId": "42fc9577-af9e-4ac9-995d-1788d8721d17",
-      "SourceLocation": "Microsoft.Z3.%s.nupkg",
-      "DestinationLocation": "Microsoft.Z3.%s.nupkg"
+      "SourceLocation": "Microsoft.Z3.x64.%s.nupkg",
+      "DestinationLocation": "Microsoft.Z3.x64.%s.nupkg"
      }
     ],
     "SigningInfo": {
@@ -155,11 +166,11 @@ nuget_sign_input = """
 }"""
 
 def sign_nuget_package():
-    package_name = "Microsoft.Z3.%s.nupkg" % version_num
+    package_name = "Microsoft.Z3.x64.%s.nupkg" % release_version
     input_file = "out/nuget_sign_input.json"
     output_path = os.path.abspath("out").replace("\\","\\\\") 
     with open(input_file, 'w') as f:
-        f.write(nuget_sign_input % (output_path, output_path, version_num, version_num))
+        f.write(nuget_sign_input % (output_path, output_path, release_version, release_version))
     subprocess.call(["EsrpClient.exe", "sign", "-a", "authorization.json", "-p", "policy.json", "-i", input_file, "-o", "out\\diagnostics.json"])
     
     

src/api/dotnet/Microsoft.Z3.targets.in

@@ -1,10 +1,10 @@
 <?xml version="1.0" encoding="utf-8"?>
 <Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
     <ItemGroup>
-        <None Include="$(MSBuildThisFileDirectory)..\runtimes\win-$(PlatformTarget)\native\libz3.dll">
+        <None Include="$(MSBuildThisFileDirectory)..\runtimes\win-x64\native\libz3.dll">
             <Visible>false</Visible>
             <Link>libz3.dll</Link>
             <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
         </None>
     </ItemGroup>
-</Project>
+</Project>

src/ast/display_dimacs.cpp

@@ -26,6 +26,7 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
     ptr_vector<expr> exprs;
     unsigned num_vars = 0;
     unsigned num_cls  = fmls.size();
+    bool is_from_dimacs = true;
     for (expr * f : fmls) {
         unsigned num_lits;
         expr * const * lits;
@@ -41,10 +42,51 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
             expr * l = lits[j];
             if (m.is_not(l))
                 l = to_app(l)->get_arg(0);
-            if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
-                num_vars++;
-                expr2var.setx(l->get_id(), num_vars, UINT_MAX);
-                exprs.setx(l->get_id(), l, nullptr);
+            if (!is_uninterp_const(l)) {
+                is_from_dimacs = false;
+                break;
+            }
+            symbol const& s = to_app(l)->get_decl()->get_name();
+            if (s.is_numerical() && s.get_num() > 0) {
+                if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
+                    ++num_vars;
+                    expr2var.setx(l->get_id(), s.get_num(), UINT_MAX);
+                    exprs.setx(l->get_id(), l, nullptr);
+                }
+                continue;
+            }
+            is_from_dimacs = false;
+            break;            
+        }
+        if (!is_from_dimacs) {
+            num_vars = 0;
+            expr2var.reset();
+            exprs.reset();
+            break;
+        }
+    }
+    
+    if (!is_from_dimacs) {
+        for (expr * f : fmls) {
+            unsigned num_lits;
+            expr * const * lits;
+            if (m.is_or(f)) {
+                num_lits = to_app(f)->get_num_args();
+                lits     = to_app(f)->get_args();
+            }
+            else {
+                num_lits = 1;
+                lits     = &f;
+            }
+            for (unsigned j = 0; j < num_lits; j++) {
+                expr * l = lits[j];
+                if (m.is_not(l))
+                    l = to_app(l)->get_arg(0);
+                if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
+                    num_vars++;
+                    expr2var.setx(l->get_id(), num_vars, UINT_MAX);
+                    exprs.setx(l->get_id(), l, nullptr);
+                }
             }
         }
     }
@@ -71,10 +113,12 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
         }
         out << "0\n";
     }
-    for (expr* e : exprs) {
-        if (e && is_app(e)) {
-            symbol const& n = to_app(e)->get_decl()->get_name();
-            out << "c " << expr2var[e->get_id()] << " " << n << "\n";            
+    if (!is_from_dimacs) {
+        for (expr* e : exprs) {
+            if (e && is_app(e)) {
+                symbol const& n = to_app(e)->get_decl()->get_name();
+                out << "c " << expr2var[e->get_id()] << " " << n << "\n";            
+            }
         }
     }
     return out;