From 5351640e9703167c2c2d26d358f9ee9a8b9aa010 Mon Sep 17 00:00:00 2001 From: Brenton Bostick Date: Thu, 18 Nov 2021 13:35:22 -0500 Subject: [PATCH 01/12] Fix stray semicolon in examples (#5669) --- examples/c/test_capi.c | 1 - 1 file changed, 1 deletion(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index a9c472f37..a6fcbdb22 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -561,7 +561,6 @@ void display_ast(Z3_context c, FILE * out, Z3_ast v) } case Z3_QUANTIFIER_AST: { fprintf(out, "quantifier"); - ; } default: fprintf(out, "#unknown"); From 41a5b930b60d083eef50aea953e8c27a8c5d82d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 11:21:51 -0800 Subject: [PATCH 02/12] update release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index dae1e81b8..790691c3d 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,14 +3,18 @@ RELEASE NOTES Version 4.8.next ================ - Planned features - - specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction - - the smtfd solver and tactic implement this strategy, but is not prime for users. + - sat.euf + - a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. + the current state is unstable. It lacks efficient ematching. + - polysat + - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. - - circuit optimization techniques for BV in-processing are available as the sat.cut - option, but at this point does not translate into benefits. It is currently - turned off by default. +Version 4.8.13 +============== +The release integrates various bug fixes and tuning. + Version 4.8.12 ============== Release provided to fix git tag discrepancy issues with 4.8.11 From feadfbfba4642cd81d36c30cb901f605c48712ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 12:00:44 -0800 Subject: [PATCH 03/12] enable publish Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/release.yml b/scripts/release.yml index adba3a8e9..7b989038a 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -309,7 +309,7 @@ stages: jobs: - job: GitHubPublish - condition: eq(1,0) + condition: eq(1,1) displayName: "Publish to GitHub" pool: vmImage: "windows-latest" @@ -387,7 +387,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(0,1) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From b95ba89dbe94f9c3822aaedb7d36e05065420541 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 13:09:13 -0800 Subject: [PATCH 04/12] update release pipeline Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/release.yml b/scripts/release.yml index 7b989038a..faeb2a1c6 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -309,7 +309,7 @@ stages: jobs: - job: GitHubPublish - condition: eq(1,1) + condition: eq(0,1) displayName: "Publish to GitHub" pool: vmImage: "windows-latest" @@ -399,7 +399,7 @@ stages: - task: DownloadSecureFile@1 name: pypirc inputs: - secureFile: 'pypirc' + secureFile: 'pypirc2' - script: python3 -m pip install --upgrade pip - script: python3 -m pip install --user -U setuptools importlib_metadata wheel twine - - script: python3 -m twine upload --config-file $(pypirc.secureFilePath) -r $(pypiReleaseServer) dist/* \ No newline at end of file + - script: python3 -m twine upload --config-file $(pypirc2.secureFilePath) -r $(pypiReleaseServer) dist/* \ No newline at end of file From 72f28f06e4d209c819741b6b97b85e728d9ab923 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 14:05:13 -0800 Subject: [PATCH 05/12] Update release.yml for Azure Pipelines --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index faeb2a1c6..acc647f67 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -402,4 +402,4 @@ stages: secureFile: 'pypirc2' - script: python3 -m pip install --upgrade pip - script: python3 -m pip install --user -U setuptools importlib_metadata wheel twine - - script: python3 -m twine upload --config-file $(pypirc2.secureFilePath) -r $(pypiReleaseServer) dist/* \ No newline at end of file + - script: python3 -m twine upload --config-file $(pypirc2) -r $(pypiReleaseServer) dist/* \ No newline at end of file From 71d5d2486c2894dfce13eda291333c4498100077 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 15:01:43 -0800 Subject: [PATCH 06/12] Update release.yml for Azure Pipelines --- scripts/release.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/release.yml b/scripts/release.yml index acc647f67..2a3d6d7d8 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -399,7 +399,7 @@ stages: - task: DownloadSecureFile@1 name: pypirc inputs: - secureFile: 'pypirc2' + secureFile: 'pypircs' - script: python3 -m pip install --upgrade pip - script: python3 -m pip install --user -U setuptools importlib_metadata wheel twine - - script: python3 -m twine upload --config-file $(pypirc2) -r $(pypiReleaseServer) dist/* \ No newline at end of file + - script: python3 -m twine upload --config-file $(pypircs.secureFilePath) -r $(pypiReleaseServer) dist/* \ No newline at end of file From 43a827c931eb496913eb54e1d5d9837894a88567 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 16:05:22 -0800 Subject: [PATCH 07/12] Update release.yml for Azure Pipelines --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 2a3d6d7d8..9a1982744 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -397,7 +397,7 @@ stages: artifact: 'PythonPackage' path: dist - task: DownloadSecureFile@1 - name: pypirc + name: pypircs inputs: secureFile: 'pypircs' - script: python3 -m pip install --upgrade pip From 4587575649f0f92757eade3bb4eb130569f50307 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 20:25:47 -0800 Subject: [PATCH 08/12] if you read this commit message you probably are a programmer who has no life Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 46cb84ddc..f1ad74181 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.8.13.0 LANGUAGES CXX) +project(Z3 VERSION 4.8.14.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 982ea194e..105c097d4 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, 8, 13, 0) + set_version(4, 8, 14, 0) # Z3 Project definition def init_project_def(): From 518ef9f9166a8aaafa58898b17c151424bfaf0d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 21:14:50 -0800 Subject: [PATCH 09/12] fix #5674 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 1 + src/api/python/z3/z3printer.py | 9 +++++++++ src/api/z3_api.h | 1 + src/ast/ast.h | 6 ++++++ src/ast/seq_decl_plugin.cpp | 11 +++++++++++ src/ast/seq_decl_plugin.h | 2 ++ src/smt/smt_model_generator.cpp | 2 +- 7 files changed, 31 insertions(+), 1 deletion(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 10a98c477..7f67879bc 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1232,6 +1232,7 @@ extern "C" { if (mk_c(c)->get_char_fid() == _d->get_family_id()) { switch (_d->get_decl_kind()) { + case OP_CHAR_CONST: return Z3_OP_CHAR_CONST; case OP_CHAR_LE: return Z3_OP_CHAR_LE; case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT; case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV; diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 7c675cc5b..2bf0675a2 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -770,6 +770,8 @@ class Formatter: return self.pp_set("Empty", a) elif k == Z3_OP_RE_FULL_SET: return self.pp_set("Full", a) + elif k == Z3_OP_CHAR_CONST: + return self.pp_char(a) return self.pp_name(a) def pp_int(self, a): @@ -1060,6 +1062,10 @@ class Formatter: def pp_set(self, id, a): return seq1(id, [self.pp_sort(a.sort())]) + def pp_char(self, a): + n = a.params()[0] + return to_format(str(n)) + def pp_pattern(self, a, d, xs): if a.num_args() == 1: return self.pp_expr(a.arg(0), d, xs) @@ -1151,6 +1157,9 @@ class Formatter: return self.pp_pbcmp(a, d, f, xs) elif k == Z3_OP_PB_EQ: return self.pp_pbcmp(a, d, f, xs) + elif k == Z3_OP_SEQ_UNIT and z3.is_app(a.arg(0)) and a.arg(0).decl().kind() == Z3_OP_CHAR_CONST: + n = a.arg(0).params()[0] + return to_format(f"\"{chr(n)}\"") elif z3.is_pattern(a): return self.pp_pattern(a, d, xs) elif self.is_infix(k): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7d1366329..19ceef7c5 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1222,6 +1222,7 @@ typedef enum { Z3_OP_RE_COMPLEMENT, // char + Z3_OP_CHAR_CONST, Z3_OP_CHAR_LE, Z3_OP_CHAR_TO_INT, Z3_OP_CHAR_TO_BV, diff --git a/src/ast/ast.h b/src/ast/ast.h index 739f63dc8..b04e67003 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1050,6 +1050,12 @@ public: */ virtual bool is_value(app * a) const { return false; } + + /** + \brief return true if the expression can be used as a model value. + */ + virtual bool is_model_value(app* a) const { return is_value(a); } + /** \brief Return true if \c a is a unique plugin value. The following property should hold for unique theory values: diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index ebae138e3..0829aa09f 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -705,6 +705,17 @@ bool seq_decl_plugin::is_value(app* e) const { } } +bool seq_decl_plugin::is_model_value(app* e) const { + if (is_app_of(e, m_family_id, OP_SEQ_EMPTY)) + return true; + if (is_app_of(e, m_family_id, OP_STRING_CONST)) + return true; + if (is_app_of(e, m_family_id, OP_SEQ_UNIT) && + m_manager->is_value(e->get_arg(0))) + return true; + return false; +} + bool seq_decl_plugin::are_equal(app* a, app* b) const { if (a == b) return true; // handle concatenations diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index f194e6a67..09a10ee9a 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -179,6 +179,8 @@ public: bool is_value(app * e) const override; + bool is_model_value(app* e) const override; + bool is_unique_value(app * e) const override; bool are_equal(app* a, app* b) const override; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index dcdb9a198..73d8cad9d 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -105,7 +105,7 @@ namespace smt { else proc = alloc(expr_wrapper_proc, m.mk_false()); } - else if (m.is_value(r->get_expr())) + else if (m.is_model_value(r->get_expr())) proc = alloc(expr_wrapper_proc, r->get_expr()); else { family_id fid = s->get_family_id(); From f83367a11ec852a5e48da4992140bdc819961538 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 22:39:30 -0800 Subject: [PATCH 10/12] mac builds Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3printer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 2bf0675a2..7972431dd 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -1159,7 +1159,7 @@ class Formatter: return self.pp_pbcmp(a, d, f, xs) elif k == Z3_OP_SEQ_UNIT and z3.is_app(a.arg(0)) and a.arg(0).decl().kind() == Z3_OP_CHAR_CONST: n = a.arg(0).params()[0] - return to_format(f"\"{chr(n)}\"") + return to_format("\"" + f"{chr(n)}" + "\"") elif z3.is_pattern(a): return self.pp_pattern(a, d, xs) elif self.is_infix(k): From 99d5215956fc8bd52bb4cc91bca829a2a8761a21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Nov 2021 00:01:19 -0800 Subject: [PATCH 11/12] revert use of f format Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3printer.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 7972431dd..228f212d9 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -1157,9 +1157,6 @@ class Formatter: return self.pp_pbcmp(a, d, f, xs) elif k == Z3_OP_PB_EQ: return self.pp_pbcmp(a, d, f, xs) - elif k == Z3_OP_SEQ_UNIT and z3.is_app(a.arg(0)) and a.arg(0).decl().kind() == Z3_OP_CHAR_CONST: - n = a.arg(0).params()[0] - return to_format("\"" + f"{chr(n)}" + "\"") elif z3.is_pattern(a): return self.pp_pattern(a, d, xs) elif self.is_infix(k): From 4928c28e63e0d3844ed08f4d6dc3bdc3c344856b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Nov 2021 08:42:32 -0800 Subject: [PATCH 12/12] fix #5675 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4931c9900..e89508b1c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3477,7 +3477,7 @@ public: st = lp::lp_status::FEASIBLE; lp().restore_x(); } - if (m_nla && st == lp::lp_status::OPTIMAL) { + if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) { st = lp::lp_status::FEASIBLE; lp().restore_x(); }