build issues, add equivalence finding to probing (disabled)

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

src/math/grobner/pdd_simplifier.cpp

@@ -493,30 +493,35 @@ namespace dd {
             unsigned sz;
             unsigned offset;
             unsigned index;
-            unsigned_vector* vars;
+            mon(unsigned sz, unsigned offset): sz(sz), offset(offset), index(UINT_MAX) {}
-            mon(unsigned sz, unsigned offset, unsigned_vector* vars): sz(sz), offset(offset), index(UINT_MAX), vars(vars) {}
+            mon(): sz(0), offset(0), index(UINT_MAX) {}
-            mon(): sz(0), offset(0), index(UINT_MAX), vars(nullptr) {}
             bool is_valid() const { return index != UINT_MAX; }
             struct hash { 
+                unsigned_vector& vars;
+                hash(unsigned_vector& vars):vars(vars) {}
                 bool operator()(mon const& m) const {
-                    if (!m.vars) return 0;
+                    return unsigned_ptr_hash(vars.c_ptr() + m.offset, m.sz, 1);
-                    return string_hash((const char*)(m.vars->c_ptr() + m.offset), m.sz*4, 1);
                 };
             };
             struct eq {
+                unsigned_vector& vars;
+                eq(unsigned_vector& vars):vars(vars) {}
                 bool operator()(mon const& a, mon const& b) const {
                     if (a.sz != b.sz) return false;
                     for (unsigned i = 0; i < a.sz; ++i) 
-                        if ((*a.vars)[a.offset+i] != (*b.vars)[b.offset+i]) return false;
+                        if (vars[a.offset+i] != vars[b.offset+i]) 
+                            return false;
                     return true;
                 }
             };
         };
-        hashtable<mon, mon::hash, mon::eq> mon2idx;
+        mon::hash mon_hash(vars);
+        mon::eq mon_eq(vars);
+        hashtable<mon, mon::hash, mon::eq> mon2idx(DEFAULT_HASHTABLE_INITIAL_CAPACITY, mon_hash, mon_eq);
         svector<mon> idx2mon;
 
