remove windowsArm64 from nightly

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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:

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);

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)));
         }

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);

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;
     }

src/sat/smt/intblast_solver.h

@@ -108,6 +108,8 @@ namespace intblast {
 
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
 
+        void finalize_model(model& mdl) override;
+
         std::ostream& display(std::ostream& out) const override;
 
         void collect_statistics(statistics& st) const override;