mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Merge branch 'master' into fix-benchmark-crashes

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-18 13:40:23 -06:00 • committed by GitHub
commit a3fb5058c6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 178 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

57
.github/workflows/pyodide-pypi.yml vendored Normal file
View file

@ -0,0 +1,57 @@
name: Pyodide Wheel (PyPI)
# Builds a PEP 783 `pyemscripten_*_wasm32` wheel for z3-solver using cibuildwheel
# and publishes it to PyPI on tag pushes. Unlike the legacy pyodide.yml (which
# uses `pyodide build` and produces a Pyodide-version-locked emscripten_* wheel
# uploaded only as a CI artifact), this wheel is installable at runtime with
# micropip from PyPI. See src/api/python/pyproject.toml [tool.cibuildwheel].
on:
release:
types: [created]
workflow_dispatch:
permissions:
contents: read
jobs:
build-pyodide:
runs-on: ubuntu-24.04
steps:
- uses: actions/checkout@v6
- name: Build Pyodide wheel
uses: pypa/cibuildwheel@v4.1.0
with:
# The Python bindings live in a subdirectory of the repo.
package-dir: src/api/python
env:
CIBW_PLATFORM: pyodide
# Exception/longjmp/bigint flags are declared in
# src/api/python/pyproject.toml ([tool.pyodide.build]) and combined
# with Pyodide's -fwasm-exceptions defaults. Don't set CFLAGS/CXXFLAGS
# here — a JS-EH -fexceptions value conflicts with the wasm-EH ABI.
- name: Store Pyodide wheel
uses: actions/upload-artifact@v7
with:
name: pyodide-wheel
path: wheelhouse/*.whl
publish:
name: Publish to PyPI
runs-on: ubuntu-24.04
if: startsWith(github.ref, 'refs/tags/')
needs: [build-pyodide]
environment: release
permissions:
id-token: write # trusted publishing (OIDC), no API token needed
steps:
- name: Download Pyodide wheel
uses: actions/download-artifact@v8
with:
name: pyodide-wheel
path: dist/
- name: Publish to PyPI
uses: pypa/gh-action-pypi-publish@release/v1

7
CMakeLists.txt
View file

@ -204,7 +204,12 @@ elseif (EMSCRIPTEN)
"-Os"
"-s ALLOW_MEMORY_GROWTH=1"
"-s ASSERTIONS=0"
"-s DISABLE_EXCEPTION_CATCHING=0"
# Use native wasm exception handling + wasm longjmp to match the ABI of the
# Pyodide / modern-emscripten main module. The legacy JS-based EH (which the
# removed "-s DISABLE_EXCEPTION_CATCHING=0" selected) makes libz3 import
# invoke_* trampolines the Pyodide runtime no longer provides.
"-fwasm-exceptions"
"-s SUPPORT_LONGJMP=wasm"
"-s ERROR_ON_UNDEFINED_SYMBOLS=1"
)
endif()

3
cmake/compiler_warnings.cmake
View file

@ -20,6 +20,9 @@ set(CLANG_ONLY_WARNINGS
"-Wno-c++98-compat"
"-Wno-c++98-compat-pedantic"
"-Wno-zero-length-array"
"-Wc99-extensions"
"-Wsuggest-override"
"-Winconsistent-missing-override"
)
set(MSVC_WARNINGS "/W3")

26
src/api/python/pyproject.toml
View file

@ -1,3 +1,29 @@
[build-system]
requires = ["setuptools>=70"]
build-backend = "setuptools.build_meta"
# --- Pyodide / WebAssembly (PEP 783) build configuration ---------------------
# Consumed by pyodide-build (invoked directly or via `cibuildwheel --platform
# pyodide`). These flags are forwarded to the emscripten toolchain that compiles
# libz3 to wasm32. setup.py's IS_PYODIDE branch appends the same -fexceptions
# flags defensively, but declaring them here is what cibuildwheel relies on.
# Pyodide 314 / emscripten 5 builds its main module with *native wasm*
# exception handling and wasm longjmp (see Pyodide's Makefile.envs). Side
# modules like libz3.so MUST match that ABI: building with the legacy
# `-fexceptions` (JS-based EH) makes libz3 import `invoke_*` trampolines that the
# Pyodide runtime no longer provides -> "cannot resolve symbol invoke_vi" at the
# first Z3 call. WASM_BIGINT is required because the Z3 C API passes 64-bit ints
# across the ctypes/JS boundary.
[tool.pyodide.build]
cflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm"
cxxflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm"
ldflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm -sWASM_BIGINT"
# --- cibuildwheel: produce a PyPI-publishable pyemscripten wheel -------------
[tool.cibuildwheel]
# Pyodide 314 ships CPython 3.14; match the single ABI it targets.
build = "cp314-*"
[tool.cibuildwheel.pyodide]
# z3test.py is the upstream smoke test; run it inside the Pyodide test venv.
test-command = "python {project}/z3test.py z3"

28
src/api/python/setup.py
View file

@ -42,9 +42,16 @@ if RELEASE_DIR is None:
BUILD_PLATFORM = "emscripten"
BUILD_ARCH = "wasm32"
BUILD_OS_VERSION = os.environ['_PYTHON_HOST_PLATFORM'].split('_')[1:-1]
build_env['CFLAGS'] = build_env.get('CFLAGS', '') + " -fexceptions"
build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -fexceptions"
build_env['LDFLAGS'] = build_env.get('LDFLAGS', '') + " -fexceptions"
# Match Pyodide's native-wasm exception/longjmp ABI (see Makefile.envs in
# Pyodide). The legacy JS-based "-fexceptions" makes libz3.so import
# invoke_* trampolines that the modern Pyodide runtime does not export,
# which surfaces as "cannot resolve symbol invoke_vi" on the first Z3
# call. These mirror [tool.pyodide.build] in pyproject.toml so direct
# `pyodide build` invocations stay consistent with cibuildwheel.
_wasm_eh = " -fwasm-exceptions -sSUPPORT_LONGJMP=wasm"
build_env['CFLAGS'] = build_env.get('CFLAGS', '') + _wasm_eh
build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + _wasm_eh
build_env['LDFLAGS'] = build_env.get('LDFLAGS', '') + _wasm_eh + " -sWASM_BIGINT"
IS_SINGLE_THREADED = True
ENABLE_LTO = False
# build with pthread doesn't work. The WASM bindings are also single threaded.
@ -305,6 +312,21 @@ class bdist_wheel(_bdist_wheel):
def finalize_options(self):
if BUILD_PLATFORM == "emscripten":
# Under pyodide-build / `cibuildwheel --platform pyodide`, the
# authoritative wheel platform tag is handed to us verbatim via
# _PYTHON_HOST_PLATFORM. For PEP 783 (Pyodide >= 0.28 / "314") this
# is e.g. "pyemscripten_2026_0_wasm32" -- a tag PyPI accepts. The
# reconstruction below instead produced "emscripten_<ver>_wasm32",
# which is locked to a Pyodide release and rejected by PyPI, so we
# defer to pyodide-build's tag when it is available.
host_platform = os.environ.get('_PYTHON_HOST_PLATFORM')
if host_platform:
self.plat_name = host_platform
else:
os_version_tag = '_'.join(BUILD_OS_VERSION) if BUILD_OS_VERSION else 'xxxxxx'
self.plat_name = f"emscripten_{os_version_tag}_wasm32"
return super().finalize_options()
if BUILD_ARCH is not None and BUILD_PLATFORM is not None:
os_version_tag = '_'.join(BUILD_OS_VERSION) if BUILD_OS_VERSION is not None else 'xxxxxx'
os_version_tag = self.remove_build_machine_os_version(BUILD_PLATFORM, os_version_tag)

60
src/cmd_context/cmd_util.h
View file

@ -17,45 +17,51 @@ Notes:
--*/
#pragma once
#define ATOMIC_CMD(CLS_NAME, NAME, DESCR, ACTION) \
#define ATOMIC_CMD(CLS_NAME, NAME, DESCR, ACTION) \
class CLS_NAME : public cmd { \
public: \
CLS_NAME():cmd(NAME) {} \
char const * get_usage() const override { return 0; } \
char const * get_descr(cmd_context & ctx) const override { \
return DESCR; \
} \
unsigned get_arity() const override { return 0; } \
void execute(cmd_context & ctx) override { ACTION } \
}
#define UNARY_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \
class CLS_NAME : public cmd { \
public: \
CLS_NAME():cmd(NAME) {} \
virtual char const * get_usage() const { return 0; } \
virtual char const * get_descr(cmd_context & ctx) const { return DESCR; } \
virtual unsigned get_arity() const { return 0; } \
virtual void execute(cmd_context & ctx) { ACTION } \
};
#define UNARY_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \
class CLS_NAME : public cmd { \
public: \
CLS_NAME():cmd(NAME) {} \
virtual char const * get_usage() const { return USAGE; } \
virtual char const * get_descr(cmd_context & ctx) const { return DESCR; } \
virtual unsigned get_arity() const { return 1; } \
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return ARG_KIND; } \
virtual void set_next_arg(cmd_context & ctx, ARG_TYPE arg) { ACTION } \
char const * get_usage() const override { return USAGE; } \
char const * get_descr(cmd_context & ctx) const override { \
return DESCR; \
} \
unsigned get_arity() const override { return 1; } \
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \
return ARG_KIND; \
} \
void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \
}
// Macro for creating commands where the first argument is a symbol
// The second argument cannot be a symbol
#define BINARY_SYM_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \
class CLS_NAME : public cmd { \
symbol m_sym; \
symbol m_sym; \
public: \
CLS_NAME():cmd(NAME) {} \
virtual char const * get_usage() const { return USAGE; } \
virtual char const * get_descr(cmd_context & ctx) const { return DESCR; } \
virtual unsigned get_arity() const { return 2; } \
virtual void prepare(cmd_context & ctx) { m_sym = symbol::null; } \
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { \
return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \
char const * get_usage() const override { return USAGE; } \
char const * get_descr(cmd_context & ctx) const override { return DESCR; } \
unsigned get_arity() const override { return 2; } \
void prepare(cmd_context & ctx) override { m_sym = symbol::null; } \
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \
return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \
} \
virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_sym = s; } \
virtual void set_next_arg(cmd_context & ctx, ARG_TYPE arg) { ACTION } \
};
void set_next_arg(cmd_context & ctx, symbol const & s) override { m_sym = s; } \
void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \
}
class ast;
class expr;

