Merge pull request #205 from VeriFIT/new_z3_4.13.4

Update Z3 to 4.13.4

.github/workflows/coverage.yml

@@ -3,6 +3,8 @@ name: Code Coverage
 on:
   push:
     branches: [ master ]
+  pull_request:
+    branches: [ master ]
   schedule:
     - cron: "0 11 * * *"
 

.github/workflows/docker-image.yml

@@ -1,8 +1,6 @@
 name: Publish Docker image
 
 on:
-  schedule:
-    - cron: "0 1 * * 0" # every Sunday at 1 am
   workflow_dispatch: # on button click
 
 permissions:
@@ -41,7 +39,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@v5.1.0
+        uses: docker/build-push-action@v6.10.0
         with:  
           context: .
           push: true

.github/workflows/msvc-static-build-clang-cl.yml

@@ -0,0 +1,23 @@
+name: MSVC Clang-CL Static Build
+
+on:
+  push:
+  pull_request:
+
+permissions:
+  contents: read # to fetch code (actions/checkout)
+
+jobs:
+  build:
+    runs-on: windows-2019
+    env:
+      BUILD_TYPE: Release
+    steps:
+    - name: Checkout Repo
+      uses: actions/checkout@v4
+
+    - name: Build
+      run: |
+        cmake -B build -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DZ3_BUILD_LIBZ3_SHARED=OFF -DZ3_BUILD_LIBZ3_MSVC_STATIC=ON -T ClangCL -DCMAKE_C_FLAGS="/EHsc" -DCMAKE_CXX_FLAGS="/EHsc"
+        cmake --build build --config ${{ env.BUILD_TYPE }} --parallel
+        

.github/workflows/pyodide.yml

@@ -0,0 +1,67 @@
+name: Pyodide Build
+
+on:
+  push:
+    branches: [ master ]
+
+env:
+  BUILD_TYPE: Release
+
+permissions:
+  contents: read
+
+jobs:
+  build:
+    runs-on: ubuntu-24.04
+
+    strategy:
+      fail-fast: false
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v4
+
+    - name: Setup packages
+      run: sudo apt-get update && sudo apt-get install -y python3-dev python3-pip python3-venv 
+
+    - name: Create venv
+      run: python3 -m venv ~/env
+
+    - name: Install pyodide
+      run:  ~/env/bin/pip install pyodide-build pyodide-cli
+
+    - name: Configure CMake and build
+      run:  |
+         git clone https://github.com/emscripten-core/emsdk.git ~/emsdk 
+         cd ~/emsdk && PYODIDE_EMSCRIPTEN_VERSION=$(~/env/bin/pyodide config get emscripten_version) 
+         ./emsdk install ${PYODIDE_EMSCRIPTEN_VERSION} 
+         ./emsdk activate ${PYODIDE_EMSCRIPTEN_VERSION}
+         
+    - name: Build Z3
+      run: |
+         source ~/emsdk/emsdk_env.sh 
+         cd src/api/python 
+         CFLAGS="${CFLAGS}" LDFLAGS="${LDFLAGS}" CXXFLAG="${CXXFLAGS}" ~/env/bin/pyodide build --exports whole_archive
+      env:
+         CFLAGS: "-fexceptions -s DISABLE_EXCEPTION_CATCHING=0 -g2"
+         LDFLAGS: "-fexceptions -s WASM_BIGINT"     
+         CXXFLAGS: "-fexceptions -s DISABLE_EXCEPTION_CATCHING=0"
+
+    - name: Setup env-pyodide
+      run: |
+         source ~/env/bin/activate 
+         source ~/emsdk/emsdk_env.sh 
+         pyodide venv ~/env-pyodide
+         
+    - name: Setup z3 wheel
+      run: |
+         ~/env-pyodide/bin/pip install src/api/python/dist/*.whl
+         ~/env-pyodide/bin/python - <src/api/python/z3test.py z3
+
+    - name: Package wheel
+      uses: actions/upload-artifact@master
+      with:
+          name: pyodide-wheel
+          path: src/api/python/dist/*.whl
+          retention-days: 1         
+

.github/workflows/wasm-release.yml

@@ -10,7 +10,7 @@ defaults:
     working-directory: src/api/js
 
 env:
-  EM_VERSION: 3.1.15
+  EM_VERSION: 3.1.73
 
 permissions:
   contents: read # to fetch code (actions/checkout)

.github/workflows/wasm.yml

@@ -10,7 +10,7 @@ defaults:
     working-directory: src/api/js
 
 env:
-  EM_VERSION: 3.1.15
+  EM_VERSION: 3.1.73
 
 permissions:
   contents: read # to fetch code (actions/checkout)

.gitignore

@@ -6,7 +6,13 @@ rebase.cmd
 callgrind.out.*
 # .hpp files are automatically generated
 *.hpp
+.env
 .z3-trace
+.env
+.genaiscript
+package-lock.json
+package.json
+node_modules
 # OCaml generated files
 *.a
 *.o
@@ -23,6 +29,8 @@ ocamlz3
 # Emacs temp files
 \#*\#
 # Directories with generated code and documentation
+node_modules/*
+.genaiscript/*
 release/*
 build/*
 trace/*
@@ -100,4 +108,5 @@ CMakeSettings.json
 .DS_Store
 dbg/**
 *.wsp
+CppProperties.json
 test-input

.gitignore.genai

@@ -0,0 +1,3 @@
+**/genaiscript.d.ts
+**/package-lock.json
+**/yarn.lock

