From 5f72325e9945f7d00e23b89e65f43b0aa2096731 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 14 Dec 2013 10:00:21 +0200
Subject: [PATCH] working on maxsat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/fu_malik.cpp    | 10 +++++++++-
 src/opt/opt_context.cpp | 15 ++++++++++++---
 2 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index af700168f..4c15aedf0 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -24,6 +24,7 @@ Notes:
 #include "probe.h"
 #include "tactic.h"
 #include "smt_context.h"
+#include "ast_pp.h"
 
 /**
    \brief Fu & Malik procedure for MaxSAT. This procedure is based on 
@@ -290,8 +291,14 @@ namespace opt {
             if (!m_soft.empty() && is_sat == l_true) {
                 solver::scoped_push _sp(s());
                 expr_ref tmp(m);
+                TRACE("opt",
+                      tout << "soft constraints:\n";
+                      for (unsigned i = 0; i < m_soft.size(); ++i) {
+                          tout << mk_pp(m_soft[i].get(), m) << "\n";
+                      });
                 for (unsigned i = 0; i < m_soft.size(); ++i) {
                     m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
+                    m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl());
                     tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
                     s().assert_expr(tmp);
                 }
@@ -304,7 +311,7 @@ namespace opt {
                 while (is_sat == l_false);
                 
                 if (is_sat == l_true) {
-                    // Get a list of satisfying m_soft
+                    // Get a list satisfying m_soft
                     s().get_model(m_model);
                     m_lower = m_upper;
                     m_assignment.reset();                    
@@ -315,6 +322,7 @@ namespace opt {
                             m_assignment.push_back(m_orig_soft[i].get());
                         }
                     }
+                    TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";);
                 }
             }
             // We are done and soft_constraints has 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index be0e6010d..ce9fedf96 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -255,6 +255,14 @@ namespace opt {
                     terms[i] = m.mk_not(terms[i].get());
                 }
             }
+            TRACE("opt", 
+                  tout << "Convert minimization " << mk_pp(orig_term, m) << "\n";
+                  tout << "to maxsat: " << term << "\n";
+                  for (unsigned i = 0; i < weights.size(); ++i) {
+                      tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n";
+                  }
+                  tout << "offset: " << offset << "\n";
+                  );
             std::ostringstream out;
             out << mk_pp(orig_term, m);
             id = symbol(out.str().c_str());
@@ -448,7 +456,7 @@ namespace opt {
                 out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
             }
             else {
-                out << "|-> " << get_lower(i) << "\n";
+                out << " |-> " << get_lower(i) << "\n";
             }
         }
     }
@@ -459,12 +467,12 @@ namespace opt {
         case O_MAXSMT: {
             symbol s = obj.m_id;
             if (s != symbol::null) {
-                out << s << " : ";
+                out << s;
             }
             break;
         }
         default:
-            out << obj.m_term << " ";
+            out << obj.m_term;
             break;
         }
     }
@@ -477,6 +485,7 @@ namespace opt {
         switch(obj.m_type) {
         case O_MAXSMT: {
             rational r = m_maxsmts.find(obj.m_id)->get_lower();
+            TRACE("opt", tout << "maxsmt: " << r << " negate: " << obj.m_neg << " offset: " << obj.m_offset << "\n";);
             if (obj.m_neg) r.neg();
             r += obj.m_offset;
             return inf_eps(r);