From ebf6b1882121309be2997476c193a2d9d8d225a4 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 16 May 2018 08:59:11 -0700
Subject: [PATCH] maxsat standalone mode

---
 src/opt/maxsmt.cpp | 56 +++++++++++++++++++++++++++++++++++++++++++++-
 src/opt/maxsmt.h   | 42 ++++++++++++++++++++++++++++++++++
 2 files changed, 97 insertions(+), 1 deletion(-)

diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index afecf7d2b..fc5bd6bbb 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -21,6 +21,7 @@ Notes:
 #include "opt/maxsmt.h"
 #include "opt/maxres.h"
 #include "opt/wmax.h"
+#include "opt/opt_params.hpp"
 #include "ast/ast_pp.h"
 #include "util/uint_set.h"
 #include "opt/opt_context.h"
@@ -409,6 +410,59 @@ namespace opt {
         m_c.model_updated(mdl);
     }
 
+    class solver_maxsat_context : public maxsat_context {
+        params_ref m_params;
+        solver_ref m_solver;
+        model_ref  m_model;
+        ref<generic_model_converter> m_fm; 
+        symbol m_maxsat_engine;
+    public:
+        solver_maxsat_context(params_ref& p, solver* s, model * m): 
+            m_params(p), 
+            m_solver(s),
+            m_model(m),
+            m_fm(alloc(generic_model_converter, s->get_manager(), "maxsmt")) {
+            opt_params _p(p);
+            m_maxsat_engine = _p.maxsat_engine();            
+        }
+        generic_model_converter& fm() override { return *m_fm.get(); }
+        bool sat_enabled() const override { return false; }
+        solver& get_solver() override { return *m_solver.get(); }
+        ast_manager& get_manager() const override { return m_solver->get_manager(); }
+        params_ref& params() override { return m_params; }
+        void enable_sls(bool force) override { } // no op
+        symbol const& maxsat_engine() const override { return m_maxsat_engine; }
+        void get_base_model(model_ref& _m) override { _m = m_model; };  
+        smt::context& smt_context() override { 
+            throw default_exception("stand-alone maxsat context does not support wmax"); 
+        }
+        unsigned num_objectives() override { return 1; }
+        bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; };
+        void set_model(model_ref& _m) override { m_model = _m; }
+        void model_updated(model* mdl) override { } // no-op
+    };
 
-
+    lbool maxsmt_wrapper::operator()(vector<std::pair<expr*,rational>>& soft) {
+        solver_maxsat_context ctx(m_params, m_solver.get(), m_model.get());
+        maxsmt maxsmt(ctx, 0);
+        for (auto const& p : soft) {
+            maxsmt.add(p.first, p.second);
+        }
+        lbool r = maxsmt();
+        if (r == l_true) {
+            ast_manager& m = m_solver->get_manager();
+            svector<symbol> labels;
+            maxsmt.get_model(m_model, labels);
+            // TBD: is m_fm applied or not?
+            unsigned j = 0;
+            expr_ref tmp(m);
+            for (unsigned i = 0; i < soft.size(); ++i) {
+                if (m_model->eval(soft[i].first, tmp) && m.is_true(tmp)) {
+                    soft[j++] = soft[i];
+                }
+            }
+            soft.shrink(j);
+        }
+        return r;
+    }
 };
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 9e52481f2..422cf26b9 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -153,6 +153,48 @@ namespace opt {
         solver& s();
     };
 
+    /**
+       \brief Standalone MaxSMT solver.
+
+       It takes as input a solver object and provides a MaxSAT solver routine.
+
+       It assumes the solver state is satisfiable and therefore there is a model
+       associated with the constraints asserted to the solver. A model of the 
+       solver state must be supplied as a last argument.
+
+       It assumes that the caller manages scope on the solver such that
+       the solver can be left in a stronger or inconsistent state upon return.
+       Callers should therefore use this feature under a push/pop.
+    */
+    class maxsmt_wrapper {
+        params_ref  m_params;
+        ref<solver> m_solver;
+        model_ref   m_model;
+    public:
+        maxsmt_wrapper(params_ref & p, solver* s, model* m): 
+            m_params(p), 
+            m_solver(s),
+            m_model(m) {}
+        
+        lbool operator()(expr_ref_vector& soft) {
+            vector<std::pair<expr*, rational>> _soft;
+            for (expr* e : soft) _soft.push_back(std::make_pair(e, rational::one()));
+            lbool r = (*this)(_soft);
+            soft.reset();
+            for (auto const& p : _soft) soft.push_back(p.first);
+            return r;
+        }
+
+        /**
+           \brief takes a vector of weighted soft constraints.
+           Returns a modified list of soft constraints that are 
+           satisfied in the maximal satisfying assignment.
+        */
+        lbool operator()(vector<std::pair<expr*,rational>> & soft);
+
+        model_ref get_model() { return m_model; }
+    };
+
 };
 
 #endif