From ac7fffa9cbf440fa01178c5b00a132dd49f168b6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 Mar 2014 08:34:31 -0700
Subject: [PATCH] fix bug exposed by example by Robert White

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/duality/duality.h       |  2 +-
 src/interp/iz3hash.h        |  4 ++--
 src/opt/weighted_maxsat.cpp | 44 +++++++++++++++++++++----------------
 3 files changed, 28 insertions(+), 22 deletions(-)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index fe86ed2ec..aa147d93e 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -29,7 +29,7 @@ using namespace stl_ext;
 
 namespace Duality {
 
-  class implicant_solver;
+  struct implicant_solver;
 
   /* Generic operations on Z3 formulas */
 
diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h
index 355c03817..e4faa9ec3 100644
--- a/src/interp/iz3hash.h
+++ b/src/interp/iz3hash.h
@@ -52,7 +52,7 @@ namespace hash_space {
     class hash<std::string> {
   public:
     size_t operator()(const std::string &s) const {
-      return string_hash(s.c_str(), s.size(), 0);
+        return string_hash(s.c_str(), static_cast<unsigned>(s.size()), 0);
     }
   };
 
@@ -374,7 +374,7 @@ namespace hash_space {
     void resize(size_t new_size) {
       const size_t old_n = buckets.size();
       if (new_size <= old_n) return;
-      const size_t n = next_prime(new_size);
+      const size_t n = next_prime(static_cast<unsigned>(new_size));
       if (n <= old_n) return;
       Table tmp(n, (Entry*)(0));
       for (size_t i = 0; i < old_n; ++i) {
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 2aeabfbb8..8a8bb2aba 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -59,6 +59,7 @@ namespace smt {
         rational                 m_rmin_cost;   // current maximal cost assignment.
         scoped_mpz               m_zcost;       // current sum of asserted costs
         scoped_mpz               m_zmin_cost;   // current maximal cost assignment.
+        bool                     m_found_optimal; 
         u_map<theory_var>        m_bool2var;    // bool_var -> theory_var
         svector<bool_var>        m_var2bool;    // theory_var -> bool_var
         bool                     m_propagate;  
@@ -79,6 +80,7 @@ namespace smt {
             m_old_values(m_mpz),
             m_zcost(m_mpz),
             m_zmin_cost(m_mpz),
+            m_found_optimal(false),
             m_propagate(false),
             m_normalize(false)
         {}
@@ -93,14 +95,21 @@ namespace smt {
         void get_assignment(svector<bool>& result) {
             result.reset();
 
-            std::sort(m_cost_save.begin(), m_cost_save.end());
-            for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
-                if (j < m_cost_save.size() && m_cost_save[j] == i) {
+            if (!m_found_optimal) {
+                for (unsigned i = 0; i < m_vars.size(); ++i) {
                     result.push_back(false);
-                    ++j;
                 }
-                else {
-                    result.push_back(true);
+            }
+            else {
+                std::sort(m_cost_save.begin(), m_cost_save.end());
+                for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
+                    if (j < m_cost_save.size() && m_cost_save[j] == i) {
+                        result.push_back(false);
+                        ++j;
+                    }
+                    else {
+                        result.push_back(true);
+                    }
                 }
             }
             TRACE("opt",
@@ -189,10 +198,6 @@ namespace smt {
             return m_min_cost_atom;
         }
 
-        bool found_solution() const {
-            return !m_cost_save.empty();
-        }
-
         // scoped_mpz leaks.
 
         class numeral_trail : public trail<context> {
@@ -273,6 +278,7 @@ namespace smt {
             m_min_cost_atom = 0;
             m_min_cost_atoms.reset();
             m_propagate = false;
+            m_found_optimal = false;
             m_assigned.reset();
         }
 
@@ -303,7 +309,7 @@ namespace smt {
         }       
 
         bool is_optimal() const {
-            return m_mpz.lt(m_zcost, m_zmin_cost);
+            return !m_found_optimal || m_zcost < m_zmin_cost;
         }
 
         expr_ref mk_block() {
@@ -329,22 +335,22 @@ namespace smt {
                 rational rw = rational(q);
                 IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << rw << ")\n";);
                 m_zmin_cost = weight;
+                m_found_optimal = true;
                 m_cost_save.reset();
                 m_cost_save.append(m_costs);
-            }
-
-            expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
-
-            TRACE("opt",
-                  tout << result << "\n";
-                  if (is_optimal()) {
+                TRACE("opt",
                       tout << "costs: ";
                       for (unsigned i = 0; i < m_costs.size(); ++i) {
                           tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
                       }
                       tout << "\n";
                       get_context().display(tout);                      
-                  });
+                      );
+            }
+            expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
+            TRACE("opt",
+                  tout << result << " weight: " << weight << "\n";
+                  tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
             return result;
         }