Reorganize combination of objectives

src/opt/objective_ast.cpp

@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    objective_ast.h
+
+Abstract:
+    Abstract data-type for compound objectives.
+
+Author:
+
+    Anh-Dung Phan (t-anphan) 2013-11-26
+
+Notes:
+
+--*/
+
+#include"objective_ast.h"
+
+namespace opt {
+
+    objective* objective::mk_max(expr_ref& e) { return alloc(min_max_objective, MAXIMIZE, e); };
+    objective* objective::mk_min(expr_ref& e) { return alloc(min_max_objective, MINIMIZE, e); };
+    objective* objective::mk_maxsat(symbol id) { return alloc(maxsat_objective, id); };
+
+    objective* objective::mk_lex(unsigned sz, objective * const* children) { 
+        return alloc(compound_objective, LEX, sz, children); 
+    };
+
+    objective* objective::mk_box(unsigned sz, objective * const* children) {
+        return alloc(compound_objective, BOX, sz, children);  
+    };
+
+    objective* objective::mk_pareto(unsigned sz, objective * const* children) {
+        return alloc(compound_objective, PARETO, sz, children); 
+    };
+
+    compound_objective& objective::get_compound() { 
+        SASSERT(m_type == LEX || m_type == BOX || m_type == PARETO); 
+        return dynamic_cast<compound_objective&>(*this);
+    }
+
+    min_max_objective& objective::get_min_max() {
+        SASSERT(m_type == MAXIMIZE || m_type == MINIMIZE); 
+        return dynamic_cast<min_max_objective&>(*this);
+    }
+
+    maxsat_objective& objective::get_maxsat() {
+        SASSERT(m_type == MAXSAT); 
+        return dynamic_cast<maxsat_objective&>(*this);
+    }
+
+};

src/opt/objective_ast.h

@@ -18,6 +18,8 @@ Notes:
 #ifndef __OBJECTIVE_AST_H_
 #define __OBJECTIVE_AST_H_
 
