From 370a4b66de424c428645ad3724af21702fbdce0a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 7 Dec 2013 22:09:57 -0800
Subject: [PATCH] update lower bounds from feasible solutiosn

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/core_maxsat.cpp     |  4 ++++
 src/opt/core_maxsat.h       |  1 +
 src/opt/fu_malik.cpp        | 14 +++++++----
 src/opt/fu_malik.h          |  1 +
 src/opt/maxsmt.cpp          | 24 +++++++++++++++----
 src/opt/maxsmt.h            | 12 ++++++++++
 src/opt/opt_context.cpp     | 47 +++++++++++++++++++++++++++++++++++--
 src/opt/opt_context.h       |  2 ++
 src/opt/opt_solver.cpp      | 13 ++--------
 src/opt/opt_solver.h        |  1 -
 src/opt/optsmt.cpp          | 41 +++++++++++++++++---------------
 src/opt/optsmt.h            |  2 ++
 src/opt/weighted_maxsat.cpp |  4 +++-
 src/opt/weighted_maxsat.h   |  1 +
 14 files changed, 123 insertions(+), 44 deletions(-)

diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp
index 11756c617..d283feab8 100644
--- a/src/opt/core_maxsat.cpp
+++ b/src/opt/core_maxsat.cpp
@@ -147,5 +147,9 @@ namespace opt {
     void core_maxsat::set_cancel(bool f) {
         
     }
+    void core_maxsat::collect_statistics(statistics& st) const {
+        // nothing specific
+    }
+
     
 };
diff --git a/src/opt/core_maxsat.h b/src/opt/core_maxsat.h
index b5ee6e422..63f92cf4a 100644
--- a/src/opt/core_maxsat.h
+++ b/src/opt/core_maxsat.h
@@ -40,6 +40,7 @@ namespace opt {
         virtual rational get_value() const;
         virtual expr_ref_vector get_assignment() const;
         virtual void set_cancel(bool f);
+        virtual void collect_statistics(statistics& st) const;
 
     private:
         void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index cf0fefe52..a83419cb6 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -93,6 +93,12 @@ namespace opt {
             }
         }
 
+        void collect_statistics(statistics& st) const {
+            if (m_s != &m_original_solver) {
+                m_s->collect_statistics(st);
+            }
+        }
+
         void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
             set.reset();
             expr_set::iterator it = set1.begin(), end = set1.end();
@@ -307,11 +313,6 @@ namespace opt {
                     }
                 }
             }
-            statistics st;
-            s().collect_statistics(st);
-            SASSERT(st.size() > 0);            
-            opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
-            opt_s.set_interim_stats(st);
             // We are done and soft_constraints has 
             // been updated with the max-sat assignment.            
             return is_sat;            
@@ -344,6 +345,9 @@ namespace opt {
     void fu_malik::set_cancel(bool f) {
         // no-op
     }
+    void fu_malik::collect_statistics(statistics& st) const {
+        m_imp->collect_statistics(st);
+    }
 
 
 
diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h
index 9375e29c2..980db707b 100644
--- a/src/opt/fu_malik.h
+++ b/src/opt/fu_malik.h
@@ -41,6 +41,7 @@ namespace opt {
         virtual rational get_value() const;
         virtual expr_ref_vector get_assignment() const;
         virtual void set_cancel(bool f);
+        virtual void collect_statistics(statistics& st) const;
     };
     
 };
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index c6298f2e8..4fc184a13 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -79,21 +79,29 @@ namespace opt {
         if (m_msolver) {
             return inf_eps(m_msolver->get_value());
         }
-        return inf_eps();
+        return inf_eps(m_upper);
     }
 
     inf_eps maxsmt::get_lower() const {
+        rational r = m_lower;
         if (m_msolver) {
-            return inf_eps(m_msolver->get_lower());
+            rational q = m_msolver->get_lower();
+            if (r < q) r = q;
         }
-        return inf_eps();
+        return inf_eps(r);
     }
 
     inf_eps maxsmt::get_upper() const {
+        rational r = m_upper;
         if (m_msolver) {
-            return inf_eps(m_msolver->get_upper());
+            rational q = m_msolver->get_upper();
+            if (r > q) r = q;
         }
-        return inf_eps(rational(m_soft_constraints.size()));
+        return inf_eps(r);
+    }
+
+    void maxsmt::update_lower(rational const& r) {
+        if (m_lower > r)  m_lower = r;
     }
 
     void maxsmt::commit_assignment() {
@@ -130,5 +138,11 @@ namespace opt {
         m_maxsat_engine = _p.maxsat_engine();        
     }
 
+    void maxsmt::collect_statistics(statistics& st) const {
+        if (m_msolver) {
+            m_msolver->collect_statistics(st);
+        }
+    }
+
 
 };
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 413727b58..14e8515b7 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -21,6 +21,7 @@ Notes:
 
 #include "solver.h"
 #include "opt_solver.h"
