more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/opt_context.cpp

@@ -27,7 +27,6 @@ Notes:
 #include "th_rewriter.h"
 #include "opt_params.hpp"
 
-
 namespace opt {
 
     context::context(ast_manager& m):
@@ -49,7 +48,7 @@ namespace opt {
 
         // really just works for opt_solver now.
         solver* s = m_solver.get(); 
-        opt_solver::scoped_push _sp(get_opt_solver(*s));
+        opt_solver::scoped_push _sp(*s);
 
         for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
             s->assert_expr(m_hard_constraints[i].get());
@@ -57,7 +56,7 @@ namespace opt {
         
         lbool is_sat;
 
-        is_sat = m_maxsmt(get_opt_solver(*s));
+        is_sat = m_maxsmt(*s);
 
         expr_ref_vector ans = m_maxsmt.get_assignment();
         for (unsigned i = 0; i < ans.size(); ++i) {
@@ -65,32 +64,17 @@ namespace opt {
         }
 
         if (is_sat == l_true) {           
-            is_sat = m_optsmt(get_opt_solver(*s));        
+            is_sat = m_optsmt(opt_solver::to_opt(*s));
         }
     }
         
 
-    opt_solver& context::get_opt_solver(solver& s) {
-        if (typeid(opt_solver) != typeid(s)) {
-            throw default_exception("BUG: optimization context has not been initialized correctly");
-        }
-        return dynamic_cast<opt_solver&>(s);
-    }
-
-    void context::cancel() {
+    void context::set_cancel(bool f) {
         if (m_solver) {
-            m_solver->cancel();
+            m_solver->set_cancel(f);
         }
-        m_optsmt.set_cancel(true);
-        m_maxsmt.set_cancel(true);
-    }
-
-    void context::reset_cancel() {
-        if (m_solver) {
-            m_solver->reset_cancel();
-        }
-        m_optsmt.set_cancel(false);
-        m_maxsmt.set_cancel(false);
+        m_optsmt.set_cancel(f);
+        m_maxsmt.set_cancel(f);
     }
 
     void context::collect_statistics(statistics& stats) {
@@ -108,8 +92,7 @@ namespace opt {
         if (m_solver) {
             m_solver->updt_params(m_params);
         }
-        opt_params _p(m_params);
-        m_optsmt.set_engine(_p.engine());        
+        m_optsmt.updt_params(m_params);
     }
 
 

src/opt/opt_context.h

@@ -28,7 +28,7 @@ Notes:
 #include "ast.h"
 #include "solver.h"
 #include "optsmt.h"
-#include "opt_maxsmt.h"
+#include "maxsmt.h"
 
 namespace opt {
 
@@ -49,8 +49,9 @@ namespace opt {
         void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f);  }
         void set_solver(solver* s) { m_solver = s; }
         void optimize();
-        void cancel();
-        void reset_cancel();
+        void set_cancel(bool f);
+        void reset_cancel() { set_cancel(false); }
+        void cancel() { set_cancel(true); }
         void collect_statistics(statistics& stats);
         static void collect_param_descrs(param_descrs & r);
         void updt_params(params_ref& p);

src/opt/opt_maxsmt.cpp

@@ -1,75 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    opt_maxsmt.cpp
-
-Abstract:
-   
-    MaxSMT optimization context.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2013-11-7
-
-Notes:
-
---*/
-
-#include "opt_maxsmt.h"
-#include "fu_malik.h"
-#include "weighted_maxsat.h"
-#include "ast_pp.h"
-
-namespace opt {
-
-    lbool maxsmt::operator()(opt_solver& s) {
-        lbool is_sat;
-        m_answer.reset();
-        m_answer.append(m_soft_constraints);
-        if (m_answer.empty()) {
-            is_sat = s.check_sat(0, 0);
-        }
-        else if (is_maxsat_problem(m_weights)) {
-            is_sat = opt::fu_malik_maxsat(s, m_answer);
-        }
-        else {
-            is_sat = weighted_maxsat(s, m_answer, m_weights);
-        }
-
-        // 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;
-    } 
-
-    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;
-    }
-    
-    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;
-    }
-
-
-
-};

src/opt/opt_maxsmt.h

@@ -1,66 +0,0 @@
-/*++
-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 "opt_solver.h"
-
-namespace opt {
-    /**
-       Takes solver with hard constraints added.
-       Returns modified soft constraints that are maximal assignments.
-    */
-
-    class maxsmt {
-        ast_manager&     m;
-        opt_solver*      s;
-        volatile bool    m_cancel;
-        expr_ref_vector  m_soft_constraints;
-        expr_ref_vector  m_answer;
-        vector<rational> m_weights;
-        symbol           m_engine;
-    public:
-        maxsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
-
-        lbool operator()(opt_solver& s);
-
-        void set_cancel(bool f);
-
-        void add(expr* f, rational const& w) {
-            m_soft_constraints.push_back(f);
-            m_weights.push_back(w);
-        }
-
-        void set_engine(symbol const& e) { m_engine = e; }
-
-        // TBD: rational get_value() 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

src/opt/opt_solver.cpp

@@ -187,6 +187,13 @@ namespace opt {
         m_objective_values.reset();
     }
 
+    opt_solver& opt_solver::to_opt(solver& s) {
+        if (typeid(opt_solver) != typeid(s)) {
+            throw default_exception("BUG: optimization context has not been initialized correctly");
+        }
+        return dynamic_cast<opt_solver&>(s);
+    }
+
     opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) {
         s.m_objective_enabled = new_value;
     }

src/opt/opt_solver.h

@@ -73,6 +73,8 @@ namespace opt {
 
         vector<inf_eps> const& get_objective_values();
         expr_ref block_lower_bound(unsigned obj_index, inf_eps const& val);
+
+        static opt_solver& to_opt(solver& s);
         
         class toggle_objective {
             opt_solver& s;
@@ -83,9 +85,9 @@ namespace opt {
         };
 
         class scoped_push {
-            opt_solver& s;
+            solver& s;
         public:
-            scoped_push(opt_solver& s):s(s) { s.push();  }
+            scoped_push(solver& s):s(s) { s.push();  }
             ~scoped_push() { s.pop(1); }
         };
 

src/opt/optsmt.cpp

@@ -47,6 +47,7 @@ Notes:
 #include "ast_pp.h"
 #include "model_pp.h"
 #include "th_rewriter.h"
+#include "opt_params.hpp"
 
 namespace opt {
 
@@ -245,8 +246,8 @@ namespace opt {
         return is_sat;
     }
 
-    inf_eps  optsmt::get_value(bool as_positive, unsigned index) const {
-        if (as_positive) {
+    inf_eps  optsmt::get_value(unsigned index) const {
+        if (m_is_max[index]) {
             return m_lower[index];
         }
         else {
@@ -258,7 +259,7 @@ namespace opt {
         unsigned sz = m_objs.size();
         for (unsigned i = 0; i < sz; ++i) {
             bool is_max = m_is_max[i];
-            inf_eps val = get_value(is_max, i);
+            inf_eps val = get_value(i);
             expr_ref obj(m_objs[i], m);
             if (!is_max) {
                 arith_util a(m);
@@ -283,6 +284,10 @@ namespace opt {
         m_is_max.push_back(is_max);
     }
 
+    void optsmt::updt_params(params_ref& p) {
+        opt_params _p(p);
+        m_engine = _p.engine();        
+    }
 
 }
 

src/opt/optsmt.h

@@ -36,7 +36,7 @@ namespace opt {
         app_ref_vector   m_objs;
         svector<bool>    m_is_max;
         svector<smt::theory_var> m_vars;
-        symbol m_engine;
+        symbol           m_engine;
     public:
         optsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {}
 
@@ -46,11 +46,11 @@ namespace opt {
 
         void set_cancel(bool f);
 
-        void set_engine(symbol const& e) { m_engine = e; }
+        void updt_params(params_ref& p);
 
         void display(std::ostream& out) const;
 
-        inf_eps get_value(bool as_positive, unsigned index) const;
+        inf_eps get_value(unsigned index) const;
 
     private: