push blocking code to optimizer context

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

src/opt/opt_context.cpp

@@ -76,7 +76,8 @@ namespace opt {
             for (unsigned i = 0; i < fmls_copy.size(); ++i) {
                 s->assert_expr(fmls_copy[i].get());
             }
-            is_sat = optimize_objectives(get_opt_solver(*s), m_objectives, values);
+            optimize_objectives obj(m, get_opt_solver(*s)); // TBD: make an attribute
+            is_sat = obj(m_objectives, values);
             std::cout << "is-sat: " << is_sat << std::endl;
 
             if (is_sat != l_true) {

src/opt/opt_solver.cpp

@@ -6,10 +6,11 @@
 
 namespace opt {
 
-    opt_solver::opt_solver(ast_manager & m, params_ref const & p, symbol const & l):
-        solver_na2as(m),
+    opt_solver::opt_solver(ast_manager & mgr, params_ref const & p, symbol const & l):
+        solver_na2as(mgr),
         m_params(p),
-        m_context(m, m_params),
+        m_context(mgr, m_params),
+        m(mgr),
         m_objective_enabled(false) {
         m_logic = l;
         if (m_logic != symbol::null)
@@ -139,9 +140,21 @@ namespace opt {
         return m_objective_vars.back();
     }
     
-    vector<opt_solver::inf_value> const& opt_solver::get_objective_values() {
+    vector<inf_eps> const& opt_solver::get_objective_values() {
         return m_objective_values;
     }
+    
+    expr_ref opt_solver::block_lower_bound(unsigned var, inf_eps const& val) {
+        if (val.get_infinity().is_pos()) {
+            return expr_ref(m.mk_false(), m);
+        }
+        else if (val.get_infinity().is_neg()) {
+            return expr_ref(m.mk_true(), m);
+        }
+        else {
+            return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], val.get_numeral()), m);
+        }
+    }
 
     void opt_solver::reset_objectives() {
         m_objective_vars.reset();

src/opt/opt_solver.h

@@ -33,17 +33,19 @@ Notes:
 
 namespace opt {
 
+    typedef inf_eps_rational<inf_rational> inf_eps;
+
+
     class opt_solver : public solver_na2as {
-    public:
-        typedef inf_eps_rational<inf_rational> inf_value;
     private:
         smt_params          m_params;
         smt::kernel         m_context;
+        ast_manager&        m;
         progress_callback * m_callback;
         symbol              m_logic;
         bool                m_objective_enabled;
         svector<smt::theory_var>  m_objective_vars;
-        vector<inf_value>         m_objective_values;
+        vector<inf_eps>         m_objective_values;
     public:
         opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
         virtual ~opt_solver();
@@ -69,7 +71,8 @@ namespace opt {
         smt::theory_var add_objective(app* term);
         void reset_objectives();
 
-        vector<inf_value> const& get_objective_values();
+        vector<inf_eps> const& get_objective_values();
+        expr_ref block_lower_bound(unsigned obj_index, inf_eps const& val);
         
         class toggle_objective {
             opt_solver& s;

src/opt/optimize_objectives.cpp

@@ -46,83 +46,92 @@ Notes:
 
 namespace opt {
 
+    class scoped_push {
+        opt_solver& s;
+    public:
+        scoped_push(opt_solver& s):s(s) {
+            s.push();
+        }
+        ~scoped_push() {
+            s.pop(1);
+        }
+    };
+
+    void optimize_objectives::set_cancel(bool f) {
+        m_cancel = true;
+    }
+
+    void optimize_objectives::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src) {
+        for (unsigned i = 0; i < src.size(); ++i) {
+            if (src[i] > dst[i]) {
+                dst[i] = src[i];
+            }
+        }
+    }
+
+
     /*
         Enumerate locally optimal assignments until fixedpoint.
     */
-    lbool mathsat_style_opt(
-        opt_solver& s, 
-        app_ref_vector const& objectives, 
-        vector<inf_eps_rational<inf_rational> >& values) 
+    lbool optimize_objectives::basic_opt(app_ref_vector& objectives, vector<inf_eps>& values)
     {
         ast_manager& m = objectives.get_manager();
         arith_util autil(m);
 
         s.reset_objectives();
+        values.reset();
         // First check_sat call to initialize theories
         lbool is_sat = s.check_sat(0, 0);
         if (is_sat == l_false) {
             return is_sat;
         }
 
-        s.push();
+        scoped_push _push(s);
 
         opt_solver::toggle_objective _t(s, true);
 
         for (unsigned i = 0; i < objectives.size(); ++i) {
-            s.add_objective(objectives[i]);            
+            s.add_objective(objectives[i].get());
+            values.push_back(inf_eps(rational(-1),inf_rational(0)));
         }
 
         is_sat = s.check_sat(0, 0);
+        
                 
-        while (is_sat == l_true) {
-            // Extract values for objectives
-            values.reset();
-            values.append(s.get_objective_values());
+        while (is_sat == l_true && !m_cancel) {
+            set_max(values, s.get_objective_values());
             IF_VERBOSE(1, 
                        for (unsigned i = 0; i < values.size(); ++i) {
                            verbose_stream() << values[i] << " ";
                        }
                        verbose_stream() << "\n";);
             expr_ref_vector disj(m);
-            expr_ref constraint(m), num(m);
-            for (unsigned i = 0; i < objectives.size(); ++i) {
+            expr_ref constraint(m);
 
-                if (!values[i].get_infinity().is_zero()) {
-                    continue;
-                }
-                num = autil.mk_numeral(values[i].get_rational(), m.get_sort(objectives[i]));
-                
-                SASSERT(values[i].get_infinitesimal().is_nonpos());
-                if (values[i].get_infinitesimal().is_neg()) {
-                    disj.push_back(autil.mk_ge(objectives[i], num));
-                }
-                else {
-                    disj.push_back(autil.mk_gt(objectives[i], num));
-                }
+            for (unsigned i = 0; i < objectives.size(); ++i) {
+                inf_eps const& v = values[i];
+                disj.push_back(s.block_lower_bound(i, v));
             }
             constraint = m.mk_or(disj.size(), disj.c_ptr());
             s.assert_expr(constraint);
             is_sat = s.check_sat(0, 0);
         }      
 
-        s.pop(1);
-       
-        if (is_sat == l_undef) {
-            return is_sat;
+        
+        if (m_cancel || is_sat == l_undef) {
+            return l_undef;
         }
-        return l_true;
+        return l_true;        
     }
 
     /**
        Takes solver with hard constraints added.
        Returns an optimal assignment to objective functions.
     */
-    
-    lbool optimize_objectives(opt_solver& s, 
-                          app_ref_vector& objectives, 
-                          vector<inf_eps_rational<inf_rational> >& values) {
-        return mathsat_style_opt(s, objectives, values);
+    lbool optimize_objectives::operator()(app_ref_vector& objectives, vector<inf_eps>& values) {
+        return basic_opt(objectives, values);
     }
+
 }
 
 #endif

src/opt/optimize_objectives.h

@@ -26,10 +26,26 @@ namespace opt {
        Takes solver with hard constraints added.
        Returns an optimal assignment to objective functions.
     */
-    
-    lbool optimize_objectives(opt_solver& s, 
-                              app_ref_vector& objectives, 
-                              vector<inf_eps_rational<inf_rational> >& values);
+
+    class optimize_objectives {
+        ast_manager& m;
+        opt_solver& s;
+        volatile bool m_cancel;
+    public:
+        optimize_objectives(ast_manager& m, opt_solver& s): m(m), s(s), m_cancel(false) {}
+
+        lbool operator()(app_ref_vector& objectives, vector<inf_eps>& values);
+
+        void set_cancel(bool f);
+
+    private:
+        
+        lbool basic_opt(app_ref_vector&  objectives, vector<inf_eps>& values);
+
+        void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src);
+
+    };
+
 };
 
 #endif

src/smt/theory_arith.h

@@ -996,6 +996,7 @@ namespace smt {
         virtual bool maximize(theory_var v);
         virtual theory_var add_objective(app* term);
         virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
+        virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
         inf_rational m_objective_value;
 
         // -----------------------------------

src/smt/theory_arith_aux.h

@@ -965,11 +965,12 @@ namespace smt {
     }
 
     //
-    // set_objective(expr* term) internalizes the arithmetic term and creates
+    // add_objective(expr* term) internalizes the arithmetic term and creates
     // a row for it if it is not already internalized. 
     // Then return the variable corresponding to the term.
     //
 
+
     template<typename Ext>
     theory_var theory_arith<Ext>::add_objective(app* term) {
         return internalize_term_core(term);
@@ -981,6 +982,20 @@ namespace smt {
         return r || at_upper(v);
     }
 
+    template<typename Ext>
+    expr* theory_arith<Ext>::block_lower_bound(theory_var v, inf_rational const& val) {
+        ast_manager& m = get_manager();
+        expr* obj = get_enode(v)->get_owner();
+        expr_ref e(m);
+        e = m_util.mk_numeral(val.get_rational(), m.get_sort(obj));
+
+        if (val.get_infinitesimal().is_neg()) {
+            return m_util.mk_ge(obj, e);
+        }
+        else {
+            return m_util.mk_gt(obj, e);
+        }
+    }
 
     template<typename Ext>
     inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) { 

src/smt/theory_diff_logic.h

@@ -307,7 +307,11 @@ namespace smt {
         virtual bool maximize(theory_var v);
         virtual theory_var add_objective(app* term);
         virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
-        numeral m_objective_value;
+        virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
+
+        // TBD: why are these public?:
+        numeral                        m_objective_value;
+
 
         typedef vector <std::pair<theory_var, rational> > objective_term;
         vector<objective_term> m_objectives;

src/smt/theory_diff_logic_def.h

@@ -1053,6 +1053,42 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::get_objective_value(theor
     return inf_eps_rational<inf_rational>(inf_rational(r, i));
 }
 
+template<typename Ext>
+expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const& val) {
+    ast_manager& m = get_manager();
+    objective_term const& t = m_objectives[v];
+    expr_ref e(m), f(m), f2(m);
+    // hacky implementation for now.
+    if (t.size() == 1 && t[0].second.is_one()) {
+        f = get_enode(t[0].first)->get_owner();
+    }
+    else if (t.size() == 1 && t[0].second.is_minus_one()) {
+        f = m_util.mk_uminus(get_enode(t[0].first)->get_owner());
+    }
+    else if (t.size() == 2 && t[0].second.is_one() && t[1].second.is_minus_one()) {
+        f = get_enode(t[0].first)->get_owner();
+        f2 = get_enode(t[1].first)->get_owner();
+        f = m_util.mk_sub(f, f2); 
+    }
+    else if (t.size() == 2 && t[1].second.is_one() && t[0].second.is_minus_one()) {
+        f = get_enode(t[1].first)->get_owner();
+        f2 = get_enode(t[0].first)->get_owner();
+        f = m_util.mk_sub(f, f2);
+    }
+    else {
+        NOT_IMPLEMENTED_YET();
+    }
+    inf_rational new_val = val - inf_rational(m_objective_consts[v]);
+    e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));
+    
+    if (new_val.get_infinitesimal().is_neg()) {
+        return m_util.mk_ge(f, e);
+    }
+    else {
+        return m_util.mk_gt(f, e);
+    }
+}
+
 template<typename Ext>
 bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) {
 

src/smt/theory_opt.h

@@ -34,6 +34,7 @@ namespace smt {
             inf_eps_rational<inf_rational> r(rational(1), inf_rational(0)); 
             return r; 
         }
+        virtual expr* block_lower_bound(theory_var v, inf_rational const& val) { return 0; }
     };
 }
 

src/util/inf_eps_rational.h

@@ -127,6 +127,10 @@ class inf_eps_rational {
         return m_r.get_uint64();
     }
 
+    Numeral const& get_numeral() const {
+        return m_r;
+    }
+
     rational const& get_rational() const {
         return m_r.get_rational();
     }