From 84a7a79e90212c14a0a4c451ab0251d9f3369455 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 17:08:01 -0800 Subject: [PATCH 01/39] fix #7037 --- src/smt/theory_datatype.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d1216c171..cfc1f06f2 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -509,10 +509,10 @@ namespace smt { // Assuming `app` is equal to a constructor term, return the constructor enode inline enode * theory_datatype::oc_get_cstor(enode * app) { theory_var v = app->get_root()->get_th_var(get_id()); - SASSERT(v != null_theory_var); + if (v == null_theory_var) + return nullptr; v = m_find.find(v); var_data * d = m_var_data[v]; - SASSERT(d->m_constructor); return d->m_constructor; } @@ -802,8 +802,9 @@ namespace smt { return false; func_decl* con = m_util.get_accessor_constructor(f); for (enode* app : ctx.enodes_of(f)) { - enode* arg = app->get_arg(0)->get_root(); - if (is_constructor(arg) && arg->get_decl() != con) + enode* arg = app->get_arg(0); + enode* arg_con = oc_get_cstor(arg); + if (arg_con && is_constructor(arg_con) && arg_con->get_decl() != con) return true; } return false; From 4a9b38e531e86f3b92435f064ae7bea678c8486d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 17:08:17 -0800 Subject: [PATCH 02/39] clean up nla_grobner --- src/math/lp/nla_grobner.cpp | 89 ++++--------------------------------- src/math/lp/nla_grobner.h | 6 --- 2 files changed, 9 insertions(+), 86 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index baf27a5bb..f9974b41c 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -59,21 +59,20 @@ namespace nla { if (m_delay_base > 0) --m_delay_base; - if (is_conflicting()) - return; - try { - if (propagate_bounds()) + + if (is_conflicting()) return; if (propagate_eqs()) return; - + if (propagate_factorization()) return; - + if (propagate_linear_equations()) return; + } catch (...) { @@ -111,17 +110,9 @@ namespace nla { return false; } - bool grobner::propagate_bounds() { - unsigned changed = 0; - for (auto eq : m_solver.equations()) - if (propagate_bounds(*eq) && ++changed >= m_solver.number_of_conflicts_to_report()) - return true; - return changed > 0; - } - bool grobner::propagate_eqs() { unsigned changed = 0; - for (auto eq : m_solver.equations()) + for (auto eq : m_solver.equations()) if (propagate_fixed(*eq) && ++changed >= m_solver.number_of_conflicts_to_report()) return true; return changed > 0; @@ -129,7 +120,7 @@ namespace nla { bool grobner::propagate_factorization() { unsigned changed = 0; - for (auto eq : m_solver.equations()) + for (auto eq : m_solver.equations()) if (propagate_factorization(*eq) && ++changed >= m_solver.number_of_conflicts_to_report()) return true; return changed > 0; @@ -165,19 +156,12 @@ namespace nla { rational d = lcm(denominator(a), denominator(b)); a *= d; b *= d; -#if 0 - c().lra.update_column_type_and_bound(v, lp::lconstraint_kind::EQ, b/a, eq.dep()); - lp::explanation exp; - explain(eq, exp); - c().add_fixed_equality(c().lra.column_to_reported_index(v), b/a, exp); -#else ineq new_eq(term(a, v), llc::EQ, b); if (c().ineq_holds(new_eq)) return false; new_lemma lemma(c(), "pdd-eq"); add_dependencies(lemma, eq); lemma |= new_eq; -#endif return true; } @@ -377,73 +361,18 @@ namespace nla { } } - bool grobner::propagate_bounds(const dd::solver::equation& e) { - return false; - // TODO - auto& di = c().m_intervals.get_dep_intervals(); - dd::pdd_interval eval(di); - eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) { - if (deps) c().m_intervals.set_var_interval(j, a); - else c().m_intervals.set_var_interval(j, a); - }; - scoped_dep_interval i(di), i_wd(di); - eval.get_interval(e.poly(), i); - return false; - } - bool grobner::propagate_linear_equations() { unsigned changed = 0; m_mon2var.clear(); for (auto const& m : c().emons()) m_mon2var[m.vars()] = m.var(); + for (auto eq : m_solver.equations()) if (propagate_linear_equations(*eq)) ++changed; -#if 0 - for (auto eq : m_solver.equations()) - if (check_missed_bound(*eq)) - return true; -#endif return changed > 0; } - - bool grobner::check_missed_bound(dd::solver::equation const& e) { - auto& di = c().m_intervals.get_dep_intervals(); - auto set_var_interval = [&](lpvar j, scoped_dep_interval& a) { - c().m_intervals.set_var_interval(j, a); - }; - scoped_dep_interval i(di), t(di), s(di), u(di); - di.set_value(i, rational::zero()); - - for (auto const& [coeff, vars] : e.poly()) { - if (vars.empty()) - di.add(coeff, i); - else { - di.set_value(t, coeff); - for (auto v : vars) { - set_var_interval(v, s); - di.mul(t, s, t); - } - if (m_mon2var.find(vars) != m_mon2var.end()) { - auto v = m_mon2var.find(vars)->second; - set_var_interval(v, u); - di.mul(coeff, u, u); - di.intersect(t, u, t); - } - di.add(i, t, i); - } - } - if (!di.separated_from_zero(i)) - return false; -// m_solver.display(verbose_stream() << "missed bound\n", e); -// exit(1); - std::function f = [this](const lp::explanation& e) { - new_lemma lemma(m_core, "pdd"); - lemma &= e; - }; - return di.check_interval_for_conflict_on_zero(i, e.dep(), f); - } - + bool grobner::propagate_linear_equations(dd::solver::equation const& e) { if (equation_is_true(e)) return false; diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index e70b5473d..be5f06136 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -35,20 +35,14 @@ namespace nla { bool is_conflicting(); bool is_conflicting(dd::solver::equation const& eq); - bool propagate_bounds(); - bool propagate_bounds(dd::solver::equation const& eq); - bool propagate_eqs(); bool propagate_fixed(dd::solver::equation const& eq); bool propagate_factorization(); bool propagate_factorization(dd::solver::equation const& eq); - bool propagate_linear_equations(); bool propagate_linear_equations(dd::solver::equation const& eq); - - bool check_missed_bound(dd::solver::equation const& eq); void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq); void explain(dd::solver::equation const& eq, lp::explanation& exp); From 5e3f1d988b2435620a45906b974bdea1d605332d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 19:38:52 -0800 Subject: [PATCH 03/39] update release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 5 ++++- scripts/release.yml | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index f46f32a1a..b00cb2398 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -9,7 +9,6 @@ Version 4.next - polysat - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. - - Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT. Version 4.12.3 ============== @@ -23,6 +22,10 @@ Version 4.12.3 - Various (ongoing) performance fixes and improvements to smt.arith.solver=6 - A working version of solver.proof.trim=true option. Proofs logs created when using sat.smt=true may be trimmed by running z3 on the generated proof log using the option solver.proof.trim=true. +- Optimizations LIA and NIA (linear integer arithmetic and non-linear integer (and real) arithmetic reasoning). + smt.arith.solver=6 is the default for most use cases. It trails smt.arith.solver=2 in some scenarios and the gap has been either removed or reduced. + smt.arith.solver=6 is complete for integrations of non-linear real arithmetic and theories, smt.arith.solver=2 is not. +- qel: Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT. Version 4.12.2 ============== diff --git a/scripts/release.yml b/scripts/release.yml index b400860a7..49679d12e 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -583,7 +583,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,0) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From 389aea3330c066215289eec36911391138e8d1d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 19:48:43 -0800 Subject: [PATCH 04/39] update release notes, update version number Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- RELEASE_NOTES.md | 5 +++++ scripts/mk_project.py | 2 +- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- 5 files changed, 9 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0ab59f18f..b98360df8 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.12.3.0 LANGUAGES CXX) +project(Z3 VERSION 4.12.4.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index b00cb2398..fa22ae0eb 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,9 @@ 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.4 +============== + Version 4.12.3 ============== - Alpha support for polymorphism. @@ -26,6 +29,8 @@ Version 4.12.3 smt.arith.solver=6 is the default for most use cases. It trails smt.arith.solver=2 in some scenarios and the gap has been either removed or reduced. smt.arith.solver=6 is complete for integrations of non-linear real arithmetic and theories, smt.arith.solver=2 is not. - qel: Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT. +- added real-closed fields features to C API, exposed more RCF over OCaml API +- fixes to FP Version 4.12.2 ============== diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 876e0fd21..3a3f19fb2 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, 12, 3, 0) # express a default build version or pick up ci build version + set_version(4, 12, 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 eebff5803..3d8f6a5b7 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '12' - Patch: '3' + Patch: '4' AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName) diff --git a/scripts/release.yml b/scripts/release.yml index 49679d12e..08731c6e2 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.12.3' + ReleaseVersion: '4.12.4' stages: From 4d4359f78aaa1428487d04ce2064c2365060b7a4 Mon Sep 17 00:00:00 2001 From: Rui Chen Date: Tue, 5 Dec 2023 10:48:15 -0500 Subject: [PATCH 05/39] fix shebang syntax issue (#7044) --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index ddfb31f26..d426da34a 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1,4 +1,4 @@ -# - !/usr/bin/env python +#!/usr/bin/env python ############################################ # Copyright (c) 2012 Microsoft Corporation # From 764f0d54a436bd93069778a385517e74aea47150 Mon Sep 17 00:00:00 2001 From: Asger Hautop Drewsen Date: Tue, 5 Dec 2023 16:48:57 +0100 Subject: [PATCH 06/39] Overload xor operator for BoolRef (#7043) --- src/api/python/z3/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f7a99f1c2..4d92af8b9 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1593,6 +1593,9 @@ class BoolRef(ExprRef): def __or__(self, other): return Or(self, other) + + def __xor__(self, other): + return Xor(self, other) def __invert__(self): return Not(self) From 9ad4d50b5d859443e3ba004bd36c560af3673a55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20G=C3=B3rny?= Date: Tue, 5 Dec 2023 16:49:32 +0100 Subject: [PATCH 07/39] Use built-in `importlib.resources` on Python 3.9+ (#7042) Use built-in `importlib.resources` module rather than the external `importlib_resources` package on Python 3.9 and newer. The latter is only intended as a backport for old Python versions, and since modern Linux distributions may no longer support such old Python versions, they also no longer provide importlib_resources (this is the case on Gentoo). --- scripts/update_api.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index d426da34a..7d3d8899f 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1831,7 +1831,10 @@ import atexit import sys, os import contextlib import ctypes -import importlib_resources +if sys.version_info >= (3, 9): + import importlib.resources as importlib_resources +else: + import importlib_resources from .z3types import * from .z3consts import * From f5ae8c324c27ae9cd1f2799e53763b306e5087a8 Mon Sep 17 00:00:00 2001 From: NikolajBjorner Date: Tue, 5 Dec 2023 08:01:59 -0800 Subject: [PATCH 08/39] make a readme file Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index cf7140e5e..33d8eeb3d 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -86,6 +86,10 @@ def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") +def mk_readme(source_root): + mk_dir("out/content") + shutil.copy(f"{source_root}/README.md", "out/content/README.md") + def create_nuget_spec(version, repo, branch, commit, symbols, arch): arch = f".{arch}" if arch == "x86" else "" @@ -140,6 +144,7 @@ class Env: mk_dir(self.packages) unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) + mk_readme(self.source_root) mk_icon(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) From 23fcb4376f661784729f534371ab002a82f10bcf Mon Sep 17 00:00:00 2001 From: NikolajBjorner Date: Tue, 5 Dec 2023 08:03:28 -0800 Subject: [PATCH 09/39] readme Signed-off-by: NikolajBjorner --- scripts/mk_nuget_task.py | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 33d8eeb3d..cafdc37e1 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -108,6 +108,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg + content/readme.md https://github.com/Z3Prover/z3 MIT From aa2e54c5a4ea8198139ecabb45fd92cb6950182f Mon Sep 17 00:00:00 2001 From: NikolajBjorner Date: Tue, 5 Dec 2023 08:18:33 -0800 Subject: [PATCH 10/39] update release pipeline Signed-off-by: NikolajBjorner --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 08731c6e2..5f049345c 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -504,7 +504,7 @@ stages: displayName: "Download Ubuntu Arm64" inputs: artifactName: 'UbuntuArm64' - targetPath: tmp + path: $(Agent.TempDirectory) - task: DownloadPipelineArtifact@2 displayName: "Download Doc" inputs: From 669f665f24ea74e0746e4e21c05f778e22c20bed Mon Sep 17 00:00:00 2001 From: NikolajBjorner Date: Tue, 5 Dec 2023 08:19:20 -0800 Subject: [PATCH 11/39] update release pipeline Signed-off-by: NikolajBjorner --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 5f049345c..6b4fbdb66 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -583,7 +583,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,1) + condition: eq(1,0) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From 7c81ee08900e43e7ec311e5502cfcaa6c0dc09b3 Mon Sep 17 00:00:00 2001 From: NikolajBjorner Date: Tue, 5 Dec 2023 09:02:08 -0800 Subject: [PATCH 12/39] fix case of README.md in nuget Signed-off-by: NikolajBjorner --- scripts/mk_nuget_task.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index cafdc37e1..13f3fc923 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -108,7 +108,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/readme.md + content/README.md https://github.com/Z3Prover/z3 MIT From a9513c19989454ac4aeaa83bdb6310cf6386835d Mon Sep 17 00:00:00 2001 From: Asger Hautop Drewsen Date: Tue, 5 Dec 2023 18:12:25 +0100 Subject: [PATCH 13/39] Improve BoolRef addition (#7045) --- 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 4d92af8b9..18d3abc9d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1572,7 +1572,12 @@ class BoolRef(ExprRef): return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) def __add__(self, other): - return If(self, 1, 0) + If(other, 1, 0) + if isinstance(other, BoolRef): + other = If(other, 1, 0) + return If(self, 1, 0) + other + + def __radd__(self, other): + return self + other def __rmul__(self, other): return self * other From 426d7f5810bcf434182af406acccc9e5120330d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 12:11:06 -0800 Subject: [PATCH 14/39] remove reference to readme in nuget task Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 5 ----- 1 file changed, 5 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 13f3fc923..18dcb52f0 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -86,9 +86,6 @@ def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") -def mk_readme(source_root): - mk_dir("out/content") - shutil.copy(f"{source_root}/README.md", "out/content/README.md") def create_nuget_spec(version, repo, branch, commit, symbols, arch): @@ -108,7 +105,6 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/README.md https://github.com/Z3Prover/z3 MIT @@ -145,7 +141,6 @@ class Env: mk_dir(self.packages) unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) - mk_readme(self.source_root) mk_icon(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) From 76c05f171ae98f81f845001279691e253bc5f3da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 12:32:30 -0800 Subject: [PATCH 15/39] specify a readme file with the nuget package Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Microsoft.Z3.csproj.in | 7 +++++++ src/api/python/setup.py | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index 85ab98b38..3999e724b 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -7,6 +7,8 @@ Microsoft.Z3 Microsoft.Z3 + README.md + Z3 .NET Interface Z3 .NET Interface @@ -65,6 +67,11 @@ ${Z3_DOTNET_COMPILE_ITEMS} + + + + + diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 1837b5bec..a20ff53a3 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -18,7 +18,7 @@ from setuptools.command.bdist_egg import bdist_egg as _bdist_egg build_env = dict(os.environ) build_env['PYTHON'] = sys.executable -build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++11" +build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -std=c++17" # determine where we're building and where sources are ROOT_DIR = os.path.abspath(os.path.dirname(__file__)) From d566eb3df7931e8f8f32a138c8a8ab445963f24e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 13:04:25 -0800 Subject: [PATCH 16/39] include readme in package Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 +++- src/api/dotnet/Microsoft.Z3.csproj.in | 4 ++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3d3996792..bd8e9d918 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1736,6 +1736,7 @@ class DotNetDLLComponent(Component): true Microsoft Microsoft + README.md false Z3 is a satisfiability modulo theories solver from Microsoft Research. Copyright Microsoft Corporation. All rights reserved. @@ -1745,9 +1746,10 @@ class DotNetDLLComponent(Component): + -""" % (version, key, self.to_src_dir) +""" % (version, key, self.to_src_dir, self.src_dir) mk_dir(os.path.join(BUILD_DIR, 'dotnet')) csproj = os.path.join('dotnet', 'z3.csproj') diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index 3999e724b..ec136809d 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -17,8 +17,8 @@ Z3 is a satisfiability modulo theories solver from Microsoft Research. .NET Interface to the Z3 Theorem Prover - Copyright (C) 2006-2019 Microsoft Corporation - Copyright (C) 2006-2019 Microsoft Corporation + Copyright (C) 2006- Microsoft Corporation + Copyright (C) 2006- Microsoft Corporation Microsoft Corporation Microsoft Corporation From 111ce017025fbfbde5641574e4986c0722ad39ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 13:47:05 -0800 Subject: [PATCH 17/39] update path reference to readme --- scripts/mk_util.py | 2 +- src/api/dotnet/README.md | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 src/api/dotnet/README.md diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bd8e9d918..6b1ad95d6 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1746,7 +1746,7 @@ class DotNetDLLComponent(Component): - + """ % (version, key, self.to_src_dir, self.src_dir) diff --git a/src/api/dotnet/README.md b/src/api/dotnet/README.md new file mode 100644 index 000000000..fe614782f --- /dev/null +++ b/src/api/dotnet/README.md @@ -0,0 +1,3 @@ +# Z3 Nuget Package + +For more information see [the Z3 github page](https://github.com/z3prover/z3.git) From 156426a0cf6c5cb23ea8a63a5fd6728bb628a560 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 15:10:13 -0800 Subject: [PATCH 18/39] use / for package path Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6b1ad95d6..0728c2cb7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1746,10 +1746,10 @@ class DotNetDLLComponent(Component): - + -""" % (version, key, self.to_src_dir, self.src_dir) +""" % (version, key, self.to_src_dir, self.to_src_dir) mk_dir(os.path.join(BUILD_DIR, 'dotnet')) csproj = os.path.join('dotnet', 'z3.csproj') From 1d6616afaced6ce9f7924b86f03c40f4719e534f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 15:41:35 -0800 Subject: [PATCH 19/39] make var-queue a template Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.h | 2 +- src/util/var_queue.h | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 3a437855e..0361fc157 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -164,7 +164,7 @@ namespace sat { unsigned m_rephase_inc; backoff m_rephase; backoff m_reorder; - var_queue m_case_split_queue; + var_queue m_case_split_queue; unsigned m_qhead; unsigned m_scope_lvl; unsigned m_search_lvl; diff --git a/src/util/var_queue.h b/src/util/var_queue.h index 7245153ca..9807e5ac2 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -21,20 +21,20 @@ Revision History: #include "util/heap.h" - +template class var_queue { typedef unsigned var; struct lt { - svector & m_activity; - lt(svector & act):m_activity(act) {} + ActivityVector & m_activity; + lt(ActivityVector & act):m_activity(act) {} bool operator()(var v1, var v2) const { return m_activity[v1] > m_activity[v2]; } }; heap m_queue; -public: +public: - var_queue(svector & act):m_queue(128, lt(act)) {} + var_queue(ActivityVector & act):m_queue(128, lt(act)) {} void activity_increased_eh(var v) { if (m_queue.contains(v)) @@ -90,11 +90,12 @@ public: return out; } - using const_iterator = decltype(m_queue)::const_iterator; + using const_iterator = const int *; const_iterator begin() const { return m_queue.begin(); } const_iterator end() const { return m_queue.end(); } }; -inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) { +template +inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) { return queue.display(out); } From 1fde3e9fb86dcee8a547871a7d96ffd5337e61a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 16:16:27 -0800 Subject: [PATCH 20/39] update release Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 6b4fbdb66..5f049345c 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -583,7 +583,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,0) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From 8111d879cdb34f8f2d1b85ace401edfb2147717e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 16:37:48 -0800 Subject: [PATCH 21/39] add README path to mk_nuget_task Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 6 ++++++ scripts/release.yml | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 18dcb52f0..dd5659ba5 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -86,6 +86,10 @@ def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") +def mk_readme(source_root): + mk_dir("out/content") + shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/icon.jpg") + def create_nuget_spec(version, repo, branch, commit, symbols, arch): @@ -105,6 +109,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg + content/README.md https://github.com/Z3Prover/z3 MIT @@ -142,6 +147,7 @@ class Env: unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) mk_icon(self.source_root) + mk_readme(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) def main(): diff --git a/scripts/release.yml b/scripts/release.yml index 5f049345c..6b4fbdb66 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -583,7 +583,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,1) + condition: eq(1,0) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From 2c8d33851a4475605f6803663e600b22938cc18c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 16:38:35 -0800 Subject: [PATCH 22/39] add README path to mk_nuget_task Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index dd5659ba5..8f238bcc2 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -88,7 +88,7 @@ def mk_icon(source_root): def mk_readme(source_root): mk_dir("out/content") - shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/icon.jpg") + shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") From fc3a7655a5456bcad6f5f3d557db1ee73178330f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 18:06:17 -0800 Subject: [PATCH 23/39] try to put readme in root Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 8f238bcc2..44987868d 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -24,10 +24,11 @@ def mk_dir(d): os_info = { 'ubuntu-latest' : ('so', 'linux-x64'), 'ubuntu-18' : ('so', 'linux-x64'), 'ubuntu-20' : ('so', 'linux-x64'), - 'x64-glibc-2.31' : ('so', 'linux-x64'), + 'x64-glibc-2.35' : ('so', 'linux-x64'), 'x64-win' : ('dll', 'win-x64'), 'x86-win' : ('dll', 'win-x86'), 'x64-osx' : ('dylib', 'osx-x64'), + 'arm-glibc-2.35' : ('so', 'linux-arm64'), 'arm64-osx' : ('dylib', 'osx-arm64'), 'debian' : ('so', 'linux-x64') } @@ -88,7 +89,7 @@ def mk_icon(source_root): def mk_readme(source_root): mk_dir("out/content") - shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") + shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/README.md") @@ -109,7 +110,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/README.md + README.md https://github.com/Z3Prover/z3 MIT From b3ef74c86da1915151bfc19d417190ff9379c550 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Dec 2023 18:50:23 -0800 Subject: [PATCH 24/39] remove readme for dist Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 44987868d..841d30e2c 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -110,7 +110,6 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - README.md https://github.com/Z3Prover/z3 MIT @@ -148,7 +147,7 @@ class Env: unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) mk_icon(self.source_root) - mk_readme(self.source_root) +# mk_readme(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) def main(): From dce2f3d88ff7b8671bd5d843f4f3f353e7089a45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Dec 2023 07:10:56 -0800 Subject: [PATCH 25/39] add release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 4 ++++ scripts/mk_nuget_task.py | 6 ++++-- scripts/release.yml | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index fa22ae0eb..f0fdc368c 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -12,6 +12,10 @@ Version 4.next Version 4.12.4 ============== +- Re-release fixing a few issues with 4.12: + - Python dependency on importlib.resources vs importlib_resources break automatic pypi installations. Supposedly fixed by conditioning dependency on Python 3.9 where the feature is built-in. + - Missing release of arm64 for Ubuntu. + - Futile attempt to streamline adding readme.md file as part of Nuget distribution. Nuget.org now requires a readme file. I was able to integrate the readme with the cmake build, but the cross-platform repackage in scripts/mk_nuget_task.py does not ingest a similar readme file with the CI pipelines. Version 4.12.3 ============== diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 841d30e2c..ef41051d8 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -28,10 +28,12 @@ os_info = { 'ubuntu-latest' : ('so', 'linux-x64'), 'x64-win' : ('dll', 'win-x64'), 'x86-win' : ('dll', 'win-x86'), 'x64-osx' : ('dylib', 'osx-x64'), - 'arm-glibc-2.35' : ('so', 'linux-arm64'), - 'arm64-osx' : ('dylib', 'osx-arm64'), 'debian' : ('so', 'linux-x64') } +# Nuget not supported for ARM +#'arm-glibc-2.35' : ('so', 'linux-arm64'), +#'arm64-osx' : ('dylib', 'osx-arm64'), + def classify_package(f, arch): diff --git a/scripts/release.yml b/scripts/release.yml index 6b4fbdb66..5f049345c 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -583,7 +583,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,0) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From 6afed0819c3c1ab515d7606bc4b703a4d8f9d405 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Dec 2023 07:13:07 -0800 Subject: [PATCH 26/39] update minor version number Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- RELEASE_NOTES.md | 3 +++ scripts/mk_project.py | 2 +- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- 5 files changed, 7 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index b98360df8..60531ca94 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.12.4.0 LANGUAGES CXX) +project(Z3 VERSION 4.12.5.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index f0fdc368c..9a7bc1856 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,9 @@ 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.5 +============== + Version 4.12.4 ============== - Re-release fixing a few issues with 4.12: diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 3a3f19fb2..77bb1b680 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, 12, 4, 0) # express a default build version or pick up ci build version + set_version(4, 12, 5, 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 3d8f6a5b7..2b1b4ca3d 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '12' - Patch: '4' + Patch: '5' AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName) diff --git a/scripts/release.yml b/scripts/release.yml index 5f049345c..76f8a8a57 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.12.4' + ReleaseVersion: '4.12.5' stages: From 4d1d067d42c3ea9d2928448b39695389c0e38552 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Dec 2023 13:34:35 -0800 Subject: [PATCH 27/39] fix divergence reported by Guido Martinez --- src/math/lp/emonics.cpp | 15 +++++++++++++++ src/math/lp/emonics.h | 1 + src/math/lp/monic.h | 3 +++ src/math/lp/nla_core.cpp | 3 +++ 4 files changed, 22 insertions(+) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index 9a9e4566b..5d0e664f2 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -611,4 +611,19 @@ void emonics::set_propagated(monic const& m) { m_u_f_stack.push(set_unpropagated(*this, m.var())); } +void emonics::set_bound_propagated(monic const& m) { + struct set_bound_unpropagated : public trail { + emonics& em; + unsigned var; + public: + set_bound_unpropagated(emonics& em, unsigned var): em(em), var(var) {} + void undo() override { + em[var].set_bound_propagated(false); + } + }; + SASSERT(!m.is_bound_propagated()); + (*this)[m.var()].set_bound_propagated(true); + m_u_f_stack.push(set_bound_unpropagated(*this, m.var())); +} + } diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index fe0b19117..55086515d 100644 --- a/src/math/lp/emonics.h +++ b/src/math/lp/emonics.h @@ -143,6 +143,7 @@ public: void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} void set_propagated(monic const& m); + void set_bound_propagated(monic const& m); // this method is required by union_find trail_stack & get_trail_stack() { return m_u_f_stack; } diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h index d981b2042..19137cd31 100644 --- a/src/math/lp/monic.h +++ b/src/math/lp/monic.h @@ -59,6 +59,7 @@ class monic: public mon_eq { bool m_rsign; mutable unsigned m_visited; bool m_propagated = false; + bool m_bound_propagated = false; public: // constructors monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): @@ -77,6 +78,8 @@ public: void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } void set_propagated(bool p) { m_propagated = p; } bool is_propagated() const { return m_propagated; } + void set_bound_propagated(bool p) { m_bound_propagated = p; } + bool is_bound_propagated() const { return m_bound_propagated; } svector::const_iterator begin() const { return vars().begin(); } svector::const_iterator end() const { return vars().end(); } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 96f1b4a30..f36fab52e 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1517,6 +1517,9 @@ void core::add_bounds() { for (lpvar j : m.vars()) { if (!var_is_free(j)) continue; + if (m.is_bound_propagated()) + continue; + m_emons.set_bound_propagated(m); // split the free variable (j <= 0, or j > 0), and return m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); TRACE("nla_solver", print_ineq(m_literals.back(), tout) << "\n"); From 6cd619d377d829a81249cef93279afebcd945b44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 11:39:55 -0800 Subject: [PATCH 28/39] kludge to fixup osver in python for Mac Signed-off-by: Nikolaj Bjorner --- src/api/python/setup.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index a20ff53a3..54992156f 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -313,6 +313,8 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv: osver = RELEASE_METADATA[3] if osver.count('.') > 1: osver = '.'.join(osver.split('.')[:2]) + if osver.startswith("11"): + osver = "11_0" if arch == 'x64': plat_name ='macosx_%s_x86_64' % osver.replace('.', '_') elif arch == 'arm64': From 8e26c2af17f33439b20c90fc865152de67cfb2df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 13:05:21 -0800 Subject: [PATCH 29/39] fix #7049 Signed-off-by: Nikolaj Bjorner --- src/ast/polymorphism_inst.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp index 4da83ee10..aa9b1e5fe 100644 --- a/src/ast/polymorphism_inst.cpp +++ b/src/ast/polymorphism_inst.cpp @@ -94,7 +94,10 @@ namespace polymorphism { t.push(value_trail(m_decl_qhead)); for (; m_decl_qhead < num_decls; ++m_decl_qhead) { func_decl* p = m_decl_queue.get(m_decl_qhead); - for (expr* e : m_occurs[m.poly_root(p)]) + func_decl* r = m.poly_root(p); + if (!m_occurs.contains(r)) + continue; + for (expr* e : m_occurs[r]) instantiate(p, e, instances); } } From 7e716f7cfe75b7da51167b0c4545c3506760351c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 13:12:05 -0800 Subject: [PATCH 30/39] try fix suggested in #7041 Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index a9f2676a7..aa4c50adf 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,3 +1,6 @@ [build-system] requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" + +[project] +dependencies = ["importlib-resources" ] \ No newline at end of file From 6282f402550e53766f28ed9354772209b93cb098 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 14:57:45 -0800 Subject: [PATCH 31/39] try add name to project Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index aa4c50adf..4c199fb26 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -3,4 +3,5 @@ requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" [project] -dependencies = ["importlib-resources" ] \ No newline at end of file +name = "z3-solver" +dependencies = ["importlib-resources", ] \ No newline at end of file From 4123405d176fb49e8e304a70405ae55448bc8ee4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 15:50:09 -0800 Subject: [PATCH 32/39] add version Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 4c199fb26..2f441d000 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -4,4 +4,5 @@ build-backend = "setuptools.build_meta" [project] name = "z3-solver" +version = "4" dependencies = ["importlib-resources", ] \ No newline at end of file From 575538d32580a7d0b2ef8f721a817abfd6e8afc6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 18:38:29 -0800 Subject: [PATCH 33/39] follow error message to put dependencies in setup args Signed-off-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 5 ----- src/api/python/setup.py | 1 + 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 2f441d000..a9f2676a7 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,8 +1,3 @@ [build-system] requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" - -[project] -name = "z3-solver" -version = "4" -dependencies = ["importlib-resources", ] \ No newline at end of file diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 54992156f..325fb4230 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -341,6 +341,7 @@ setup( license='MIT License', keywords=['z3', 'smt', 'sat', 'prover', 'theorem'], packages=['z3'], + install_requires = ['importlib-resources'], include_package_data=True, package_data={ 'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')] From e580c384b89c89f6536cc3e2e6a72471b0139bbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Dec 2023 12:46:06 -0800 Subject: [PATCH 34/39] import updates to rational from polysat Signed-off-by: Nikolaj Bjorner --- src/util/mpq.cpp | 6 ++++++ src/util/mpq.h | 8 ++++++++ src/util/mpz.cpp | 13 +++++++++++++ src/util/mpz.h | 7 +++++++ src/util/rational.h | 27 ++++++++++++++++++++++++++- 5 files changed, 60 insertions(+), 1 deletion(-) diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index 324750cfa..f90843e36 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -316,6 +316,12 @@ unsigned mpq_manager::prev_power_of_two(mpq const & a) { return prev_power_of_two(_tmp); } +template +unsigned mpq_manager::next_power_of_two(mpq const & a) { + _scoped_numeral > _tmp(*this); + ceil(a, _tmp); + return next_power_of_two(_tmp); +} template template diff --git a/src/util/mpq.h b/src/util/mpq.h index e254ade69..1bdf8f31b 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -848,6 +848,14 @@ public: unsigned prev_power_of_two(mpz const & a) { return mpz_manager::prev_power_of_two(a); } unsigned prev_power_of_two(mpq const & a); + /** + \brief Return the smallest k s.t. a <= 2^k. + + \remark Return 0 if a is not positive. + */ + unsigned next_power_of_two(mpz const & a) { return mpz_manager::next_power_of_two(a); } + unsigned next_power_of_two(mpq const & a); + bool is_int_perfect_square(mpq const & a, mpq & r) { SASSERT(is_int(a)); reset_denominator(r); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index c3ba30161..296b4426e 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -2288,6 +2288,19 @@ unsigned mpz_manager::bitsize(mpz const & a) { return mlog2(a) + 1; } +template +unsigned mpz_manager::next_power_of_two(mpz const & a) { + if (is_nonpos(a)) + return 0; + if (is_one(a)) + return 0; + unsigned shift; + if (is_power_of_two(a, shift)) + return shift; + else + return log2(a) + 1; +} + template bool mpz_manager::is_perfect_square(mpz const & a, mpz & root) { if (is_neg(a)) diff --git a/src/util/mpz.h b/src/util/mpz.h index a1bb19395..bb1141ea7 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -692,6 +692,13 @@ public: \remark Return 0 if a is not positive. */ unsigned prev_power_of_two(mpz const & a) { return log2(a); } + + /** + \brief Return the smallest k s.t. a <= 2^k. + + \remark Return 0 if a is not positive. + */ + unsigned next_power_of_two(mpz const & a); /** \brief Return true if a^{1/n} is an integer, and store the result in a. diff --git a/src/util/rational.h b/src/util/rational.h index f47fddefe..88a0552ba 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -55,7 +55,7 @@ public: explicit rational(double z) { UNREACHABLE(); } explicit rational(char const * v) { m().set(m_val, v); } - + explicit rational(unsigned const * v, unsigned sz) { m().set(m_val, sz, v); } struct i64 {}; @@ -489,6 +489,18 @@ public: return get_num_digits(rational(10)); } + /** + * \brief Return the biggest k s.t. 2^k <= a. + * \remark Return 0 if a is not positive. + */ + unsigned prev_power_of_two() const { return m().prev_power_of_two(m_val); } + + /** + * \brief Return the smallest k s.t. a <= 2^k. + * \remark Return 0 if a is not positive. + */ + unsigned next_power_of_two() const { return m().next_power_of_two(m_val); } + bool get_bit(unsigned index) const { return m().get_bit(m_val, index); } @@ -501,6 +513,15 @@ public: return k; } + /** Number of trailing zeros in an N-bit representation */ + unsigned parity(unsigned num_bits) const { + SASSERT(!is_neg()); + SASSERT(*this < rational::power_of_two(num_bits)); + if (is_zero()) + return num_bits; + return trailing_zeros(); + } + static bool limit_denominator(rational &num, rational const& limit); }; @@ -649,3 +670,7 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val); return result; } + +inline void swap(rational& r1, rational& r2) { + r1.swap(r2); +} From 70d4f32ffd56b2508bb2c2ae8bc37a8452561d5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Dec 2023 13:00:43 -0800 Subject: [PATCH 35/39] port updates from poly/polysat Signed-off-by: Nikolaj Bjorner --- src/util/dlist.h | 10 ++++++++++ src/util/var_queue.h | 2 ++ 2 files changed, 12 insertions(+) diff --git a/src/util/dlist.h b/src/util/dlist.h index e5c95b8cf..07aefa97e 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -223,6 +223,16 @@ public: } }; +template +class dll_elements { + T const* m_list; +public: + dll_elements(T const* list) : m_list(list) {} + dll_iterator begin() const { return dll_iterator::mk_begin(m_list); } + dll_iterator end() const { return dll_iterator::mk_end(m_list); } +}; + + template < typename T , typename U = std::enable_if_t, T>> // should only match if T actually inherits from dll_base > diff --git a/src/util/var_queue.h b/src/util/var_queue.h index 9807e5ac2..0af4de3b8 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -68,6 +68,8 @@ public: void reset() { m_queue.reset(); } + + bool contains(var v) const { return m_queue.contains(v); } bool empty() const { return m_queue.empty(); } From 91837c3aeeafb5a0d1c4a7e3225f572f99d17e39 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 10:22:35 -0800 Subject: [PATCH 36/39] try adding readme again Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index ef41051d8..8e67bd65e 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -149,7 +149,7 @@ class Env: unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) mk_icon(self.source_root) -# mk_readme(self.source_root) + mk_readme(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) def main(): From 5732c3c98031e51eb803839b637f5aba4aed25a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 11:11:37 -0800 Subject: [PATCH 37/39] add readme under content Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 8e67bd65e..fe06bdba2 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -91,7 +91,7 @@ def mk_icon(source_root): def mk_readme(source_root): mk_dir("out/content") - shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/README.md") + shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") @@ -112,6 +112,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg + content/README>md https://github.com/Z3Prover/z3 MIT @@ -121,6 +122,9 @@ Linux Dependencies: + + + """.format(version, repo, branch, commit, arch) print(contents) sym = "sym." if symbols else "" From 5fc039d6ea60e12bb319fa01c4b76e9818949596 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 12:33:29 -0800 Subject: [PATCH 38/39] nuget spec: does this work? Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index fe06bdba2..5e6d3e039 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -88,9 +88,6 @@ def mk_targets(source_root): def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") - -def mk_readme(source_root): - mk_dir("out/content") shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") @@ -124,6 +121,7 @@ Linux Dependencies: + """.format(version, repo, branch, commit, arch) print(contents) @@ -153,7 +151,6 @@ class Env: unpack(self.packages, self.symbols, self.arch) mk_targets(self.source_root) mk_icon(self.source_root) - mk_readme(self.source_root) create_nuget_spec(self.version, self.repo, self.branch, self.commit, self.symbols, self.arch) def main(): From 0f4e96ac5d76bbf860ee80a6d0943e0a5589db1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Dec 2023 20:50:32 -0800 Subject: [PATCH 39/39] fix character Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 5e6d3e039..d3f402773 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -109,7 +109,7 @@ Linux Dependencies: © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/README>md + content/README.md https://github.com/Z3Prover/z3 MIT