working on pre-processing

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

src/ast/pb_decl_plugin.h

@@ -89,14 +89,14 @@ public:
     bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); }
     bool is_at_least_k(app *a, rational& k) const;
     rational get_k(func_decl *a) const;
-    rational get_k(app *a) const { return get_k(a->get_decl()); }
+    rational get_k(expr *a) const { return get_k(to_app(a)->get_decl()); }
     bool is_le(func_decl *a) const;
     bool is_le(expr *a) const { return is_app(a) && is_le(to_app(a)->get_decl()); }
     bool is_le(app* a, rational& k) const;
     bool is_ge(func_decl* a) const;
     bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); }
     bool is_ge(app* a, rational& k) const;
-    rational get_coeff(app* a, unsigned index) const { return get_coeff(a->get_decl(), index); }
+    rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); }
     rational get_coeff(func_decl* a, unsigned index) const; 
 private:
     rational to_rational(parameter const& p) const;

src/ast/rewriter/pb_rewriter_def.h

@@ -36,7 +36,7 @@ void pb_rewriter_util<PBU>::display(std::ostream& out, typename PBU::args_t& arg
 template<typename PBU>
 void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::numeral& k) {
     
-    TRACE("pb", display(tout << "pre-unique:", args, k););
+    TRACE("pb_verbose", display(tout << "pre-unique:", args, k););
     for (unsigned i = 0; i < args.size(); ++i) {
         if (m_util.is_negated(args[i].first)) {
             args[i].first = m_util.negate(args[i].first);
@@ -73,9 +73,7 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
             args[i] = args[j];
         }
     }
-    if (i + 1 < args.size()) {
     args.resize(i+1);
-    }
 
     // remove 0s.
     for (i = 0, j = 0; j < args.size(); ++j) {
@@ -86,22 +84,22 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
             ++i;
         }
     }
