integrating diff opt

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

src/opt/opt_context.cpp

@@ -312,18 +312,17 @@ namespace opt {
                      mk_simplify_tactic(m));   
         tactic_ref tac2 = mk_elim01_tactic(m);
         tactic_ref tac3 = mk_lia2card_tactic(m);
-        tactic_ref tac;
         opt_params optp(m_params);
         if (optp.elim_01()) {
-            tac = and_then(tac0.get(), tac2.get(), tac3.get());
+            m_simplify = and_then(tac0.get(), tac2.get(), tac3.get());
         }
         else {
-            tac = tac0.get();
+            m_simplify = tac0.get();
         }
         proof_converter_ref pc;
         expr_dependency_ref core(m);
         goal_ref_buffer result;
-        (*tac)(g, result, m_model_converter, pc, core);  // TBD: have this an attribute so we can cancel.
+        (*m_simplify)(g, result, m_model_converter, pc, core); 
         SASSERT(result.size() == 1);
         goal* r = result[0];
         fmls.reset();
@@ -708,6 +707,9 @@ namespace opt {
         if (m_solver) {
             m_solver->set_cancel(f);
         }
+        if (m_simplify) {
+            m_simplify->set_cancel(f);
+        }
         m_optsmt.set_cancel(f);
         map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
         for (; it != end; ++it) {
@@ -719,6 +721,9 @@ namespace opt {
         if (m_solver) {
             m_solver->collect_statistics(stats);
         }
+        if (m_simplify) {
+            m_simplify->collect_statistics(stats);
+        }
         map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
         for (; it != end; ++it) {
             it->m_value->collect_statistics(stats);

src/opt/opt_context.h

@@ -30,6 +30,7 @@ Notes:
 #include "optsmt.h"
 #include "maxsmt.h"
 #include "model_converter.h"
+#include "tactic.h"
 
 namespace opt {
 
@@ -89,6 +90,7 @@ namespace opt {
         obj_map<func_decl, unsigned> m_objective_fns;
         obj_map<func_decl, expr*> m_objective_orig;
         func_decl_ref_vector m_objective_refs;
+        tactic_ref          m_simplify;
     public:
         context(ast_manager& m);
         ~context();

src/opt/opt_solver.cpp

@@ -133,15 +133,17 @@ namespace opt {
         return r;
     }
 
-    void opt_solver::maximize_objectives() {
+    void opt_solver::maximize_objectives(expr_ref_vector& blockers) {
+        expr_ref blocker(m);
         for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
-            maximize_objective(i);
+            maximize_objective(i, blocker);
+            blockers.push_back(blocker);
         }
     }
 
-    void opt_solver::maximize_objective(unsigned i) {
+    void opt_solver::maximize_objective(unsigned i, expr_ref& blocker) {
         smt::theory_var v = m_objective_vars[i];
-        m_objective_values[i] = get_optimizer().maximize(v);
+        m_objective_values[i] = get_optimizer().maximize(v, blocker);
         m_context.get_context().update_model();        
         TRACE("opt", { model_ref mdl; get_model(mdl); model_smt2_pp(tout << "update model: ", m, *mdl, 0); });
     }
@@ -231,20 +233,7 @@ namespace opt {
 
         // difference logic?
         return expr_ref(m.mk_true(), m);
-    }
+    } 
- 
-    expr_ref opt_solver::mk_gt(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 {
-            inf_rational n = val.get_numeral();            
-            return expr_ref(get_optimizer().mk_gt(m_objective_vars[var], n), m);
-        }
-    }
 
     void opt_solver::reset_objectives() {
         m_objective_vars.reset();

src/opt/opt_solver.h

@@ -75,12 +75,11 @@ namespace opt {
 
         smt::theory_var add_objective(app* term);
         void reset_objectives();
-        void maximize_objective(unsigned i);
+        void maximize_objective(unsigned i, expr_ref& blocker);
-        void maximize_objectives();
+        void maximize_objectives(expr_ref_vector& blockers);
 
         vector<inf_eps> const& get_objective_values();
         inf_eps const & get_objective_value(unsigned obj_index);
-        expr_ref mk_gt(unsigned obj_index, inf_eps const& val);
         expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
 
         filter_model_converter& mc() { return m_fm; }

src/opt/optsmt.cpp

@@ -124,7 +124,8 @@ namespace opt {
     }
 
     void optsmt::update_lower() {
-        m_s->maximize_objectives();
+        expr_ref_vector disj(m);
+        m_s->maximize_objectives(disj);
         m_s->get_model(m_model);
         set_max(m_lower, m_s->get_objective_values());
         IF_VERBOSE(1, 
@@ -134,13 +135,7 @@ namespace opt {
                    verbose_stream() << "\n";
                    model_pp(verbose_stream(), *m_model);
                    );
-        expr_ref_vector disj(m);
+        expr_ref constraint(m);        
-        expr_ref constraint(m);
-        
-        for (unsigned i = 0; i < m_lower.size(); ++i) {
-            inf_eps const& v = m_lower[i];
-            disj.push_back(m_s->mk_gt(i, v));
-        }
         constraint = m.mk_or(disj.size(), disj.c_ptr());
         m_s->assert_expr(constraint);
     }
@@ -237,25 +232,23 @@ namespace opt {
 
     lbool optsmt::basic_lex(unsigned obj_index) {
         lbool is_sat = l_true;
-        expr_ref block(m);        
+        expr_ref block(m), tmp(m);
-
 
         while (is_sat == l_true && !m_cancel) {
             is_sat = m_s->check_sat(0, 0); 
             if (is_sat != l_true) break;
             
-            m_s->maximize_objective(obj_index);
+            m_s->maximize_objective(obj_index, block);
             m_s->get_model(m_model);
             inf_eps obj = m_s->get_objective_value(obj_index);
             if (obj > m_lower[obj_index]) {
                 m_lower[obj_index] = obj;
                 IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";);
                 for (unsigned i = obj_index+1; i < m_vars.size(); ++i) {
-                    m_s->maximize_objective(i);
+                    m_s->maximize_objective(i, tmp);
                     m_lower[i] = m_s->get_objective_value(i);
                 }
             }
-            block = m_s->mk_gt(obj_index, obj);
             m_s->assert_expr(block);
             
             // TBD: only works for simplex 
@@ -289,14 +282,13 @@ namespace opt {
             is_sat = m_s->check_sat(0, 0); 
             if (is_sat != l_true) break;
             was_sat = true;
-            m_s->maximize_objective(obj_index);
+            m_s->maximize_objective(obj_index, block);
             m_s->get_model(m_model);
             inf_eps obj = m_s->get_objective_value(obj_index);
             if (obj > m_lower[obj_index]) {
                 m_lower[obj_index] = obj;
                 IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";);
             }
-            block = m_s->mk_gt(obj_index, obj);
             m_s->assert_expr(block);
         }
         
@@ -347,10 +339,12 @@ namespace opt {
 
 
     inf_eps optsmt::get_lower(unsigned i) const {
+        if (i >= m_lower.size()) return inf_eps();
         return m_lower[i];
     }
 
     inf_eps optsmt::get_upper(unsigned i) const {
+        if (i >= m_upper.size()) return inf_eps();
         return m_upper[i];
     }
 

src/smt/theory_arith.h

@@ -998,9 +998,8 @@ namespace smt {
         // Optimization
         //
         // -----------------------------------
-        virtual inf_eps_rational<inf_rational> maximize(theory_var v);
+        virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker);
         virtual theory_var add_objective(app* term);
-        virtual expr* mk_gt(theory_var v, inf_rational const& val);
         virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
         void enable_record_conflict(expr* bound);
         void record_conflict(unsigned num_lits, literal const * lits, 
@@ -1008,6 +1007,8 @@ namespace smt {
                           unsigned num_params, parameter* params);
         inf_eps_rational<inf_rational> conflict_minimize();
     private:
+        virtual expr_ref mk_gt(theory_var v);
+
         bool_var m_bound_watch;
         inf_eps_rational<inf_rational> m_upper_bound;
         bool get_theory_vars(expr * n, uint_set & vars);

src/smt/theory_arith_aux.h

@@ -1065,13 +1065,17 @@ namespace smt {
     }
 
     template<typename Ext>
-    inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v) {
+    inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v, expr_ref& blocker) {
         TRACE("opt", tout << "data-size: " << m_data.size() << "\n";);
         max_min_t r = max_min(v, true); 
         if (r == UNBOUNDED) {
+            blocker = get_manager().mk_false();
             return inf_eps_rational<inf_rational>::infinity();
         }
-        return inf_eps_rational<inf_rational>(get_value(v));
+        else {
+            blocker = mk_gt(v);
+            return inf_eps_rational<inf_rational>(get_value(v));
+        }
         
     }
 
@@ -1081,8 +1085,9 @@ namespace smt {
        for the theory of aritmetic.
     */
     template<typename Ext>
-    expr* theory_arith<Ext>::mk_gt(theory_var v, inf_rational const& val) {
+    expr_ref theory_arith<Ext>::mk_gt(theory_var v) {
         ast_manager& m = get_manager();
+        inf_numeral const& val = get_value(v);
         expr* obj = get_enode(v)->get_owner();
         expr_ref e(m);
         rational r = val.get_rational();
@@ -1094,19 +1099,20 @@ namespace smt {
                 r = ceil(r);
             }
             e = m_util.mk_numeral(r, m.get_sort(obj));
-            return m_util.mk_ge(obj, e);
+            e = m_util.mk_ge(obj, e);
         }
         else {
             // obj is over the reals.
             e = m_util.mk_numeral(r, m.get_sort(obj));
             
             if (val.get_infinitesimal().is_neg()) {
-                return m_util.mk_ge(obj, e);
+                e = m_util.mk_ge(obj, e);
             }
             else {
-                return m_util.mk_gt(obj, e);
+                e = m_util.mk_gt(obj, e);
             }
         }
+        return e;
     }
 
     /**

src/smt/theory_diff_logic.h

@@ -308,9 +308,9 @@ namespace smt {
         //
         // -----------------------------------
 
-        virtual inf_eps_rational<inf_rational> maximize(theory_var v);
+        virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker);
         virtual theory_var add_objective(app* term);
-        virtual expr* mk_gt(theory_var v, inf_rational const& val);
+        virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
         virtual expr* mk_ge(theory_var v, inf_rational const& val) { return 0; }
 
         bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);

src/smt/theory_diff_logic_def.h

@@ -999,10 +999,11 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
 }
 
 template<typename Ext>
-inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
+inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) {
     
     typedef simplex::simplex<simplex::mpq_ext> Simplex;
     Simplex S;
+    ast_manager& m = get_manager();
     objective_term const& objective = m_objectives[v];
 
     IF_VERBOSE(1,
@@ -1067,30 +1068,37 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
     // optimize    
     lbool is_sat = S.make_feasible();
     if (is_sat == l_undef) {
+        blocker = m.mk_false();
         return inf_eps_rational<inf_rational>::infinity();        
     }
-    TRACE("opt", S.display(tout); );
+    TRACE("opt", S.display(tout); );    
     SASSERT(is_sat != l_false);
     lbool is_fin = S.minimize(w);
     switch (is_fin) {
     case l_true: {
         simplex::mpq_ext::eps_numeral const& val = S.get_value(w);
         inf_rational r(-rational(val.first), -rational(val.second));
-        TRACE("opt", tout << r << " " << "\n"; );
+        TRACE("opt", tout << r << " " << "\n"; 
+              S.display_row(tout, row, true););
         Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row);
-        S.display_row(std::cout, row, true);
+        expr_ref_vector& core = m_objective_assignments[v];
+        expr_ref tmp(m);
+        core.reset();
         for (; it != end; ++it) {
             unsigned v = it->m_var;
             if (num_nodes <= v && v < num_nodes + num_edges) {
                 unsigned edge_id = v - num_nodes;
                 literal lit = m_graph.get_explanation(edge_id);
-                std::cout << lit << "\n";
+                get_context().literal2expr(lit, tmp);
+                core.push_back(tmp);
             }
         }
+        blocker = mk_gt(v, r);
         return inf_eps_rational<inf_rational>(rational(0), r);
     }
     default:
         TRACE("opt", tout << "unbounded\n"; );        
+        blocker = m.mk_false();
         return inf_eps_rational<inf_rational>::infinity();        
     }
 }
@@ -1135,7 +1143,9 @@ expr_ref theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational cons
     }
     else {
         // 
-        f = m.mk_true();
+        expr_ref_vector const& core = m_objective_assignments[v];
+        f = m.mk_not(m.mk_and(core.size(), core.c_ptr()));
+        TRACE("arith", tout << "block: " << f << "\n";);
         return f;
     }
 
@@ -1152,8 +1162,10 @@ expr_ref theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational cons
 }
 
 template<typename Ext>
-expr* theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
     expr_ref o = block_objective(v, val);
+    return o;
+#if 0
     context & ctx = get_context();
     model_ref mdl;
     ctx.get_model(mdl);
@@ -1162,6 +1174,7 @@ expr* theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
     model_implicant impl_extractor(m);
     expr_ref_vector implicants = impl_extractor.minimize_literals(formulas, mdl);
     return m.mk_and(o, m.mk_not(m.mk_and(implicants.size(), implicants.c_ptr())));
+#endif
 }
 
 template<typename Ext>

src/smt/theory_opt.h

@@ -29,9 +29,8 @@ namespace smt {
     class theory_opt {
     public:
         typedef inf_eps_rational<inf_rational> inf_eps;
-        virtual inf_eps maximize(theory_var v) { UNREACHABLE(); return inf_eps::infinity(); }
+        virtual inf_eps maximize(theory_var v, expr_ref& blocker) = 0; // { UNREACHABLE(); return inf_eps::infinity(); }
         virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; }
-        virtual expr* mk_gt(theory_var v, inf_rational const& val) { UNREACHABLE(); return 0; }
         virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; }
     };
 }