+#include "statistics.h"
 
 namespace opt {
 
@@ -33,6 +34,7 @@ namespace opt {
         virtual rational get_value() const = 0;
         virtual expr_ref_vector get_assignment() const = 0;
         virtual void set_cancel(bool f) = 0;
+        virtual void collect_statistics(statistics& st) const = 0;
     };
     /**
        Takes solver with hard constraints added.
@@ -46,6 +48,8 @@ namespace opt {
         expr_ref_vector  m_soft_constraints;
         expr_ref_vector  m_answer;
         vector<rational> m_weights;
+        rational         m_lower;
+        rational         m_upper;
         scoped_ptr<maxsmt_solver> m_msolver;
         symbol           m_maxsat_engine;
     public:
@@ -58,8 +62,11 @@ namespace opt {
         void updt_params(params_ref& p);
 
         void add(expr* f, rational const& w) {
+            SASSERT(m.is_bool(f));
+            SASSERT(w.is_pos());
             m_soft_constraints.push_back(f);
             m_weights.push_back(w);
+            m_upper += w;
         }
 
         unsigned size() const { return m_soft_constraints.size(); }
@@ -70,10 +77,15 @@ namespace opt {
         inf_eps get_value() const;
         inf_eps get_lower() const;
         inf_eps get_upper() const;
+        void update_lower(rational const& r);
+
 
         expr_ref_vector get_assignment() const;
 
         void display_answer(std::ostream& out) const;
+        
+        void collect_statistics(statistics& st) const;
+
 
     private:
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2d1b9c268..f38605a61 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -85,6 +85,7 @@ namespace opt {
             return is_sat;
         }
         s.get_model(m_model);
+        update_lower();
         switch (m_objectives.size()) {
         case 0:
             return is_sat;
@@ -223,11 +224,15 @@ namespace opt {
             rational coeff(0);
             // minimize 2*x + 3*y 
             // <=>
-            // (assret-soft (not x) 2)
+            // (assert-soft (not x) 2)
             // (assert-soft (not y) 3)
             //
             if (get_pb_sum(term, terms, weights, coeff) && coeff.is_zero()) {
-                // TBD: and weights are positive?
+                for (unsigned i = 0; i < weights.size(); ++i) {
+                    if (!weights[i].is_pos()) {
+                        return false;
+                    }
+                }
                 for (unsigned i = 0; i < terms.size(); ++i) {
                     terms[i] = m.mk_not(terms[i].get());
                 }
@@ -348,6 +353,40 @@ namespace opt {
         }
     }
 
+    void context::update_lower() {
+        arith_util a(m);
+        expr_ref val(m);
+        rational r(0);
+        for (unsigned i = 0; i < m_objectives.size(); ++i) {
+            objective const& obj = m_objectives[i];
+            switch(obj.m_type) {
+            case O_MINIMIZE:
+            case O_MAXIMIZE:
+                if (m_model->eval(obj.m_term, val) && a.is_numeral(val, r)) {
+                    m_optsmt.update_lower(obj.m_index, r);
+                }
+                break;
+            case O_MAXSMT: {
+                bool ok = true;
+                for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) {
+                    if (m_model->eval(obj.m_terms[j], val)) {
+                        if (!m.is_true(val)) {
+                            r += obj.m_weights[j];
+                        }
+                    }
+                    else {
+                        ok = false;
+                    }
+                }
+                if (ok) {
+                    m_maxsmts.find(obj.m_id)->update_lower(r);
+                }
+                break;
+            }
+            }
+        }
+    }
+
     void context::display_assignment(std::ostream& out) {
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
@@ -459,6 +498,10 @@ namespace opt {
         if (m_solver) {
             m_solver->collect_statistics(stats);
         }
+        map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
+        for (; it != end; ++it) {
+            it->m_value->collect_statistics(stats);
+        }        
     }
 
     void context::collect_param_descrs(param_descrs & r) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 9bc1007de..b1424d165 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -128,6 +128,8 @@ namespace opt {
         void from_fmls(expr_ref_vector const& fmls);
         void simplify_fmls(expr_ref_vector& fmls);
 
+        void update_lower();
+
         opt_solver& get_solver();
 
     };
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index d6877e5db..01d64b6cc 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -55,14 +55,8 @@ namespace opt {
         m_context.collect_param_descrs(r);
     }
     
-    void opt_solver::collect_statistics(statistics & st) const {
-        // HACK: display fu_malik statistics
-        if (m_stats.size() > 0) {
-            st.copy(m_stats);
-        }
-        else {
-            m_context.collect_statistics(st);
-        }
+    void opt_solver::collect_statistics(statistics & st) const {        
+        m_context.collect_statistics(st);
     }
     
     void opt_solver::assert_expr(expr * t) {
@@ -241,9 +235,6 @@ namespace opt {
         return dynamic_cast<opt_solver&>(s);
     }
 
-    void opt_solver::set_interim_stats(statistics & st) {
-        m_stats.copy(st);
-    }
     
     void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, 
                                        char const * status, char const * attributes) {        
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index f35a79203..d5fb58afe 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -79,7 +79,6 @@ namespace opt {
         expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
 
         static opt_solver& to_opt(solver& s);
-        void set_interim_stats(statistics & st);
         bool dump_benchmarks();
 
         class toggle_objective {
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 91a421adb..e8df01b5a 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -105,6 +105,13 @@ namespace opt {
         return l_true;        
     }
 
+    void optsmt::update_lower(unsigned idx, rational const& r) {
+        inf_eps v(r);
+        if (m_lower[idx] < v) {
+            m_lower[idx] = v;
+        }
+    }
+
     void optsmt::update_lower() {
         model_ref md;
         s->get_model(md);
@@ -202,30 +209,26 @@ namespace opt {
        Returns an optimal assignment to objective functions.
     */
     lbool optsmt::operator()(opt_solver& solver) {
+        if (m_objs.empty()) {
+            return l_true;
+        }
+        lbool is_sat = l_true;
         s = &solver;
-        s->reset_objectives();
+        solver.reset_objectives();
         m_vars.reset();
 
         // First check_sat call to initialize theories
-        lbool is_sat = s->check_sat(0, 0);
-        solver::scoped_push _push(*s);
-        if (is_sat == l_true && !m_objs.empty()) {
-            for (unsigned i = 0; i < m_objs.size(); ++i) {
-                m_vars.push_back(s->add_objective(m_objs[i].get()));
-            }            
+        solver::scoped_push _push(solver);
 
-            if (m_engine == symbol("basic")) {
-                is_sat = basic_opt();
-            }
-            else if (m_engine == symbol("farkas")) {
-                is_sat = farkas_opt();
-            }
-            else {
-                // TODO: implement symba engine
-                // report error on bad configuration.
-                NOT_IMPLEMENTED_YET();
-                UNREACHABLE();
-            }
+        for (unsigned i = 0; i < m_objs.size(); ++i) {
+            m_vars.push_back(solver.add_objective(m_objs[i].get()));
+        }            
+
+        if (m_engine == symbol("farkas")) {
+            is_sat = farkas_opt();
+        }
+        else {
+            is_sat = basic_opt();
         }
 
         IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << std::endl;
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index 0fbfeb7b2..c8be7a730 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -56,6 +56,8 @@ namespace opt {
         inf_eps get_value(unsigned index) const;
         inf_eps get_lower(unsigned index) const;
         inf_eps get_upper(unsigned index) const;
+
+        void update_lower(unsigned idx, rational const& r);
         
     private:
         
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 206117224..613ce41d5 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -370,7 +370,9 @@ namespace opt {
     void wmaxsmt::set_cancel(bool f) {
         // no-op
     }
-
+    void wmaxsmt::collect_statistics(statistics& st) const {
+        // no-op
+    }
 
 
     
diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h
index 8621ff9e1..3b00e1690 100644
--- a/src/opt/weighted_maxsat.h
+++ b/src/opt/weighted_maxsat.h
@@ -39,6 +39,7 @@ namespace opt {
         virtual rational get_value() const;
         virtual expr_ref_vector get_assignment() const;
         virtual void set_cancel(bool f);
+        virtual void collect_statistics(statistics& st) const;
     };
 };