From c2e73a6aaee3ec5a3cd5758046c14fedefc97e95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2023 15:19:28 -0700 Subject: [PATCH 01/17] logging pre-processing Signed-off-by: Nikolaj Bjorner --- src/solver/simplifier_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index d70d232e4..0c4c2a7b6 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -110,12 +110,13 @@ class simplifier_solver : public solver { expr_ref_vector orig_assumptions(assumptions); m_core_replace.reset(); if (qhead < m_fmls.size() || !assumptions.empty()) { - TRACE("solver", tout << "qhead " << qhead << "\n"); m_preprocess_state.replay(qhead, assumptions); m_preprocess_state.freeze(assumptions); m_preprocess.reduce(); if (!m.inc()) return; + TRACE("solver", tout << "qhead " << qhead << "\n"; + m_preprocess_state.display(tout)); m_preprocess_state.advance_qhead(); for (unsigned i = 0; i < assumptions.size(); ++i) m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); From 99239068baec84c16acb231182341ff1633e46ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2023 15:21:49 -0700 Subject: [PATCH 02/17] some template instantiations #6869 Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/elim_term_ite.cpp | 2 ++ src/ast/rewriter/rewriter.cpp | 5 +++++ 2 files changed, 7 insertions(+) diff --git a/src/ast/normal_forms/elim_term_ite.cpp b/src/ast/normal_forms/elim_term_ite.cpp index 3376e9dda..077f66d1f 100644 --- a/src/ast/normal_forms/elim_term_ite.cpp +++ b/src/ast/normal_forms/elim_term_ite.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/normal_forms/elim_term_ite.h" #include "ast/ast_smt2_pp.h" +#include "ast/rewriter/rewriter_def.h" br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) { if (!m.is_term_ite(f)) { @@ -38,3 +39,4 @@ br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* return BR_DONE; } +template class rewriter_tpl; diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp index 3b25b9409..51c4764df 100644 --- a/src/ast/rewriter/rewriter.cpp +++ b/src/ast/rewriter/rewriter.cpp @@ -17,6 +17,8 @@ Notes: --*/ #include "ast/rewriter/rewriter_def.h" +#include "ast/rewriter/push_app_ite.h" +#include "ast/rewriter/elim_bounds.h" #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" #include "ast/ast_smt2_pp.h" @@ -417,3 +419,6 @@ void inv_var_shifter::process_var(var * v) { } template class rewriter_tpl; +template class rewriter_tpl; +template class rewriter_tpl; +template class rewriter_tpl; From 4d9af7848dcbb51293ba3002875b3e63c4c5733b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2023 15:27:37 -0700 Subject: [PATCH 03/17] add parameter to disable pattern inference #6884 Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/pattern_inference.cpp | 9 +++++---- src/params/pattern_inference_params.cpp | 2 ++ src/params/pattern_inference_params.h | 11 +++++------ src/params/pattern_inference_params_helper.pyg | 1 + 4 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 4391d8bf8..7c7576c84 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -624,9 +624,11 @@ bool pattern_inference_cfg::reduce_quantifier( proof_ref & result_pr) { TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";); - if (!is_forall(q)) { + if (!m_params.m_pi_enabled) + return false; + + if (!is_forall(q)) return false; - } int weight = q->get_weight(); @@ -653,9 +655,8 @@ bool pattern_inference_cfg::reduce_quantifier( } } - if (q->get_num_patterns() > 0) { + if (q->get_num_patterns() > 0) return false; - } if (m_params.m_pi_nopat_weight >= 0) weight = m_params.m_pi_nopat_weight; diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp index aac574c6e..0e548c896 100644 --- a/src/params/pattern_inference_params.cpp +++ b/src/params/pattern_inference_params.cpp @@ -21,6 +21,7 @@ Revision History: void pattern_inference_params::updt_params(params_ref const & _p) { pattern_inference_params_helper p(_p); + m_pi_enabled = p.enabled(); m_pi_max_multi_patterns = p.max_multi_patterns(); m_pi_block_loop_patterns = p.block_loop_patterns(); m_pi_decompose_patterns = p.decompose_patterns(); @@ -35,6 +36,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) { #define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void pattern_inference_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_pi_enabled); DISPLAY_PARAM(m_pi_max_multi_patterns); DISPLAY_PARAM(m_pi_block_loop_patterns); DISPLAY_PARAM(m_pi_decompose_patterns); diff --git a/src/params/pattern_inference_params.h b/src/params/pattern_inference_params.h index b037411ec..e558a6a7b 100644 --- a/src/params/pattern_inference_params.h +++ b/src/params/pattern_inference_params.h @@ -27,7 +27,8 @@ enum arith_pattern_inference_kind { }; struct pattern_inference_params { - unsigned m_pi_max_multi_patterns; + bool m_pi_enabled = true; + unsigned m_pi_max_multi_patterns = 1; bool m_pi_block_loop_patterns; bool m_pi_decompose_patterns; arith_pattern_inference_kind m_pi_arith; @@ -35,13 +36,11 @@ struct pattern_inference_params { unsigned m_pi_arith_weight; unsigned m_pi_non_nested_arith_weight; bool m_pi_pull_quantifiers; - int m_pi_nopat_weight; - bool m_pi_avoid_skolems; + int m_pi_nopat_weight = -1; + bool m_pi_avoid_skolems = true; bool m_pi_warnings; - pattern_inference_params(params_ref const & p = params_ref()): - m_pi_nopat_weight(-1), - m_pi_avoid_skolems(true) { + pattern_inference_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg index cb1f02877..80d36e3ec 100644 --- a/src/params/pattern_inference_params_helper.pyg +++ b/src/params/pattern_inference_params_helper.pyg @@ -7,6 +7,7 @@ def_module_params(class_name='pattern_inference_params_helper', ('decompose_patterns', BOOL, True, 'allow decomposition of patterns into multipatterns'), ('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'), ('use_database', BOOL, False, 'use pattern database'), + ('enabled', BOOL, True, 'enable a heuristic to infer patterns, when they are not provided'), ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'), ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'), ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'), From 3aea4ebf42dd2b26261657e9a4823f91f9b3e736 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 5 Sep 2023 16:58:47 -0700 Subject: [PATCH 04/17] Bump actions/checkout from 3 to 4 (#6888) Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to 4. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](https://github.com/actions/checkout/compare/v3...v4) --- updated-dependencies: - dependency-name: actions/checkout dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/android-build.yml | 2 +- .github/workflows/coverage.yml | 2 +- .github/workflows/cross-build.yml | 2 +- .github/workflows/docker-image.yml | 2 +- .github/workflows/msvc-static-build.yml | 2 +- .github/workflows/wasm-release.yml | 2 +- .github/workflows/wasm.yml | 2 +- .github/workflows/wip.yml | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/android-build.yml b/.github/workflows/android-build.yml index 019eb18b1..8a6a32c6b 100644 --- a/.github/workflows/android-build.yml +++ b/.github/workflows/android-build.yml @@ -21,7 +21,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Configure CMake and build run: | diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 366a2224e..2ed02aab1 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -21,7 +21,7 @@ jobs: COV_DETAILS_PATH: ${{github.workspace}}/cov-details steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Setup run: | diff --git a/.github/workflows/cross-build.yml b/.github/workflows/cross-build.yml index 83fae7a5d..8745215d2 100644 --- a/.github/workflows/cross-build.yml +++ b/.github/workflows/cross-build.yml @@ -19,7 +19,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Install cross build tools run: apt update && apt install -y ninja-build cmake python3 g++-11-${{ matrix.arch }}-linux-gnu diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 301ee2c87..583e36034 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -15,7 +15,7 @@ jobs: steps: - name: Check out the repo - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Log in to GitHub Docker registry uses: docker/login-action@v2 diff --git a/.github/workflows/msvc-static-build.yml b/.github/workflows/msvc-static-build.yml index 2db222161..b329d5abc 100644 --- a/.github/workflows/msvc-static-build.yml +++ b/.github/workflows/msvc-static-build.yml @@ -14,7 +14,7 @@ jobs: BUILD_TYPE: Release steps: - name: Checkout Repo - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Build run: | diff --git a/.github/workflows/wasm-release.yml b/.github/workflows/wasm-release.yml index de15a242c..defcd8fea 100644 --- a/.github/workflows/wasm-release.yml +++ b/.github/workflows/wasm-release.yml @@ -21,7 +21,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup node uses: actions/setup-node@v3 diff --git a/.github/workflows/wasm.yml b/.github/workflows/wasm.yml index e8ac095e5..9e321947e 100644 --- a/.github/workflows/wasm.yml +++ b/.github/workflows/wasm.yml @@ -21,7 +21,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup node uses: actions/setup-node@v3 diff --git a/.github/workflows/wip.yml b/.github/workflows/wip.yml index ffea6225c..5ed29a457 100644 --- a/.github/workflows/wip.yml +++ b/.github/workflows/wip.yml @@ -15,7 +15,7 @@ jobs: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Configure CMake run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} From 0a444f357a82f37db5b089bcf90cd91473838795 Mon Sep 17 00:00:00 2001 From: Sijmen Date: Mon, 11 Sep 2023 21:58:03 +0200 Subject: [PATCH 05/17] Slightly improve Z3_LIBRARY_PATH error message (#6895) --- scripts/update_api.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 5f8db1932..c68597ea2 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1887,10 +1887,10 @@ if _lib is None: print(" - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via") if sys.version < '3': print(" import __builtin__") - print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext) + print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] \# directory containing libz3.%s" % _ext) else: print(" import builtins") - print(" builtins.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext) + print(" builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] \# directory containing libz3.%s" % _ext) print(_failures) raise Z3Exception("libz3.%s not found." % _ext) From e718bb64737fac5c4b365919530fca77104560aa Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 12 Sep 2023 08:09:01 +0100 Subject: [PATCH 06/17] Bump docker/build-push-action from 4.1.1 to 4.2.1 (#6896) Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 4.1.1 to 4.2.1. - [Release notes](https://github.com/docker/build-push-action/releases) - [Commits](https://github.com/docker/build-push-action/compare/v4.1.1...v4.2.1) --- updated-dependencies: - dependency-name: docker/build-push-action dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 583e36034..bf8138bec 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -41,7 +41,7 @@ jobs: type=edge type=sha,prefix=ubuntu-20.04-bare-z3-sha- - name: Build and push Bare Z3 Docker Image - uses: docker/build-push-action@v4.1.1 + uses: docker/build-push-action@v4.2.1 with: context: . push: true From 50d76a2fe3373bf840fd2b1ec727bf1aab6ee44c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Sep 2023 16:03:56 -0700 Subject: [PATCH 07/17] fix #6894 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/solve_context_eqs.cpp | 67 +++++++++++++++++++---- src/ast/simplifiers/solve_context_eqs.h | 4 +- 2 files changed, 60 insertions(+), 11 deletions(-) diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index b56802caf..31696dc54 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -243,8 +243,8 @@ namespace euf { void solve_context_eqs::collect_nested_equalities(dependent_expr const& df, expr_mark& visited, dep_eq_vector& eqs) { - svector> todo; - todo.push_back({ false, 0, df.fml()}); + svector> todo; + todo.push_back({ false, 0, df.fml(), 0}); // even depth is conjunctive context, odd is disjunctive // when alternating between conjunctive and disjunctive context, increment depth. @@ -255,37 +255,84 @@ namespace euf { return (0 == depth % 2) ? depth : depth + 1; }; - while (!todo.empty()) { - auto [s, depth, f] = todo.back(); - todo.pop_back(); + for (unsigned i = 0; i < todo.size(); ++i) { + auto [s, depth, f, p] = todo[i]; if (visited.is_marked(f)) continue; visited.mark(f, true); if (s && m.is_and(f)) { for (auto* arg : *to_app(f)) - todo.push_back({ s, inc_or(depth), arg }); + todo.push_back({ s, inc_or(depth), arg, i }); } else if (!s && m.is_or(f)) { for (auto* arg : *to_app(f)) - todo.push_back({ s, inc_or(depth), arg }); + todo.push_back({ s, inc_or(depth), arg, i }); } if (!s && m.is_and(f)) { for (auto* arg : *to_app(f)) - todo.push_back({ s, inc_and(depth), arg }); + todo.push_back({ s, inc_and(depth), arg, i }); } else if (s && m.is_or(f)) { for (auto* arg : *to_app(f)) - todo.push_back({ s, inc_and(depth), arg }); + todo.push_back({ s, inc_and(depth), arg, i }); } else if (m.is_not(f, f)) - todo.push_back({ !s, depth, f }); + todo.push_back({ !s, depth, f, i }); else if (!s && 1 <= depth) { + unsigned sz = eqs.size(); for (extract_eq* ex : m_solve_eqs.m_extract_plugins) { ex->set_allow_booleans(false); ex->get_eqs(dependent_expr(m, f, nullptr, df.dep()), eqs); ex->set_allow_booleans(true); } + // prune eqs for solutions that are not safe in df.fml() + for (; sz < eqs.size(); ++sz) { + if (!is_safe_var(eqs[sz].var, i, df.fml(), todo)) { + eqs[sz] = eqs.back(); + --sz; + eqs.pop_back(); + } + } } } } + + bool solve_context_eqs::is_safe_var(expr* x, unsigned i, expr* f, svector> const& todo) { + m_contains_v.reset(); + m_todo.push_back(f); + mark_occurs(m_todo, x, m_contains_v); + SASSERT(m_todo.empty()); + + auto is_parent = [&](unsigned p, unsigned i) { + while (p != i && i != 0) { + auto [_s,_depth, _f, _p] = todo[i]; + i = _p; + } + return p == i; + }; + + // retrieve oldest parent of i whose sign is false + unsigned pi = i; + while (pi != 0) { + auto [s, depth, f, p] = todo[pi]; + if (s) + break; + pi = p; + } + + // determine if j and j have common conjunctive parent + // for every j in todo. + for (unsigned j = 0; j < todo.size(); ++j) { + auto [s, depth, f, p] = todo[j]; + if (i == j || !m_contains_v.is_marked(f)) + continue; + if (is_parent(j, i)) // j is a parent if i + continue; + if (is_parent(pi, j)) // pi is a parent of j + continue; + return false; + } + return true; + } + } diff --git a/src/ast/simplifiers/solve_context_eqs.h b/src/ast/simplifiers/solve_context_eqs.h index 8332d3a73..a11a1043b 100644 --- a/src/ast/simplifiers/solve_context_eqs.h +++ b/src/ast/simplifiers/solve_context_eqs.h @@ -45,7 +45,9 @@ namespace euf { bool contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts); bool is_conjunction(bool sign, expr* f) const; - void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs); + void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs); + + bool is_safe_var(expr* x, unsigned i, expr* f, svector> const& todo); public: From b87a91379ce6ac5d71dc5b46805e0df77b90219c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Sep 2023 17:10:53 -0700 Subject: [PATCH 08/17] fix #6894 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/solve_context_eqs.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index 31696dc54..c58786f0e 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -311,11 +311,12 @@ namespace euf { return p == i; }; - // retrieve oldest parent of i whose sign is false + // retrieve oldest parent of i within the same alternation of and unsigned pi = i; + auto [_s, _depth, _f, _p] = todo[i]; while (pi != 0) { auto [s, depth, f, p] = todo[pi]; - if (s) + if (depth != _depth) break; pi = p; } From ff33fa355a33aeff4c559f63232325979f395b71 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 18 Sep 2023 09:44:37 +0100 Subject: [PATCH 09/17] fix debug single-thread build --- src/api/api_context.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 2b7a4ce43..53f53347e 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -157,6 +157,9 @@ namespace api { flush_objects(); for (auto& kv : m_allocated_objects) { api::object* val = kv.m_value; +#ifdef SINGLE_THREAD +# define m_concurrent_dec_ref false +#endif DEBUG_CODE(if (!m_concurrent_dec_ref) warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name());); dealloc(val); } From b1c52c0b16906f4d835261b672c80905b396456a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 18 Sep 2023 10:16:19 +0100 Subject: [PATCH 10/17] don't crash when a function doesn't have a model when converting a solver to string --- src/ast/converters/model_converter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/converters/model_converter.cpp b/src/ast/converters/model_converter.cpp index 716970cba..d053394ca 100644 --- a/src/ast/converters/model_converter.cpp +++ b/src/ast/converters/model_converter.cpp @@ -24,7 +24,8 @@ Notes: * Add or overwrite value in model. */ void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) { - VERIFY(e); + if (!e) + return; VERIFY(f->get_range() == e->get_sort()); ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n"; } From 858477f3e3dcec52409846b95e291e5612dc41b8 Mon Sep 17 00:00:00 2001 From: John Fleisher Date: Mon, 18 Sep 2023 12:03:56 -0400 Subject: [PATCH 11/17] Add c++ flags for vulcan assembly compliance (#6906) --- scripts/mk_util.py | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 74d585dae..3d3996792 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2519,19 +2519,19 @@ def mk_config(): 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( - 'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt)) + 'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) + 'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) elif VS_ARM: print("ARM on VS is unsupported") exit(1) else: config.write( - 'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt)) + 'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) + 'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) else: # Windows Release mode LTCG=' /LTCG' if SLOW_OPTIMIZE else '' @@ -2544,19 +2544,19 @@ def mk_config(): extra_opt = '%s /D _TRACE ' % extra_opt if VS_X64: config.write( - 'CXXFLAGS=/c%s %s /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt)) + 'CXXFLAGS=/c%s %s /Zi /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n' - 'SLINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) + 'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n' + 'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) elif VS_ARM: print("ARM on VS is unsupported") exit(1) else: config.write( - 'CXXFLAGS=/c%s %s /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt)) + 'CXXFLAGS=/c%s %s /Zi /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' - 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt)) + 'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt)) config.write('CFLAGS=$(CXXFLAGS)\n') From 31c91e167425989476829d36fe3f9329cadb84d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Sep 2023 12:52:26 -0700 Subject: [PATCH 12/17] #6902 add parse check for identifiers used for datatype declarations. --- src/parsers/smt2/smt2parser.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 5e22d9d29..98323816a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -963,6 +963,7 @@ namespace smt2 { unsigned line = m_scanner.get_line(); unsigned pos = m_scanner.get_pos(); symbol dt_name = curr_id(); + check_identifier("unexpected token used as datatype name"); next(); m_dt_name2idx.reset(); From 643512613ab696b021892907a4ed0432f020a513 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Sep 2023 12:52:50 -0700 Subject: [PATCH 13/17] simplify last_index function --- src/ast/rewriter/seq_rewriter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 24df51845..90ba5bb3a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1716,6 +1716,10 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) { result = m_autil.mk_numeral(rational(idx), true); return BR_DONE; } + if (a == b) { + result = m_autil.mk_int(0); + return BR_DONE; + } return BR_FAILED; } From 3b78c6318cc803dc397467bdf43694fef34b1885 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 18 Sep 2023 17:48:16 -0700 Subject: [PATCH 14/17] Bump docker/build-push-action from 4.2.1 to 5.0.0 (#6909) Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 4.2.1 to 5.0.0. - [Release notes](https://github.com/docker/build-push-action/releases) - [Commits](https://github.com/docker/build-push-action/compare/v4.2.1...v5.0.0) --- updated-dependencies: - dependency-name: docker/build-push-action dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index bf8138bec..41e47c7de 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -41,7 +41,7 @@ jobs: type=edge type=sha,prefix=ubuntu-20.04-bare-z3-sha- - name: Build and push Bare Z3 Docker Image - uses: docker/build-push-action@v4.2.1 + uses: docker/build-push-action@v5.0.0 with: context: . push: true From 17a38b7ae0bff5010ff4cf7c69ac94bdc4b916a9 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 18 Sep 2023 17:48:35 -0700 Subject: [PATCH 15/17] Bump docker/metadata-action from 4 to 5 (#6910) Bumps [docker/metadata-action](https://github.com/docker/metadata-action) from 4 to 5. - [Release notes](https://github.com/docker/metadata-action/releases) - [Upgrade guide](https://github.com/docker/metadata-action/blob/master/UPGRADE.md) - [Commits](https://github.com/docker/metadata-action/compare/v4...v5) --- updated-dependencies: - dependency-name: docker/metadata-action dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 41e47c7de..67c728b0f 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -29,7 +29,7 @@ jobs: # ------- - name: Extract metadata (tags, labels) for Bare Z3 Docker Image id: meta - uses: docker/metadata-action@v4 + uses: docker/metadata-action@v5 with: images: ghcr.io/z3prover/z3 flavor: | From 345d6ec8a5ec7bfb48ca5b2f20c736440a322c39 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 18 Sep 2023 17:49:00 -0700 Subject: [PATCH 16/17] Bump docker/login-action from 2 to 3 (#6911) Bumps [docker/login-action](https://github.com/docker/login-action) from 2 to 3. - [Release notes](https://github.com/docker/login-action/releases) - [Commits](https://github.com/docker/login-action/compare/v2...v3) --- updated-dependencies: - dependency-name: docker/login-action dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 67c728b0f..82e0c4c0b 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -18,7 +18,7 @@ jobs: uses: actions/checkout@v4 - name: Log in to GitHub Docker registry - uses: docker/login-action@v2 + uses: docker/login-action@v3 with: registry: ghcr.io username: ${{ secrets.DOCKER_USERNAME }} From fba5de3a25afc762e3c060c660b55bb334a675f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2023 14:42:55 -0700 Subject: [PATCH 17/17] remove unused code Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_monotone_lemmas.h | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index d13f588e8..fb9c469a8 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/src/math/lp/nla_monotone_lemmas.h @@ -7,16 +7,14 @@ --*/ #pragma once namespace nla { -class core; -class monotone : common { -public: - monotone(core *core); - void monotonicity_lemma(); -private: - void monotonicity_lemma(monic const& m); - void monotonicity_lemma_gt(const monic& m); - void monotonicity_lemma_lt(const monic& m); - std::vector get_sorted_key(const monic& rm) const; - vector> get_sorted_key_with_rvars(const monic& a) const; -}; + class core; + class monotone : common { + public: + monotone(core *core); + void monotonicity_lemma(); + private: + void monotonicity_lemma(monic const& m); + void monotonicity_lemma_gt(const monic& m); + void monotonicity_lemma_lt(const monic& m); + }; }