enable answer generation

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

src/opt/fu_malik.cpp

@@ -39,14 +39,17 @@ namespace opt {
         ast_manager& m;
         solver& s;
         expr_ref_vector m_soft;
+        expr_ref_vector m_orig_soft;
         expr_ref_vector m_aux;
         expr_ref_vector m_assignment;
+        unsigned        m_upper_size;
 
 
         imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
             m(m),
             s(s),
             m_soft(soft),
+            m_orig_soft(soft),
             m_aux(m),
             m_assignment(m)
         {
@@ -54,6 +57,7 @@ namespace opt {
                 m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
                 s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
             }
+            m_upper_size = m_soft.size() + 1;
         }
 
 
@@ -136,9 +140,10 @@ namespace opt {
             if (!m_soft.empty() && is_sat == l_true) {
                 opt_solver::scoped_push _sp(s);
                 
-                lbool is_sat = l_true;
+                lbool is_sat = l_true;                
                 do {
                     is_sat = step();
+                    --m_upper_size;
                 }
                 while (is_sat == l_false);
                 
@@ -148,11 +153,11 @@ namespace opt {
                     s.get_model(model);
 
                     m_assignment.reset();                    
-                    for (unsigned i = 0; i < m_soft.size(); ++i) {
+                    for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
                         expr_ref val(m);
-                        VERIFY(model->eval(m_soft[i].get(), val));
+                        VERIFY(model->eval(m_orig_soft[i].get(), val));
                         if (m.is_true(val)) {
-                            m_assignment.push_back(m_soft[i].get());
+                            m_assignment.push_back(m_orig_soft[i].get());
                         }
                     }
                 }
@@ -175,15 +180,12 @@ namespace opt {
         return (*m_imp)();
     }
     rational fu_malik::get_lower() const {
-        NOT_IMPLEMENTED_YET();
         return rational(0);
     }
     rational fu_malik::get_upper() const {
-        NOT_IMPLEMENTED_YET();
-        return rational(m_imp->m_soft.size());
+        return rational(m_imp->m_upper_size);
     }
     rational fu_malik::get_value() const {
-        NOT_IMPLEMENTED_YET();
         return rational(m_imp->m_assignment.size());
     }
     expr_ref_vector fu_malik::get_assignment() const {

src/opt/maxsmt.cpp

@@ -28,7 +28,7 @@ namespace opt {
         lbool is_sat;
         m_answer.reset();
         m_msolver = 0;
-        if (m_answer.empty()) {
+        if (m_soft_constraints.empty()) {
             m_msolver = 0;
             is_sat = s.check_sat(0, 0);
             m_answer.append(m_soft_constraints);
@@ -46,11 +46,11 @@ namespace opt {
         }
 
         // 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);
-        }
+        IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << "\n";
+                   if (is_sat == l_true) {
+                       verbose_stream() << "Satisfying soft constraints\n";
+                       display_answer(verbose_stream());
+                   });
         return is_sat;
     }
 

src/opt/maxsmt.h

@@ -62,7 +62,6 @@ namespace opt {
         }
 
         void commit_assignment();
-
         inf_eps get_value() const;
         inf_eps get_lower() const;
         inf_eps get_upper() const;

src/opt/opt_cmds.cpp

@@ -201,13 +201,14 @@ public:
         for (; it != end; ++it) {
             opt.add_hard_constraint(*it);
         }
+        lbool r = l_undef;
         cancel_eh<opt::context> eh(opt);        
         {
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);
             cmd_context::scoped_watch sw(ctx);
             try {
-                opt.optimize();
+                r = opt.optimize();
             }
             catch (z3_error& ex) {
                 ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
@@ -216,6 +217,19 @@ public:
                 ctx.regular_stream() << "(error: " << ex.msg() << "\")" << std::endl;
             }
         }
+        switch(r) {
+        case l_true:
+            ctx.regular_stream() << "sat\n";
+            opt.display_assignment(ctx.regular_stream());
+            break;
+        case l_false:
+            ctx.regular_stream() << "unsat\n";
+            break;
+        case l_undef:
+            ctx.regular_stream() << "unknown\n";
+            opt.display_range_assignment(ctx.regular_stream());
+            break;
+        }
         if (p.get_bool("print_statistics", false)) {
             display_statistics(ctx);
         }

src/opt/opt_context.cpp

@@ -6,6 +6,7 @@ Module Name:
     opt_context.cpp
 
 Abstract:
+
     Facility for running optimization problem.
 
 Author:
@@ -14,17 +15,11 @@ Author:
 
 Notes:
 
-    TODO:
-
-    - there are race conditions for cancelation.
-
 --*/
 
 #include "opt_context.h"
 #include "ast_pp.h"
 #include "opt_solver.h"
-#include "arith_decl_plugin.h"
-#include "th_rewriter.h"
 #include "opt_params.hpp"
 
 namespace opt {
@@ -55,8 +50,12 @@ namespace opt {
         ms->add(f, w);
     }
 
-    void context::optimize() {
+    lbool context::optimize() {
+        // TBD: add configurtion parameter
+        return optimize_box();
+    }
 
+    lbool context::optimize_box() {
         opt_solver& s = *m_solver.get(); 
         opt_solver::scoped_push _sp(s);
 
@@ -73,6 +72,55 @@ namespace opt {
         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;
+    }
+
+    void context::display_assignment(std::ostream& out) {
+        map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
+        for (; it != end; ++it) {
+            maxsmt* ms = it->m_value;
+            if (it->m_key != symbol::null) {
+                out << it->m_key << " : ";
+            }
+            out << ms->get_value() << "\n";
+        }
+        m_optsmt.display_assignment(out);
+    }
+
+    void context::display_range_assignment(std::ostream& out) {
+        map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
+        for (; it != end; ++it) {
+            maxsmt* ms = it->m_value;
+            if (it->m_key != symbol::null) {
+                out << it->m_key << " : ";
+            }
+            out << "[" << ms->get_lower() << ":" << ms->get_upper() << "]\n";
+        }
+        m_optsmt.display_range_assignment(out);
     }
         
     void context::set_cancel(bool f) {
@@ -86,7 +134,7 @@ namespace opt {
         }
     }
 
-    void context::collect_statistics(statistics& stats) {
+    void context::collect_statistics(statistics& stats) const {
         if (m_solver) {
             m_solver->collect_statistics(stats);
         }

src/opt/opt_context.h

@@ -48,11 +48,15 @@ namespace opt {
         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_hard_constraint(expr* f) { m_hard_constraints.push_back(f);  }
-        void optimize();
+        lbool optimize();
+        lbool optimize_pareto();
+        lbool optimize_box();
         void set_cancel(bool f);
         void reset_cancel() { set_cancel(false); }
         void cancel() { set_cancel(true); }
-        void collect_statistics(statistics& stats);
+        void collect_statistics(statistics& stats) const;
+        void display_assignment(std::ostream& out);
+        void display_range_assignment(std::ostream& out);
         static void collect_param_descrs(param_descrs & r);
         void updt_params(params_ref& p);
     };

src/opt/optsmt.cpp

@@ -238,8 +238,8 @@ namespace opt {
             }
         }
 
-        std::cout << "is-sat: " << is_sat << std::endl;
-        display(std::cout);
+        IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << std::endl;
+                   display_assignment(verbose_stream()););
 
         return is_sat;
     }
@@ -262,22 +262,35 @@ namespace opt {
         s->assert_expr(s->block_upper_bound(i, get_lower(i)));
     }
 
-    void optsmt::display(std::ostream& out) const {
+    std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const {
+        bool is_max = m_is_max[i];
+        inf_eps val = get_value(i);
+        expr_ref obj(m_objs[i], m);
+        if (!is_max) {
+            arith_util a(m);
+            th_rewriter rw(m);
+            obj = a.mk_uminus(obj);
+            rw(obj, obj);
+        }
+        return out << obj;
+    }
+
+    void optsmt::display_assignment(std::ostream& out) const {
         unsigned sz = m_objs.size();
         for (unsigned i = 0; i < sz; ++i) {
-            bool is_max = m_is_max[i];
-            inf_eps val = get_value(i);
-            expr_ref obj(m_objs[i], m);
-            if (!is_max) {
-                arith_util a(m);
-                th_rewriter rw(m);
-                obj = a.mk_uminus(obj);
-                rw(obj, obj);
-            }
-            out << "objective value: " << obj << " |-> " << val << std::endl;                
+            display_objective(out, i) << " |-> " << get_value(i) << std::endl;                
         }        
     }
 
+    void optsmt::display_range_assignment(std::ostream& out) const {
+        unsigned sz = m_objs.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            display_objective(out, i) << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]" << std::endl;                
+        }        
+    }
+
+
+
     void optsmt::add(app* t, bool is_max) {
         expr_ref t1(t, m), t2(m);
         th_rewriter rw(m);

src/opt/optsmt.h

@@ -44,20 +44,23 @@ namespace opt {
 
         void add(app* t, bool is_max);
 
-        void commit_assignment(unsigned i);
-
         void set_cancel(bool f);
 
         void updt_params(params_ref& p);
 
-        void display(std::ostream& out) const;
+        void display_assignment(std::ostream& out) const;
+        void display_range_assignment(std::ostream& out) const;
 
+        unsigned get_num_objectives() const { return m_vars.size(); }
+        void commit_assignment(unsigned i);
         inf_eps get_value(unsigned index) const;
         inf_eps get_lower(unsigned index) const;
         inf_eps get_upper(unsigned index) const;
         
     private:
         
+        std::ostream& display_objective(std::ostream& out, unsigned i) const;
+
         lbool basic_opt();
 
         lbool farkas_opt();

src/opt/weighted_maxsat.h

@@ -6,7 +6,8 @@ Module Name:
     weighted_maxsat.h
 
 Abstract:
-   Weighted MAXSAT module
+
+    Weighted MAXSAT module
 
 Author:
 
@@ -14,6 +15,10 @@ Author:
 
 Notes:
 
+    Takes solver with hard constraints added.
+    Returns a maximal satisfying subset of weighted soft_constraints
+    that are still consistent with the solver state.
+
 --*/
 #ifndef _OPT_WEIGHTED_MAX_SAT_H_
 #define _OPT_WEIGHTED_MAX_SAT_H_
@@ -22,11 +27,6 @@ Notes:
 #include "maxsmt.h"
 
 namespace opt {
-    /**
-       Takes solver with hard constraints added.
-       Returns a maximal satisfying subset of weighted soft_constraints
-       that are still consistent with the solver state.
-    */
     class wmaxsmt : public maxsmt_solver {
         struct imp;
         imp* m_imp;