From 816029c862ab08eef09056e6bc0a15f567636b01 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Nov 2013 20:04:30 -0800
Subject: [PATCH] missing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxsmt.cpp | 114 +++++++++++++++++++++++++++++++++++++++++++++
 src/opt/maxsmt.h   |  82 ++++++++++++++++++++++++++++++++
 2 files changed, 196 insertions(+)
 create mode 100644 src/opt/maxsmt.cpp
 create mode 100644 src/opt/maxsmt.h

diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
new file mode 100644
index 000000000..f68e4a50b
--- /dev/null
+++ b/src/opt/maxsmt.cpp
@@ -0,0 +1,114 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_maxsmt.cpp
+
+Abstract:
+   
+    MaxSMT optimization context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-7
+
+Notes:
+
+--*/
+
+#include "maxsmt.h"
+#include "fu_malik.h"
+#include "weighted_maxsat.h"
+#include "ast_pp.h"
+
+namespace opt {
+
+    lbool maxsmt::operator()(solver& s) {
+        lbool is_sat;
+        m_answer.reset();
+        m_msolver = 0;
+        if (m_answer.empty()) {
+            m_msolver = 0;
+            is_sat = s.check_sat(0, 0);
+            m_answer.append(m_soft_constraints);
+        }
+        else if (is_maxsat_problem(m_weights)) {
+            m_msolver = alloc(fu_malik, m, s, m_soft_constraints);
+        }
+        else {
+            m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights);
+        }
+
+        if (m_msolver) {
+            is_sat = (*m_msolver)();
+            m_answer.append(m_msolver->get_assignment());
+        }
+
+        // Infrastructure for displaying and storing solution is TBD.
+        std::cout << "is-sat: " << is_sat << "\n";
+        if (is_sat == l_true) {
+            std::cout << "Satisfying soft constraints\n";
+            display_answer(std::cout);
+        }
+        return is_sat;
+    }
+
+    expr_ref_vector maxsmt::get_assignment() const {
+        return m_answer;
+    } 
+
+    inf_eps maxsmt::get_value() const {
+        if (m_msolver) {
+            return inf_eps(m_msolver->get_value());
+        }
+        return inf_eps();
+    }
+
+    inf_eps maxsmt::get_lower() const {
+        if (m_msolver) {
+            return inf_eps(m_msolver->get_lower());
+        }
+        return inf_eps();
+    }
+
+    inf_eps maxsmt::get_upper() const {
+        if (m_msolver) {
+            return inf_eps(m_msolver->get_upper());
+        }
+        return inf_eps();
+    }
+
+    void maxsmt::commit_assignment() {
+        for (unsigned i = 0; i < m_answer.size(); ++i) {
+            s->assert_expr(m_answer[i].get());
+        }
+    }
+
+    void maxsmt::display_answer(std::ostream& out) const {
+        for (unsigned i = 0; i < m_answer.size(); ++i) {
+            out << mk_pp(m_answer[i], m) << "\n";
+        } 
+    }
+    
+    void maxsmt::set_cancel(bool f) {
+        m_cancel = f;
+        if (m_msolver) {
+            m_msolver->set_cancel(f);
+        }
+    }
+    
+    bool maxsmt::is_maxsat_problem(vector<rational> const& ws) const {
+        for (unsigned i = 0; i < ws.size(); ++i) {
+            if (!ws[i].is_one()) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    void maxsmt::updt_params(params_ref& p) {
+    }
+
+
+};
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
new file mode 100644
index 000000000..b23d8811e
--- /dev/null
+++ b/src/opt/maxsmt.h
@@ -0,0 +1,82 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    opt_maxsmt.h
+
+Abstract:
+   
+    MaxSMT optimization context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-7
+
+Notes:
+
+--*/
+#ifndef _OPT_MAXSMT_H_
+#define _OPT_MAXSMT_H_
+
+#include "solver.h"
+#include "opt_solver.h"
+
+namespace opt {
+
+    class maxsmt_solver {
+    public:        
+        virtual ~maxsmt_solver() {}
+        virtual lbool operator()() = 0;
+        virtual rational get_lower() const = 0;
+        virtual rational get_upper() const = 0;
+        virtual rational get_value() const = 0;
+        virtual expr_ref_vector get_assignment() const = 0;
+        virtual void set_cancel(bool f) = 0;
+    };
+    /**
+       Takes solver with hard constraints added.
+       Returns modified soft constraints that are maximal assignments.
+    */
+
+    class maxsmt {
+        ast_manager&     m;
+        solver*          s;
+        volatile bool    m_cancel;
+        expr_ref_vector  m_soft_constraints;
+        expr_ref_vector  m_answer;
+        vector<rational> m_weights;
+        scoped_ptr<maxsmt_solver> m_msolver;
+    public:
+        maxsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
+
+        lbool operator()(solver& s);
+
+        void set_cancel(bool f);
+
+        void updt_params(params_ref& p);
+
+        void add(expr* f, rational const& w) {
+            m_soft_constraints.push_back(f);
+            m_weights.push_back(w);
+        }
+
+        void commit_assignment();
+
+        inf_eps get_value() const;
+        inf_eps get_lower() const;
+        inf_eps get_upper() const;
+
+        expr_ref_vector get_assignment() const;
+
+        void display_answer(std::ostream& out) const;
+
+    private:
+
+        bool is_maxsat_problem(vector<rational> const& ws) const;        
+
+    };
+
+};
+
+#endif