working on DL opt

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

src/math/simplex/simplex_def.h

@@ -636,9 +636,11 @@ namespace simplex {
             // 
 
             pivot(x_i, x_j, a_ij);
-            move_to_bound(x_i, inc != m.is_pos(a_ij));            
+            TRACE("simplex", display(tout << "after pivot\n"););
+            move_to_bound(x_i, !inc);
             SASSERT(well_formed_row(row(m_vars[x_j].m_base2row)));
             TRACE("simplex", display(tout););
+            SASSERT(is_feasible());
         }
         return l_true;
     }
@@ -685,7 +687,8 @@ namespace simplex {
                 em.sub(*bound, vs.m_value, delta2);
                 em.mul(delta2, base_coeff, delta2);
                 em.div(delta2, coeff, delta2);
-                abs(delta2);
+                em.abs(delta2);
+                TRACE("simplex", tout << "Delta for v" << s << " " << delta2 << "\n";);
                 if (delta2 < delta) {
                     delta = delta2;
                 }
@@ -697,6 +700,15 @@ namespace simplex {
         update_value(x, delta);        
     }
 
+    /**
+       \brief 
+       Arguments:
+       v   - base variable of row(v) to optimize
+       x_i - base variable of row(x_i) to become non-base
+       x_j - variable in row(v) to make a base variable
+       a_ij - coefficient to x_j in row(x_i)
+       inc  - whether to increment x_j (true if coefficient in row(v) is negative).
+     */
     template<typename Ext>
     void simplex<Ext>::select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij, bool& inc) {
         row r(m_vars[v].m_base2row);
@@ -758,7 +770,7 @@ namespace simplex {
             numeral const& a_ij = it.get_row_entry().m_coeff;
             numeral const& a_ii = vi.m_base_coeff;
             bool inc_s = (m.is_pos(a_ii) != m.is_pos(a_ij)) ? inc : !inc;
-            TRACE("simplex", tout << "v" << x_j << " incs: " << inc_s 
+            TRACE("simplex", tout << "v" << x_j << " base v" << s << " incs: " << inc_s 
                   << " upper valid:" << vi.m_upper_valid 
                   << " lower valid:" << vi.m_lower_valid << "\n";
                   display_row(tout, r););
@@ -775,13 +787,13 @@ namespace simplex {
             if (is_neg(curr_gain)) {
                 curr_gain.neg();
             }
-            if (x_i == null_var || (gain < curr_gain) || 
+            if (x_i == null_var || (curr_gain < gain) || 
                 (is_zero(gain) && is_zero(curr_gain) && s < x_i)) {
                 x_i = s;
                 gain = curr_gain;
                 new_a_ij = a_ij;
                 TRACE("simplex", tout << "x_j v" << x_j << " x_i v" << x_i << " gain: ";
-                      tout << em.to_string(curr_gain) << "\n";);
+                      tout << curr_gain << "\n";);
             }
         }
         return x_i;

src/smt/theory_diff_logic.h

@@ -190,7 +190,7 @@ namespace smt {
         typedef vector <std::pair<theory_var, rational> > objective_term;
         vector<objective_term>         m_objectives;
         vector<rational>               m_objective_consts;
-        vector<vector<numeral> >       m_objective_assignments;
+        vector<expr_ref_vector>        m_objective_assignments;
 
         // Set a conflict due to a negative cycle.
         void set_neg_cycle_conflict();
@@ -317,7 +317,7 @@ namespace smt {
 
     private:     
 
-        virtual expr* block_objective(theory_var v, inf_rational const& val);
+        expr_ref block_objective(theory_var v, inf_rational const& val);
 
         virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j);
 

src/smt/theory_diff_logic_def.h

@@ -1000,8 +1000,9 @@ 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) {
-
+    
-    simplex::simplex<simplex::mpq_ext> S;
+    typedef simplex::simplex<simplex::mpq_ext> Simplex;
+    Simplex S;
     objective_term const& objective = m_objectives[v];
 
     IF_VERBOSE(1,
@@ -1059,7 +1060,7 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
     }
     coeffs.push_back(mpq(1));
     vars.push_back(w);
-    S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr());
+    Simplex::row row = S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr());
 
     TRACE("opt", S.display(tout); display(tout););
     
@@ -1076,6 +1077,16 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
         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"; );
+        Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row);
+        S.display_row(std::cout, row, true);
+        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";
+            }
+        }
         return inf_eps_rational<inf_rational>(rational(0), r);
     }
     default:
@@ -1089,7 +1100,7 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
     objective_term objective;
     theory_var result = m_objectives.size();
     rational q(1), r(0);
-    vector<numeral> vr;
+    expr_ref_vector vr(get_manager());
     if (internalize_objective(term, q, r, objective)) {
         m_objectives.push_back(objective);
         m_objective_consts.push_back(r);
@@ -1102,7 +1113,7 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
 }
 
 template<typename Ext>
-expr* theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic<Ext>::block_objective(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);
@@ -1123,55 +1134,26 @@ expr* theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational const&
         f = m_util.mk_sub(f, f2);
     }
     else {
-        expr_ref_vector disj(m);
+        // 
-        vector<numeral> const & ns = m_objective_assignments[v];
+        f = m.mk_true();
-        inf_rational val;
+        return f;
-        rational r, s;
-        rational r0 = ns[0].get_rational().to_rational();
-        rational s0 = ns[0].get_infinitesimal().to_rational();
-        app * x;
-        app * x0 = get_enode(t[0].first)->get_owner();
-        // Assert improved bounds for x_i - x_0
-        for (unsigned i = 1; i < t.size(); ++i) {
-            r = ns[i].get_rational().to_rational();
-            s = ns[i].get_infinitesimal().to_rational(); 
-            val = inf_rational(r - r0, s - s0);
-            x = get_enode(t[i].first)->get_owner();
-            f = m_util.mk_sub(x, x0);
-            e = m_util.mk_numeral(val.get_rational(), m.get_sort(f));
-            if (t[i].second.is_neg() && val.get_infinitesimal().is_pos()) {
-                disj.push_back(m_util.mk_le(f, e));
-            }
-            else if (t[i].second.is_neg()) {
-                disj.push_back(m_util.mk_lt(f, e));
-            }
-            else if (t[i].second.is_pos() && val.get_infinitesimal().is_neg()) {
-                disj.push_back(m_util.mk_ge(f, e));
-            }
-            else if (t[i].second.is_pos()) {
-                disj.push_back(m_util.mk_gt(f, e));
-            }
-            else {
-                UNREACHABLE();
-            }
-        }
-        return m.mk_or(disj.size(), disj.c_ptr());
     }
 
     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);
+        f = m_util.mk_ge(f, e);
     }
     else {
-        return m_util.mk_gt(f, e);
+        f = m_util.mk_gt(f, e);
     }
+    return f;
 }
 
 template<typename Ext>
 expr* theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
-    expr * o = block_objective(v, val);
+    expr_ref o = block_objective(v, val);
     context & ctx = get_context();
     model_ref mdl;
     ctx.get_model(mdl);

src/util/mpq_inf.cpp

@@ -38,5 +38,6 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
     return s;
 }
 
+
 template class mpq_inf_manager<true>;
 template class mpq_inf_manager<false>;

src/util/mpq_inf.h

@@ -271,6 +271,11 @@ public:
     }
 
     std::string to_string(mpq_inf const & a);
+
+    void display(std::ostream & out, mpq_inf const & a) {
+        out << to_string(a);
+    }
+
 };
 
 typedef mpq_inf_manager<true>  synch_mpq_inf_manager;