Merge branch 'master' into update_z3

.github/workflows/coverage.yml

@@ -56,9 +56,10 @@ jobs:
         ./test-z3 -a
         cd -
 
+# Disabled:       ${{github.workspace}}/build/examples/c_example_build_dir/c_example
+
     - name: Run examples
       run: |
-        ${{github.workspace}}/build/examples/c_example_build_dir/c_example
         ${{github.workspace}}/build/examples/cpp_example_build_dir/cpp_example
         ${{github.workspace}}/build/examples/tptp_build_dir/z3_tptp5 --help
         ${{github.workspace}}/build/examples/c_maxsat_example_build_dir/c_maxsat_example ${{github.workspace}}/examples/maxsat/ex.smt

.github/workflows/docker-image.yml

@@ -41,7 +41,7 @@ jobs:
             type=edge
             type=sha,prefix=ubuntu-20.04-bare-z3-sha-
       - name: Build and push Bare Z3 Docker Image
-        uses: docker/build-push-action@v3.2.0
+        uses: docker/build-push-action@v4.0.0
         with:  
           context: .
           push: true

.github/workflows/wasm-release.yml

@@ -36,7 +36,7 @@ jobs:
           cp ../../../LICENSE.txt .
 
       - name: Setup emscripten
-        uses: mymindstorm/setup-emsdk@v11
+        uses: mymindstorm/setup-emsdk@v12
         with:
           no-install: true
           version: ${{env.EM_VERSION}}

.github/workflows/wasm.yml

@@ -29,7 +29,7 @@ jobs:
           node-version: "lts/*"
 
       - name: Setup emscripten
-        uses: mymindstorm/setup-emsdk@v11
+        uses: mymindstorm/setup-emsdk@v12
         with:
           no-install: true
           version: ${{env.EM_VERSION}}

.gitignore

@@ -9,9 +9,12 @@ callgrind.out.*
 .z3-trace
 # OCaml generated files
 *.a
+*.o
 *.cma
 *.cmo
 *.cmi
+*.cmx
+*.byte
 *.cmxa
 ocamlz3
 # Java generated files
