use PB solver instead of full arithmetic for bouding Pareto fronts so that difference logic theory isn't broken. Codeplex issue 175

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

src/opt/opt_context.cpp

@@ -327,78 +327,66 @@ namespace opt {
 
     expr_ref context::mk_le(unsigned i, model_ref& mdl) {
         objective const& obj = m_objectives[i];
-        expr_ref val(m), result(m), term(m);
-        mk_term_val(mdl, obj, term, val);
-        switch (obj.m_type) {
-        case O_MINIMIZE:
-            result = mk_ge(term, val);
-            break;
-        case O_MAXSMT:
-            result = mk_ge(term, val);
-            break;
-        case O_MAXIMIZE:
-            result = mk_ge(val, term);
-            break;
-        }
-        return result;
+        return mk_cmp(false, mdl, obj);
     }
     
     expr_ref context::mk_ge(unsigned i, model_ref& mdl) {
         objective const& obj = m_objectives[i];
-        expr_ref val(m), result(m), term(m);
-        mk_term_val(mdl, obj, term, val);
-        switch (obj.m_type) {
-        case O_MINIMIZE:
-            result = mk_ge(val, term);
-            break;
-        case O_MAXSMT:
-            result = mk_ge(val, term);
-            break;
-        case O_MAXIMIZE:
-            result = mk_ge(term, val);
-            break;
-        }
-        return result;
+        return mk_cmp(true, mdl, obj);
     }
     
+    
     expr_ref context::mk_gt(unsigned i, model_ref& mdl) {
         expr_ref result = mk_le(i, mdl);
         result = m.mk_not(result);
         return result;
     }
-    
-    void context::mk_term_val(model_ref& mdl, objective const& obj, expr_ref& term, expr_ref& val) {
-        rational r;
+
+    expr_ref context::mk_cmp(bool is_ge, model_ref& mdl, objective const& obj) {
+        rational k(0);
+        expr_ref val(m), result(m);
         switch (obj.m_type) {
         case O_MINIMIZE:
+            is_ge = !is_ge;
         case O_MAXIMIZE:
-            term = obj.m_term;
-            break;
-        case O_MAXSMT: {
-            unsigned sz = obj.m_terms.size();
-            expr_ref_vector sum(m);
-            expr_ref zero(m);
-            zero = m_arith.mk_numeral(rational(0), false);
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* t = obj.m_terms[i];
-                rational const& w = obj.m_weights[i];
-                sum.push_back(m.mk_ite(t, m_arith.mk_numeral(w, false), zero));                    
-            }
-            if (sum.empty()) {
-                term = zero;
+            VERIFY(mdl->eval(obj.m_term, val) && is_numeral(val, k));
+            if (is_ge) {
+                result = mk_ge(obj.m_term, val);
             }
             else {
-                term = m_arith.mk_add(sum.size(), sum.c_ptr());
-            }                           
+                result = mk_ge(val, obj.m_term);
+            }
+            break;
+        case O_MAXSMT: {
+            m_opt_solver->ensure_pb();
+            pb_util      pb(m);
+            unsigned sz = obj.m_terms.size();
+            ptr_vector<expr> terms;
+            vector<rational> coeffs;
+            for (unsigned i = 0; i < sz; ++i) {
+                terms.push_back(obj.m_terms[i]);
+                coeffs.push_back(obj.m_weights[i]);
+                VERIFY(mdl->eval(obj.m_terms[i], val));
+                if (m.is_true(val)) {
+                    k += obj.m_weights[i];
+                }
+            }
+            if (is_ge) {
+                result = pb.mk_ge(sz, coeffs.c_ptr(), terms.c_ptr(), k);
+            }
+            else {
+                result = pb.mk_le(sz, coeffs.c_ptr(), terms.c_ptr(), k);
+            }
             break;
         }
         }
         TRACE("opt", 
-              model_smt2_pp(tout << "Model:\n", m, *mdl, 0);
-              mdl->eval(term, val); tout << term << " " << val << "\n";);
-        VERIFY(mdl->eval(term, val) && is_numeral(val, r));
-    }        
-
+              tout << (is_ge?">= ":"<= ") << k << "\n";
+              display_objective(tout, obj);
+              tout << "\n";
+              tout << result << "\n";);
+        return result;
+    }    
 
     expr_ref context::mk_ge(expr* t, expr* s) {
         expr_ref result(m);

src/opt/opt_context.h

@@ -282,7 +282,7 @@ namespace opt {
         // pareto
         void yield();
         expr_ref mk_ge(expr* t, expr* s);
-        void mk_term_val(model_ref& mdl, objective const& obj, expr_ref& term, expr_ref& val);
+        expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj);
 
     };
 

src/opt/opt_pareto.cpp

@@ -68,7 +68,7 @@ namespace opt {
         fmls.push_back(m.mk_or(gt.size(), gt.c_ptr()));
         fml = m.mk_and(fmls.size(), fmls.c_ptr());
         IF_VERBOSE(10, verbose_stream() << "dominates: " << fml << "\n";);
-        TRACE("opt", tout << fml << "\n";);
+        TRACE("opt", tout << fml << "\n"; model_smt2_pp(tout, m, *m_model, 0););
         m_solver->assert_expr(fml);        
     }
 

src/opt/opt_solver.cpp

@@ -86,6 +86,14 @@ namespace opt {
         m_context.set_logic(logic);
     }
 
+    void opt_solver::ensure_pb() {
+        smt::theory_id th_id = m.get_family_id("pb");
+        smt::theory* th = get_context().get_theory(th_id);               
+        if (!th) {
+            get_context().register_plugin(alloc(smt::theory_pb, m, m_params));
+        }
+    }
+
     smt::theory_opt& opt_solver::get_optimizer() {
         smt::context& ctx = m_context.get_context();                        
         smt::theory_id arith_id = m_context.m().get_family_id("arith");     

src/opt/opt_solver.h

@@ -122,6 +122,7 @@ namespace opt {
         bool dump_benchmarks();
 
         smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat.
+        void ensure_pb();
         
         smt::theory_opt& get_optimizer();