Parallel solving

src/smt/smt_context.h

@@ -51,6 +51,7 @@ Revision History:
 #include "solver/progress_callback.h"
 #include "solver/assertions/asserted_formulas.h"
 #include "smt/priority_queue.h"
+#include "util/dlist.h"
 #include <tuple>
 
 // there is a significant space overhead with allocating 1000+ contexts in
@@ -191,6 +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;
@@ -908,6 +916,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);
@@ -916,6 +926,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("formula has not been simplified");
+                throw default_exception(std::string("formula has not been simplified") + " : " + mk_pp(n, m));
             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) {
-                vars.push_back(v);
-            }
+            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);