From 4867073290378ec4a31eb06b4df507c815a12473 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Dec 2023 10:04:49 -0800 Subject: [PATCH] remove windowsArm64 from nightly Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 45 ------------------------ src/ast/rewriter/arith_rewriter.cpp | 2 +- src/sat/smt/arith_axioms.cpp | 17 +++++++-- src/sat/smt/euf_model.cpp | 2 +- src/sat/smt/intblast_solver.cpp | 53 +++++++++++++++-------------- src/sat/smt/intblast_solver.h | 2 ++ 6 files changed, 47 insertions(+), 74 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 0f533765409..5c1bdff6ae8 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -233,46 +233,6 @@ stages: symbolServerType: TeamServices detailedLog: true - - job: "WindowsArm64" - displayName: "WindowsArm64" - pool: - vmImage: "windows-latest" - variables: - arch: "amd64_arm64" - bindings: "-DCMAKE_BUILD_TYPE=RelWithDebInfo" - steps: - - script: md build - - script: | - cd build - call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch) - cmake $(bindings) -G "NMake Makefiles" ../ - nmake - cd .. - - task: CopyFiles@2 - inputs: - sourceFolder: build - contents: '*z3*.*' - targetFolder: $(Build.ArtifactStagingDirectory) - - task: PublishPipelineArtifact@1 - inputs: - targetPath: $(Build.ArtifactStagingDirectory) - artifactName: 'WindowsArm64' - - task: CopyFiles@2 - displayName: 'Collect Symbols' - inputs: - sourceFolder: build - contents: '**/*.pdb' - targetFolder: '$(Build.ArtifactStagingDirectory)/symbols' - # Publish symbol archive to match nuget package - # Index your source code and publish symbols to a file share or Azure Artifacts symbol server - - task: PublishSymbols@2 - inputs: - symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols' - searchPattern: '**/*.pdb' - indexSources: false # Github not supported - publishSymbols: true - symbolServerType: TeamServices - detailedLog: true - stage: Package @@ -576,11 +536,6 @@ stages: inputs: artifactName: 'Windows32' targetPath: tmp - - task: DownloadPipelineArtifact@2 - displayName: "Download windowsArm64" - inputs: - artifactName: 'WindowsArm64' - targetPath: tmp - task: DownloadPipelineArtifact@2 displayName: "Download windows64" inputs: diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d8a06ada65b..13e50da4a4b 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1435,7 +1435,7 @@ br_status arith_rewriter::mk_lshr_core(unsigned sz, expr* arg1, expr* arg2, expr } if (is_num_x && is_num_y) { if (y >= sz) - result = m_util.mk_int(N-1); + result = m_util.mk_int(0); else { rational d = div(x, rational::power_of_two(y.get_unsigned())); result = m_util.mk_int(d); diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index ae67783ebd8..20bc7826057 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -260,6 +260,9 @@ namespace arith { if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + rational r = mod(valx * rational::power_of_two(k), N); + if (r == valn) + return true; sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N))); if (s().value(eq) == l_true) return true; @@ -272,6 +275,9 @@ namespace arith { if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + rational r = mod(div(valx, rational::power_of_two(k)), N); + if (r == valn) + return true; sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k)))); if (s().value(eq) == l_true) return true; @@ -284,6 +290,12 @@ namespace arith { if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + bool signvalx = x >= N/2; + rational valxdiv2k = div(valx, rational::power_of_two(k)); + if (signvalx) + valxdiv2k = mod(valxdiv2k - rational::power_of_two(sz - k), N); + if (valn == valxdiv2k) + return true; sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); sat::literal eq; expr* xdiv2k; @@ -335,9 +347,10 @@ namespace arith { expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); + add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); + add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); + if (a.is_band(n)) { - add_clause(mk_literal(a.mk_ge(n, a.mk_int(0)))); - add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1)))); add_clause(mk_literal(a.mk_le(n, x))); add_clause(mk_literal(a.mk_le(n, y))); } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 073d164be79..2035e16b643 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -282,7 +282,7 @@ namespace euf { } void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) { - out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n"; + out << "Failed to validate b" << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n"; s().display(out); euf::enode_vector nodes; nodes.push_back(n); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index fed43e2173c..55ab4846cbe 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -148,7 +148,7 @@ namespace intblast { auto a = expr2literal(e); auto b = mk_literal(r); ctx.mark_relevant(b); -// verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; + // verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n"; add_equiv(a, b); } return true; @@ -305,28 +305,6 @@ namespace intblast { sorted.push_back(arg); } } - - // - // Add ground equalities to ensure the model is valid with respect to the current case splits. - // This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal - // assignment from complete level. - // E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment. - // If intblast is SAT, then force the model and literal assignment on the rest of the literals. - // - if (!is_ground(e)) - continue; - euf::enode* n = ctx.get_enode(e); - if (!n) - continue; - if (n == n->get_root()) - continue; - expr* r = n->get_root()->get_expr(); - es.push_back(m.mk_eq(e, r)); - r = es.back(); - if (!visited.is_marked(r) && !is_translated(r)) { - visited.mark(r); - sorted.push_back(r); - } } else if (is_quantifier(e)) { quantifier* q = to_quantifier(e); @@ -646,7 +624,7 @@ namespace intblast { } case OP_BUDIV: case OP_BUDIV_I: { - expr* x = arg(0), * y = umod(e, 1); + expr* x = umod(e, 0), * y = umod(e, 1); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y)); break; } @@ -978,13 +956,38 @@ namespace intblast { arith::arith_value av(ctx); rational r; VERIFY(av.get_value(b2i->get_expr(), r)); - verbose_stream() << ctx.bpp(n) << " := " << r << "\n"; value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr())); + verbose_stream() << ctx.bpp(n) << " := " << value << "\n"; } values.set(n->get_root_id(), value); TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); } + void solver::finalize_model(model& mdl) { + for (auto n : ctx.get_egraph().nodes()) { + expr* e = n->get_expr(); + if (!bv.is_bv(e)) + continue; + if (!is_translated(e)) + continue; + expr* f = translated(e); + rational r1, r2; + expr_ref val1 = mdl(e); + expr_ref val2 = mdl(f); + if (bv.is_numeral(val1, r1) && a.is_numeral(val2, r2) && r1 != r2) { + rational N = rational::power_of_two(bv.get_bv_size(e)); + r2 = mod(r2, N); + if (r1 == r2) + continue; + verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n"; + verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n"; + for (expr* arg : *to_app(e)) { + verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n"; + } + } + } + } + sat::literal_vector const& solver::unsat_core() { return m_core; } diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index d59dac9355f..1739fc09bbf 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -108,6 +108,8 @@ namespace intblast { bool add_dep(euf::enode* n, top_sort& dep) override; + void finalize_model(model& mdl) override; + std::ostream& display(std::ostream& out) const override; void collect_statistics(statistics& st) const override;