Merge branch 'parallel-solving' of github.com:ilanashapiro/z3 into parallel-solving

src/ast/euf/euf_ac_plugin.cpp

@@ -278,17 +278,9 @@ namespace euf {
         if (!m_shared.empty())
             out << "shared monomials:\n";
         for (auto const& s : m_shared) {
-            out << g.bpp(s.n) << ": " << s.m << " r: " << g.bpp(s.n->get_root()) << "\n";
+            out << g.bpp(s.n) << " r " << g.bpp(s.n->get_root()) << " - " << s.m << ": " << m_pp_ll(*this, monomial(s.m)) << "\n";
         }
-#if 0
+
-        i = 0;
-        for (auto m : m_monomials) {
-            out << i << ": ";
-            display_monomial_ll(out, m);
-            out << "\n";
-            ++i;
-        }
-#endif
         for (auto n : m_nodes) {
             if (!n)
                 continue;
@@ -361,19 +353,16 @@ namespace euf {
         if (!orient_equation(eq))
             return false;
 
-#if 1
         if (is_reducing(eq))
             is_active = true;
-#else
-
-        is_active = true; // set to active by default
-#endif
 
         if (!is_active) {
             m_passive.push_back(eq);
             return true;          
         }
 
+        eq.status = eq_status::is_to_simplify_eq;
+
         m_active.push_back(eq);
         auto& ml = monomial(eq.l);
         auto& mr = monomial(eq.r);
@@ -621,9 +610,9 @@ namespace euf {
             // simplify eq using processed
             TRACE(plugin,
                 for (auto other_eq : forward_iterator(eq_id))
-                    tout << "forward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n");
+                    tout << "forward iterator " << eq_pp_ll(*this, m_active[eq_id]) << " vs " << eq_pp_ll(*this, m_active[other_eq])  << "\n");
             for (auto other_eq : forward_iterator(eq_id))
-                if (is_processed(other_eq) && forward_simplify(eq_id, other_eq))
+                if ((is_processed(other_eq) || is_reducing(other_eq)) && forward_simplify(eq_id, other_eq))
                     goto loop_start;
 
             auto& eq = m_active[eq_id];
@@ -914,6 +903,8 @@ namespace euf {
             set_status(dst_eq, eq_status::is_dead_eq);
             return true;
         }
+        SASSERT(!are_equal(m_active[src_eq], m_active[dst_eq]));
+        
         if (!is_equation_oriented(src))
             return false;
         // check that src.l is a subset of dst.r
@@ -1088,23 +1079,18 @@ namespace euf {
     // rewrite monomial to normal form.
     bool ac_plugin::reduce(ptr_vector<node>& m, justification& j) {
         bool change = false;
-        unsigned sz = m.size();
         do {
         init_loop:
-            if (m.size() == 1)
-                return change;
             bloom b;
             init_ref_counts(m, m_m_counts);
             for (auto n : m) {
                 if (n->is_zero) {
                     m[0] = n;
                     m.shrink(1);
+                    change = true;
                     break;
                 }
                 for (auto eq : n->eqs) {
-                    continue;
-                    if (!is_reducing(eq)) // also can use processed?
-                        continue;
                     auto& src = m_active[eq];
 
                     if (!is_equation_oriented(src))
@@ -1116,17 +1102,16 @@ namespace euf {
 
                     TRACE(plugin, display_equation_ll(tout << "reduce ", src) << "\n");
                     SASSERT(is_correct_ref_count(monomial(src.l), m_eq_counts));
-                    //display_equation_ll(std::cout << "reduce ", src) << ": ";
+                    for (auto n : m)
-                    //display_monomial_ll(std::cout, m);
+                        for (auto s : n->shared)
+                            m_shared_todo.insert(s);
                     rewrite1(m_eq_counts, monomial(src.r), m_m_counts, m);
-                    //display_monomial_ll(std::cout << " -> ", m) << "\n";
                     j = join(j, eq);
                     change = true;
                     goto init_loop;
                 }
             }
         } while (false);
-        VERIFY(sz >= m.size());
         return change;
     }
 
@@ -1287,6 +1272,8 @@ namespace euf {
                 continue;
             }
             change = true;
+            for (auto s : n->shared)
+                m_shared_todo.insert(s);
             if (r.size() == 0)
                 // if r is empty, we can remove n from l
                 continue;
@@ -1407,9 +1394,11 @@ namespace euf {
         TRACE(plugin_verbose, tout << "num shared todo " << m_shared_todo.size() << "\n");
         if (m_shared_todo.empty())
             return;
+
         while (!m_shared_todo.empty()) {
             auto idx = *m_shared_todo.begin();
-            m_shared_todo.remove(idx);
+            m_shared_todo.remove(idx);        
+            TRACE(plugin, tout << "index " << idx << " shared size " << m_shared.size() << "\n");
             if (idx < m_shared.size())
                 simplify_shared(idx, m_shared[idx]);
         }
@@ -1431,7 +1420,7 @@ namespace euf {
         auto old_m = s.m;
         auto old_n = monomial(old_m).m_src;
         ptr_vector<node> m1(monomial(old_m).m_nodes);
-        TRACE(plugin_verbose, tout << "simplify shared: " << g.bpp(old_n) << ": " << m_pp_ll(*this, monomial(old_m)) << "\n");
+        TRACE(plugin, tout << "simplify shared: " << g.bpp(old_n) << ": " << m_pp_ll(*this, monomial(old_m)) << "\n");
         if (!reduce(m1, j))
             return;
 

src/ast/simplifiers/euf_completion.cpp

@@ -268,7 +268,6 @@ namespace euf {
         expr_ref r(f, m);
         m_rewriter(r);
         f = r.get();
-        // verbose_stream() << r << "\n";
         auto cons = m.mk_app(symbol("consequence"), 1, &f, m.mk_bool_sort());
         m_fmls.add(dependent_expr(m, cons, nullptr, nullptr));
     }
@@ -317,35 +316,43 @@ namespace euf {
             expr_ref y1(y, m);
             m_rewriter(x1);
             m_rewriter(y1);
-            
+
             add_quantifiers(x1);
             add_quantifiers(y1);
             enode* a = mk_enode(x1);
             enode* b = mk_enode(y1);
+
             if (a->get_root() == b->get_root())
-                return;           
+                return;
-            m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
+
-            m_egraph.propagate();
+            TRACE(euf, tout << "merge and propagate\n");
             add_children(a);
             add_children(b);
+            m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
+            m_egraph.propagate();
+            m_should_propagate = true; 
+
+#if 0
             auto a1 = mk_enode(x);
-            if (a1->get_root() != a->get_root()) {
+            auto b1 = mk_enode(y);
+
+            if (a->get_root() != a1->get_root()) {
+                add_children(a1);;
                 m_egraph.merge(a, a1, nullptr);
                 m_egraph.propagate();
-                add_children(a1);
-            }
-            auto b1 = mk_enode(y);
-            if (b1->get_root() != b->get_root()) {
-                TRACE(euf, tout << "merge and propagate\n");
-                m_egraph.merge(b, b1, nullptr);
-                m_egraph.propagate();
-                add_children(b1);
             }
 
-            m_should_propagate = true;
+            if (b->get_root() != b1->get_root()) {
-            if (m_side_condition_solver)
+                add_children(b1);
+                m_egraph.merge(b, b1, nullptr);
+                m_egraph.propagate();
+            }
+#endif
+            
+            if (m_side_condition_solver && a->get_root() != b->get_root())
                 m_side_condition_solver->add_constraint(f, pr, d);
-            IF_VERBOSE(1, verbose_stream() << "eq: " << mk_pp(x1, m) << " == " << mk_pp(y1, m) << "\n");
+            IF_VERBOSE(1, verbose_stream() << "eq: " << a->get_root_id() << " " << b->get_root_id() << " " 
+                 << x1 << " == " << y1 << "\n");
         }
         else if (m.is_not(f, f)) {
             enode* n = mk_enode(f);
@@ -689,7 +696,7 @@ namespace euf {
         b = new (mem) binding(q, pat, max_generation, min_top, max_top);
         b->init(b);
         for (unsigned i = 0; i < n; ++i)
-            b->m_nodes[i] = _binding[i];
+            b->m_nodes[i] = _binding[i]->get_root();
 
         m_bindings.insert(b);
         get_trail().push(insert_map<bindings, binding*>(m_bindings, b));
@@ -748,12 +755,13 @@ namespace euf {
 
     void completion::apply_binding(binding& b, quantifier* q, expr_ref_vector const& s) {
         var_subst subst(m);
-        expr_ref r = subst(q->get_expr(), s);        
+        expr_ref r = subst(q->get_expr(), s);      
         scoped_generation sg(*this, b.m_max_top_generation + 1);
         auto [pr, d] = get_dependency(q);
         if (pr)
             pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data());
         m_consequences.push_back(r);
+        TRACE(euf_completion, tout << "new instantiation: " << r << " q: " << mk_pp(q, m) << "\n");
         add_constraint(r, pr, d);
         propagate_rules();
         m_egraph.propagate();
@@ -1022,7 +1030,7 @@ namespace euf {
 
         }
         enode* n = m_egraph.find(f);
-        
+        if (!n) n = mk_enode(f);
         enode* r = n->get_root();
         d = m.mk_join(d, explain_eq(n, r));
         d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));

src/smt/smt_context.h

@@ -192,11 +192,13 @@ namespace smt {
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
         updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
+
         struct lit_node : dll_base<lit_node> {
             literal lit;
             lit_node(literal l) : lit(l) { init(this); }
         };
         lit_node* m_dll_lits;
+
         svector<std::array<double, 2>> m_lit_scores; 
 
         clause_vector               m_aux_clauses;

src/smt/smt_parallel.cpp

@@ -113,6 +113,7 @@ namespace smt {
 
         auto cube_pq = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
             unsigned k = 3; // Number of top literals you want
+
             ast_manager& m = ctx.get_manager();
 
             // Get the entire fixed-size priority queue (it's not that big)
@@ -194,6 +195,9 @@ namespace smt {
                 unsigned sz = pctx.assigned_literals().size();
                 for (unsigned j = unit_lim[i]; j < sz; ++j) {
                     literal lit = pctx.assigned_literals()[j];
+                    //IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";);
+                    if (!pctx.is_relevant(lit.var()))
+                        continue;
                     expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m);
                     if (lit.sign()) e = pctx.m.mk_not(e);
                     expr_ref ce(tr(e.get()), ctx.m);
@@ -309,7 +313,7 @@ namespace smt {
                         finished_id = i;
                         result = r;                        
                     }
-                    else if (!first) return;
+                    else if (!first) return; // nothing new to contribute
                 }
 
                 // Cancel limits on other threads now that a result is known

src/solver/smt_logics.cpp

@@ -29,52 +29,56 @@ bool smt_logics::supported_logic(symbol const & s) {
 }
 
 bool smt_logics::logic_has_reals_only(symbol const& s) {
+    auto str = s.str();
     return
-        s.str().find("LRA") != std::string::npos ||
+        str.find("LRA") != std::string::npos ||
-        s.str().find("LRA") != std::string::npos ||
+        str.find("LRA") != std::string::npos ||
-        s.str().find("NRA") != std::string::npos ||
+        str.find("NRA") != std::string::npos ||
-        s.str().find("RDL") != std::string::npos;
+        str.find("RDL") != std::string::npos;
 }
 
 bool smt_logics::logic_has_arith(symbol const & s) {
+    auto str = s.str();
     return
-        s.str().find("LRA") != std::string::npos ||
+        str.find("LRA") != std::string::npos ||
-        s.str().find("LIRA") != std::string::npos ||
+        str.find("LIRA") != std::string::npos ||
-        s.str().find("LIA") != std::string::npos ||
+        str.find("LIA") != std::string::npos ||
-        s.str().find("LRA") != std::string::npos ||
+        str.find("LRA") != std::string::npos ||
-        s.str().find("NRA") != std::string::npos ||
+        str.find("NRA") != std::string::npos ||
-        s.str().find("NIRA") != std::string::npos ||
+        str.find("NIRA") != std::string::npos ||
-        s.str().find("NIA") != std::string::npos ||
+        str.find("NIA") != std::string::npos ||
-        s.str().find("IDL") != std::string::npos ||
+        str.find("IDL") != std::string::npos ||
-        s.str().find("RDL") != std::string::npos ||
+        str.find("RDL") != std::string::npos ||
-        s == "QF_BVRE" ||
+        str == "QF_BVRE" ||
-        s == "QF_FP" ||
+        str == "QF_FP" ||
-        s == "FP" ||
+        str == "FP" ||
-        s == "QF_FPBV" ||
+        str == "QF_FPBV" ||
-        s == "QF_BVFP" ||
+        str == "QF_BVFP" ||
-        s == "QF_S" ||
+        str == "QF_S" ||
         logic_is_all(s) ||
-        s == "QF_FD" ||
+        str == "QF_FD" ||
-        s == "HORN";
+        str == "HORN";
 }
 
 bool smt_logics::logic_has_bv(symbol const & s) {
+    auto str = s.str();
     return
-        s.str().find("BV") != std::string::npos ||
+        str.find("BV") != std::string::npos ||
-        s == "FP" ||
+        str == "FP" ||
         logic_is_all(s) ||
-        s == "QF_FD" ||
+        str == "QF_FD" ||
-        s == "SMTFD" ||
+        str == "SMTFD" ||
-        s == "HORN";
+        str == "HORN";
 }
 
 bool smt_logics::logic_has_array(symbol const & s) {
+    auto str = s.str();
     return
-        s.str().starts_with("QF_A") ||   
+        str.starts_with("QF_A") ||
-        s.str().starts_with("A") ||   
+        str.starts_with("A") ||
         logic_is_all(s) ||
-        s == "SMTFD" ||
+        str == "SMTFD" ||
-        s == "HORN";
+        str == "HORN";
 }
 
 bool smt_logics::logic_has_seq(symbol const & s) {
@@ -82,17 +86,28 @@ bool smt_logics::logic_has_seq(symbol const & s) {
 }
 
 bool smt_logics::logic_has_str(symbol const & s) {
-    return s == "QF_S" || s == "QF_SLIA" || s == "QF_SNIA" || logic_is_all(s);
+    auto str = s.str();
+    return str == "QF_S" ||
+           str == "QF_SLIA" ||
+           str == "QF_SNIA" ||
+           logic_is_all(s);
 }
 
 bool smt_logics::logic_has_fpa(symbol const & s) {
-    return s == "FP" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA"  || logic_is_all(s);
+    auto str = s.str();
+    return str == "FP" ||
+           str == "QF_FP" ||
+           str == "QF_FPBV" ||
+           str == "QF_BVFP" ||
+           str == "QF_FPLRA"  ||
+           logic_is_all(s);
 }
 
 bool smt_logics::logic_has_uf(symbol const & s) {
+    auto str = s.str();
     return 
-        s.str().find("UF") != std::string::npos ||
+        str.find("UF") != std::string::npos ||
-        s == "SMTFD";
+        str == "SMTFD";
 }
 
 bool smt_logics::logic_has_horn(symbol const& s) {
@@ -104,9 +119,10 @@ bool smt_logics::logic_has_pb(symbol const& s) {
 }
 
 bool smt_logics::logic_has_datatype(symbol const& s) {
+    auto str = s.str();
     return 
-        s.str().find("DT") != std::string::npos ||
+        str.find("DT") != std::string::npos ||
-        s == "QF_FD" ||
+        str == "QF_FD" ||
         logic_is_all(s) ||
         logic_has_horn(s);
 }

src/util/event_handler.h

@@ -28,9 +28,8 @@ enum event_handler_caller_t {
 
 class event_handler {
 protected:
-    event_handler_caller_t m_caller_id;
+    event_handler_caller_t m_caller_id = UNSET_EH_CALLER;
 public:
-    event_handler(): m_caller_id(UNSET_EH_CALLER) {}
     virtual ~event_handler() = default;
     virtual void operator()(event_handler_caller_t caller_id) = 0;
     event_handler_caller_t caller_id() const { return m_caller_id; }

src/util/gparams.cpp

@@ -416,7 +416,7 @@ public:
         symbol sp(p.c_str());
         std::ostringstream buffer;
         ps.display(buffer, sp);
-        return buffer.str();
+        return std::move(buffer).str();
     }
 
     std::string get_default(param_descrs const & d, std::string const & p, std::string const & m) {