-        auto insert_mon = [&,this](unsigned n, unsigned const* vs) {
+        auto insert_mon = [&](unsigned n, unsigned const* vs) {
-            mon mm(n, vars.size(), &vars);
+            mon mm(n, vars.size());
             vars.append(n, vs);
             auto* e = mon2idx.insert_if_not_there2(mm);
             if (!e->get_data().is_valid()) {
@@ -564,7 +569,7 @@ namespace dd {
                     continue;
                 }
                 unsigned n = m.vars.size();
-                mon mm(n, vars.size(), &vars);
+                mon mm(n, vars.size());
                 vars.append(n, m.vars.c_ptr());
                 VERIFY(mon2idx.find(mm, mm));
                 vars.shrink(vars.size() - n);

src/sat/sat_aig_simplifier.cpp

@@ -121,7 +121,7 @@ namespace sat {
             }
         }
 
-        std::function<void(aig_def)> force_var = [&, this] (aig_def a) {
+        std::function<void(aig_def)> force_var = [&] (aig_def a) {
             for (unsigned i = 0; i < a.sz; ++i) {
                 unsigned v = literals[a.offset + i].var();
                 if (!ins[v]) {
@@ -130,7 +130,7 @@ namespace sat {
                 }
             }
         };
-        std::function<void(unsigned)> add_var = [&, this] (unsigned v) {
+        std::function<void(unsigned)> add_var = [&] (unsigned v) {
             if (!outs[v] && ins[v]) {
                 aigc.add_var(v);
                 outs[v] = true;
@@ -229,7 +229,7 @@ namespace sat {
         unsigned_vector sorted = top_sort();
         vector<cut_set> cuts;    
         cuts.resize(m_aig.size());
-        max_cut_size = std::min(cut::max_cut_size, max_cut_size);
+        max_cut_size = std::min(cut().max_cut_size, max_cut_size);
         cut_set cut_set2;
         cut_set2.init(m_region, max_cutset_size + 1);
         for (unsigned id : sorted) {

src/sat/sat_cutset.h

@@ -17,12 +17,12 @@
 namespace sat {
 
     struct cut {
-        static const unsigned max_cut_size = 6;
+        unsigned max_cut_size;
         unsigned m_filter;
         unsigned m_size;
-        unsigned m_elems[max_cut_size];
+        unsigned m_elems[6];
         uint64_t m_table;
-        cut(): m_filter(0), m_size(0), m_table(0) {}
+        cut(): m_filter(0), m_size(0), m_table(0), max_cut_size(6) {}
 
         cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2) { m_elems[0] = id; }
 
@@ -61,13 +61,13 @@ namespace sat {
 
         uint64_t shift_table(cut const& other) const;
 
-        bool merge(cut const& a, cut const& b, unsigned max_cut_size) {
+        bool merge(cut const& a, cut const& b, unsigned max_sz) {
             SASSERT(a.m_size > 0 && b.m_size > 0);
             unsigned i = 0, j = 0;
             unsigned x = a[i];
             unsigned y = b[j];
             while (x != UINT_MAX || y != UINT_MAX) {
-                if (!add(std::min(x, y), max_cut_size)) {
+                if (!add(std::min(x, y), max_sz)) {
                     return false;
                 }
                 if (x < y) {

src/sat/sat_probing.cpp

@@ -19,11 +19,13 @@ Revision History:
 --*/
 #include "sat/sat_probing.h"
 #include "sat/sat_solver.h"
+#include "sat/sat_elim_eqs.h"
 #include "sat/sat_simplifier_params.hpp"
 
 namespace sat {
     probing::probing(solver & _s, params_ref const & p):
-        s(_s) {
+        s(_s),
+        m_big(s.rand()) {
         updt_params(p);
         reset_statistics();
         m_stopped_at = 0;
@@ -137,9 +139,21 @@ namespace sat {
         m_assigned.reset();
         unsigned tr_sz = s.m_trail.size();
         for (unsigned i = old_tr_sz; i < tr_sz; i++) {
-            m_assigned.insert(s.m_trail[i]);
+            literal lit = s.m_trail[i];
+            m_assigned.insert(lit);
+
+#if 0
+            // learn equivalences during probing:
+            if (implies(lit, l)) {
+                if (nullptr == find_binary_watch(s.get_wlist(lit), l) ||
+                    nullptr == find_binary_watch(s.get_wlist(~l), ~lit)) {
+                    m_equivs.push_back(std::make_pair(lit, l));
+                }
+            }
+#endif
         }
         cache_bins(l, old_tr_sz);
+        
         s.pop(1);
 
         if (!try_lit(~l, true))
@@ -177,23 +191,24 @@ namespace sat {
     }
 
     struct probing::report {
-        probing    & m_probing;
+        probing    & p;
         stopwatch    m_watch;
         unsigned     m_num_assigned;        
         report(probing & p):
-            m_probing(p),
+            p(p),
             m_num_assigned(p.m_num_assigned) {
             m_watch.start();
         }
 
         ~report() {
             m_watch.stop();
-            unsigned units = (m_probing.m_num_assigned - m_num_assigned);
+            unsigned units = (p.m_num_assigned - m_num_assigned);
             IF_VERBOSE(2,
                        verbose_stream() << " (sat-probing";
                        if (units > 0) verbose_stream() << " :probing-assigned " << units;
-                       verbose_stream() << " :cost " << m_probing.m_counter;
+                       if (!p.m_equivs.empty()) verbose_stream() << " :equivs " << p.m_equivs.size();
-                       if (m_probing.m_stopped_at != 0) verbose_stream() << " :stopped-at " << m_probing.m_stopped_at;
+                       verbose_stream() << " :cost " << p.m_counter;
+                       if (p.m_stopped_at != 0) verbose_stream() << " :stopped-at " << p.m_stopped_at;
                        verbose_stream() << mem_stat() << m_watch << ")\n";);
         }
     };
@@ -215,6 +230,8 @@ namespace sat {
         report rpt(*this);
         bool r    = true;
         m_counter = 0;
+        m_equivs.reset();
+        m_big.init(s, true);
         int limit = -static_cast<int>(m_probing_limit);
         unsigned i;
         unsigned num = s.num_vars();
@@ -248,9 +265,26 @@ namespace sat {
         }
         CASSERT("probing", s.check_invariant());
         finalize();
+        if (!m_equivs.empty()) {
+            union_find_default_ctx ctx;
+            union_find<> uf(ctx);
+            for (unsigned i = 2*s.num_vars(); i--> 0; ) uf.mk_var();
+            for (auto const& p : m_equivs) {
+                literal l1 = p.first, l2 = p.second;
+                uf.merge(l1.index(), l2.index());
+                uf.merge((~l1).index(), (~l2).index());
+            }
+            elim_eqs elim(s);
+            elim(uf);
+        }
+        
         return r;
     }
 
+    bool probing::implies(literal a, literal b) {
+        return m_big.connected(a, b);
+    }
+
     void probing::updt_params(params_ref const & _p) {
         sat_simplifier_params p(_p);
         m_probing             = p.probing();

src/sat/sat_probing.h

@@ -21,6 +21,7 @@ Revision History:
 #define SAT_PROBING_H_
 
 #include "sat/sat_types.h"
+#include "sat/sat_big.h"
 #include "util/params.h"
 #include "util/statistics.h"
 
@@ -43,7 +44,7 @@ namespace sat {
         unsigned long long m_probing_cache_limit; // memory limit for enabling caching.
 
         // stats
-        unsigned           m_num_assigned;
+        unsigned           m_num_assigned;        
         
         struct cache_entry {
             bool           m_available;
@@ -60,6 +61,11 @@ namespace sat {
         void process(bool_var v);
         void process_core(bool_var v);
 
+        // learn equivalences from probing.
+        svector<std::pair<literal, literal>> m_equivs;
+        big                                  m_big;
+        bool implies(literal a, literal b);
+
     public:
         probing(solver & s, params_ref const & p);
         

src/util/hash.h

@@ -68,6 +68,10 @@ inline unsigned hash_u_u(unsigned a, unsigned b) {
 
 unsigned string_hash(const char * str, unsigned len, unsigned init_value);
 
+inline unsigned unsigned_ptr_hash(unsigned const* vec, unsigned len, unsigned init_value) {
+    return string_hash((char const*)(vec), len*4, init_value);
+}
+
 template<typename Composite, typename GetKindHashProc, typename GetChildHashProc>
 unsigned get_composite_hash(Composite app, unsigned n, GetKindHashProc const & khasher = GetKindHashProc(), GetChildHashProc const & chasher = GetChildHashProc()) {
     unsigned a, b, c;