Merge branch 'Z3Prover:master' into parallel-solving

src/smt/smt_context.h

@@ -914,6 +914,8 @@ namespace smt {
 
         void add_or_rel_watches(app * n);
 
+        void add_implies_rel_watches(app* n);
+
         void add_ite_rel_watches(app * n);
 
         void mk_not_cnstr(app * n);
@@ -922,6 +924,8 @@ namespace smt {
 
         void mk_or_cnstr(app * n);
 
+        void mk_implies_cnstr(app* n);
+
         void mk_iff_cnstr(app * n, bool sign);
 
         void mk_ite_cnstr(app * n);

src/smt/smt_internalizer.cpp

@@ -696,6 +696,10 @@ namespace smt {
                 mk_or_cnstr(to_app(n));
                 add_or_rel_watches(to_app(n));
                 break;
+            case OP_IMPLIES:
+                mk_implies_cnstr(to_app(n));
+                add_implies_rel_watches(to_app(n));
+                break;
             case OP_EQ:
                 if (m.is_iff(n))
                     mk_iff_cnstr(to_app(n), false);
@@ -711,8 +715,7 @@ namespace smt {
                 mk_iff_cnstr(to_app(n), true);
                 break;
             case OP_DISTINCT:
-            case OP_IMPLIES:
+                throw default_exception(std::string("formula has not been simplified") + " : " + mk_pp(n, m));
-                throw default_exception("formula has not been simplified");
             case OP_OEQ:
                 UNREACHABLE();
             default:
@@ -1712,6 +1715,14 @@ namespace smt {
         }
     }
 
+    void context::add_implies_rel_watches(app* n) {
+        if (relevancy()) {
+            relevancy_eh* eh = m_relevancy_propagator->mk_implies_relevancy_eh(n);
+            add_rel_watch(~get_literal(n->get_arg(0)), eh);
+            add_rel_watch(get_literal(n->get_arg(1)), eh);
+        }
+    }
+
     void context::add_ite_rel_watches(app * n) {
         if (relevancy()) {
             relevancy_eh * eh = m_relevancy_propagator->mk_ite_relevancy_eh(n);
@@ -1758,9 +1769,24 @@ namespace smt {
         mk_gate_clause(buffer.size(), buffer.data());
     }
 
+    void context::mk_implies_cnstr(app* n) {
+        literal l = get_literal(n);
+        literal_buffer buffer;
+        buffer.push_back(~l);
+        auto arg1 = n->get_arg(0);
+        literal l_arg1 = get_literal(arg1);
+        mk_gate_clause(l, l_arg1);
+        buffer.push_back(~l_arg1);
+        auto arg2 = n->get_arg(1);
+        literal l_arg2 = get_literal(arg2);
+        mk_gate_clause(l, ~l_arg2);
+        buffer.push_back(l_arg2);
+        mk_gate_clause(buffer.size(), buffer.data());
+    }
+
     void context::mk_iff_cnstr(app * n, bool sign) {
         if (n->get_num_args() != 2) 
-            throw default_exception("formula has not been simplified");
+            throw default_exception(std::string("formula has not been simplified") + " : " + mk_pp(n, m));
         literal l  = get_literal(n);
         literal l1 = get_literal(n->get_arg(0));
         literal l2 = get_literal(n->get_arg(1));

src/smt/smt_lookahead.cpp

@@ -72,9 +72,14 @@ namespace smt {
         svector<bool_var> vars;
         for (bool_var v = 0; v < static_cast<bool_var>(sz); ++v) {
             expr* b = ctx.bool_var2expr(v);
-            if (b && ctx.get_assignment(v) == l_undef) {
+            if (!b)
+                continue;
+            if (ctx.get_assignment(v) != l_undef)
+                continue;
+            if (m.is_and(b) || m.is_or(b) || m.is_not(b) || m.is_ite(b) || m.is_implies(b) || m.is_iff(b) || m.is_xor(b))
+                continue; // do not choose connectives
             vars.push_back(v);
-            }
+            
         }
         compare comp(ctx);
         std::sort(vars.begin(), vars.end(), comp);

src/smt/smt_parallel.cpp

@@ -77,13 +77,16 @@ namespace smt {
             throw default_exception("trace streams have to be off in parallel mode");
 
         
+        params_ref params = ctx.get_params();
         for (unsigned i = 0; i < num_threads; ++i) {
             smt_params.push_back(ctx.get_fparams());
+            smt_params.back().m_preprocess = false;
         }
+                    
         for (unsigned i = 0; i < num_threads; ++i) {
             ast_manager* new_m = alloc(ast_manager, m, true);
             pms.push_back(new_m);
-            pctxs.push_back(alloc(context, *new_m, smt_params[i], ctx.get_params())); 
+            pctxs.push_back(alloc(context, *new_m, smt_params[i], params)); 
             context& new_ctx = *pctxs.back();
             context::copy(ctx, new_ctx, true);
             new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);
@@ -178,6 +181,7 @@ namespace smt {
         for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0);
 
         std::function<void(void)> collect_units = [&,this]() {
+            //return; -- has overhead
             for (unsigned i = 0; i < num_threads; ++i) {
                 context& pctx = *pctxs[i];
                 pctx.pop_to_base_lvl();

src/smt/smt_relevancy.cpp

@@ -62,6 +62,13 @@ namespace smt {
         void operator()(relevancy_propagator & rp) override;
     };
 
+    class implies_relevancy_eh : public relevancy_eh {
+        app* m_parent;
+    public:
+        implies_relevancy_eh(app* p) :m_parent(p) {}
+        void operator()(relevancy_propagator& rp) override;
+    };
+
     class ite_relevancy_eh : public relevancy_eh {
         app * m_parent;
     public:
@@ -108,6 +115,11 @@ namespace smt {
         return mk_relevancy_eh(or_relevancy_eh(n));
     }
 
+    relevancy_eh* relevancy_propagator::mk_implies_relevancy_eh(app* n) {
+        SASSERT(get_manager().is_implies(n));
+        return mk_relevancy_eh(implies_relevancy_eh(n));
+    }
+
     relevancy_eh * relevancy_propagator::mk_and_relevancy_eh(app * n) {
         SASSERT(get_manager().is_and(n));
         return mk_relevancy_eh(and_relevancy_eh(n));
@@ -359,6 +371,36 @@ namespace smt {
             }
         } 
         
+        void propagate_relevant_implies(app* n) {
+            SASSERT(get_manager().is_implies(n));
+            lbool val = m_context.find_assignment(n);
+            // If val is l_undef, then the expression
+            // is a root, and no boolean variable was created for it.
+            if (val == l_undef)
+                val = l_true;
+            switch (val) {
+            case l_false:
+                propagate_relevant_app(n);
+                break;
+            case l_undef:
+                break;
+            case l_true: {
+                expr* true_arg = nullptr;
+                auto arg0 = n->get_arg(0);
+                auto arg1 = n->get_arg(1);
+                if (m_context.find_assignment(arg0) == l_false) {
+                    if (!is_relevant_core(arg0))
+                        mark_as_relevant(arg0);
+                    return;
+                }
+                if (m_context.find_assignment(arg1) == l_true) {
+                    if (!is_relevant_core(arg1))
+                        mark_as_relevant(arg1);
+                    return;
+                }
+            }
+            }
+        }
         /**
            \brief Propagate relevancy for an or-application.
         */
@@ -470,6 +512,9 @@ namespace smt {
                         case OP_AND:
                             propagate_relevant_and(to_app(n));
                             break;
+                        case OP_IMPLIES:
+                            propagate_relevant_implies(to_app(n));
+                            break;
                         case OP_ITE:
                             propagate_relevant_ite(to_app(n));
                             break;
@@ -505,6 +550,8 @@ namespace smt {
                     propagate_relevant_or(to_app(n));
                 else if (m.is_and(n))
                     propagate_relevant_and(to_app(n));
+                else if (m.is_implies(n))
+                    propagate_relevant_implies(to_app(n));
             }
             relevancy_ehs * ehs = get_watches(n, val);
             while (ehs != nullptr) {
@@ -644,6 +691,11 @@ namespace smt {
             static_cast<relevancy_propagator_imp&>(rp).propagate_relevant_or(m_parent);
     }
 
+    void implies_relevancy_eh::operator()(relevancy_propagator& rp) {
+        if (rp.is_relevant(m_parent))
+            static_cast<relevancy_propagator_imp&>(rp).propagate_relevant_implies(m_parent);
+    }
+
     void ite_relevancy_eh::operator()(relevancy_propagator & rp) {
         if (rp.is_relevant(m_parent)) {
             static_cast<relevancy_propagator_imp&>(rp).propagate_relevant_ite(m_parent);

src/smt/smt_relevancy.h

@@ -188,6 +188,7 @@ namespace smt {
         void add_dependency(expr * src, expr * target);
         
         relevancy_eh * mk_or_relevancy_eh(app * n);
+        relevancy_eh* mk_implies_relevancy_eh(app* n);
         relevancy_eh * mk_and_relevancy_eh(app * n);
         relevancy_eh * mk_ite_relevancy_eh(app * n);
         relevancy_eh * mk_term_ite_relevancy_eh(app * c, app * t, app * e);