+#include"ast.h"
+
 namespace opt {
 
     enum objective_t {
@@ -46,35 +48,45 @@ namespace opt {
         // constructors;
         static objective* mk_max(expr_ref& e);
         static objective* mk_min(expr_ref& e);
+        static objective* mk_maxsat(symbol id);
+
         static objective* mk_lex(unsigned sz, objective * const* children);
         static objective* mk_box(unsigned sz, objective * const* children);
         static objective* mk_pareto(unsigned sz, objective * const* children);
-        static objective* mk_maxsat(symbol id);
 
         // accessors (implicit cast operations)
-        compound_objective& get_compound(); // eg. SASSERT(m_type == LEX/BOX/PARETO); return dynamic_cast<compound_objective&>(*this); 
-        min_max_objective&  get_min_max();
-        maxsat_objective&   get_maxsat();
+        compound_objective& get_compound();
+        min_max_objective& get_min_max();
+        maxsat_objective& get_maxsat();
     };
 
     class compound_objective : public objective {
         ptr_vector<objective> m_children;
     public:
-        compound_objective(objective_t t): objective(t) {}
+        compound_objective(objective_t t, unsigned sz, objective * const* children): 
+            objective(t), 
+            m_children(sz, children) {}
+
         virtual ~compound_objective() { 
-            // dealloc vector m_children; 
+            ptr_vector<objective>::iterator it = m_children.begin(), end = m_children.end();
+            for (; it != end; ++it) {
+                dealloc(*it);
+            }
         }
 
         objective *const* children() const { return m_children.c_ptr(); }
 
         unsigned num_children() const { return m_children.size(); }
-    }
+    };
 
     class min_max_objective : public objective {
         bool     m_is_max;
         expr_ref m_expr;
     public:
-        min_max_objective(bool is_max, expr_ref& e): m_is_max(is_max), m_expr(e) {}
+        min_max_objective(bool is_max, expr_ref& e): 
+            objective(is_max ? MAXIMIZE : MINIMIZE), 
+            m_is_max(is_max), 
+            m_expr(e) {}
 
         virtual ~min_max_objective() {}
 
@@ -85,7 +97,7 @@ namespace opt {
     class maxsat_objective : public objective {
         symbol m_id;
     public:
-        maxsat_objective(symbol const& id): m_id(id) {}
+        maxsat_objective(symbol const& id): objective(MAXSAT), m_id(id) {}
         virtual ~maxsat_objective() {}
         
         symbol const& get_id() const { return m_id; }

src/opt/opt_context.cpp

@@ -27,7 +27,8 @@ namespace opt {
     context::context(ast_manager& m):
         m(m),
         m_hard_constraints(m),
-        m_optsmt(m)
+        m_optsmt(m),
+        m_objs(m)
     {
         m_params.set_bool("model", true);
         m_params.set_bool("unsat_core", true);
@@ -50,57 +51,98 @@ namespace opt {
         ms->add(f, w);
     }
 
-    lbool context::optimize() {
-        if (m_params.get_bool("pareto", false)) {            
-            return optimize_pareto();
-        }
-        else {
-            return optimize_box();
+    lbool context::execute(objective & obj, bool committed) {
+        switch (obj.type()) {
+        case MINIMIZE:
+        case MAXIMIZE: 
+            return execute_min_max(obj.get_min_max(), committed);
+        case MAXSAT:
+            return execute_maxsat(obj.get_maxsat(), committed);
+        case LEX:
+            return execute_lex(obj.get_compound());
+        case BOX:
+            return execute_box(obj.get_compound());
+        case PARETO:
+            return execute_pareto(obj.get_compound());
+        default:
+            UNREACHABLE();
+            return l_undef;
         }
     }
 
-    lbool context::optimize_box() {
+    lbool context::execute_min_max(min_max_objective & obj, bool committed) {
+        // HACK: reuse m_optsmt but add only a single objective each round
+        m_optsmt.add(to_app(obj.term()), obj.is_max());
+        opt_solver& s = *m_solver.get();
+        lbool result = m_optsmt(s);
+        if (committed) m_optsmt.commit_assignment(0);
+        return result;
+    }
+
+    lbool context::execute_maxsat(maxsat_objective & obj, bool committed) {
+        maxsmt* ms;
+        SASSERT(m_maxsmts.find(obj.get_id(), ms));
+        opt_solver& s = *m_solver.get();
+        lbool result = (*ms)(s);
+        if (committed) ms->commit_assignment();
+        return result;
+    }
+    
+    lbool context::execute_lex(compound_objective & obj) {
+        ptr_vector<objective> children(obj.num_children(), obj.children());
+        for (unsigned i = 0; i < children.size(); ++i) {
+            lbool result = execute(*children[i], true);
+            if (result != l_true) return result;
+        }
+        return l_true;
+    }
+
+    lbool context::execute_box(compound_objective & obj) {
+        ptr_vector<objective> children(obj.num_children(), obj.children());
+        for (unsigned i = 0; i < children.size(); ++i) {
+            lbool result = execute(*children[i], false);
+            if (result != l_true) return result;
+        }
+        return l_true;
+    }
+
+    lbool context::execute_pareto(compound_objective & obj) {
+        // TODO: record a stream of results from pareto front
+        return execute_lex(obj);
+    }
+
+    lbool context::optimize() {
+        // Construct objectives
+        ptr_vector<objective> objectives;
+        map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
+        for (; it != end; ++it) {
+            objectives.push_back(objective::mk_maxsat(it->m_key));
+        }
+
+        for (unsigned i = 0; i < m_objs.size(); ++i) {
+            expr_ref e(m_objs[i].get(), m);
+            objective * o = m_ismaxs[i] ? objective::mk_max(e) : objective::mk_min(e);
+            objectives.push_back(o);
+        }
+
+        objective * objective;
+        if (m_params.get_bool("pareto", false)) {            
+            objective = objective::mk_pareto(objectives.size(), objectives.c_ptr());
+        }
+        else {
+            objective = objective::mk_box(objectives.size(), objectives.c_ptr());
+        }
+
         opt_solver& s = *m_solver.get(); 
         solver::scoped_push _sp(s);
 
         for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
             s.assert_expr(m_hard_constraints[i].get());
         }
-                
-        lbool is_sat = l_true;
-        map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
-        for (; is_sat == l_true && it != end; ++it) {
-            maxsmt& ms = *it->m_value;
-            is_sat = ms(s);
-        }
-        if (is_sat == l_true) {           
-            is_sat = m_optsmt(s);
-        }
-        return is_sat;
-    }
 
-    // finds a random pareto front.
-    // enumerating more is TBD, e.g., 
-    lbool context::optimize_pareto() {
-        opt_solver& s = *m_solver.get(); 
-        opt_solver::scoped_push _sp(s);
-
-        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
-            s.assert_expr(m_hard_constraints[i].get());
-        }
-                
-        lbool is_sat = l_true;
-        map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
-        for (; is_sat == l_true && it != end; ++it) {
-            maxsmt* ms = it->m_value;
-            is_sat = (*ms)(s);
-            ms->commit_assignment();            
-        }
-        for (unsigned i = 0; is_sat == l_true && i < m_optsmt.get_num_objectives(); ++i) {
-            is_sat = m_optsmt(s);
-            m_optsmt.commit_assignment(i);
-        }
-        return is_sat;
+        lbool result = execute(*objective, false);
+        dealloc(objective);
+        return result;
     }
 
     void context::display_assignment(std::ostream& out) {

src/opt/opt_context.h

@@ -29,6 +29,7 @@ Notes:
 #include "opt_solver.h"
 #include "optsmt.h"
 #include "maxsmt.h"
+#include "objective_ast.h"
 
 namespace opt {
 
@@ -42,12 +43,22 @@ namespace opt {
         params_ref          m_params;
         optsmt              m_optsmt;
         map_t               m_maxsmts;
+        expr_ref_vector     m_objs;
+        svector<bool>       m_ismaxs;
     public:
         context(ast_manager& m);
         ~context();
         void add_soft_constraint(expr* f, rational const& w, symbol const& id);
-        void add_objective(app* t, bool is_max) { m_optsmt.add(t, is_max); }
+        void add_objective(app* t, bool is_max) { m_objs.push_back(t); m_ismaxs.push_back(is_max); }
         void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f);  }
+
+        lbool execute(objective & obj, bool committed);
+        lbool execute_min_max(min_max_objective & obj, bool committed);
+        lbool execute_maxsat(maxsat_objective & obj, bool committed);
+        lbool execute_lex(compound_objective & obj);
+        lbool execute_box(compound_objective & obj);
+        lbool execute_pareto(compound_objective & obj);
+
         lbool optimize();
         void set_cancel(bool f);
         void reset_cancel() { set_cancel(false); }
@@ -58,9 +69,6 @@ namespace opt {
         static void collect_param_descrs(param_descrs & r);
         void updt_params(params_ref& p);
     private:
-        lbool optimize_pareto();
-        lbool optimize_box();
-
         void validate_feasibility(maxsmt& ms);
     };
 

src/opt/opt_solver.cpp

@@ -56,7 +56,7 @@ namespace opt {
     }
     
     void opt_solver::collect_statistics(statistics & st) const {
-        // Hack to display fu_malik statistics
+        // HACK: display fu_malik statistics
         if (m_stats.size() > 0) {
             st.copy(m_stats);
         }