@@ -22,6 +25,7 @@ ocamlz3
 # Directories with generated code and documentation
 release/*
 build/*
+trace/*
 build-dist/*
 dist/*
 src/out/*
@@ -95,9 +99,4 @@ CMakeSettings.json
 *.swp
 .DS_Store
 dbg/**
-.idea
-CMakeFiles
-cli/CTestTestfile.cmake
-cli/cmake_install.cmake
-cli/version.cc
-cli/Makefile
+*.wsp

CMakeLists.txt

@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.4)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.12.0.0 LANGUAGES CXX)
+project(Z3 VERSION 4.12.2.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version

README-CMake.md

@@ -90,6 +90,37 @@ CFLAGS="-m32" CXXFLAGS="-m32" CC=gcc CXX=g++ cmake ../
 Note like with the ``CC`` and ``CXX`` flags this must be done on the very first invocation
 to CMake in the build directory.
 
+### Adding Z3 as a dependency to a CMAKE Project
+
+CMake's [FetchContent](https://cmake.org/cmake/help/latest/module/FetchContent.html) allows
+the fetching and populating of an external project. This is useful when a certain version
+of z3 is required that may not match with the system version. With the following code in the 
+cmake file of your project, z3 version 4.12.1 is downloaded to the build directory and the
+cmake targets are added to the project:
+
+```
+FetchContent_Declare(z3
+        GIT_REPOSITORY https://github.com/Z3Prover/z3
+        GIT_TAG        z3-4.12.1
+)
+FetchContent_MakeAvailable(z3)
+```
+
+The header files can be added to the included directories as follows:
+
+```
+include_directories( ${z3_SOURCE_DIR}/src/api )
+```
+
+Finally, the z3 library can be linked to a `yourTarget` using
+
+```
+target_link_libraries(yourTarget libz3)
+```
+Note that this is `libz3` not `z3` (`libz3` refers to the library target from `src/CMakeLists.txt`).
+
+
+
 ### Ninja
 
 [Ninja](https://ninja-build.org/) is a simple build system that is built for speed.

RELEASE_NOTES.md

@@ -10,6 +10,32 @@ Version 4.next
     - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
 
+
+Version 4.12.2
+==============
+- remove MSF (Microsoft Solver Foundation) plugin
+- updated propagate-ineqs tactic and implementing it as a simplifier, bound_simplifier.
+  It now eliminates occurrences of "mod" operators when bounds information
+  implies that the modulus is redundant. This tactic is useful for
+  benchmarks created by converting bit-vector semantics to integer 
+  reasoning.
+- add API function Z3_mk_real_int64 to take two int64 as arguments. The Z3_mk_real function takes integers.
+- Add _simplifiers_ as optional incremental pre-processing to solvers.
+  They are exposed over the SMTLIB API using the command [`set-simplifier`](https://microsoft.github.io/z3guide/docs/strategies/simplifiers).
+  Simplifiers are similar to tactics, but they operate on solver state that can be incrementally updated. 
+  The exposed simplifiers cover all the pre-processing techniques used internally with some additional simplifiers, such as `solve-eqs`
+  and `elim-predicates` that go beyond incremental pre-processing used internally. The advantage of using `solve-eqs` during pre-processing
+  can be significant. Incremental pre-processing simplification using `solve-eqs` and other simplifiers that change interpretations 
+  was not possible before.
+- Optimize added to JS API, thanks to gbagan
+- SMTLIB2 proposal for bit-vector overflow predicates added, thanks to aehyvari 
+- bug fixes, thanks to Clemens Eisenhofer, hgvk94, Lev Nachmanson, and others
+
+
+Version 4.12.1
+==============
+- change macos build to use explicit reference to Macos version 11. Hosted builds are migrating to macos-12 and it broke a user Issue #6539.
+
 Version 4.12.0
 ==============
 - add clause logging API.
@@ -112,6 +138,8 @@ Version 4.12.0
     theory clauses. 
   - integration of pre-processing proofs with logging proofs. There is 
     currently no supported bridge to create a end-to-end proof objects.
+- experimental API for accessing E-graphs. Exposed over Python. This API should be considered temporary
+and subject to be changed depending on use cases or removed. The functions are `Z3_solver_congruence_root`, `Z3_solver_congruence_next`.
 
 
 Version 4.11.2

azure-pipelines.yml

@@ -202,7 +202,7 @@ jobs:
         setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env'
         setupCmd3: 'set /P JlCxxDir=<tmp.env'
         bindings:  '-DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx $(cmakeJava) $(cmakeNet) $(cmakePy) -DCMAKE_BUILD_TYPE=RelWithDebInfo'
-        runTests:  'True'
+        runTests:  'False'
       arm64:
         arch: 'amd64_arm64'
         setupCmd1: ''

contrib/qprofdiff/main.cpp

@@ -65,7 +65,7 @@ int parse(string const & filename, map<string, map_entry> & data) {
                 inx != string::npos;
                 inx = line.find(" : ", from)) {
                 tokens[ti] = trim(line.substr(from, inx-from));
-                from = inx+1;
+                from = inx+3; //3 is the length of " : "
                 ti++;
             }
             if (from != line.length() && ti < 4)

doc/mk_params_doc.py

@@ -37,7 +37,7 @@ def help(ous):
     out = subprocess.Popen([z3_exe, "-pm"],stdout=subprocess.PIPE).communicate()[0]
     modules = ["global"]
     if out != None:
-        out = out.decode(sys.stdout.encoding)
+        out = out.decode(sys.getdefaultencoding())
         module_re = re.compile(r"\[module\] (.*)\,")
         lines = out.split("\n")
         for line in lines:
@@ -48,7 +48,7 @@ def help(ous):
             out = subprocess.Popen([z3_exe, "-pmmd:%s" % module],stdout=subprocess.PIPE).communicate()[0]
             if out == None:
                 continue
-            out = out.decode(sys.stdout.encoding)
+            out = out.decode(sys.getdefaultencoding())
             out = out.replace("\r","")
             ous.write(out)
 

doc/mk_tactic_doc.py

@@ -0,0 +1,129 @@
+# Copyright (c) Microsoft Corporation 2015
+"""
+Tactic documentation generator script
+"""
+
+import os
+import re
+import sys
+import subprocess
+
+BUILD_DIR='../build'
+SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__))
+OUTPUT_DIRECTORY = os.path.join(os.getcwd(), 'api')
+
+def doc_path(path):
+    return os.path.join(SCRIPT_DIR, path)
+
+is_doc = re.compile("Tactic Documentation")
+is_doc_end = re.compile("\-\-\*\/")
+is_tac_name = re.compile("## Tactic (.*)")
+is_simplifier = re.compile("ADD_SIMPLIFIER\(.*\"([^\"]*)\".*,.*\"([^\"]*)\".*,.*\"([^\"]*)\"\.*\)")
+
+def is_ws(s):
+    return all([0 for ch in s if ch != ' ' and ch != '\n'])
+
+def extract_params(ous, tac):
+    z3_exe = BUILD_DIR + "/z3"
+    out = subprocess.Popen([z3_exe, f"-tacticsmd:{tac}"], stdout=subprocess.PIPE).communicate()[0]
+    if not out:
+        return
+    out = out.decode(sys.getdefaultencoding())
+    if is_ws(out):
+        return
+    ous.write("### Parameters\n\n")
+    for line in out:
+        ous.write(line.replace("\r",""))
+    ous.write("\n")
+
+def generate_tactic_doc(ous, f, ins):
+    tac_name = None
+    for line in ins:
+        m = is_tac_name.search(line)
+        if m:
+            tac_name = m.group(1)
+        if is_doc_end.search(line):
+            if tac_name:
+                extract_params(ous, tac_name)
+            break
+        ous.write(line)
+
+def extract_tactic_doc(ous, f):
+    with open(f) as ins:
+        for line in ins:
+            if is_doc.search(line):
+                generate_tactic_doc(ous, f, ins)
+
+def generate_simplifier_doc(ous, name, desc):
+    ous.write("## Simplifier [" + name + "](https://microsoft.github.io/z3guide/docs/strategies/summary/#tactic-" + name + ")\n")
+    ous.write("### Description\n" + desc + "\n")
+
+
+def extract_simplifier_doc(ous, f):
+    with open(f) as ins:
+        for line in ins:
+            m = is_simplifier.search(line)
+            if m:
+                generate_simplifier_doc(ous, m.group(1), m.group(2))
+
+def find_tactic_name(path):
+    with open(path) as ins:
+        for line in ins:
+            m = is_tac_name.search(line)
+            if m:
+                return m.group(1)
+    print(f"no tactic in {path}")
+    return ""
+
+def find_simplifier_name(path):
+    with open(path) as ins:
+        for line in ins:
+            m = is_simplifier.search(line)
+            if m:
+                return m.group(1)
+    print(f"no simplifier in {path}")
+    return ""
+
+def presort_files(find_fn):
+    tac_files = []
+    for root, dirs, files in os.walk(doc_path("../src")):
+        for f in files:
+            if f.endswith("~"):
+                continue
+            if f.endswith("tactic.h") or "simplifiers" in root:
+                tac_files += [(f, os.path.join(root, f))]
+    tac_files = sorted(tac_files, key = lambda x: find_fn(x[1]))
+    return tac_files
+
+
+def help(ous):
+    ous.write("---\n")
+    ous.write("title: Tactics Summary\n")
+    ous.write("sidebar_position: 6\n")
+    ous.write("---\n")
+    tac_files = presort_files(find_tactic_name)
+    for file, path in tac_files:
+        extract_tactic_doc(ous, path)
+
+
+
+def help_simplifier(ous):
+    ous.write("---\n")
+    ous.write("title: Simplifiers Summary\n")
+    ous.write("sidebar_position: 7\n")
+    ous.write("---\n")
+    tac_files = presort_files(find_simplifier_name)
+    for file, path in tac_files:
+        extract_simplifier_doc(ous, path)
+
+def mk_dir(d):
+    if not os.path.exists(d):
+        os.makedirs(d)
+
+mk_dir(os.path.join(OUTPUT_DIRECTORY, 'md'))
+
+with open(OUTPUT_DIRECTORY + "/md/tactics-summary.md",'w') as ous:
+    help(ous)
+
+with open(OUTPUT_DIRECTORY + "/md/simplifier-summary.md",'w') as ous:
+    help_simplifier(ous)

examples/java/JavaExample.java

@@ -2259,6 +2259,24 @@ public void translationExample() {
         System.out.println(e1.equals(e3));
     }
 
+    public void stringExample() {
+	System.out.println("String example");
+	Context ctx = new Context();
+	Expr a = ctx.mkToRe(ctx.mkString("abcd"));
+	Expr b = ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort()));
+	System.out.println(a);
+	System.out.println(b);
+	System.out.println(a.getSort());
+	System.out.println(b.getSort());
+	Expr c = ctx.mkConcat(ctx.mkToRe(ctx.mkString("abc")),
+			     ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort())),
+			     ctx.mkEmptyRe(ctx.mkReSort(ctx.mkStringSort())),
+			     ctx.mkAllcharRe(ctx.mkReSort(ctx.mkStringSort())),
+			     ctx.mkToRe(ctx.mkString("d")));
+	System.out.println(c);
+
+    }    
+
     public static void main(String[] args)
     {
         JavaExample p = new JavaExample();
@@ -2274,12 +2292,15 @@ public static void main(String[] args)
             System.out.print("Z3 Full Version String: ");
             System.out.println(Version.getFullVersion());
 
+	    p.stringExample();
+
             p.simpleExample();
 
             { // These examples need model generation turned on.
                 HashMap<String, String> cfg = new HashMap<String, String>();
                 cfg.put("model", "true");
                 Context ctx = new Context(cfg);
+
 
                 p.optimizeExample(ctx);
                 p.basicTests(ctx);