From c2e73a6aaee3ec5a3cd5758046c14fedefc97e95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Sep 2023 15:19:28 -0700 Subject: [PATCH 01/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] #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/20] 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/20] 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/20] 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/20] 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 85db8163fa6a9e9c99c15899a306d59e20be9b6c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2023 13:57:28 -0700 Subject: [PATCH 17/20] move allocator to memory_manager and std_vector to vector Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_bound_propagator.h | 23 ++++++----------------- src/math/lp/nla_monotone_lemmas.h | 2 +- src/util/memory_manager.h | 13 +++++++++++++ src/util/vector.h | 3 +++ 4 files changed, 23 insertions(+), 18 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 6a01d4ace..d035d9bcb 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -9,29 +9,18 @@ #include "math/lp/lp_settings.h" #include "util/uint_set.h" #include "math/lp/implied_bound.h" -#include +#include "util/vector.h" namespace lp { -template -struct my_allocator { - using value_type = T; - - T* allocate(std::size_t n) { - return static_cast(memory::allocate(n * sizeof(T))); - } - - void deallocate(T* p, std::size_t n) { - memory::deallocate(p); - } -}; + template class lp_bound_propagator { - uint_set m_visited_rows; + uint_set m_visited_rows; // these maps map a column index to the corresponding index in ibounds u_map m_improved_lower_bounds; u_map m_improved_upper_bounds; T& m_imp; - std::vector> m_ibounds; + std_vector m_ibounds; map, default_eq> m_val2fixed_row; // works for rows of the form x + y + sum of fixed = 0 @@ -119,10 +108,10 @@ private: ~reset_cheap_eq() { p.reset_cheap_eq_eh(); } }; - public: +public: lp_bound_propagator(T& imp) : m_imp(imp) {} - const std::vector>& ibounds() const { return m_ibounds; } + const std_vector& ibounds() const { return m_ibounds; } void init() { m_improved_upper_bounds.reset(); diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index d13f588e8..2cb646777 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/src/math/lp/nla_monotone_lemmas.h @@ -16,7 +16,7 @@ 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; + // std_vector get_sorted_key(const monic& rm) const; vector> get_sorted_key_with_rvars(const monic& a) const; }; } diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 7dab520df..053816449 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -128,6 +128,19 @@ void dealloc_svect(T * ptr) { memory::deallocate(ptr); } +template +struct std_allocator { + using value_type = T; + + T* allocate(std::size_t n) { + return static_cast(memory::allocate(n * sizeof(T))); + } + + void deallocate(T* p, std::size_t n) { + memory::deallocate(p); + } +}; + struct mem_stat { }; diff --git a/src/util/vector.h b/src/util/vector.h index 1cb25a8c4..9ca9a1103 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -33,6 +33,7 @@ Revision History: #include "util/memory_manager.h" #include "util/hash.h" #include "util/z3_exception.h" +#include // disable warning for constant 'if' expressions. // these are used heavily in templates. @@ -40,6 +41,8 @@ Revision History: #pragma warning(disable:4127) #endif +template +class std_vector : public std::vector> {}; #if 0 From 4d742001ab4d871e2929224d4f7649bd20d20667 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2023 14:36:21 -0700 Subject: [PATCH 18/20] formatting of else Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index fa73788e6..9357b7a65 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2176,7 +2176,8 @@ public: if (is_infeasible()) { get_infeasibility_explanation_and_set_conflict(); // verbose_stream() << "unsat\n"; - } else { + } + else { for (auto &ib : m_bp.ibounds()) { m.inc(); if (ctx().inconsistent()) From fba5de3a25afc762e3c060c660b55bb334a675f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2023 14:42:55 -0700 Subject: [PATCH 19/20] 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); + }; } From f07553ed3a2ca03c69b0a60b13671a579b7313b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2023 15:18:38 -0700 Subject: [PATCH 20/20] formatting updates Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_bound_propagator.h | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index d035d9bcb..8af04c793 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -181,13 +181,12 @@ public: void propagate_monic(lpvar monic_var, const svector& vars) { lpvar non_fixed, zero_var; - if (!is_linear(vars, zero_var, non_fixed)) { - return; - } + if (!is_linear(vars, zero_var, non_fixed)) + return; - if (zero_var != null_lpvar) { + if (zero_var != null_lpvar) add_bounds_for_zero_var(monic_var, zero_var); - } else { + else { rational k = rational(1); for (auto v : vars) if (v != non_fixed) { @@ -195,19 +194,18 @@ public: if (k.is_big()) return; } - if (non_fixed != null_lpvar) { + if (non_fixed != null_lpvar) propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k); - } else { // all variables are fixed + else // all variables are fixed propagate_monic_with_all_fixed(monic_var, vars, k); - } } } void propagate_monic_with_non_fixed(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k) { - lp::impq bound_value; - bool is_strict; + lp::impq bound_value; + bool is_strict; - if (lower_bound_is_available(non_fixed)) { + if (lower_bound_is_available(non_fixed)) { bound_value = lp().column_lower_bound(non_fixed); is_strict = !bound_value.y.is_zero(); auto lambda = [vars, non_fixed](int* s) {