From e4198c38e2184432ce6f38967749fea4a05e75b5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Jan 2018 11:45:39 -0800
Subject: [PATCH] add solution_prefix per #1463, have parto with single
 objective behave similar to multipe-objectives #1439

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp      |  1 +
 src/opt/maxsmt.cpp      |  6 +++++-
 src/opt/maxsmt.h        |  1 +
 src/opt/opt_context.cpp | 19 ++++++++++++++++++-
 src/opt/opt_context.h   |  6 +++++-
 src/opt/opt_params.pyg  |  1 +
 6 files changed, 31 insertions(+), 3 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index b06773223..9d32d48e3 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -727,6 +727,7 @@ public:
         }
 
         m_model = mdl;
+        m_c.model_updated(mdl);
 
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             m_assignment[i] = is_true(m_soft[i]);
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 8df6c04a6..6df375240 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -155,7 +155,7 @@ namespace opt {
                    rational l = m_adjust_value(m_lower);
                    rational u = m_adjust_value(m_upper);
                    if (l > u) std::swap(l, u);
-                   verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);        
+                   verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);                
     }
 
     lbool maxsmt_solver_base::find_mutexes(obj_map<expr, rational>& new_soft) {
@@ -391,6 +391,10 @@ namespace opt {
         return m_c.get_solver(); 
     }
 
+    void maxsmt::model_updated(model* mdl) {
+        m_c.model_updated(mdl);
+    }
+
 
 
 };
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 0541a9a88..7b4be9842 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -147,6 +147,7 @@ namespace opt {
         bool get_assignment(unsigned index) const;
         void display_answer(std::ostream& out) const;        
         void collect_statistics(statistics& st) const;
+        void model_updated(model* mdl);
     private:
         bool is_maxsat_problem(weights_t& ws) const;        
         void verify_assignment();
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4ccf30563..743ab20d9 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -138,6 +138,7 @@ namespace opt {
         p.set_bool("unsat_core", true);
         p.set_bool("elim_to_real", true);
         updt_params(p);
+        m_model_counter = 0;
     }
 
     context::~context() {
@@ -1007,6 +1008,22 @@ namespace opt {
         }
     }
 
+    void context::model_updated(model* md) {
+        opt_params optp(m_params);
+        symbol prefix = optp.solution_prefix();
+        if (prefix == symbol::null) return;        
+        model_ref mdl = md->copy();
+        fix_model(mdl);
+        std::ostringstream buffer;
+        buffer << prefix << (m_model_counter++) << ".smt2";
+        std::ofstream out(buffer.str());        
+        if (out) {
+            model_smt2_pp(out, m, *mdl, 0);
+            out.close();
+        }
+    }
+
+
     bool context::verify_model(unsigned index, model* md, rational const& _v) {
         rational r;
         app_ref term = m_objectives[index].m_term;
@@ -1015,7 +1032,7 @@ namespace opt {
         }
         rational v = m_objectives[index].m_adjust_value(_v);
         expr_ref val(m);
-        model_ref mdl = md;
+        model_ref mdl = md->copy();
         fix_model(mdl);
 
         if (!mdl->eval(term, val)) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 513f2dd85..372c6672c 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -57,6 +57,7 @@ namespace opt {
         virtual unsigned num_objectives() = 0;
         virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
         virtual void set_model(model_ref& _m) = 0;
+        virtual void model_updated(model* mdl) = 0;
     };
 
     /**
@@ -154,9 +155,10 @@ namespace opt {
         map_t               m_maxsmts;
         scoped_state        m_scoped_state;
         vector<objective>   m_objectives;
-        model_ref           m_model;
+        model_ref           m_model;        
         model_converter_ref          m_model_converter;
         filter_model_converter       m_fm;
+        unsigned                     m_model_counter;
         obj_map<func_decl, unsigned> m_objective_fns;
         obj_map<func_decl, expr*>    m_objective_orig;
         func_decl_ref_vector         m_objective_refs;
@@ -231,6 +233,8 @@ namespace opt {
 
 
         virtual bool verify_model(unsigned id, model* mdl, rational const& v);
+        
+        virtual void model_updated(model* mdl);
 
     private:
         lbool execute(objective const& obj, bool committed, bool scoped);
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index cfcc5e47e..09d849e1a 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -5,6 +5,7 @@ def_module_params('opt',
                           ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
+                          ('solution_prefix', SYMBOL, None, "path prefix to dump intermediary, but non-optimal, solutions"),
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                           ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
                           ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),