2
src/math/lp/dioph_eq.cpp
View file

@ -580,7 +580,7 @@ namespace lp {
const lar_term* m_t;
undo_add_term(imp& s, const lar_term* t) : m_s(s), m_t(t) {}
void undo() {
void undo() override {
m_s.undo_add_term_method(m_t);
}
};

22
src/math/lp/static_matrix.h
View file

@ -60,6 +60,14 @@ std::ostream& operator<<(std::ostream& out, const row_strip<T>& r) {
return out << "\n";
}
// Below, static_matrix has a superclass when Z3DEBUG is set, and some
// methods are overrides in that case.
#ifdef Z3DEBUG
#define DEBUG_OVERRIDE override
#else
#define DEBUG_OVERRIDE
#endif
// each assignment for this matrix should be issued only once!!!
template <typename T, typename X>
class static_matrix
@ -119,9 +127,13 @@ public:
void init_empty_matrix(unsigned m, unsigned n);
unsigned row_count() const { return static_cast<unsigned>(m_rows.size()); }
unsigned row_count() const DEBUG_OVERRIDE {
return static_cast<unsigned>(m_rows.size());
}
unsigned column_count() const { return static_cast<unsigned>(m_columns.size()); }
unsigned column_count() const DEBUG_OVERRIDE {
return static_cast<unsigned>(m_columns.size());
}
unsigned lowest_row_in_column(unsigned col);
@ -197,7 +209,7 @@ public:
void cross_out_row_from_column(unsigned col, unsigned k);
T get_elem(unsigned i, unsigned j) const;
T get_elem(unsigned i, unsigned j) const DEBUG_OVERRIDE;
unsigned number_of_non_zeroes_in_column(unsigned j) const { return static_cast<unsigned>(m_columns[j].size()); }
@ -218,8 +230,8 @@ public:
#ifdef Z3DEBUG
unsigned get_number_of_rows() const { return row_count(); }
unsigned get_number_of_columns() const { return column_count(); }
virtual void set_number_of_rows(unsigned /*m*/) { }
virtual void set_number_of_columns(unsigned /*n*/) { }
void set_number_of_rows(unsigned /*m*/) override { }
void set_number_of_columns(unsigned /*n*/) override { }
#endif
T get_balance() const;

9
src/smt/smt_model_finder.cpp
View file

@ -2205,11 +2205,12 @@ namespace smt {
if (is_app(curr)) {
if (to_app(curr)->get_family_id() == m.get_basic_family_id() && m.is_bool(curr)) {
switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
case OP_IMPLIES:
case OP_IMPLIES:
process_literal(to_app(curr)->get_arg(0), neg(pol));
process_literal(to_app(curr)->get_arg(1), pol);
break;
case OP_XOR:
// Implies/XOR should be simplified away but handle gracefully
// by treating as uninterpreted boolean.
process_literal(curr, pol);
process_iff(to_app(curr));
break;
case OP_OR:
case OP_AND:

10
src/solver/assertions/asserted_formulas.h
View file

@ -185,12 +185,12 @@ class asserted_formulas {
public: \
FUNCTOR m_functor; \
NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \
m_functor(j.fml(), n, p); \
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { \
m_functor(j.fml(), n, p); \
} \
virtual void post_op() { if (REDUCE) af.reduce_and_solve(); } \
virtual bool should_apply() const { return APP; } \
}; \
void post_op() override { if (REDUCE) af.reduce_and_solve(); } \
bool should_apply() const override { return APP; } \
};
#define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)