CMakeLists.txt

@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.16)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.13.0.0 LANGUAGES CXX)
+project(Z3 VERSION 4.13.4.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version
@@ -191,6 +191,8 @@ if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
 elseif (WIN32)
   message(STATUS "Platform: Windows")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
+  # workaround for #7420
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR")  
 elseif (EMSCRIPTEN)
   message(STATUS "Platform: Emscripten")
   z3_add_cxx_flag("-pthread" REQUIRED)
@@ -257,6 +259,21 @@ else()
   message(STATUS "Thread-safe build")
 endif()
 
+
+################################################################################
+# Use polling based timeout. This avoids spawning threads for timer tasks
+################################################################################
+option(Z3_POLLING_TIMER
+  "Use polling based timeout checks"
+  OFF
+)
+if (Z3_POLLING_TIMER)
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-DPOLLING_TIMER")
+  message(STATUS "Polling based timer")
+endif()
+
+
+
 ################################################################################
 # FP math
 ################################################################################

README-CMake.md

@@ -310,6 +310,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Z3_BUILD_TEST_EXECUTABLES`` - BOOL. If set to ``TRUE`` build the z3 test executables. Defaults to ``TRUE`` unless z3 is being built as a submodule in which case it defaults to ``FALSE``.
 * ``Z3_SAVE_CLANG_OPTIMIZATION_RECORDS`` - BOOL. If set to ``TRUE`` saves Clang optimization records by setting the compiler flag ``-fsave-optimization-record``.
 * ``Z3_SINGLE_THREADED`` - BOOL. If set to ``TRUE`` compiles Z3 for single threaded mode.
+* ``Z3_POLLING_TIMER`` - BOOL. If set to ``TRUE`` compiles Z3 to use polling based timer instead of requiring a thread. This is useful for wasm builds and avoids spawning threads that interfere with how WASM is run.
 
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.

README-Z3.md

@@ -12,11 +12,15 @@ Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. I
 
 See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.
 
+[![Try the online Z3 Guide](z3guide.jpeg)](https://microsoft.github.io/z3guide/)
+
+
+
 ## Build status
 
-| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build | Windows Build |
-| --------------- | --------------|-----------|---------------|------------|---------------|
-| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [![Windows](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml)
+| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build | Windows Build | Pyodide Build |
+| --------------- | --------------|-----------|---------------|------------|---------------|---------------|
+| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [![Windows](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [![Pyodide Build](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml)
 
 <a href="https://github.com/z3prover/z3/pkgs/container/z3">Docker image</a>.
 
@@ -46,7 +50,7 @@ cd build
 nmake
 ```
 
-Z3 uses C++17. The recommended version of Visual Studio is therefore VS2019. 
+Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019. 
 
 ## Building Z3 using make and GCC/Clang
 
@@ -163,7 +167,7 @@ See [``examples/ml``](examples/ml) for examples.
 
 ### ``Python``
 
-You can install the Python wrapper for Z3 for the latest release from pypi using the command
+You can install the Python wrapper for Z3 for the latest release from pypi using the command:
 
 ```bash
    pip install z3-solver
@@ -206,7 +210,7 @@ See [``examples/python``](examples/python) for examples.
 
 ### ``Julia``
 
-The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C++ API of Z3. Information about updating and building the Julia bindings can be found in [src/api/julia](src/api/julia).
+The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C API of Z3. A previous version of it wrapped the C++ API: Information about updating and building the Julia bindings can be found in [src/api/julia](src/api/julia).
 
 ### ``Web Assembly`` / ``TypeScript`` / ``JavaScript``
 
@@ -226,7 +230,7 @@ to Z3's C API. For more information, see [MachineArithmetic/README.md](https://g
 * Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu)
 
 * Other native foreign function interfaces:
-* [C++ API](https://z3prover.github.io/api/html/group__cppapi.html)
+* [C++ API](https://z3prover.github.io/api/html/namespacez3.html)
 * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
 * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
 * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html))
@@ -236,4 +240,7 @@ to Z3's C API. For more information, see [MachineArithmetic/README.md](https://g
 * [Julia](https://github.com/ahumenberger/Z3.jl)
 * [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (supports Pharo and Smalltalk/X)
 
+## Power Tools
+* The [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) currently developed by ETH Zurich
+
 

README.md

@@ -5,7 +5,7 @@
 
 Z3-Noodler is an SMT solver for string constraints such as those that occur in symbolic execution and analysis of programs, 
 reasoning about configuration files of cloud services and smart contracts, etc.
-Z3-Noodler is based on the SMT solver [Z3 v4.13.0](https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0), in which it replaces the solver for the theory of strings. 
+Z3-Noodler is based on the SMT solver [Z3 v4.13.4](https://github.com/Z3Prover/z3/releases/tag/z3-4.13.4), in which it replaces the solver for the theory of strings. 
 The core of the string solver implements several decision procedures, but mainly it relies on the equation stabilization algorithm (see [Publications](#publications)).
 
 Z3-Noodler utilizes the automata library [Mata](https://github.com/VeriFIT/mata/) for efficient representation of automata and their processing.

RELEASE_NOTES.md

@@ -10,6 +10,44 @@ Version 4.next
     - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
 
+Version 4.13.4
+==============
+- several updates to emscripten including #7473
+- add preliminary pyodie build
+- address issues with Java bindings
+- Include start of sls-smt functionality SLS modulo theories as co-processor to SMT core and stand-alone tactic.
+
+Version 4.13.3
+==============
+- Fixes, including #7363
+- Fix paths to Java binaries in release
+- Remove internal build names from pypi wheels
+
+Version 4.13.2
+==============
+- Performance regression fix. #7404
+
+Version 4.13.1
+==============
+- single-sample cell projection in nlsat was designed by Haokun Li and Bican Xia. 
+- using simple-checker together with and variable ordering supported by qfnra_tactic was developed by Mengyu Zhao (Linxi) and Shaowei Cai.
+
+   The projection is described in paper by Haokun Li and Bican Xia,   [Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection](https://arxiv.org/abs/2003.00409). The code ported from https://github.com/hybridSMT/hybridSMT.git
+
+- Add API for providing hints for the solver/optimize contexts for which initial values to attempt to use for variables.
+ The new API function are Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively. Supply these functions with a Boolean or numeric variable, and a value. The solver will then attempt to use these values in the initial phase of search. The feature is aimed at resolving nearly similar problems, or problems with a predicted model and the intent is that restarting the solver based on a near solution can avoid prune the space of constraints that are initially infeasible.
+ The SMTLIB front-end contains the new command (set-initial-value var value). For example,
+ (declare-const x Int)
+ (set-initial-value x 10)
+ (push)
+ (assert (> x 0))
+ (check-sat)
+ (get-model)
+ produces a model where x = 10. We use (push) to ensure that z3 doesn't run a
+ specialized pre-processor that eliminates x, which renders the initialization
+ without effect.
+
+
 Version 4.13.0
 ==============
 - add ARM64 wheels for Python, thanks to Steven Moy, smoy