different strategies for weighted

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

src/opt/core_maxsat.cpp

@@ -147,6 +147,9 @@ namespace opt {
     void core_maxsat::collect_statistics(statistics& st) const {
         // nothing specific
     }
+    void core_maxsat::updt_params(params_ref& p) {
+        // no-op
+    }
     void core_maxsat::get_model(model_ref& mdl) {
         mdl = m_model.get();
         if (!mdl) {

src/opt/core_maxsat.h

@@ -43,6 +43,7 @@ namespace opt {
         virtual void set_cancel(bool f);
         virtual void collect_statistics(statistics& st) const;
         virtual void get_model(model_ref& mdl);
+        virtual void updt_params(params_ref& p);
     private:
         void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
         expr_ref mk_at_most(expr_set const& set, unsigned k);

src/opt/fu_malik.cpp

@@ -368,6 +368,10 @@ namespace opt {
         m_imp->get_model(m);
     }
 
+    void fu_malik::updt_params(params_ref& p) {
+        // no-op
+    }
+
 
 
 

src/opt/fu_malik.h

@@ -42,6 +42,7 @@ namespace opt {
         virtual void set_cancel(bool f);
         virtual void collect_statistics(statistics& st) const;
         virtual void get_model(model_ref& m);
+        virtual void updt_params(params_ref& p);
     };
     
 };

src/opt/maxsmt.cpp

@@ -51,6 +51,7 @@ namespace opt {
         }
 
         if (m_msolver) {
+            m_msolver->updt_params(m_params);
             is_sat = (*m_msolver)();
             if (is_sat == l_true) {
                 m_msolver->get_model(m_model);
@@ -149,6 +150,10 @@ namespace opt {
     void maxsmt::updt_params(params_ref& p) {
         opt_params _p(p);
         m_maxsat_engine = _p.maxsat_engine();        
+        m_params = p;
+        if (m_msolver) {
+            m_msolver->updt_params(p);
+        }
     }
 
     void maxsmt::collect_statistics(statistics& st) const {

src/opt/maxsmt.h

@@ -34,6 +34,8 @@ namespace opt {
         virtual void set_cancel(bool f) = 0;
         virtual void collect_statistics(statistics& st) const = 0;
         virtual void get_model(model_ref& mdl) = 0;
+        virtual void updt_params(params_ref& p) = 0;
+
     };
     /**
        Takes solver with hard constraints added.
@@ -52,6 +54,7 @@ namespace opt {
         scoped_ptr<maxsmt_solver> m_msolver;
         symbol           m_maxsat_engine;
         model_ref        m_model;
+        params_ref       m_params;
     public:
         maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
 

src/opt/opt_context.cpp

@@ -193,7 +193,14 @@ namespace opt {
         tactic_ref tac0 = mk_simplify_tactic(m);
         tactic_ref tac1 = mk_elim01_tactic(m);
         tactic_ref tac2 = mk_lia2card_tactic(m);
-        tactic_ref tac  = and_then(tac0.get(), tac1.get(), tac2.get());
+        tactic_ref tac;
+        opt_params optp(m_params);
+        if (optp.elim_01()) {
+            tac = and_then(tac0.get(), tac1.get(), tac2.get());
+        }
+        else {
+            tac = tac0;
+        }
         proof_converter_ref pc;
         expr_dependency_ref core(m);
         goal_ref_buffer result;

src/opt/opt_params.pyg

@@ -8,6 +8,11 @@ def_module_params('opt',
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('print_model', BOOL, False, 'display model for satisfiable constraints'),
                           ('debug_conflict', BOOL, False, 'debug conflict resolution'),
+                          ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'iwmax' (iterative), 'bwmax' (bisection)"),
+                          ('pb_conflict_freq', UINT, 0, 'conflict frequency for pb theory'),
+                          ('pb_learn_comp', BOOL, True, 'learn complement literals'),
+                          ('elim_01', BOOL, True, 'eliminate 01 variables')
+
                           ))
 
 

src/opt/opt_solver.cpp

@@ -18,14 +18,16 @@ Notes:
     Based directly on smt_solver.
    
 --*/
-#include"reg_decl_plugins.h"
+#include "reg_decl_plugins.h"
-#include"opt_solver.h"
+#include "opt_solver.h"
-#include"smt_context.h"
+#include "smt_context.h"
-#include"theory_arith.h"
+#include "theory_arith.h"
-#include"theory_diff_logic.h"
+#include "theory_diff_logic.h"
+#include "theory_pb.h"
 #include "ast_pp.h"
 #include "ast_smt_pp.h"
 #include "pp_params.hpp"
+#include "opt_params.hpp"
 #include "model_smt2_pp.h"
 
 namespace opt {
@@ -46,10 +48,18 @@ namespace opt {
     opt_solver::~opt_solver() {
     }
 
-    void opt_solver::updt_params(params_ref const & p) {
+    void opt_solver::updt_params(params_ref & _p) {
-        m_dump_benchmarks = p.get_bool("dump_benchmarks", false);
+        opt_params p(_p);
-        m_params.updt_params(p);
+        m_dump_benchmarks = p.dump_benchmarks();
-        m_context.updt_params(p);
+        m_params.updt_params(_p);
+        m_context.updt_params(_p);
+        smt::theory_id th_id = m.get_family_id("pb");
+        smt::theory* _th = get_context().get_theory(th_id);               
+        if (_th) {
+            smt::theory_pb* th = dynamic_cast<smt::theory_pb*>(_th);
+            th->set_conflict_frequency(p.pb_conflict_freq());
+            th->set_learn_complements(p.pb_learn_comp());
+        }            
     }
 
     void opt_solver::collect_param_descrs(param_descrs & r) {

src/opt/opt_solver.h

@@ -55,7 +55,7 @@ namespace opt {
         opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
         virtual ~opt_solver();
 
-        virtual void updt_params(params_ref const & p);
+        virtual void updt_params(params_ref & p);
         virtual void collect_param_descrs(param_descrs & r);
         virtual void collect_statistics(statistics & st) const;
         virtual void assert_expr(expr * t);

src/opt/weighted_maxsat.cpp

@@ -20,14 +20,23 @@ Notes:
 #include "smt_theory.h"
 #include "smt_context.h"
 #include "ast_pp.h"
+#include "opt_params.hpp"
+#include "pb_decl_plugin.h"
 
 namespace smt {
 
     class theory_weighted_maxsat : public theory {
+        struct stats {
+            unsigned m_num_blocks;
+            void reset() { memset(this, 0, sizeof(*this)); }
+            stats() { reset(); }
+        };
+        
         opt::opt_solver&         s;
         app_ref_vector           m_vars;       // Auxiliary variables per soft clause
         expr_ref_vector          m_fmls;       // Formulas per soft clause
         app_ref                  m_min_cost_atom; // atom tracking modified lower bound
+        app_ref_vector           m_min_cost_atoms;
         bool_var                 m_min_cost_bv;   // max cost Boolean variable
         vector<rational>         m_weights;    // weights of theory variables.
         svector<theory_var>      m_costs;      // set of asserted theory variables
@@ -38,6 +47,7 @@ namespace smt {
         svector<bool_var>        m_var2bool;   // theory_var -> bool_var
         bool                     m_propagate;  
         svector<bool>            m_assigned;
+        stats                    m_stats;
 
     public:
         theory_weighted_maxsat(ast_manager& m, opt::opt_solver& s):
@@ -46,6 +56,7 @@ namespace smt {
             m_vars(m),
             m_fmls(m),
             m_min_cost_atom(m),
+            m_min_cost_atoms(m),
             m_propagate(false)
         {}
 
@@ -88,41 +99,8 @@ namespace smt {
             bool initialized = !m_var2bool.empty();
             m_propagate = true;
 
-            for (unsigned i = 0; !initialized && i < m_vars.size(); ++i) {
+            for (unsigned i = 0; i < m_min_cost_atoms.size(); ++i) {
-                app* var = m_vars[i].get();  
+                app* var = m_min_cost_atoms[i].get();
-                bool_var bv;
-                theory_var v;
-                SASSERT(!ctx.e_internalized(var));
-                enode* x = ctx.mk_enode(var, false, true, true);
-                if (ctx.b_internalized(var)) {
-                    bv = ctx.get_bool_var(var);
-                }
-                else {
-                    bv = ctx.mk_bool_var(var);
-                }
-                ctx.set_var_theory(bv, get_id());                    
-                ctx.set_enode_flag(bv, true);
-                v = mk_var(x);
-                ctx.attach_th_var(x, this, v);
-                m_bool2var.insert(bv, v);
-                SASSERT(v == m_var2bool.size());
-                SASSERT(i == v);
-                m_var2bool.push_back(bv);
-                SASSERT(ctx.bool_var2enode(bv));
-            }
-
-            if (!initialized && m_min_cost_atom) {
-                app* var = m_min_cost_atom;
-                if (!ctx.e_internalized(var)) {
-                    ctx.mk_enode(var, false, true, true);
-                }
-                if (ctx.b_internalized(var)) {
-                    m_min_cost_bv = ctx.get_bool_var(var);
-                }
-                else {
-                    m_min_cost_bv = ctx.mk_bool_var(var);
-                }                
-                ctx.set_enode_flag(m_min_cost_bv, true);
             }
         }
 
@@ -139,6 +117,33 @@ namespace smt {
             m_fmls.push_back(fml);
             m_assigned.push_back(false);
             m_min_cost += w;
+            
+            register_var(var, true);
+        }
+
+        bool_var register_var(app* var, bool attach) {
+            context & ctx = get_context();
+            ast_manager& m = get_manager();
+            bool_var bv;
+            SASSERT(!ctx.e_internalized(var));
+            enode* x = ctx.mk_enode(var, false, true, true);
+            if (ctx.b_internalized(var)) {
+                bv = ctx.get_bool_var(var);
+            }
+            else {
+                bv = ctx.mk_bool_var(var);
+            }
+            ctx.set_enode_flag(bv, true);
+            if (attach) {
+                ctx.set_var_theory(bv, get_id());                    
+                theory_var v = mk_var(x);
+                ctx.attach_th_var(x, this, v);
+                m_bool2var.insert(bv, v);
+                SASSERT(v == m_var2bool.size());
+                m_var2bool.push_back(bv);
+                SASSERT(ctx.bool_var2enode(bv));
+            }
+            return bv;
         }
 
         rational const& get_min_cost() const { 
@@ -151,7 +156,11 @@ namespace smt {
             strm << "cost <= " << c;
             m_min_cost = c; 
             m_min_cost_atom = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort());
+            m_min_cost_atoms.push_back(m_min_cost_atom);
             s.mc().insert(m_min_cost_atom->get_decl());
+
+            m_min_cost_bv = register_var(m_min_cost_atom, false);
+
             return m_min_cost_atom;
         }
 
@@ -206,8 +215,10 @@ namespace smt {
             m_bool2var.reset();
             m_var2bool.reset();
             m_min_cost_atom = 0;
+            m_min_cost_atoms.reset();
             m_propagate = false;
             m_assigned.reset();
+            m_stats.reset();
         }
 
         virtual theory * mk_fresh(context * new_ctx) { return 0; }
@@ -216,6 +227,10 @@ namespace smt {
         virtual void new_eq_eh(theory_var v1, theory_var v2) { }
         virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
 
+        virtual void collect_statistics(::statistics & st) const {
+            st.update("wmaxsat num blocks", m_stats.m_num_blocks);
+        }
+
         virtual bool can_propagate() {
             return m_propagate;
         }
@@ -253,7 +268,7 @@ namespace smt {
                 disj.push_back(m.mk_not(m_min_cost_atom));
             }
             if (is_optimal()) {
-                IF_VERBOSE(1, verbose_stream() << "(wmaxsat with lower bound: " << weight << ")\n";);
+                IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << weight << ")\n";);
                 m_min_cost = weight;
                 m_cost_save.reset();
                 m_cost_save.append(m_costs);
@@ -281,6 +296,7 @@ namespace smt {
             if (m_vars.empty()) {
                 return;
             }
+            ++m_stats.m_num_blocks;
             ast_manager& m = get_manager();
             context& ctx = get_context();
             literal_vector lits;
@@ -317,43 +333,12 @@ namespace smt {
                 return m_th.m_weights[v] > m_th.m_weights[w]; 
             }
         };
-
-
     };
 
 }
 
 namespace opt {
 
-    /**
-       Iteratively increase cost until there is an assignment during
-       final_check that satisfies min_cost.
-
-       Takes: log (n / log(n)) iterations
-    */
-
-    static lbool iterative_weighted_maxsat(opt_solver& s, smt::theory_weighted_maxsat& wth) {
-        ast_manager& m = s.get_context().get_manager();
-        rational cost = wth.get_min_cost();
-        rational log_cost(1), tmp(1);
-        while (tmp < cost) {
-            ++log_cost;
-            tmp *= rational(2);
-        }
-        expr_ref_vector bounds(m);
-        expr_ref bound(m);
-        lbool result = l_false;
-        while (log_cost <= cost && !wth.found_solution() && result != l_undef) {
-            std::cout << "cost: " << log_cost << "\n";
-            bound = wth.set_min_cost(log_cost);
-            bounds.push_back(bound);
-            result = s.check_sat_core(1,bounds.c_ptr()+bounds.size()-1);
-            log_cost *= rational(2);
-        }
-        return result;
-    }
-
-
     struct wmaxsmt::imp {
         ast_manager&     m;
         opt_solver&      s;
@@ -363,6 +348,7 @@ namespace opt {
         rational         m_upper;
         rational         m_lower;
         model_ref        m_model;
+        symbol           m_engine;
         volatile bool    m_cancel;
 
         imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights):
@@ -403,44 +389,17 @@ namespace opt {
         */
         
         lbool operator()() {
-            TRACE("opt", tout << "weighted maxsat\n";);
+            if (m_engine == symbol("iwmax")) {
-            smt::theory_weighted_maxsat& wth = ensure_theory();
+                return iterative_solve();
-            lbool is_sat = l_true;
-            {
-                solver::scoped_push _s(s);
-                bool was_sat = false;
-                for (unsigned i = 0; i < m_soft.size(); ++i) {
-                    wth.assert_weighted(m_soft[i].get(), m_weights[i]);
-                }
-                while (l_true == is_sat) {
-                    is_sat = s.check_sat_core(0,0);
-                    if (m_cancel) {
-                        is_sat = l_undef;
-                    }
-                    if (is_sat == l_true) {
-                        if (wth.is_optimal()) {
-                            s.get_model(m_model);
-                        }
-                        expr_ref fml = wth.mk_block();
-                        s.assert_expr(fml);
-                        was_sat = true;
-                    }
-                }
-                if (was_sat) {
-                    wth.get_assignment(m_assignment);
-                }
-                if (is_sat == l_false && was_sat) {
-                    is_sat = l_true;
-                }
             }
-            m_upper = wth.get_min_cost();
+            if (m_engine == symbol("bwmax")) {
-            if (is_sat == l_true) {
+                return bisection_solve();
-                m_lower = m_upper;
             }
-            TRACE("opt", tout << "min cost: " << m_upper << "\n";);
+            if (m_engine == symbol("pwmax")) {
-            wth.reset();
+                return pb_solve();
-            return is_sat;            
+            }
-        }        
+            return incremental_solve();
+        }
 
         rational get_lower() const {
             return m_lower;
@@ -454,6 +413,219 @@ namespace opt {
             mdl = m_model.get();
         }
 
+
+
+        lbool incremental_solve() {
+            TRACE("opt", tout << "weighted maxsat\n";);
+            smt::theory_weighted_maxsat& wth = ensure_theory();
+            solver::scoped_push _s(s);
+            lbool is_sat = l_true;
+            bool was_sat = false;
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                wth.assert_weighted(m_soft[i].get(), m_weights[i]);
+            }
+            solver::scoped_push __s(s);
+            while (l_true == is_sat) {
+                is_sat = s.check_sat_core(0,0);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                if (is_sat == l_true) {
+                    if (wth.is_optimal()) {
+                        s.get_model(m_model);
+                    }
+                    expr_ref fml = wth.mk_block();
+                    s.assert_expr(fml);
+                    was_sat = true;
+                }
+            }
+            if (was_sat) {
+                wth.get_assignment(m_assignment);
+            }
+            if (is_sat == l_false && was_sat) {
+                is_sat = l_true;
+            }
+            m_upper = wth.get_min_cost();
+            if (is_sat == l_true) {
+                m_lower = m_upper;
+            }
+            TRACE("opt", tout << "min cost: " << m_upper << "\n";);
+            return is_sat;            
+        }        
+
+        /**
+           Iteratively increase cost until there is an assignment during
+           final_check that satisfies min_cost.
+           
+           Takes: log (n / log(n)) iterations
+        */
+        
+        lbool iterative_solve() {
+            smt::theory_weighted_maxsat& wth = ensure_theory();
+            solver::scoped_push _s(s);
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                wth.assert_weighted(m_soft[i].get(), m_weights[i]);
+            }
+            solver::scoped_push __s(s);
+            rational cost = wth.get_min_cost();
+            rational log_cost(1), tmp(1);
+            while (tmp < cost) {
+                ++log_cost;
+                tmp *= rational(2);
+            }
+            expr_ref_vector bounds(m);
+            expr_ref bound(m);
+            lbool result = l_false;
+            unsigned nsc = 0;
+            m_upper = cost;
+            while (log_cost <= cost && result == l_false) {
+                bound = wth.set_min_cost(log_cost);
+                s.push_core();
+                ++nsc;
+                IF_VERBOSE(1, verbose_stream() << "(wmaxsat.iwmax min cost: " << log_cost << ")\n";);
+                TRACE("opt", tout << "cost: " << log_cost << " " << bound << "\n";);
+                bounds.push_back(bound);
+                result = conditional_solve(bound);
+                if (result == l_false) {
+                    m_lower = log_cost;        
+                }
+                log_cost *= rational(2);
+                if (m_cancel) {
+                    result = l_undef;
+                }
+            }
+            s.pop_core(nsc);
+            return result;
+        }
+
+        lbool conditional_solve(expr* cond) {
+            smt::theory_weighted_maxsat& wth = *get_theory();
+            bool was_sat = false;
+            lbool is_sat = l_true;
+            while (l_true == is_sat) {
+                is_sat = s.check_sat_core(1,&cond);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                if (is_sat == l_true) {
+                    if (wth.is_optimal()) {
+                        s.get_model(m_model);
+                        was_sat = true;
+                    }
+                    expr_ref fml = wth.mk_block();
+                    s.assert_expr(fml);
+                }
+            }
+            if (was_sat) {
+                wth.get_assignment(m_assignment);
+            }
+            if (is_sat == l_false && was_sat) {
+                is_sat = l_true;
+            }
+            if (is_sat == l_true) {
+                m_lower = m_upper = wth.get_min_cost();
+            }
+            TRACE("opt", tout << "min cost: " << m_upper << "\n";);
+            return is_sat;            
+        }
+
+        lbool bisection_solve() {
+            TRACE("opt", tout << "weighted maxsat\n";);
+            smt::theory_weighted_maxsat& wth = ensure_theory();
+            solver::scoped_push _s(s);
+            lbool is_sat = l_true;
+            bool was_sat = false;
+            expr_ref_vector bounds(m);
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                wth.assert_weighted(m_soft[i].get(), m_weights[i]);
+            }
+            solver::scoped_push __s(s);
+            m_lower = rational::zero();
+            m_upper = wth.get_min_cost();
+            while (m_lower < m_upper) {
+                rational cost = div(m_upper + m_lower, rational(2));
+                bounds.push_back(wth.set_min_cost(cost));
+                is_sat = s.check_sat_core(1,bounds.c_ptr()+bounds.size()-1);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                switch(is_sat) {
+                case l_true: {
+                    if (wth.is_optimal()) {
+                        s.get_model(m_model);
+                    }
+                    expr_ref fml = wth.mk_block();
+                    s.assert_expr(fml);
+                    m_upper = wth.get_min_cost();
+                    break;
+                }
+                case l_false: {
+                    m_lower = cost;
+                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bwmax min cost: " << m_lower << ")\n";);
+                    break;
+                }
+                case l_undef:
+                    return l_undef;
+                }                
+            }
+            if (was_sat) {
+                is_sat = l_true;
+            }
+            return is_sat;
+        }
+
+        // convert bounds constraint into pseudo-Boolean
+
+        lbool pb_solve() {
+            pb_util u(m);
+            expr_ref fml(m), val(m);
+            expr_ref_vector nsoft(m);
+            m_lower = m_upper = rational::zero();
+            rational minw(0);
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                m_upper += m_weights[i];
+                if (m_weights[i] < minw || minw.is_zero()) {
+                    minw = m_weights[i];
+                }
+                nsoft.push_back(m.mk_not(m_soft[i].get()));
+            }
+            solver::scoped_push __s(s);
+            lbool is_sat = l_true;
+            bool was_sat = false;
+            while (l_true == is_sat) {
+                is_sat = s.check_sat_core(0,0);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                if (is_sat == l_true) {
+                    s.get_model(m_model);
+                    m_upper = rational::zero();
+                    for (unsigned i = 0; i < m_soft.size(); ++i) {
+                        VERIFY(m_model->eval(m_soft[i].get(), val));
+                        m_assignment[i] = !m.is_false(val);
+                        if (!m_assignment[i]) {
+                            m_upper += m_weights[i];
+                        }
+                    }
+                    
+                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";);
+                    fml = u.mk_le(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper - minw);
+                    s.assert_expr(fml);
+                    was_sat = true;
+                }
+            }            
+            if (is_sat == l_false && was_sat) {
+                is_sat = l_true;
+                m_lower = m_upper;
+            }
+            return is_sat;
+        }
+
+        void updt_params(params_ref& p) {
+            opt_params _p(p);
+            m_engine = _p.wmaxsat_engine();        
+        }
+
     };
 
     wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
@@ -486,8 +658,9 @@ namespace opt {
         m_imp->get_model(mdl);
     }
 
-
+    void wmaxsmt::updt_params(params_ref& p) {
-    
+        m_imp->updt_params(p);
+    }    
 
 };
 

src/opt/weighted_maxsat.h

@@ -40,6 +40,7 @@ namespace opt {
         virtual void set_cancel(bool f);
         virtual void collect_statistics(statistics& st) const;
         virtual void get_model(model_ref& mdl);
+        virtual void updt_params(params_ref& p);
     };
 };
 

src/smt/smt_context.cpp

@@ -1334,6 +1334,7 @@ namespace smt {
         TRACE("propagate_bool_var_enode_bug", tout << "var: " << v << " #" << bool_var2expr(v)->get_id() << "\n";);
         SASSERT(v < static_cast<int>(m_b_internalized_stack.size()));
         enode * n  = bool_var2enode(v);
+        CTRACE("mk_bool_var", !n, tout << "No enode for " << v << "\n";);
         bool sign  = val == l_false;
         if (n->merge_tf())
             add_eq(n, sign ? m_false_enode : m_true_enode, eq_justification(literal(v, sign)));

src/smt/theory_pb.cpp

@@ -328,7 +328,9 @@ namespace smt {
     theory_pb::theory_pb(ast_manager& m):
         theory(m.mk_family_id("pb")),
         m_util(m),
-        m_lemma(null_literal)
+        m_lemma(null_literal),
+        m_learn_complements(false),
+        m_conflict_frequency(0xF)
     {}
 
     theory_pb::~theory_pb() {
@@ -716,10 +718,11 @@ namespace smt {
         
         numeral k = c.k();
         numeral coeff = c.coeff(w);
-        
+        bool add_more = c.watch_sum() - coeff < k + c.max_watch();
-        for (unsigned i = c.watch_size(); c.watch_sum() - coeff < k + c.max_watch() && i < c.size(); ++i) {
+        for (unsigned i = c.watch_size(); add_more && i < c.size(); ++i) {
             if (ctx.get_assignment(c.lit(i)) != l_false) {
                 add_watch(c, i);
+                add_more = c.watch_sum() - coeff < k + c.max_watch();
             }
         }        
         
@@ -750,8 +753,9 @@ namespace smt {
                 
                 literal_vector& lits = get_unhelpful_literals(c, true);
                 lits.push_back(c.lit());
+                numeral deficit = c.watch_sum() - k;
                 for (unsigned i = 0; i < c.size(); ++i) {
-                    if (c.watch_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
+                    if (ctx.get_assignment(c.lit(i)) == l_undef && deficit < c.coeff(i)) {
                         DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
                         add_assign(c, lits, c.lit(i));                            
                     }
@@ -1044,12 +1048,18 @@ namespace smt {
               tout << "\n";
               display(tout, c, true););
 
-        if (true || (c.m_num_propagations & 0xF) == 0) {
+        justification* js = 0;
+
+        if (m_conflict_frequency == 0 || (0 == (c.m_num_propagations % m_conflict_frequency))) {
             resolve_conflict(c);
         }
 
-        justification* js = 0;
         ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
+
+        //        if (true || (c.m_num_propagations & 0xF) == 0) {
+        //    resolve_conflict(c);
+        //}
+
     }
 
 
@@ -1090,7 +1100,7 @@ namespace smt {
 
         if (ctx.get_assignment(l) != l_false) {
             m_lemma.m_k -= coeff;
-            if (true && false && is_marked(v)) {
+            if (m_learn_complements && is_marked(v)) {
                 SASSERT(ctx.get_assignment(l) == l_true);
                 numeral& lcoeff = m_lemma.m_args[m_conseq_index[v]].second; 
                 lcoeff -= coeff;

src/smt/theory_pb.h

@@ -111,6 +111,8 @@ namespace smt {
         pb_util                  m_util;
         stats                    m_stats;
         ptr_vector<ineq>         m_to_compile;  // inequalities to compile.
+        unsigned                 m_conflict_frequency;
+        bool                     m_learn_complements;
 
         // internalize_atom:
         literal compile_arg(expr* arg);
@@ -189,5 +191,8 @@ namespace smt {
         virtual void collect_statistics(::statistics & st) const;
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & m);        
+
+        void set_conflict_frequency(unsigned f) { m_conflict_frequency = f; }
+        void set_learn_complements(bool l) { m_learn_complements = l; }
     };
 };