-    if (i < args.size()) {
     args.resize(i);
-    }
+    TRACE("pb_verbose", display(tout << "post-unique:", args, k););
-    TRACE("pb", display(tout << "post-unique:", args, k););
 }
 
 template<typename PBU>
 lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k) {
-    TRACE("pb", display(tout << "pre-normalize:", args, k););
+    TRACE("pb_verbose", display(tout << "pre-normalize:", args, k););
 
+    DEBUG_CODE(
         bool found = false;
         for (unsigned i = 0; !found && i < args.size(); ++i) {
             found = args[i].second.is_zero();
         }
-    if (found) display(std::cout, args, k);
+        if (found) display(verbose_stream(), args, k);
-    SASSERT(!found);
+        SASSERT(!found););
+
     // 
     // Ensure all coefficients are positive:
     //    c*l + y >= k 

src/opt/opt_context.cpp

@@ -116,8 +116,8 @@ namespace opt {
         mdl = m_model;
         if (m_model_converter) {
             (*m_model_converter)(mdl, 0);
-            get_solver().mc()(mdl, 0);
         }
+        get_solver().mc()(mdl, 0);
     }
 
     lbool context::execute_min_max(unsigned index, bool committed) {

src/opt/opt_solver.cpp

@@ -124,11 +124,10 @@ namespace opt {
             std::stringstream file_name;
             file_name << "opt_solver" << ++m_dump_count << ".smt2";
             std::ofstream buffer(file_name.str().c_str());
-            to_smt2_benchmark(buffer, "opt_solver", "");
+            to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver", "");
             buffer.close();
         }
-        lbool r = m_context.check(num_assumptions, assumptions);
+        return m_context.check(num_assumptions, assumptions);
-        return r;
     }
 
     void opt_solver::maximize_objectives() {
@@ -257,7 +256,9 @@ namespace opt {
     }
 
     
-    void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, 
+    void opt_solver::to_smt2_benchmark(std::ofstream & buffer, 
+                                       unsigned num_assumptions, expr * const * assumptions,
+                                       char const * name, char const * logic, 
                                        char const * status, char const * attributes) {        
         ast_smt_pp pp(m);
         pp.set_benchmark_name(name);
@@ -266,10 +267,14 @@ namespace opt {
         pp.add_attributes(attributes);
         pp_params params;
         pp.set_simplify_implies(params.simplify_implies());
-        for (unsigned i = 0; i < get_num_assertions(); ++i) {
+
-            pp.add_assumption(to_expr(get_assertion(i)));
+        for (unsigned i = 0; i < num_assumptions; ++i) {
+            pp.add_assumption(assumptions[i]);
         }
-        pp.display_smt2(buffer, to_expr(m.mk_true()));        
+        for (unsigned i = 0; i < get_num_assertions(); ++i) {
+            pp.add_assumption(get_assertion(i));
+        }
+        pp.display_smt2(buffer, m.mk_true());        
     }
 
 

src/opt/opt_solver.h

@@ -92,7 +92,9 @@ namespace opt {
         
         smt::theory_opt& get_optimizer();
 
-        void to_smt2_benchmark(std::ofstream & buffer, char const * name = "benchmarks", 
+        void to_smt2_benchmark(std::ofstream & buffer, 
+                               unsigned num_assumptions, expr * const * assumptions,
+                               char const * name = "benchmarks", 
                                char const * logic = "", char const * status = "unknown", char const * attributes = "");
     };
 }

src/opt/weighted_maxsat.cpp

@@ -23,6 +23,11 @@ Notes:
 #include "opt_params.hpp"
 #include "pb_decl_plugin.h"
 #include "uint_set.h"
+#include "pb_preprocess_tactic.h"
+#include "simplify_tactic.h"
+#include "tactical.h"
+#include "tactic.h"
+#include "model_smt2_pp.h"
 
 namespace smt {
 
@@ -637,6 +642,53 @@ namespace opt {
             return is_sat;
         }
 
+        lbool pb_simplify_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 _s1(s);
+            lbool is_sat = l_true;
+            bool was_sat = false;
+            fml = m.mk_true();
+            while (l_true == is_sat) {
+                solver::scoped_push _s2(s);
+                s.assert_expr(fml);
+                is_sat = simplify_and_check_sat(0,0);
+                if (m_cancel) {
+                    is_sat = l_undef;
+                }
+                if (is_sat == l_true) {
+                    rational old_upper = m_upper;
+                    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);
+                    was_sat = true;
+                }
+            }            
+            if (is_sat == l_false && was_sat) {
+                is_sat = l_true;
+                m_lower = m_upper;
+            }
+            return is_sat;
+        }
+
+
         lbool wpm2_solve() {
             solver::scoped_push _s(s);
             pb_util u(m);
@@ -645,6 +697,7 @@ namespace opt {
             expr_ref_vector block(m), ans(m), al(m), am(m);
             m_lower = m_upper = rational::zero();
             obj_map<expr, unsigned> ans_index;
+
             vector<rational> amk;
             vector<uint_set> sc;
             for (unsigned i = 0; i < m_soft.size(); ++i) {
@@ -804,7 +857,7 @@ namespace opt {
             }            
             m_imp = alloc(imp, m, m_solver, nbs, ws); // race condition.
             m_imp->updt_params(m_params);
-            lbool is_sat = m_imp->pb_solve();
+            lbool is_sat = m_imp->pb_simplify_solve();
             k = m_imp->m_lower;
             m_solver.pop_core(1);
             return is_sat;
@@ -819,6 +872,49 @@ namespace opt {
             }
         }
 
+        lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) {
+            lbool is_sat = l_true;
+            tactic_ref tac1 = mk_simplify_tactic(m);
+            tactic_ref tac2 = mk_pb_preprocess_tactic(m); 
+            tactic_ref tac  = and_then(tac1.get(), tac2.get());  // TBD: make attribute for cancelation.
+            proof_converter_ref pc;
+            expr_dependency_ref core(m);
+            model_converter_ref mc;
+            goal_ref_buffer result;
+            goal_ref g(alloc(goal, m, true, false));
+            for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
+                g->assert_expr(s.get_assertion(i));
+            }
+            for (unsigned i = 0; i < n; ++i) {
+                NOT_IMPLEMENTED_YET();
+                // add assumption in a wrapper.
+            }
+            (*tac)(g, result, mc, pc, core);
+            if (result.empty()) {
+                is_sat = l_false;
+            }
+            else {
+                SASSERT(result.size() == 1);
+                goal* r = result[0];
+                solver::scoped_push _s(m_solver);
+                // TBD ptr_vector<expr> asms;
+                for (unsigned i = 0; i < r->size(); ++i) {
+                    // TBD collect assumptions from r
+                    m_solver.assert_expr(r->form(i));
+                }
+                is_sat = m_solver.check_sat_core(0, 0);
+                if (l_true == is_sat) {
+                    m_solver.get_model(m_model);
+                    if (mc) (*mc)(m_model, 0);
+                    IF_VERBOSE(2, 
+                               g->display(verbose_stream() << "goal:\n");
+                               r->display(verbose_stream() << "reduced:\n");
+                               model_smt2_pp(verbose_stream(), m, *m_model, 0););
+                }
+            }
+            return is_sat;
+        }
+
     };
 
     wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {

src/smt/theory_pb.cpp

@@ -168,8 +168,6 @@ namespace smt {
         bool_var abv = ctx.mk_bool_var(atom);
         ctx.set_var_theory(abv, get_id());
 
-        IF_VERBOSE(3, verbose_stream() << mk_pp(atom, m) << "\n";);
-
         ineq* c = alloc(ineq, literal(abv));
         c->m_k = m_util.get_k(atom);
         numeral& k = c->m_k;
@@ -192,21 +190,19 @@ namespace smt {
         else {
             SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom));
         }
-        TRACE("pb", display(tout, *c););
         c->unique();
         lbool is_true = c->normalize();
         c->prune();
-        TRACE("pb", display(tout, *c););
 
         literal lit(abv);
 
+        TRACE("pb", display(tout << mk_pp(atom, m), *c); tout << " := " << lit << "\n";);        
         switch(is_true) {
         case l_false: 
             lit = ~lit;
             // fall-through
         case l_true: 
             ctx.mk_th_axiom(get_id(), 1, &lit);
-            TRACE("pb", tout << mk_pp(atom, m) << " := " << lit << "\n";);
             dealloc(c);
             return true;
         case l_undef: 
@@ -1246,14 +1242,12 @@ namespace smt {
                 sum += c.coeff(i);
             }
         }
-        if (sum >= c.k()) {
+        CTRACE("pb", (sum >= c.k()),
-            IF_VERBOSE(0, 
+               display(tout << "invalid assign" , c, true);
-                       display(verbose_stream(), c, true);
                for (unsigned i = 0; i < lits.size(); ++i) {
-                           verbose_stream() << lits[i] << " ";
+                   tout << lits[i] << " ";
-                       }
-                       verbose_stream() << " => " << l << "\n";);
                }
+               tout << " => " << l << "\n";);
         SASSERT(sum < c.k());
     }
 

src/tactic/core/pb_preprocess_tactic.cpp

@@ -16,6 +16,20 @@ Author:
 
 Notes:
 
+    Resolution for PB constraints require the implicit 
+    inequalities that each variable ranges over [0,1]
+    so not all resolvents produce smaller sets of clauses.
+
+    We here implement subsumption resolution.  
+
+    x + y >= 1
+    A~x + B~y + Cz >= k
+    ---------------------
+    Cz >= k - B    
+
+    where A <= B, x, y do not occur elsewhere.    
+
+
 --*/
 #include "pb_preprocess_tactic.h"
 #include "tactical.h"
@@ -25,30 +39,100 @@ Notes:
 #include "expr_substitution.h"
 #include "ast_pp.h"
 
+class pb_preproc_model_converter : public model_converter {
+    ast_manager& m;
+    pb_util      pb;
+    expr_ref_vector                  m_refs;
+    svector<std::pair<app*, expr*> > m_const;
+
+public:
+    pb_preproc_model_converter(ast_manager& m):m(m), pb(m), m_refs(m) {}
+
+    virtual void operator()(model_ref & mdl, unsigned goal_idx) {
+        SASSERT(goal_idx == 0);
+        for (unsigned i = 0; i < m_const.size(); ++i) {
+            mdl->register_decl(m_const[i].first->get_decl(), m_const[i].second);
+        }
+    }
+
+    void set_value(app* e, expr* v) {
+        SASSERT(e->get_num_args() == 0);  
+        SASSERT(is_uninterp_const(e));
+        m_const.push_back(std::make_pair(e, v));
+        m_refs.push_back(e);
+        m_refs.push_back(v);
+    }
+
+    void set_value(expr* e, bool p) {
+        if (m.is_not(e, e)) {
+            set_value(e, !p);
+        }
+        else {
+            SASSERT(is_app(e));
+            set_value(to_app(e), p?m.mk_true():m.mk_false());
+        }
+    }
+
+    virtual model_converter * translate(ast_translation & translator) {
+        pb_preproc_model_converter* mc = alloc(pb_preproc_model_converter, translator.to());
+        for (unsigned i = 0; i < m_const.size(); ++i) {
+            mc->set_value(translator(m_const[i].first), translator(m_const[i].second));
+        }
+        return mc;
+    }
+
+};
+
 class pb_preprocess_tactic : public tactic {
     struct rec { unsigned_vector pos, neg; rec() { } };
-    typedef obj_map<expr, rec> var_map;
+    typedef obj_map<app, rec> var_map;
     ast_manager&     m;
     pb_util          pb;
     var_map          m_vars;    
     unsigned_vector  m_ge;
     unsigned_vector  m_other;
+    bool             m_progress;
     th_rewriter      m_r;
     
 
     struct declassifier {
-        obj_map<expr, rec>& m_vars;        
+        var_map& m_vars;        
-        declassifier(obj_map<expr, rec>& v): m_vars(v) {}
+        declassifier(var_map& v): m_vars(v) {}
 
         void operator()(app* e) {
             if (m_vars.contains(e)) {
                 m_vars.remove(e);
             }
         }
-        void operator()(var* e) {}
+        void operator()(var*) {}
-        void operator()(quantifier* q) {}
+        void operator()(quantifier*) {}
     };
 
+    void display_annotation(std::ostream& out, goal_ref const& g) {
+        for (unsigned i = 0; i < m_ge.size(); ++i) {
+            out << "ge " << m_ge[i] << ": " << mk_pp(g->form(m_ge[i]), m) << "\n";
+        }
+        for (unsigned i = 0; i < m_other.size(); ++i) {
+            out << "ot " << m_other[i] << ": " << mk_pp(g->form(m_other[i]), m) << "\n";
+        }
+                
+        var_map::iterator it  = m_vars.begin();
+        var_map::iterator end = m_vars.end();
+        for (; it != end; ++it) {
+            app* e = it->m_key;
+            unsigned_vector const& pos = it->m_value.pos;
+            unsigned_vector const& neg = it->m_value.neg;
+            out << mk_pp(e, m) << ": ";
+            for (unsigned i = 0; i < pos.size(); ++i) {
+                out << "p: " << pos[i] << " ";
+            }
+            for (unsigned i = 0; i < neg.size(); ++i) {
+                out << "n: " << neg[i] << " ";
+            }
+            out << "\n";
+        }
+    }
+
 public:
     pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): 
         m(m), pb(m), m_r(m) {}
@@ -68,14 +152,31 @@ public:
         SASSERT(g->is_well_sorted());
         mc = 0; pc = 0; core = 0;
 
+        // TBD: bail out if cores are enabled.
+        // TBD: bail out if proofs are enabled/add proofs.
+        // TBD: model construction by back-filling solutions.
+
+        pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
+        mc = pp;
+
+        g->inc_depth();        
+        result.push_back(g.get());       
+        while (simplify(g, *pp));
+
+    }
+
+    bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
         reset();
+        normalize(g);
+        if (g->inconsistent()) {
+            return false;
+        }
         for (unsigned i = 0; i < g->size(); ++i) {
-            process_vars(i, g->form(i));
+            process_vars(i, g);
         }
         
         if (m_ge.empty()) {
-            result.push_back(g.get());       
+            return false;
-            return;
         }
         
         for (unsigned i = 0; i < m_ge.size(); ++i) {
@@ -89,44 +190,46 @@ public:
         }
         
         if (m_vars.empty()) {
-            result.push_back(g.get());       
+            return false;
-            return;
         }
         
-        g->inc_depth();        
+        // display_annotation(tout, g);
+        m_progress = false;
         // first eliminate variables
         var_map::iterator it = next_resolvent(m_vars.begin()); 
         while (it != m_vars.end()) {            
-            expr * e = it->m_key;
+            app * e = it->m_key;
             rec const& r = it->m_value;
             if (r.pos.empty()) {                
                 replace(r.neg, e, m.mk_false(), g);
+                mc.set_value(e, m.mk_false());
             }
             else if (r.neg.empty()) {
                 replace(r.pos, e, m.mk_true(), g);
+                mc.set_value(e, m.mk_true());
             }
+            if (g->inconsistent()) return false;
             ++it;
             it = next_resolvent(it);
         }        
         // now resolve clauses.
         it = next_resolvent(m_vars.begin());
         while (it != m_vars.end()) {
-            expr * e = it->m_key;
+            
+            app * e = it->m_key;
             rec const& r = it->m_value;
-            if (r.pos.size() == 1) {
+            if (r.pos.size() == 1 && !r.neg.empty()) {
-                resolve(r.pos[0], r.neg, e, true, g);
+                resolve(mc, r.pos[0], r.neg, e, true, g);
             }
-            else if (r.neg.size() == 1) {
+            else if (r.neg.size() == 1 && !r.pos.empty()) {
-                resolve(r.neg[0], r.pos, e, false, g);                
+                resolve(mc, r.neg[0], r.pos, e, false, g);                
             }
+            if (g->inconsistent()) return false;
             ++it;
             it = next_resolvent(it);
         }
-
-
         g->elim_true();
-
+        return m_progress;
-        result.push_back(g.get());       
     }
 
     virtual void set_cancel(bool f) {
@@ -146,9 +249,37 @@ private:
         m_vars.reset();
     }
 
+    expr* negate(expr* e) {
+        if (m.is_not(e, e)) return e;
+        return m.mk_not(e);
+    }
 
-    void process_vars(unsigned i, expr* e) {
+    void normalize(goal_ref const& g) {
         expr* r;
+        expr_ref tmp(m);
+        for (unsigned i = 0; !g->inconsistent() && i < g->size(); ++i) {
+            expr* e = g->form(i);
+            if (m.is_not(e, r) && pb.is_ge(r)) {
+                rational k = pb.get_k(r);
+                rational sum(0);
+                expr_ref_vector args(m);
+                vector<rational> coeffs;
+                for (unsigned j = 0; j < to_app(r)->get_num_args(); ++j) {
+                    sum += pb.get_coeff(r, j);
+                    coeffs.push_back(pb.get_coeff(r, j));
+                    args.push_back(negate(to_app(r)->get_arg(j)));
+                }
+                tmp = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), sum - k + rational::one());
+                g->update(i, tmp);
+            }
+        }
+    }
+
+
+    void process_vars(unsigned i, goal_ref const& g) {
+        expr* r, *e;
+        e = g->form(i);
+
         if (is_uninterp_const(e)) {
             m_ge.push_back(i);
         }
@@ -168,8 +299,8 @@ private:
 
     void classify_vars(unsigned idx, app* e) {
         expr* r;
-        if (m.is_not(e, r)) {
+        if (m.is_not(e, r) && is_uninterp_const(r)) {
-            insert(idx, r, false);
+            insert(idx, e, false);
             return;
         }
         if (is_uninterp_const(e)) {
@@ -182,15 +313,17 @@ private:
                 // no-op
             }
             else if (m.is_not(arg, r)) {
-                insert(idx, r, false);
+                SASSERT(is_uninterp_const(r));
+                insert(idx, to_app(r), false);
             }
             else {
-                insert(idx, arg, true);
+                SASSERT(is_uninterp_const(arg));
+                insert(idx, to_app(arg), true);
             }
         }
     }
 
-    void insert(unsigned i, expr* e, bool pos) {
+    void insert(unsigned i, app* e, bool pos) {
         if (!m_vars.contains(e)) {
             m_vars.insert(e, rec());
         }
@@ -252,82 +385,86 @@ private:
         return true;
     }
 
-    void resolve(unsigned idx1, unsigned_vector const& positions, expr* e, bool pos, goal_ref const& g) {
+    // Implement very special case of resolution.
-        if (!is_app(g->form(idx1))) {
+    
-            return;
+    void resolve(pb_preproc_model_converter& mc, unsigned idx1, 
+                 unsigned_vector const& positions, app* e, bool pos, goal_ref const& g) {
+        if (positions.size() != 1) return;
+        unsigned idx2 = positions[0];
+        expr_ref tmp1(m), tmp2(m);
+        expr* fml1 = g->form(idx1);
+        expr* fml2 = g->form(idx2);
+        expr_ref_vector args1(m), args2(m);
+        vector<rational> coeffs1, coeffs2;        
+        rational k1, k2;
+        if (!to_ge(fml1, args1, coeffs1, k1)) return;
+        if (!k1.is_one()) return;
+        if (!to_ge(g->form(idx2), args2, coeffs2, k2)) return;
+        // check that each variable in idx1 occurs only in idx2
+        unsigned min_index = 0;
+        rational min_coeff(0);
+        unsigned_vector indices;
+        for (unsigned i = 0; i < args1.size(); ++i) {
+            expr* x = args1[i].get();
+            m.is_not(x, x);
+            if (!is_app(x)) return;
+            if (!m_vars.contains(to_app(x))) return;            
+            rec const& r = m_vars.find(to_app(x));
+            if (r.pos.size() != 1 || r.neg.size() != 1) return;
+            if (r.pos[0] != idx2 && r.neg[0] != idx2) return;
+            for (unsigned j = 0; j < args2.size(); ++j) {
+                if (is_complement(args1[i].get(), args2[j].get())) {
+                    if (i == 0) {
+                        min_coeff = coeffs2[j];
                     }
-        app* fml = to_app(g->form(idx1));
+                    else if (min_coeff > coeffs2[j]) {
-        if (m.is_true(fml)) {
+                        min_coeff = coeffs2[j];
-            return;
+                        min_index = j;
                     }
-        if (!is_valid(positions, g)) {
+                    indices.push_back(j);
-            return;
                 }                
-        if (positions.size() > 1 && !is_reduction(positions, fml, g)) {
-            return;
             }
-        IF_VERBOSE(1, verbose_stream() << "resolving: " << mk_pp(fml, m) << "\n";);
+        }
-        m_r.set_substitution(0);
+        for (unsigned i = 0; i < indices.size(); ++i) {
-        expr_ref tmp1(m), tmp2(m), e1(m), e2(m);
+            unsigned j = indices[i];
-        ptr_vector<expr> args;
+            expr* arg = args2[j].get();
-        vector<rational> coeffs;        
+            if (j == min_index) {
-        rational k1, k2, c1, c2;
+                args2[j] = m.mk_false();
-        if (pos) {
-            e1 = e;
-            e2 = m.mk_not(e);
             }
             else {
-            e1 = m.mk_not(e);
+                args2[j] = m.mk_true();
-            e2 = e;
             }
-        VERIFY(to_ge(fml, args, coeffs, k1));
+            mc.set_value(arg, j != min_index);
-        c1 = get_coeff(args.size(), args.c_ptr(), coeffs.c_ptr(), e1);
-        if (c1.is_zero()) {
-            return;
         }
-        unsigned sz = coeffs.size();
+        
-        for (unsigned i = 0; i < positions.size(); ++i) {
+        tmp1 = pb.mk_ge(args2.size(), coeffs2.c_ptr(), args2.c_ptr(), k2);
-            unsigned idx2 = positions[i];
+        IF_VERBOSE(3, verbose_stream() << " " << tmp1 << "\n";
-            if (idx2 == idx1) {
+                   for (unsigned i = 0; i < args2.size(); ++i) {
-                continue;
+                       verbose_stream() << mk_pp(args2[i].get(), m) << " ";
                    }
-            app* fml2 = to_app(g->form(idx2));
+                   verbose_stream() << "\n";
-            if (m.is_true(fml2)) continue;
+                   );
-            VERIFY(to_ge(fml2, args, coeffs, k2));
-            c2 = get_coeff(args.size()-sz, args.c_ptr()+sz, coeffs.c_ptr()+sz, e2);
-            if (!c2.is_zero()) {
-                rational m1(1), m2(1);
-                if (c1 != c2) {
-                    rational lc = lcm(c1, c2);
-                    m1 = lc/c1;
-                    m2 = lc/c2;
-                    for (unsigned j = 0; j < sz; ++j) {
-                        coeffs[j] *= m1;
-                    }
-                    for (unsigned j = sz; j < args.size(); ++j) {
-                        coeffs[j] *= m2;
-                    }
-                }
-                tmp1 = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), m1*k1 + m2*k2);
         m_r(tmp1, tmp2);
-                TRACE("pb", tout << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
+        if (pb.is_ge(tmp2) && pb.get_k(to_app(tmp2)).is_one()) {
-                IF_VERBOSE(1, verbose_stream() << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
+            tmp2 = m.mk_or(to_app(tmp2)->get_num_args(), to_app(tmp2)->get_args());
+        }
+        IF_VERBOSE(3, 
+                   verbose_stream() << "resolve: " << mk_pp(fml1, m) << "\n" << mk_pp(fml2, m) << "\n" << tmp1 << "\n";
+                   verbose_stream() << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";);
 
-                g->update(idx2, tmp2); // proof & dependencies
-
-                if (!m1.is_one()) {
-                    for (unsigned j = 0; j < sz; ++j) {
-                        coeffs[j] /= m1;
-                    }
-                }
-            }
-            args.resize(sz);
-            coeffs.resize(sz);
-        }
         g->update(idx1, m.mk_true()); // proof & dependencies
+        g->update(idx2, tmp2);        // proof & dependencies
+        m_progress = true;
+        //IF_VERBOSE(0, if (!g->inconsistent()) display_annotation(verbose_stream(), g););
     }
 
-    bool to_ge(app* e, ptr_vector<expr>& args, vector<rational>& coeffs, rational& k) {
+    bool is_complement(expr* x, expr* y) const {
+        if (m.is_not(x,x)) return x == y;
+        if (m.is_not(y,y)) return x == y;
+        return false;
+    }
+
+    bool to_ge(expr* e, expr_ref_vector& args, vector<rational>& coeffs, rational& k) {
         expr* r;
         if (is_uninterp_const(e)) {
             args.push_back(e);
@@ -340,17 +477,19 @@ private:
             k = rational::one();
         }
         else if (pb.is_ge(e)) {
-            SASSERT(pure_args(e));
+            app* a = to_app(e);
-            for (unsigned i = 0; i < e->get_num_args(); ++i) {
+            SASSERT(pure_args(a));
-                args.push_back(e->get_arg(i));
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                coeffs.push_back(pb.get_coeff(e, i));
+                args.push_back(a->get_arg(i));
+                coeffs.push_back(pb.get_coeff(a, i));
             }
             k = pb.get_k(e);
         }
         else if (m.is_or(e)) {
+            app* a = to_app(e);
             SASSERT(pure_args(e));
-            for (unsigned i = 0; i < e->get_num_args(); ++i) {
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                args.push_back(e->get_arg(i));
+                args.push_back(a->get_arg(i));
                 coeffs.push_back(rational::one());
             }
             k = rational::one();
@@ -375,8 +514,10 @@ private:
                 TRACE("pb", tout << mk_pp(f, m) << " -> " << tmp 
                       << " by " << mk_pp(e, m) << " |-> " << mk_pp(v, m) << "\n";);
                 g->update(idx, tmp); // proof & dependencies.
+                m_progress = true;
             }
         }
+        m_r.set_substitution(0);
     }
 };
 
@@ -384,3 +525,83 @@ private:
 tactic * mk_pb_preprocess_tactic(ast_manager & m, params_ref const & p) {
     return alloc(pb_preprocess_tactic, m);
 }
+
+#if 0
+
+    struct resolve_t {
+        app*  e;
+        expr* lhs;
+        expr* rhs;
+        expr* res;
+        resolve_t(app* e, expr* lhs, expr* rhs, expr* res):
+            e(e), lhs(lhs), rhs(rhs), res(res)
+        {}        
+    };
+
+    svector<resolve_t>               m_resolve;
+
+    void satisfy(model_ref& mdl, expr* e) {
+        if (m.is_true(e)) {
+            return;
+        }
+        if (pb.is_ge(e)) {
+            rational k = pb.get_k(e);
+            rational c(0);
+            app* a = to_app(e);
+            for (unsigned i = 0; c < k && i < a->get_num_args(); ++i) {
+                expr* arg = a->get_arg(i);
+                if (is_uninterp_const(arg)) {
+                    mdl->register_decl(to_app(arg)->get_decl(), m.mk_true());
+                    std::cout << mk_pp(arg, m) << " |-> true\n";
+                    c += pb.get_coeff(a, i);
+                }
+                else if (m.is_not(arg, arg) && is_uninterp_const(arg)) {
+                    mdl->register_decl(to_app(arg)->get_decl(), m.mk_false());
+                    std::cout << mk_pp(arg, m) << " |-> false\n";
+                    c += pb.get_coeff(a, i);
+                }
+            }
+            SASSERT(c >= k);
+            return;
+        }
+        UNREACHABLE();
+    }
+
+        for (unsigned i = m_resolve.size(); i > 0; ) {
+            --i;
+            resolve_t const& r = m_resolve[i];
+            expr_ref tmp1(m), tmp2(m), tmp3(m), tmp4(m);
+            VERIFY(mdl->eval(r.rhs, tmp2));
+            satisfy(mdl, tmp2);
+
+            VERIFY(mdl->eval(r.lhs, tmp1));
+            satisfy(mdl, tmp1);
+            
+            if (m.is_false(tmp2) || m.is_false(tmp1)) {
+                VERIFY(mdl->eval(r.res, tmp3));
+                th_rewriter rw(m);
+                rw(r.res, tmp4);
+                std::cout << "L:" << mk_pp(r.lhs,m) << " " << tmp1 << "\n";
+                std::cout << "R:" << mk_pp(r.rhs,m) << " " << tmp2 << "\n";
+                std::cout << "LR:" << mk_pp(r.res,m) << "\n" << tmp4 << "\n" << tmp3 << "\n";
+                exit(0);
+            }
+            VERIFY(mdl->eval(r.e, tmp3));
+            if (r.e == tmp3) {
+                mdl->register_decl(r.e->get_decl(), m.mk_true());
+            }
+            // evaluate lhs, rhs
+            // determine how to 
+            // assign e based on residue.            
+        }
+
+    void resolve(app* e, expr* lhs, expr* rhs, expr* res) {
+        m_refs.push_back(e);
+        m_refs.push_back(lhs);
+        m_refs.push_back(rhs);
+        m_refs.push_back(res);
+        m_resolve.push_back(resolve_t(e, lhs, rhs, res));
+    }
+
+
+#endif