From 48aa2f6988f62466ecfed284587357d4ca0722f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Oct 2024 12:47:17 -0700 Subject: [PATCH 01/27] setup python dist to remove internal build suffix for macos --- scripts/release.yml | 2 +- src/api/python/setup.py | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 148adc26b..308fcfff4 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -98,7 +98,7 @@ stages: - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/aarch64-none-linux-gnu/libc/usr/bin' - script: echo $PATH - script: stat /tmp/arm-toolchain/bin/aarch64-none-linux-gnu-gcc - - script: python scripts/mk_unix_dist.py --nodotnet --nojava --arch=arm64 + - script: python scripts/mk_unix_dist.py --nodotnet --arch=arm64 - task: CopyFiles@2 inputs: sourceFolder: dist diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 11ba42cf8..616686f2c 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -250,10 +250,25 @@ class sdist(_sdist): self.execute(_copy_sources, (), msg="Copying source files") _sdist.run(self) +# The Azure Dev Ops pipelines use internal OS version tagging that don't correspond +# to releases. + +internal_build_re = re.compile("((.+)\_7") + class bdist_wheel(_bdist_wheel): + + def remove_build_machine_os_version(self, platform, os_version_tag): + if platform in ["osx", "darwin", "sequoia"]: + m = internal_build_re.search(os_version_tag): + if m: + return m.group(1) + return os_version_tag + + def finalize_options(self): if BUILD_ARCH is not None and BUILD_PLATFORM is not None: os_version_tag = '_'.join(BUILD_OS_VERSION[:2]) if BUILD_OS_VERSION is not None else 'xxxxxx' + os_version_tag = self.remove_build_machine_os_version(BUILD_PLATFORM, os_version_tag) TAGS = { # linux tags cannot be deployed - they must be auditwheel'd to pick the right compatibility tag based on imported libc symbol versions ("linux", "x86_64"): "linux_x86_64", From 5dc1b1acd4dfb0b6db110251883853f4b1274b14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Oct 2024 13:01:27 -0700 Subject: [PATCH 02/27] remove hard-wired osx=11.0 Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 74768fbea..0cf37a11d 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -43,7 +43,7 @@ stages: pool: vmImage: "macOS-latest" steps: - - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0 + - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 - script: git clone https://github.com/z3prover/z3test z3test - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. - task: PublishPipelineArtifact@1 diff --git a/scripts/release.yml b/scripts/release.yml index 308fcfff4..3b25ca084 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -48,7 +48,7 @@ stages: pool: vmImage: "macOS-latest" steps: - - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0 + - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 - script: git clone https://github.com/z3prover/z3test z3test - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. - task: PublishPipelineArtifact@1 From fe71b75ffdaaa775b8ff931b3d411aee7dcc13ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Oct 2024 13:21:27 -0700 Subject: [PATCH 03/27] remove : from setup.py Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 616686f2c..bcf55a76d 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -259,7 +259,7 @@ class bdist_wheel(_bdist_wheel): def remove_build_machine_os_version(self, platform, os_version_tag): if platform in ["osx", "darwin", "sequoia"]: - m = internal_build_re.search(os_version_tag): + m = internal_build_re.search(os_version_tag) if m: return m.group(1) return os_version_tag From 00f1f1b83da7c583d0290280b1b3bbb6097a6be8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Oct 2024 14:19:10 -0700 Subject: [PATCH 04/27] fix typo in setup.py Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index bcf55a76d..aac6d9943 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -253,7 +253,7 @@ class sdist(_sdist): # The Azure Dev Ops pipelines use internal OS version tagging that don't correspond # to releases. -internal_build_re = re.compile("((.+)\_7") +internal_build_re = re.compile("(.+)\_7") class bdist_wheel(_bdist_wheel): From b268b56519f09828cc3b41d989b89377fae178cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Oct 2024 10:34:31 -0700 Subject: [PATCH 05/27] update release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index c35875fed..020e34a9d 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,12 @@ 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.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 From 6e3b99fb9ee02cbc37c6fb3ba289a5fd0fb59134 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Oct 2024 14:19:23 -0700 Subject: [PATCH 06/27] downgrade to macos13 in builds until fully supported by pypi Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 4 ++-- scripts/release.yml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 0cf37a11d..916779a58 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -12,7 +12,7 @@ stages: - job: MacBuild displayName: "Mac Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - task: PythonScript@0 displayName: Build @@ -41,7 +41,7 @@ stages: - job: MacBuildArm64 displayName: "Mac ARM64 Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 - script: git clone https://github.com/z3prover/z3test z3test diff --git a/scripts/release.yml b/scripts/release.yml index 3b25ca084..6657ff894 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -17,7 +17,7 @@ stages: - job: MacBuild displayName: "Mac Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - task: PythonScript@0 displayName: Build @@ -46,7 +46,7 @@ stages: - job: MacBuildArm64 displayName: "Mac ARM64 Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 - script: git clone https://github.com/z3prover/z3test z3test From 54d30f26f72ce62f5dcb5a5258f632f84858714f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Oct 2024 15:52:10 -0700 Subject: [PATCH 07/27] add _0 to platform tag for pypi Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index aac6d9943..c39cdd6b0 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -261,7 +261,7 @@ class bdist_wheel(_bdist_wheel): if platform in ["osx", "darwin", "sequoia"]: m = internal_build_re.search(os_version_tag) if m: - return m.group(1) + return m.group(1) + "_0" return os_version_tag From efde65603622ae54ef82050b0ade3f3218b2d54b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Oct 2024 16:38:00 -0700 Subject: [PATCH 08/27] fix recursive self call for slice_solver check-sat-cc method Signed-off-by: Nikolaj Bjorner --- src/solver/slice_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solver/slice_solver.cpp b/src/solver/slice_solver.cpp index 7c4e1fb82..28815b4d6 100644 --- a/src/solver/slice_solver.cpp +++ b/src/solver/slice_solver.cpp @@ -373,7 +373,7 @@ public: lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { flush(); - return check_sat_cc(cube, clauses); + return s->check_sat_cc(cube, clauses); } lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { From 7a0b58bcd5e28ce819a58832b8a2a61e6ad26595 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Oct 2024 17:27:07 -0700 Subject: [PATCH 09/27] increment minor version number Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 797087641..a66e2c9b0 100644 --- a/CMakeLists.txt +++ b/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.3.0 LANGUAGES CXX) +project(Z3 VERSION 4.13.4.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 5d1b2983f..e0fd260ba 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 13, 3, 0) # express a default build version or pick up ci build version + set_version(4, 13, 4, 0) # express a default build version or pick up ci build version # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 916779a58..c8dc16d62 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '13' - Patch: '3' + Patch: '4' ReleaseVersion: $(Major).$(Minor).$(Patch) AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.buildId) diff --git a/scripts/release.yml b/scripts/release.yml index 6657ff894..435c92935 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.13.3' + ReleaseVersion: '4.13.4' stages: From 3a8195b9c3875cbce4fe6a89c6874923d34479a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Oct 2024 11:48:30 -0700 Subject: [PATCH 10/27] #7419 Signed-off-by: Nikolaj Bjorner --- src/params/context_params.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 1d5d10b39..a5c907208 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -202,7 +202,7 @@ bool context_params::is_shell_only_parameter(char const* _p) const { std::string p(_p); lower_case(p); if (p == "dump_models" || p == "well_sorted_check" || - p == "model_validate" || p == "smtlib2_compliant" || + p == "model_validate" || p == "stats") return true; From 56b706ac550724b63bf8251a53cf4b0118a31b79 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Oct 2024 15:52:13 -0700 Subject: [PATCH 11/27] fixes for #7420 #7405 --- CMakeLists.txt | 2 ++ scripts/mk_util.py | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a66e2c9b0..cfd435714 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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") list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0177dc564..5296e12d8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2500,7 +2500,7 @@ def mk_config(): config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED, IS_ARCH_ARM64 if IS_WINDOWS: - CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++20' + CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++20 -D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR' config.write( 'CC=cl\n' 'CXX=cl\n' From 62478db7d52c8fe20f4c67dd6101832634dee392 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Oct 2024 19:50:56 -0700 Subject: [PATCH 12/27] Update docker-image.yml make docker publish manual --- .github/workflows/docker-image.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index c3949d6c5..cf930c86e 100644 --- a/.github/workflows/docker-image.yml +++ b/.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: From 5993735b34affd8868bca0e6b13cf066e7cbb91a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Oct 2024 14:32:33 -0700 Subject: [PATCH 13/27] simplify string patterns into prefix/suffix constraints Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 7e39931f4..216f23e93 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4541,6 +4541,15 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { result = m_br.mk_eq_rw(a, b_s); return BR_REWRITE_FULL; } + expr* c = nullptr, *d = nullptr, *e = nullptr; + if (re().is_concat(b, c, d) && re().is_to_re(c, e) && re().is_full_seq(d)) { + result = str().mk_prefix(e, a); + return BR_REWRITE1; + } + if (re().is_concat(b, c, d) && re().is_to_re(d, e) && re().is_full_seq(c)) { + result = str().mk_suffix(e, a); + return BR_REWRITE1; + } expr* b1 = nullptr; expr* eps = nullptr; if (re().is_opt(b, b1) || From 3896e1822755365ad496b71318c6108934d70385 Mon Sep 17 00:00:00 2001 From: stormckey Date: Tue, 15 Oct 2024 23:56:35 +0800 Subject: [PATCH 14/27] fix the code to cube at the correct frequency (#7422) Co-authored-by: stormckey --- src/smt/smt_parallel.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 82bda1d39..17abe66be 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -149,7 +149,7 @@ namespace smt { expr_ref c(pm); pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts); - if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) + if (num_rounds > 0 && (num_rounds % pctx.get_fparams().m_threads_cube_frequency) == 0) cube(pctx, lasms, c); IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; if (num_rounds > 0) verbose_stream() << " :round " << num_rounds; From 8ff4036f68876942dacf111614a9477785eb316c Mon Sep 17 00:00:00 2001 From: stormckey Date: Thu, 17 Oct 2024 01:23:13 +0800 Subject: [PATCH 15/27] update unit_lim to the correct value (#7423) Co-authored-by: stormckey --- src/smt/smt_parallel.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 17abe66be..ccbefa69e 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -134,7 +134,7 @@ namespace smt { dst = tr(unit_trail.get(j)); pctx.assert_expr(dst); } - unit_lim[i] = sz; + unit_lim[i] = pctx.assigned_literals().size(); } IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n"); }; From 5a5e39ae74f6f22324a7b31fd99e96de11801d78 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2024 12:18:09 -0700 Subject: [PATCH 16/27] fix incrementality bug for pre-processing: replay has to be invoked on every push regardless. --- src/ast/simplifiers/elim_unconstrained.cpp | 8 ++++---- .../simplifiers/model_reconstruction_trail.cpp | 15 +++++++++++++++ src/ast/simplifiers/model_reconstruction_trail.h | 12 ++---------- src/solver/simplifier_solver.cpp | 10 +++++----- 4 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 818800d99..44b1ee091 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -80,7 +80,7 @@ void elim_unconstrained::eliminate() { continue; } expr* e = get_parent(v); - IF_VERBOSE(11, for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";); + TRACE("elim_unconstrained", for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";); if (!e || !is_app(e) || !is_ground(e)) { n.m_refcount = 0; continue; @@ -107,13 +107,13 @@ void elim_unconstrained::eliminate() { n.m_refcount = 0; m_args.shrink(sz); if (!inverted) { - IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n"); + TRACE("elim_unconstrained", tout << "not inverted " << mk_bounded_pp(e, m) << "\n"); continue; } - IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); + IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " : " << rr << " -> " << r << "\n"); - TRACE("elim_unconstrained", tout << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); + TRACE("elim_unconstrained", tout << mk_pp(t, m) << " : " << rr << " -> " << r << "\n"); SASSERT(r->get_sort() == t->get_sort()); m_stats.m_num_eliminated++; m_trail.push_back(r); diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 47ebea525..1f3c74ea2 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -20,6 +20,19 @@ Author: #include "ast/converters/generic_model_converter.h" +void model_reconstruction_trail::add_vars(expr* e, ast_mark& free_vars) { + for (expr* t : subterms::all(expr_ref(e, m))) { + if (is_app(t) && is_uninterp(t)) { + func_decl* f = to_app(t)->get_decl(); + TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); + free_vars.mark(f, true); + if (m_model_vars.is_marked(f)) + m_intersects_with_model = true; + } + } +} + + // accumulate a set of dependent exprs, updating m_trail to exclude loose // substitutions that use variables from the dependent expressions. @@ -27,6 +40,8 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt if (m_trail.empty()) return; + if (qhead == st.qtail()) + return; ast_mark free_vars; m_intersects_with_model = false; diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index c2d8b0001..4c064124a 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -101,6 +101,7 @@ class model_reconstruction_trail { */ void add_model_var(func_decl* f) { if (!m_model_vars.is_marked(f)) { + verbose_stream() << "add model var " << f->get_name() << "\n"; m_model_vars_trail.push_back(f); m_model_vars.mark(f, true); m_trail_stack.push(undo_model_var(*this)); @@ -112,16 +113,7 @@ class model_reconstruction_trail { * record if there is an intersection with the model_vars that are * registered when updates are added to the trail. */ - void add_vars(expr* e, ast_mark& free_vars) { - for (expr* t : subterms::all(expr_ref(e, m))) - if (is_app(t) && is_uninterp(t)) { - func_decl* f = to_app(t)->get_decl(); - TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); - free_vars.mark(f, true); - if (m_model_vars.is_marked(f)) - m_intersects_with_model = true; - } - } + void add_vars(expr* e, ast_mark& free_vars); void add_vars(dependent_expr const& d, ast_mark& free_vars) { add_vars(d.fml(), free_vars); diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index ae1d6b8a2..b114f364f 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -130,6 +130,10 @@ class simplifier_solver : public solver { unsigned qhead = m_preprocess_state.qhead(); expr_ref_vector orig_assumptions(assumptions); m_core_replace.reset(); + m_preprocess_state.replay(qhead, assumptions); + for (unsigned i = 0; i < assumptions.size(); ++i) + m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); + if (qhead < m_fmls.size()) { m_preprocess.reduce(); if (!m.inc()) @@ -138,11 +142,7 @@ class simplifier_solver : public solver { m_preprocess_state.display(tout)); m_preprocess_state.advance_qhead(); } - if (!assumptions.empty()) { - m_preprocess_state.replay(m_preprocess_state.qhead(), assumptions); - for (unsigned i = 0; i < assumptions.size(); ++i) - m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); - } + m_mc = m_preprocess_state.model_trail().get_model_converter(); m_cached_mc = nullptr; for (; qhead < m_fmls.size(); ++qhead) From 92376e67f283445073af27214976b45721784579 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2024 13:07:04 -0700 Subject: [PATCH 17/27] better model replay for loose entries --- src/ast/simplifiers/elim_unconstrained.cpp | 2 +- .../model_reconstruction_trail.cpp | 25 +++++++++++++++++-- .../simplifiers/model_reconstruction_trail.h | 1 - 3 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 44b1ee091..34579b710 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -80,7 +80,7 @@ void elim_unconstrained::eliminate() { continue; } expr* e = get_parent(v); - TRACE("elim_unconstrained", for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";); + TRACE("elim_unconstrained", for (expr* p : n.m_parents) tout << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";); if (!e || !is_app(e) || !is_ground(e)) { n.m_refcount = 0; continue; diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 1f3c74ea2..500e67f78 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -61,7 +61,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt return; for (auto& t : m_trail) { - TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << "\n"); + TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << " loose " << t->is_loose() << "\n"); if (!t->m_active) continue; @@ -74,9 +74,22 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt // loose entries that intersect with free vars are deleted from the trail // and their removed formulas are added to the resulting constraints. - if (t->is_loose()) { + + if (t->is_loose() && !t->is_def() && t->is_subst()) { + for (auto const& [k, v] : t->m_subst->sub()) + st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr)); + t->m_active = false; + continue; + } + + bool all_const = true; + for (auto const& [d, def, dep] : t->m_defs) + all_const &= d->get_arity() == 0; + + if (t->is_loose() && (!t->is_def() || !all_const || t->is_subst())) { for (auto r : t->m_removed) { add_vars(r, free_vars); + TRACE("simplifier", tout << "replay removed " << r << "\n"); st.add(r); } m_trail_stack.push(value_trail(t->m_active)); @@ -116,6 +129,12 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt assumptions[i] = g; // ignore dep. } + if (t->is_loose()) { + SASSERT(all_const); + SASSERT(!t->is_subst()); + for (auto const& [d, def, dep] : t->m_defs) + st.add(dependent_expr(m, m.mk_eq(m.mk_const(d), def), nullptr, nullptr)); + } continue; } @@ -156,6 +175,8 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt // ignore dep. } } + + TRACE("simplifier", st.display(tout)); } /** diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index 4c064124a..02271c6b4 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -101,7 +101,6 @@ class model_reconstruction_trail { */ void add_model_var(func_decl* f) { if (!m_model_vars.is_marked(f)) { - verbose_stream() << "add model var " << f->get_name() << "\n"; m_model_vars_trail.push_back(f); m_model_vars.mark(f, true); m_trail_stack.push(undo_model_var(*this)); From a23a8cdfc5a9d3bf6d6ce287d58752cb4a7227ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2024 19:08:33 -0700 Subject: [PATCH 18/27] add variables from definitions Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/model_reconstruction_trail.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 500e67f78..6905e0967 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -76,8 +76,10 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt // and their removed formulas are added to the resulting constraints. if (t->is_loose() && !t->is_def() && t->is_subst()) { - for (auto const& [k, v] : t->m_subst->sub()) + for (auto const& [k, v] : t->m_subst->sub()) { + add_vars(v, free_vars); st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr)); + } t->m_active = false; continue; } From 5cee19fa09555323f1b82baf8038cfdb858e6ee6 Mon Sep 17 00:00:00 2001 From: "Kirill A. Korinsky" Date: Mon, 21 Oct 2024 05:00:36 +0200 Subject: [PATCH 19/27] It uses C++20 BTW (#7429) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5350bc38b..00e5acf71 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,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 From 45ef6d0109e721396f547885b586a0fd38cf43e4 Mon Sep 17 00:00:00 2001 From: Jonas Jongejan <227529+HalfdanJ@users.noreply.github.com> Date: Tue, 22 Oct 2024 12:15:49 -0400 Subject: [PATCH 20/27] js: Adding manual release methods (#7428) * js: Adding manual release methods * Add unregister token * Add pointer assertion * Add missing line --- src/api/js/src/high-level/high-level.ts | 74 ++++++++++++++++++------- src/api/js/src/high-level/types.ts | 22 +++++++- 2 files changed, 75 insertions(+), 21 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 0869dbd7b..2c69848c3 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -178,6 +178,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { ctxs.forEach(other => assert('ctx' in other ? ctx === other.ctx : ctx === other, 'Context mismatch')); } + function _assertPtr(ptr: T | null): asserts ptr is T { + if (ptr == null) throw new TypeError('Expected non-null pointer'); + } + // call this after every nontrivial call to the underlying API function throwIfError() { if (Z3.get_error_code(contextPtr) !== Z3_error_code.Z3_OK) { @@ -1203,7 +1207,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { const myAst = this.ast; Z3.inc_ref(contextPtr, myAst); - cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst)); + cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst), this); } get ast(): Z3_ast { @@ -1240,8 +1244,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { class SolverImpl implements Solver { declare readonly __typename: Solver['__typename']; - readonly ptr: Z3_solver; readonly ctx: Context; + private _ptr: Z3_solver | null; + get ptr(): Z3_solver { + _assertPtr(this._ptr); + return this._ptr; + } constructor(ptr: Z3_solver | string = Z3.mk_solver(contextPtr)) { this.ctx = ctx; @@ -1251,9 +1259,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } else { myPtr = ptr; } - this.ptr = myPtr; + this._ptr = myPtr; Z3.solver_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr), this); } set(key: string, value: any): void { @@ -1327,21 +1335,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.solver_from_string(contextPtr, this.ptr, s); throwIfError(); } + + release() { + Z3.solver_dec_ref(contextPtr, this.ptr); + // Mark the ptr as null to prevent double free + this._ptr = null; + cleanup.unregister(this); + } } class OptimizeImpl implements Optimize { declare readonly __typename: Optimize['__typename']; - readonly ptr: Z3_optimize; readonly ctx: Context; + private _ptr: Z3_optimize | null; + get ptr(): Z3_optimize { + _assertPtr(this._ptr); + return this._ptr; + } constructor(ptr: Z3_optimize = Z3.mk_optimize(contextPtr)) { this.ctx = ctx; let myPtr: Z3_optimize; myPtr = ptr; - this.ptr = myPtr; + this._ptr = myPtr; Z3.optimize_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr), this); } set(key: string, value: any): void { @@ -1363,11 +1382,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { }); } - addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id: number | string = "") { + addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id: number | string = '') { if (isCoercibleRational(weight)) { weight = `${weight.numerator}/${weight.denominator}`; } - check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id))) + check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id))); } addAndTrack(expr: Bool, constant: Bool | string) { @@ -1395,9 +1414,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(expr); return expr.ast; }); - const result = await asyncMutex.runExclusive(() => - check(Z3.optimize_check(contextPtr, this.ptr, assumptions)), - ); + const result = await asyncMutex.runExclusive(() => check(Z3.optimize_check(contextPtr, this.ptr, assumptions))); switch (result) { case Z3_lbool.Z3_L_FALSE: return 'unsat'; @@ -1422,17 +1439,28 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.optimize_from_string(contextPtr, this.ptr, s); throwIfError(); } - } + release() { + Z3.optimize_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } + } class ModelImpl implements Model { declare readonly __typename: Model['__typename']; readonly ctx: Context; + private _ptr: Z3_model | null; + get ptr(): Z3_model { + _assertPtr(this._ptr); + return this._ptr; + } - constructor(readonly ptr: Z3_model = Z3.mk_model(contextPtr)) { + constructor(ptr: Z3_model = Z3.mk_model(contextPtr)) { this.ctx = ctx; + this._ptr = ptr; Z3.model_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr), this); } length() { @@ -1594,6 +1622,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(sort); return new AstVectorImpl(check(Z3.model_get_sort_universe(contextPtr, this.ptr, sort.ptr))); } + + release() { + Z3.model_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } } class FuncEntryImpl implements FuncEntry { @@ -1604,7 +1638,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_func_entry) { this.ctx = ctx; Z3.func_entry_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr), this); } numArgs() { @@ -1627,7 +1661,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_func_interp) { this.ctx = ctx; Z3.func_interp_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr), this); } elseValue(): Expr { @@ -1922,7 +1956,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { this.ptr = myPtr; Z3.tactic_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr), this); } } @@ -2586,7 +2620,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_ast_vector = Z3.mk_ast_vector(contextPtr)) { this.ctx = ctx; Z3.ast_vector_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr), this); } length(): number { @@ -2684,7 +2718,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_ast_map = Z3.mk_ast_map(contextPtr)) { this.ctx = ctx; Z3.ast_map_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr), this); } [Symbol.iterator](): Iterator<[Key, Value]> { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 6f3630a6d..45a06bda6 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -663,6 +663,13 @@ export interface Solver { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; + + /** + * Manually decrease the reference count of the solver + * This is automatically done when the solver is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } export interface Optimize { @@ -695,8 +702,14 @@ export interface Optimize { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; -} + /** + * Manually decrease the reference count of the optimize + * This is automatically done when the optimize is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; +} /** @hidden */ export interface ModelCtor { @@ -746,6 +759,13 @@ export interface Model extends Iterable, defaultValue: CoercibleToMap, Name>, ): FuncInterp; + + /** + * Manually decrease the reference count of the model + * This is automatically done when the model is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /** From d18831c8d5e58730f0bad1cbeb5de0dc9d59055c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Oct 2024 10:18:51 -0700 Subject: [PATCH 21/27] Update sat_ddfw.cpp --- src/sat/sat_ddfw.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index ccf5a55db..83feed145 100644 --- a/src/sat/sat_ddfw.cpp +++ b/src/sat/sat_ddfw.cpp @@ -213,6 +213,7 @@ namespace sat { } void ddfw::add(solver const& s) { + set_seed(s.get_config().m_random_seed); for (auto& ci : m_clauses) m_alloc.del_clause(ci.m_clause); m_clauses.reset(); From 253f7d7675fc04683a865bfae13240ef0a189bb9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Oct 2024 09:59:12 -0700 Subject: [PATCH 22/27] fix non-termination bug in elim-unconstrained, add parameter validation to fix #7432 --- src/ast/simplifiers/elim_unconstrained.cpp | 13 +++++++------ src/cmd_context/pdecl.cpp | 6 +++++- src/sat/sat_ddfw.cpp | 1 - 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 34579b710..a355f823a 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -86,7 +86,7 @@ void elim_unconstrained::eliminate() { continue; } if (m_heap.contains(root(e))) { - IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n"); + TRACE("elim_unconstrained", tout << "already in heap " << mk_bounded_pp(e, m) << "\n"); continue; } app* t = to_app(e); @@ -111,9 +111,9 @@ void elim_unconstrained::eliminate() { continue; } - IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " : " << rr << " -> " << r << "\n"); + IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); - TRACE("elim_unconstrained", tout << mk_pp(t, m) << " : " << rr << " -> " << r << "\n"); + TRACE("elim_unconstrained", tout << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); SASSERT(r->get_sort() == t->get_sort()); m_stats.m_num_eliminated++; m_trail.push_back(r); @@ -147,10 +147,10 @@ expr* elim_unconstrained::get_parent(unsigned n) const { } void elim_unconstrained::invalidate_parents(expr* e) { - ptr_vector todo; + ptr_buffer todo; do { node& n = get_node(e); - if (!n.m_dirty) { + if (!n.m_dirty && e == n.m_term) { n.m_dirty = true; for (expr* e : n.m_parents) todo.push_back(e); @@ -299,7 +299,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) { return expr_ref(t, m); if (!is_node(t)) return expr_ref(t, m); - ptr_vector todo; + ptr_buffer todo; todo.push_back(t); while (!todo.empty()) { t = todo.back(); @@ -310,6 +310,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) { unsigned sz0 = todo.size(); if (is_app(t)) { if (n.m_term != t) { + n.m_dirty = false; todo.pop_back(); continue; } diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index f343be94d..de977edd7 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -225,7 +225,9 @@ class psort_app : public psort { sort * a = m_args[i]->instantiate(m, n, s); args_i.push_back(a); } - r = m_decl->instantiate(m, args_i.size(), args_i.data()); + r = m_decl->instantiate(m, args_i.size(), args_i.data()); + if (m_num_params != n) + throw default_exception("mismatch between number of declared and supplied sort parameters"); cache(m, s, r); return r; } @@ -771,6 +773,8 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { for (unsigned i = 0; i < d->get_num_params(); ++i) { ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr)); } + verbose_stream() << ps.size() << " " << ps << "\n"; + dts.m_buffer.push_back(d->instantiate_decl(m, ps.size(), ps.data())); } sort_ref_vector sorts(m.m()); diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index 83feed145..73e8afe00 100644 --- a/src/sat/sat_ddfw.cpp +++ b/src/sat/sat_ddfw.cpp @@ -262,7 +262,6 @@ namespace sat { m_assumptions.append(sz, assumptions); add_assumptions(); for (unsigned v = 0; v < num_vars(); ++v) { - literal lit(v, false), nlit(v, true); value(v) = (m_rand() % 2) == 0; // m_use_list[lit.index()].size() >= m_use_list[nlit.index()].size(); } init_clause_data(); From 0ebea1c298ab38165b60b1744e7e700796601b31 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Oct 2024 11:58:16 -0700 Subject: [PATCH 23/27] remove debug out Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 ++ src/cmd_context/pdecl.cpp | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5c2a35995..43571167d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1073,6 +1073,8 @@ class ExprRef(AstRef): _z3_assert(is_app(self), "Z3 application expected") return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx) + + def num_args(self): """Return the number of arguments of a Z3 application. diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index de977edd7..4dfb0f8bb 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -773,7 +773,6 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { for (unsigned i = 0; i < d->get_num_params(); ++i) { ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr)); } - verbose_stream() << ps.size() << " " << ps << "\n"; dts.m_buffer.push_back(d->instantiate_decl(m, ps.size(), ps.data())); } From 78d1139ba0b6523d6d0012ed9918517a101bff8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Oct 2024 13:04:41 -0700 Subject: [PATCH 24/27] add shortcut to retrieve kind of application Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 43571167d..290a8f58e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1073,7 +1073,12 @@ class ExprRef(AstRef): _z3_assert(is_app(self), "Z3 application expected") return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx) - + def kind(self): + """Return the Z3 internal kind of a function application.""" + if z3_debug(): + _z3_assert(is_app(self), "Z3 application expected") + return Z3_get_decl_kind(self.ctx_ref(), Z3_get_app_decl(self.ctx_ref(), self.ast)) + def num_args(self): """Return the number of arguments of a Z3 application. From 8b657f27aabaa921e8d951b0a8a0c83a43495879 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Oct 2024 13:05:58 -0700 Subject: [PATCH 25/27] add shortcut to retrieve kind of application Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 290a8f58e..38538509c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1400,7 +1400,7 @@ def is_app_of(a, k): >>> is_app_of(n, Z3_OP_MUL) False """ - return is_app(a) and a.decl().kind() == k + return is_app(a) and a.kind() == k def If(a, b, c, ctx=None): @@ -9454,7 +9454,7 @@ _ROUNDING_MODES = frozenset({ def set_default_rounding_mode(rm, ctx=None): global _dflt_rounding_mode if is_fprm_value(rm): - _dflt_rounding_mode = rm.decl().kind() + _dflt_rounding_mode = rm.kind() else: _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode") _dflt_rounding_mode = rm From b0fef6429fb29a33eb14adf9a61353b59f0f7fd0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Oct 2024 01:33:09 -0700 Subject: [PATCH 26/27] Add assert_and_track support to Optimize class in .NET binding (#7437) Related to #7436 #7436 --- For more details, open the [Copilot Workspace session](https://copilot-workspace.githubnext.com/Z3Prover/z3/issues/7436?shareId=XXXX-XXXX-XXXX-XXXX). --- src/api/dotnet/Optimize.cs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 891ed4105..3bc06de16 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -148,6 +148,28 @@ namespace Microsoft.Z3 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject); } } + + /// + /// Assert a constraint into the optimize solver, and track it (in the unsat) core + /// using the Boolean constant p. + /// + /// + /// This API is an alternative to with assumptions for extracting unsat cores. + /// Both APIs can be used in the same solver. The unsat core will contain a combination + /// of the Boolean variables provided using + /// and the Boolean literals + /// provided using with assumptions. + /// + public void AssertAndTrack(BoolExpr constraint, BoolExpr p) + { + Debug.Assert(constraint != null); + Debug.Assert(p != null); + Context.CheckContextMatch(constraint); + Context.CheckContextMatch(p); + + Native.Z3_optimize_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject); + } + /// /// Handle to objectives returned by objective functions. /// From ecdfab81a640c7591d572602b7a58a1cc04a11c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Oct 2024 17:50:53 -0700 Subject: [PATCH 27/27] fix #7434 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 7b54f76a1..20241536f 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2785,9 +2785,16 @@ br_status bv_rewriter::mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result) { result = m.mk_false(); return BR_REWRITE1; } - if (m_util.is_bv2int(lhs, x) && m_util.is_bv2int(rhs, y)) { + if (m_util.is_bv2int(lhs, x) && + m_util.is_bv2int(rhs, y)) { + auto szx = m_util.get_bv_size(x); + auto szy = m_util.get_bv_size(y); + if (szx < szy) + x = m_util.mk_zero_extend(szy - szx, x); + else if (szx > szy) + y = m_util.mk_zero_extend(szx - szy, y); result = m.mk_eq(x, y); - return BR_REWRITE1; + return BR_REWRITE2; } return BR_FAILED; }