bug fixes

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

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -831,15 +831,17 @@ struct pb2bv_rewriter::imp {
             p.get_bool("keep_pb_constraints", false) ||
             p.get_bool("sat.pb.solver", false) ||
             p.get_bool("pb.solver", false) ||
-            gparams::get_module("sat").get_bool("pb.solver", false);
+            gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("solver") ;
     }
 
     bool pb_num_system() const {
-        return m_params.get_bool("pb_num_system", false);
+        return m_params.get_bool("pb_num_system", false) ||
+            gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("sorting");
     }
 
     bool pb_totalizer() const {
-        return m_params.get_bool("pb_totalizer", false);
+        return m_params.get_bool("pb_totalizer", false) ||
+            gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("totalizer");
     }
 
     imp(ast_manager& m, params_ref const& p): 

src/sat/card_extension.cpp

@@ -241,7 +241,7 @@ namespace sat {
 
         if (slack < bound) {
             literal lit = p[j].second;
-            SASSERT(value(p[j].second) == l_false);
+            SASSERT(value(lit) == l_false);
             for (unsigned i = j + 1; i < sz; ++i) {
                 if (lvl(lit) < lvl(p[i].second)) {
                     lit = p[i].second;
@@ -365,7 +365,10 @@ namespace sat {
             literal_vector to_assign;
             while (!m_pb_undef.empty()) {
                 index1 = m_pb_undef.back();
+                if (index1 == num_watch) index1 = index; // it was swapped with index above.
                 literal lit = p[index1].second;
+                if (value(lit) != l_undef) std::cout << "not undef: " << index1 << " " << lit << " " << value(lit) << "\n";
+                SASSERT(value(lit) == l_undef);
                 TRACE("sat", tout << index1 << " " << lit << "\n";);
                 if (slack >= bound + p[index1].first) {
                     break;
@@ -376,9 +379,7 @@ namespace sat {
 
             for (literal lit : to_assign) {
                 if (inconsistent()) break;
-                if (value(lit) == l_undef) {
+                assign(p, lit);
-                    assign(p, lit);
-                }				
             }
         }
 
@@ -594,8 +595,8 @@ namespace sat {
         unsigned sz = x.size();
         TRACE("sat", tout << "assign: " << x.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";);
 
-        SASSERT(value(alit) != l_undef);
         SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
+        SASSERT(value(alit) != l_undef);
         unsigned index = 0;
         for (; index <= 2; ++index) {
             if (x[index].var() == alit.var()) break;
@@ -791,9 +792,7 @@ namespace sat {
                     m_bound += offset;
                     inc_coeff(consequent, offset);
                     get_xor_antecedents(consequent, idx, js, m_lemma);
-                    for (unsigned i = 0; i < m_lemma.size(); ++i) {
+                    for (literal l : m_lemma) process_antecedent(~l, offset);
-                        process_antecedent(~m_lemma[i], offset);
-                    }
                     ++m_stats.m_num_xor_resolves;
                 }
                 else if (is_pb_index(index)) {
@@ -803,9 +802,7 @@ namespace sat {
                     inc_coeff(consequent, offset);
                     get_pb_antecedents(consequent, p, m_lemma);
                     TRACE("sat", display(tout, p, true); tout << m_lemma << "\n";);
-                    for (unsigned i = 0; i < m_lemma.size(); ++i) {
+                    for (literal l : m_lemma) process_antecedent(~l, offset);
-                        process_antecedent(~m_lemma[i], offset);
-                    }
                     ++m_stats.m_num_pb_resolves;
                 }
                 else {
@@ -1063,12 +1060,16 @@ namespace sat {
 
 
     void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
+        SASSERT(value(l) == l_true);
         TRACE("sat", tout << l << " " << idx << "\n";);
         if (is_pb_index(idx)) {
             pb& p = index2pb(idx);
             if (l.var() == p.lit().var()) {
                 init_watch(p, !l.sign());
             }
+            else if (p.lit() != null_literal && value(p.lit()) != l_true) {
+                keep = false;
+            }
             else {
                 keep = l_undef != add_assign(p, ~l);
             }
@@ -1078,6 +1079,9 @@ namespace sat {
             if (l.var() == c.lit().var()) {
                 init_watch(c, !l.sign());
             }
+            else if (c.lit() != null_literal && value(c.lit()) != l_true) {
+                keep = false;
+            }
             else {
                 keep = l_undef != add_assign(c, ~l);
             }
@@ -1087,6 +1091,9 @@ namespace sat {
             if (l.var() == x.lit().var()) {
                 init_watch(x, !l.sign());
             }
+            else if (x.lit() != null_literal && value(x.lit()) != l_true) {
+                keep = false;
+            }
             else {
                 keep = l_undef != add_assign(x, ~l);
             }
@@ -1206,6 +1213,16 @@ namespace sat {
         SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
         TRACE("sat", display(tout, p, true););
 
+        if (value(l) == l_false) {
+            for (wliteral wl : p) {
+                literal lit = wl.second;
+                if (lit != l && value(lit) == l_false) {
+                    r.push_back(~lit);
+                } 
+            }
+            return;
+        }
+
         // unsigned coeff = get_coeff(p, l);
         unsigned coeff = 0;
         for (unsigned j = 0; j < p.num_watch(); ++j) {
@@ -1214,6 +1231,13 @@ namespace sat {
                 break;
             }
         }
+        if (coeff == 0) {
+            
+            std::cout << l << " coeff: " << coeff << "\n";
+            display(std::cout, p, true);                
+        }
+
+        SASSERT(coeff > 0);
         unsigned slack = p.slack() - coeff;
         unsigned i = p.num_watch();
 
@@ -1225,6 +1249,10 @@ namespace sat {
         }
         for (; i < p.size(); ++i) {
             literal lit = p[i].second;
+            if (l_false != value(lit)) {
+                std::cout << l << " index: " << i << " slack: " << slack << " h: " << h << " coeff: " << coeff << "\n";
+                display(std::cout, p, true);                
+            }
             SASSERT(l_false == value(lit));
             r.push_back(~lit);
         }

src/sat/card_extension.h

@@ -82,6 +82,9 @@ namespace sat {
             unsigned index() const { return m_index; }
             literal lit() const { return m_lit; }
             wliteral operator[](unsigned i) const { return m_wlits[i]; }
+            wliteral const* begin() const { return m_wlits; }
+            wliteral const* end() const { return (wliteral const*)m_wlits + m_size; }
+
             unsigned k() const { return m_k; }
             unsigned size() const { return m_size; }
             unsigned slack() const { return m_slack; }

src/sat/sat_config.cpp

@@ -147,6 +147,24 @@ namespace sat {
         m_step_size_min  = 0.06;
         m_reward_multiplier = 0.9;
         m_reward_offset = 1000000.0;
+
+        // PB parameters
+        s = p.pb_solver();
+        if (s == symbol("circuit")) {
+            m_pb_solver = PB_CIRCUIT;
+        }
+        else if (s == symbol("sorting")) {
+            m_pb_solver = PB_SORTING;
+        }
+        else if (s == symbol("totalizer")) {
+            m_pb_solver = PB_TOTALIZER;
+        }
+        else if (s == symbol("solver")) {
+            m_pb_solver = PB_SOLVER;
+        }
+        else {
+            throw sat_param_exception("invalid PB solver");
+        }
     }
 
     void config::collect_param_descrs(param_descrs & r) {

src/sat/sat_config.h

@@ -50,6 +50,13 @@ namespace sat {
         BH_LRB
     };
 
+    enum pb_solver {
+        PB_SOLVER,
+        PB_CIRCUIT,
+        PB_SORTING,
+        PB_TOTALIZER
+    };
+
     struct config {
         unsigned long long m_max_memory;
         phase_selection    m_phase;
@@ -99,7 +106,9 @@ namespace sat {
         symbol             m_psm;        
         symbol             m_glue;        
         symbol             m_glue_psm;        
-        symbol             m_psm_glue;        
+        symbol             m_psm_glue;      
+
+        pb_solver          m_pb_solver;
         
         // branching heuristic settings.
         branching_heuristic m_branching_heuristic;

src/sat/sat_params.pyg

@@ -29,7 +29,7 @@ def_module_params('sat',
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
                           ('drat.check', BOOL, False, 'build up internal proof and check'),
                           ('cardinality.solver', BOOL, False, 'use cardinality solver'),
-                          ('pb.solver', BOOL, False, 'use pb solver'),
+                          ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
 	                  ('xor.solver', BOOL, False, 'use xor solver'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),

src/sat/sat_solver.cpp

@@ -1961,10 +1961,8 @@ namespace sat {
             }
             case justification::EXT_JUSTIFICATION: {
                 fill_ext_antecedents(consequent, js);
-                literal_vector::iterator it  = m_ext_antecedents.begin();
+                for (literal l : m_ext_antecedents) 
-                literal_vector::iterator end = m_ext_antecedents.end();
+                    process_antecedent(l, num_marks);
-                for (; it != end; ++it)
-                    process_antecedent(*it, num_marks);
                 break;
             }
             default:
@@ -2082,10 +2080,9 @@ namespace sat {
         }
         case justification::EXT_JUSTIFICATION: {
             fill_ext_antecedents(consequent, js);
-            literal_vector::iterator it  = m_ext_antecedents.begin();
+            for (literal l : m_ext_antecedents) {
-            literal_vector::iterator end = m_ext_antecedents.end();
+                process_antecedent_for_unsat_core(l);
-            for (; it != end; ++it)
+            }
-                process_antecedent_for_unsat_core(*it);
             break;
         }
         default:
@@ -2199,10 +2196,9 @@ namespace sat {
             SASSERT(not_l != null_literal);
             r = lvl(not_l);
             fill_ext_antecedents(~not_l, js);
-            literal_vector::iterator it  = m_ext_antecedents.begin();
+            for (literal l : m_ext_antecedents) {
-            literal_vector::iterator end = m_ext_antecedents.end();
+                r = std::max(r, lvl(l));
-            for (; it != end; ++it)
+            }
-                r = std::max(r, lvl(*it));
             return r;
         }
         default:
@@ -2414,10 +2410,8 @@ namespace sat {
             case justification::EXT_JUSTIFICATION: {
                 literal consequent(var, value(var) == l_false);
                 fill_ext_antecedents(consequent, js);
-                literal_vector::iterator it  = m_ext_antecedents.begin();
+                for (literal l : m_ext_antecedents) {
-                literal_vector::iterator end = m_ext_antecedents.end();
+                    if (!process_antecedent_for_minimization(l)) {
-                for (; it != end; ++it) {
-                    if (!process_antecedent_for_minimization(*it)) {
                         reset_unmark(old_size);
                         return false;
                     }
@@ -2540,10 +2534,8 @@ namespace sat {
             }
             case justification::EXT_JUSTIFICATION: {
                 fill_ext_antecedents(m_lemma[i], js);
-                literal_vector::iterator it  = m_ext_antecedents.begin();
+                for (literal l : m_ext_antecedents) {
-                literal_vector::iterator end = m_ext_antecedents.end();
+                    update_lrb_reasoned(l);
-                for (; it != end; ++it) {
-                    update_lrb_reasoned(*it);
                 }
                 break;
             }
@@ -3776,11 +3768,9 @@ namespace sat {
         }
         case justification::EXT_JUSTIFICATION: {
             fill_ext_antecedents(lit, js);
-            literal_vector::iterator it  = m_ext_antecedents.begin();
+            for (literal l : m_ext_antecedents) {
-            literal_vector::iterator end = m_ext_antecedents.end();
+                if (check_domain(lit, l) && all_found) {
-            for (; it != end; ++it) {
+                    s |= m_antecedents.find(l.var());
-                if (check_domain(lit, *it) && all_found) {
-                    s |= m_antecedents.find(it->var());
                 }
                 else {
                     all_found = false;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -266,8 +266,10 @@ public:
         m_params.append(p);
         sat_params p1(p);
         m_params.set_bool("elim_vars", false);
-        m_params.set_bool("keep_cardinality_constraints", p1.pb_solver() || p1.cardinality_solver());
+        m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
-        m_params.set_bool("keep_pb_constraints", p1.pb_solver());
+        m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER);
+        m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING);
+        m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
         m_params.set_bool("xor_solver", p1.xor_solver());
         m_solver.updt_params(m_params);
         m_optimize_model = m_params.get_bool("optimize_model", false);

src/util/gparams.cpp

@@ -425,6 +425,8 @@ public:
         return r;
     }
 
+    // unfortunately, params_ref is not thread safe
+    // so better create a local copy of the parameters.
     params_ref get_module(symbol const & module_name) {
         params_ref result;
         params_ref * ps = 0;

src/util/params.cpp

@@ -333,8 +333,21 @@ public:
         reset();
     }
 
-    void inc_ref() { m_ref_count++; }
+    void inc_ref() { 
-    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+        #pragma omp critical (params)
+        {
+            m_ref_count++;         
+        }
+    }
+    void dec_ref() { 
+        bool is_last;
+        SASSERT(m_ref_count > 0); 
+        #pragma omp critical (params)
+        {
+            is_last = 0 == --m_ref_count;         
+        }
+        if (is_last) dealloc(this); 
+    }
 
     bool empty() const { return m_entries.empty(); }
     bool contains(symbol const & k) const;
@@ -344,7 +357,6 @@ public:
     void reset(symbol const & k);
     void reset(char const * k);
 
-
     void validate(param_descrs const & p) {
         svector<params::entry>::iterator it  = m_entries.begin();  
         svector<params::entry>::iterator end = m_entries.end();