merge

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

src/sat/ba_solver.cpp

@@ -1832,6 +1832,7 @@ namespace sat {
 
             SASSERT(coeff > 0);
             unsigned slack = p.slack() - coeff;
+            j = std::max(j + 1, p.num_watch());
             
             for (; j < p.size(); ++j) {
                 literal lit = p[j].second;
@@ -2162,10 +2163,12 @@ namespace sat {
     }
 
     void ba_solver::gc() {
-        for (auto & c : m_learned) update_psm(*c);
-        std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt());
-        gc_half("glue-psm");
-        cleanup_constraints(m_learned, true);
+        if (m_learned.size() >= 2 * m_constraints.size()) {
+            for (auto & c : m_learned) update_psm(*c);
+            std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt());
+            gc_half("glue-psm");
+            cleanup_constraints(m_learned, true);
+        }
     }
 
     void ba_solver::gc_half(char const* st_name) {
@@ -2319,7 +2322,7 @@ namespace sat {
         }        
         while (m_simplify_change || trail_sz < s().init_trail_size());
 
-        IF_VERBOSE(1, verbose_stream() << "(ba.simplify :trail " << trail_sz 
+        IF_VERBOSE(1, verbose_stream() << "(ba.simplify "
                    << " :vars " << s().num_vars() - trail_sz 
                    << " :constraints " << m_constraints.size() 
                    << " :lemmas " << m_learned.size() 
@@ -3178,6 +3181,85 @@ namespace sat {
         return result;
     }
 
+    void ba_solver::init_use_list(ext_use_list& ul) {
+        ul.init(s().num_vars());
+        for (constraint const* cp : m_constraints) {
+            ext_constraint_idx idx = cp->index();
+            if (cp->lit() != null_literal) {
+                ul.insert(cp->lit(), idx);
+                ul.insert(~cp->lit(), idx);                
+            }
+            switch (cp->tag()) {
+            case card_t: {
+                card const& c = cp->to_card();
+                for (literal l : c) {
+                    ul.insert(l, idx);
+                }
+                break;
+            }
+            case pb_t: {
+                pb const& p = cp->to_pb();
+                for (wliteral w : p) {
+                    ul.insert(w.second, idx);
+                }
+                break;
+            }
+            case xor_t: {
+                xor const& x = cp->to_xor();
+                for (literal l : x) {
+                    ul.insert(l, idx);
+                    ul.insert(~l, idx);
+                }
+                break;
+            }
+            default:
+                UNREACHABLE();
+            }                            
+        }
+    }
+
+    //
+    // literal is used in a clause (C or l), it
+    // it occurs negatively in constraint c.
+    // all literals in C are marked
+    // 
+    bool ba_solver::is_blocked(literal l, ext_constraint_idx idx) {
+        constraint const& c = index2constraint(idx);
+        simplifier& sim = s().m_simplifier;
+        if (c.lit() != null_literal) return false;
+        switch (c.tag()) {
+        case card_t: {
+            card const& ca = c.to_card();
+            unsigned weight = 0;
+            for (literal l2 : ca) {
+                if (sim.is_marked(~l2)) ++weight;
+            }
+            return weight >= ca.k();
+        }
+        case pb_t: {
+            pb const& p = c.to_pb();
+            unsigned weight = 0, offset = 0;
+            for (wliteral l2 : p) {
+                if (~l2.second == l) {
+                    offset = l2.first;
+                    break;
+                }
+            }
+            SASSERT(offset != 0);
+            for (wliteral l2 : p) {
+                if (sim.is_marked(~l2.second)) {
+                    weight += std::min(offset, l2.first);
+                }
+            }
+            return weight >= p.k();
+        }
+        default:
+            break;
+        }
+        return false;
+    }
+
+
     void ba_solver::find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {
         literal_set slits(lits);
         bool change = false;

src/sat/ba_solver.h

@@ -449,6 +449,8 @@ namespace sat {
         virtual void gc(); 
         virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const;
         virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r);
+        virtual void init_use_list(ext_use_list& ul);
+        virtual bool is_blocked(literal l, ext_constraint_idx idx);
 
         ptr_vector<constraint> const & constraints() const { return m_constraints; }
 

src/sat/sat_extension.h

@@ -31,8 +31,20 @@ namespace sat {
 
     class literal_occs_fun {
     public:
-        virtual double operator()(literal l) = 0;
-        
+        virtual double operator()(literal l) = 0;        
+    };
+
+
+    typedef svector<ext_constraint_idx> ext_constraint_list;
+
+    class ext_use_list {
+        vector<ext_constraint_list> m_use_list;
+    public:
+        void init(unsigned num_vars) { m_use_list.reset(); m_use_list.resize(num_vars*2); }
+        void insert(literal l, ext_constraint_idx idx) { get(l).push_back(idx); }
+        ext_constraint_list & get(literal l) { return m_use_list[l.index()]; }
+        ext_constraint_list const & get(literal l) const { return m_use_list[l.index()]; }
+        void finalize() { m_use_list.finalize(); }
     };
 
     class extension {
@@ -63,6 +75,8 @@ namespace sat {
         virtual void gc() = 0;
         virtual void pop_reinit() = 0;
         virtual bool validate() = 0;
+        virtual void init_use_list(ext_use_list& ul) = 0;
+        virtual bool is_blocked(literal l, ext_constraint_idx) = 0;
     };
 
 };

src/sat/sat_simplifier.cpp

@@ -70,7 +70,13 @@ namespace sat {
 
     inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
 
-    inline bool simplifier::is_external(bool_var v) const { return s.is_external(v); }
+    inline bool simplifier::is_external(bool_var v) const { 
+        return 
+            s.is_assumption(v) ||
+            (s.is_external(v) && 
+             (!m_ext_use_list.get(literal(v, false)).empty() ||
+              !m_ext_use_list.get(literal(v, true)).empty()));
+    }
 
     inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); }
 
@@ -130,6 +136,7 @@ namespace sat {
         m_visited.finalize();
         m_bs_cs.finalize();
         m_bs_ls.finalize();
+        m_ext_use_list.finalize();
     }
 
     void simplifier::initialize() {
@@ -137,6 +144,7 @@ namespace sat {
         s.m_cleaner(true);
         m_last_sub_trail_sz = s.m_trail.size();
         m_use_list.init(s.num_vars());
+        if (s.m_ext) s.m_ext->init_use_list(m_ext_use_list);
         m_sub_todo.reset();
         m_sub_bin_todo.reset();
         m_elim_todo.reset();
@@ -187,7 +195,7 @@ namespace sat {
                 subsume();
             if (s.inconsistent())
                 return;
-            if (!learned && m_resolution)
+            if (!learned && m_resolution && s.m_config.m_num_threads == 1)
                 elim_vars();
             if (s.inconsistent())
                 return;
@@ -937,7 +945,7 @@ namespace sat {
         }
 
         bool process_var(bool_var v) {
-            return !s.is_external(v) && !s.was_eliminated(v);
+            return !s.s.is_assumption(v) &&  !s.was_eliminated(v);
         }
 
         void operator()(unsigned num_vars) {
@@ -989,7 +997,7 @@ namespace sat {
                     }
                     s.unmark_all(c);
                     it.next();
-                    }
+                }
             }
             for (clause* c : m_to_remove) {
                 s.remove_clause(*c);
@@ -1028,33 +1036,34 @@ namespace sat {
         }
 
         bool all_tautology(literal l) {
-            {
-                watch_list & wlist = s.get_wlist(l);
-                m_counter -= wlist.size();
-                watch_list::iterator it  = wlist.begin();
-                watch_list::iterator end = wlist.end();
-                for (; it != end; ++it) {
-                    if (!it->is_binary_non_learned_clause())
-                        continue;
-                    if (!s.is_marked(~it->get_literal()))
-                        return false;
-                }
+            watch_list & wlist = s.get_wlist(l);
+            m_counter -= wlist.size();
+            for (auto const& w : wlist) {
+                if (w.is_binary_non_learned_clause() && 
+                    !s.is_marked(~w.get_literal()))
+                    return false;
             }
-            {
-                clause_use_list & neg_occs = s.m_use_list.get(~l);
-                clause_use_list::iterator it = neg_occs.mk_iterator();
-                while (!it.at_end()) {
-                    clause & c = it.curr();
-                    m_counter -= c.size();
-                    unsigned sz = c.size();
-                    unsigned i;
-                    for (i = 0; i < sz; i++) {
-                        if (s.is_marked(~c[i]))
-                            break;
-                    }
-                    if (i == sz)
-                        return false;
-                    it.next();
+
+            clause_use_list & neg_occs = s.m_use_list.get(~l);
+            clause_use_list::iterator it = neg_occs.mk_iterator();
+            while (!it.at_end()) {
+                clause & c = it.curr();
+                m_counter -= c.size();
+                unsigned sz = c.size();
+                unsigned i;
+                for (i = 0; i < sz; i++) {
+                    if (s.is_marked(~c[i]))
+                        break;
+                }
+                if (i == sz)
+                    return false;
+                it.next();
+            }
+
+            ext_constraint_list const& ext_list = s.m_ext_use_list.get(~l);
+            for (ext_constraint_idx idx : ext_list) {
+                if (!s.s.m_ext->is_blocked(l, idx)) {
+                    return false;
                 }
             }
             return true;
@@ -1171,8 +1180,8 @@ namespace sat {
         SASSERT(c1.contains(l));
         SASSERT(c2.contains(~l));
         bool res = true;
+        m_elim_counter -= c1.size() + c2.size();
         unsigned sz = c1.size();
-        m_elim_counter -= sz;
         for (unsigned i = 0; i < sz; ++i) {
             literal l2 = c1[i];
             if (l == l2)
@@ -1183,7 +1192,6 @@ namespace sat {
 
         literal not_l = ~l;
         sz = c2.size();
-        m_elim_counter -= sz;
         for (unsigned i = 0; i < sz; ++i) {
             literal l2 = c2[i];
             if (not_l == l2)
@@ -1199,8 +1207,6 @@ namespace sat {
         sz = c1.size();
         for (unsigned i = 0; i < sz; ++i) {
             literal l2 = c1[i];
-            if (l == l2)
-                continue;
             m_visited[l2.index()] = false;
         }
         return res;

src/sat/sat_simplifier.h

@@ -26,6 +26,7 @@ Revision History:
 #include"sat_clause_set.h"
 #include"sat_clause_use_list.h"
 #include"sat_watched.h"
+#include"sat_extension.h"
 #include"sat_model_converter.h"
 #include"heap.h"
 #include"statistics.h"
@@ -51,6 +52,7 @@ namespace sat {
         solver &               s;
         unsigned               m_num_calls;
         use_list               m_use_list;
+        ext_use_list           m_ext_use_list;
         clause_set             m_sub_todo;
         svector<bin_clause>    m_sub_bin_todo;
         unsigned               m_last_sub_trail_sz; // size of the trail since last cleanup