install importlib-resources for ubuntu doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 4, 2023 · f7415bb · f7415bb
1 parent 17913f3
commit f7415bb
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 17 deletions.
diff --git a/scripts/release.yml b/scripts/release.yml
@@ -133,6 +133,7 @@ stages:
     pool:
       vmImage: "ubuntu-latest"
     steps:
+    - script: pip3 install importlib-resources
     - script: sudo apt-get install ocaml opam libgmp-dev
     - script: opam init -y
     - script: eval `opam config env`; opam install zarith ocamlfind -y

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
@@ -399,7 +399,7 @@ namespace nla {
         for (auto eq : m_solver.equations()) 
             if (propagate_linear_equations(*eq))
                 ++changed;
-#if 0
+#if 1
         for (auto eq : m_solver.equations()) 
             if (check_missed_bound(*eq))
                 return true;
@@ -419,22 +419,24 @@ namespace nla {
             if (vars.empty())
                 di.add(coeff, i);
             else {
-                di.set_value(t, rational::one());
+                di.set_value(t, coeff);
                 for (auto v : vars) {
                     set_var_interval(v, s);
-                    di.mul<dd::w_dep::with_deps>(coeff, s, s);
-                    di.add<dd::w_dep::with_deps>(t, s, t);
+                    di.mul<dd::w_dep::with_deps>(t, s, t);
                 }
                 if (m_mon2var.find(vars) != m_mon2var.end()) {
                     auto v = m_mon2var.find(vars)->second;
                     set_var_interval(v, u);
+                    di.mul<dd::w_dep::with_deps>(coeff, u, u);
                     di.intersect<dd::w_dep::with_deps>(t, u, t);
                 }
                 di.add<dd::w_dep::with_deps>(i, t, i);
             }
         }
         if (!di.separated_from_zero(i)) 
             return false;
+//        m_solver.display(verbose_stream() << "missed bound\n", e);
+//        exit(1);
         std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
             new_lemma lemma(m_core, "pdd");
             lemma &= e;

diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
@@ -409,6 +409,11 @@ namespace array {
         def1 = a.mk_default(store);
         def2 = a.mk_default(store->get_arg(0));
 
+        prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
+
+        euf::enode* ndef1 = e_internalize(def1);
+        euf::enode* ndef2 = e_internalize(def2);
+
         if (has_unitary_domain(store)) {
             def2 = store->get_arg(num_args - 1);
         }
@@ -417,8 +422,8 @@ namespace array {
             // let A = store(B, i, v)
             // 
             // Add:
-            //   default(A) = ite(epsilon1 = i, v, default(B))
-            //   A[diag(i)] = B[diag(i)]
+            //   default(A) = A[epsilon]
+            //   default(B) = B[epsilon]
             // 
             expr_ref_vector eqs(m);
             expr_ref_vector args1(m), args2(m);
@@ -428,22 +433,20 @@ namespace array {
             for (unsigned i = 1; i + 1 < num_args; ++i) {
                 expr* arg = store->get_arg(i);
                 sort* srt = arg->get_sort();
-                auto ep = mk_epsilon(srt);
-                eqs.push_back(m.mk_eq(ep.first, arg));
-                args1.push_back(m.mk_app(ep.second, arg));
-                args2.push_back(m.mk_app(ep.second, arg));
+                auto [ep, d] = mk_epsilon(srt);
+                eqs.push_back(m.mk_eq(ep, arg));
+                args1.push_back(ep);
+                args2.push_back(ep);
             }
-            expr_ref eq(m.mk_and(eqs), m);
-            def2 = m.mk_ite(eq, store->get_arg(num_args - 1), def2);
             app_ref sel1(m), sel2(m);
             sel1 = a.mk_select(args1);
             sel2 = a.mk_select(args2);
-            prop |= !ctx.get_enode(sel1) || !ctx.get_enode(sel2);
-            if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom()))
-                prop = true;
+            return 
+                ctx.propagate(e_internalize(sel1), ndef1, array_axiom()) ||
+                ctx.propagate(e_internalize(sel2), ndef2, array_axiom());
         }
-        prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
-        if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()))
+        // default(A) == default(B)
+        if (ctx.propagate(ndef1, ndef2, array_axiom()))
             prop = true;
         return prop;
     }