adding parallel threads

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

contrib/cmake/src/sat/CMakeLists.txt

@@ -12,6 +12,7 @@ z3_add_component(sat
     sat_integrity_checker.cpp
     sat_model_converter.cpp
     sat_mus.cpp
+    sat_par.cpp
     sat_probing.cpp
     sat_scc.cpp
     sat_simplifier.cpp

src/api/c++/z3++.h

@@ -1816,6 +1816,7 @@ namespace z3 {
                                    fmls,
                                    fml));
         }
+
         param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
 
     };

src/sat/sat_config.cpp

@@ -77,6 +77,7 @@ namespace sat {
         m_burst_search    = p.burst_search();
         
         m_max_conflicts   = p.max_conflicts();
+        m_num_parallel    = p.parallel_threads();
         
         // These parameters are not exposed
         m_simplify_mult1  = _p.get_uint("simplify_mult1", 300);

src/sat/sat_config.h

@@ -57,6 +57,7 @@ namespace sat {
         unsigned           m_random_seed;
         unsigned           m_burst_search;
         unsigned           m_max_conflicts;
+        unsigned           m_num_parallel;
 
         unsigned           m_simplify_mult1;
         double             m_simplify_mult2;

src/sat/sat_par.cpp

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_par.cpp
+
+Abstract:
+
+    Utilities for parallel SAT solving.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-1-29.
+
+Revision History:
+
+--*/
+#include "sat_par.h"
+
+
+namespace sat {
+
+    par::par() {}
+
+    void par::exchange(literal_vector const& in, unsigned& limit, literal_vector& out) {
+        #pragma omp critical (par_solver)
+        {
+            if (limit < m_units.size()) {
+                // this might repeat some literals.
+                out.append(m_units.size() - limit, m_units.c_ptr() + limit);
+            }
+            for (unsigned i = 0; i < in.size(); ++i) {
+                literal lit = in[i];
+                if (!m_unit_set.contains(lit.index())) {
+                    m_unit_set.insert(lit.index());
+                    m_units.push_back(lit);
+                }
+            }
+            limit = m_units.size();
+        }
+    }
+    
+};
+

src/sat/sat_par.h

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_par.h
+
+Abstract:
+
+    Utilities for parallel SAT solving.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-1-29.
+
+Revision History:
+
+--*/
+#ifndef SAT_PAR_H_
+#define SAT_PAR_H_
+
+#include"sat_types.h"
+#include"hashtable.h"
+#include"map.h"
+
+namespace sat {
+
+    class par {
+        typedef hashtable<unsigned, u_hash, u_eq> index_set;
+        literal_vector m_units;
+        index_set      m_unit_set;
+    public:
+        par();
+        void exchange(literal_vector const& in, unsigned& limit, literal_vector& out);
+    };
+
+};
+
+#endif

src/sat/sat_params.pyg

@@ -22,4 +22,5 @@ def_module_params('sat',
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
                           ('core.minimize', BOOL, False, 'minimize computed core'),
                           ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
+                          ('parallel_threads', UINT, 1, 'number of parallel threads to use'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

src/sat/sat_solver.cpp

@@ -35,6 +35,7 @@ namespace sat {
         m_rlimit(l),
         m_config(p),
         m_ext(ext),
+        m_par(0),
         m_cleaner(*this),
         m_simplifier(*this, p),
         m_scc(*this, p),
@@ -72,6 +73,8 @@ namespace sat {
 
     void solver::copy(solver const & src) {
         SASSERT(m_mc.empty() && src.m_mc.empty());
+        SASSERT(scope_lvl() == 0);
+        SASSERT(src.scope_lvl() == 0);
         // create new vars
         if (num_vars() < src.num_vars()) {
             for (bool_var v = num_vars(); v < src.num_vars(); v++) {
@@ -81,19 +84,25 @@ namespace sat {
                 VERIFY(v == mk_var(ext, dvar));
             }
         }
+        unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
+        for (unsigned i = 0; i < sz; ++i) {
+            assign(src.m_trail[i], justification());
+        }
+
         {
             // copy binary clauses
-            vector<watch_list>::const_iterator it  = src.m_watches.begin();
+            unsigned sz = src.m_watches.size();
-            vector<watch_list>::const_iterator end = src.m_watches.begin();
+            for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
-            for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
-                watch_list const & wlist = *it;
                 literal l = ~to_literal(l_idx);
-                watch_list::const_iterator it2  = wlist.begin();
+                watch_list const & wlist = src.m_watches[l_idx];
-                watch_list::const_iterator end2 = wlist.end();
+                watch_list::const_iterator it  = wlist.begin();
-                for (; it2 != end2; ++it2) {
+                watch_list::const_iterator end = wlist.end();
-                    if (!it2->is_binary_non_learned_clause())
+                for (; it != end; ++it) {
+                    if (!it->is_binary_non_learned_clause())
+                        continue;
+                    literal l2 = it->get_literal();
+                    if (l.index() > l2.index()) 
                         continue;
-                    literal l2 = it2->get_literal();
                     mk_clause_core(l, l2);
                 }
             }
@@ -711,6 +720,9 @@ namespace sat {
         pop_to_base_level();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(scope_lvl() == 0);
+        if (m_config.m_num_parallel > 0 && !m_par) {
+            return check_par(num_lits, lits);
+        }
 #ifdef CLONE_BEFORE_SOLVING
         if (m_mc.empty()) {
             m_clone = alloc(solver, m_params, 0 /* do not clone extension */);
@@ -759,6 +771,7 @@ namespace sat {
 
                 restart();
                 simplify_problem();
+                exchange_par();
                 if (check_inconsistent()) return l_false;
                 gc();
 
@@ -774,6 +787,121 @@ namespace sat {
         }
     }
 
+    enum par_exception_kind {
+        DEFAULT_EX,
+        ERROR_EX
+    };
+
+    lbool solver::check_par(unsigned num_lits, literal const* lits) {
+        int num_threads = static_cast<int>(m_config.m_num_parallel);
+        scoped_limits scoped_rlimit(rlimit());
+        vector<reslimit> rlims(num_threads);
+        ptr_vector<sat::solver> solvers(num_threads);
+        sat::par par;
+        for (int i = 0; i < num_threads; ++i) {
+            m_params.set_uint("random_seed", i);
+            solvers[i] = alloc(sat::solver, m_params, rlims[i], 0);
+            solvers[i]->copy(*this);
+            solvers[i]->set_par(&par);
+            scoped_rlimit.push_child(&solvers[i]->rlimit());
+        }
+        int finished_id = -1;
+        std::string        ex_msg;
+        par_exception_kind ex_kind;
+        unsigned error_code = 0;
+        lbool result = l_undef;
+        #pragma omp parallel for
+        for (int i = 0; i < num_threads; ++i) {
+            try {                
+                lbool r = solvers[i]->check(num_lits, lits);
+                bool first = false;
+                #pragma omp critical (par_solver)
+                {
+                    if (finished_id == UINT_MAX) {
+                        finished_id = i;
+                        first = true;
+                        result = r;
+                    }
+                }
+                if (first) {
+                    if (r == l_true) {
+                        set_model(solvers[i]->get_model());
+                    }
+                    else if (r == l_false) {
+                        m_core.reset();
+                        m_core.append(solvers[i]->get_core());
+                    }
+                    for (int j = 0; j < num_threads; ++j) {
+                        if (i != j) {
+                            rlims[j].cancel();
+                        }
+                    }
+                }                
+            }
+            catch (z3_error & err) {
+                if (i == 0) {
+                    error_code = err.error_code();
+                    ex_kind = ERROR_EX;
+                }
+            }
+            catch (z3_exception & ex) {
+                if (i == 0) {
+                    ex_msg = ex.msg();
+                    ex_kind = DEFAULT_EX;
+                }
+            }
+        }
+        for (int i = 0; i < num_threads; ++i) {
+            dealloc(solvers[i]);
+        }
+        if (finished_id == -1) {
+            switch (ex_kind) {
+            case ERROR_EX: throw z3_error(error_code);
+            default: throw default_exception(ex_msg.c_str());
+            }
+        }
+        return result;
+
+    }
+
+    /*
+      \brief import lemmas/units from parallel sat solvers.
+     */
+    void solver::exchange_par() {
+        if (m_par && scope_lvl() == 0) {
+            unsigned num_in = 0, num_out = 0;
+            SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
+            literal_vector in, out;
+            for (unsigned i = m_par_limit_out; i < m_trail.size(); ++i) {
+                literal lit = m_trail[i];
+                if (lit.var() < m_par_num_vars) {
+                    ++num_out;
+                    out.push_back(lit);
+                }
+            }
+            m_par_limit_out = m_trail.size();
+            m_par->exchange(out, m_par_limit_in, in);
+            for (unsigned i = 0; !inconsistent() && i < in.size(); ++i) {
+                literal lit = in[i];
+                SASSERT(lit.var() < m_par_num_vars);
+                if (lvl(lit.var()) != 0 || value(lit) != l_true) {
+                    ++num_in;
+                    assign(lit, justification());
+                }
+            }
+            if (num_in > 0 || num_out > 0) {
+                IF_VERBOSE(1, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";);
+            }
+        }
+    }
+
+    void solver::set_par(par* p) {
+        m_par = p;
+        m_par_num_vars = num_vars();
+        m_par_limit_in = 0;
+        m_par_limit_out = 0;
+    }
+
     bool_var solver::next_var() {
         bool_var next;
 

src/sat/sat_solver.h

@@ -33,6 +33,7 @@ Revision History:
 #include"sat_iff3_finder.h"
 #include"sat_probing.h"
 #include"sat_mus.h"
+#include"sat_par.h"
 #include"params.h"
 #include"statistics.h"
 #include"stopwatch.h"
@@ -74,6 +75,7 @@ namespace sat {
         config                  m_config;
         stats                   m_stats;
         extension *             m_ext;
+        par*                    m_par;
         random_gen              m_rand;
         clause_allocator        m_cls_allocator;
         cleaner                 m_cleaner;
@@ -128,6 +130,10 @@ namespace sat {
         literal_set             m_assumption_set;   // set of enabled assumptions
         literal_vector          m_core;             // unsat core
 
+        unsigned                m_par_limit_in;
+        unsigned                m_par_limit_out;
+        unsigned                m_par_num_vars;
+
         void del_clauses(clause * const * begin, clause * const * end);
 
         friend class integrity_checker;
@@ -241,7 +247,9 @@ namespace sat {
             m_num_checkpoints = 0;
             if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
         }
+        void set_par(par* p);
         bool canceled() { return !m_rlimit.inc(); }
+        config const& get_config() { return m_config; }
         typedef std::pair<literal, literal> bin_clause;
     protected:
         watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
@@ -317,6 +325,8 @@ namespace sat {
         bool check_model(model const & m) const;
         void restart();
         void sort_watch_lits();
+        void exchange_par();
+        lbool check_par(unsigned num_lits, literal const* lits);
 
         // -----------------------
         //

src/sat/sat_solver/inc_sat_solver.cpp

@@ -140,6 +140,7 @@ public:
         if (r != l_true) return r;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
+        
         switch (r) {
         case l_true:
             if (sz > 0) {
@@ -276,6 +277,8 @@ public:
         return r;
     }
 
+
+
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
         sat::literal_vector ls;
         u_map<expr*> lit2var;

src/smt/theory_seq.cpp

@@ -2940,8 +2940,8 @@ void theory_seq::deque_axiom(expr* n) {
   encode that s is not contained in of xs1
   where s1 is all of s, except the last element.
 
-  lit or s = "" or s = s1*(unit c)
+  s = "" or s = s1*(unit c)
-  lit or s = "" or !contains(x*s1, s)
+  s = "" or !contains(x*s1, s)
 */
 void theory_seq::tightest_prefix(expr* s, expr* x) {
     expr_ref s1 = mk_first(s);

src/tactic/tactical.cpp

@@ -461,13 +461,6 @@ enum par_exception_kind {
 
 class par_tactical : public or_else_tactical {
 
-    struct scoped_limits {
-        reslimit&  m_limit;
-        unsigned   m_sz;
-        scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {}
-        ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
-        void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
-    };
 
 public:
     par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {}

src/util/rlimit.h

@@ -61,4 +61,13 @@ public:
 
 };
 
+struct scoped_limits {
+    reslimit&  m_limit;
+    unsigned   m_sz;
+    scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {}
+    ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
+    void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
+};
+
+
 #endif