integrating new integer primal loop

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

src/smt/diff_logic.h

@@ -1193,6 +1193,10 @@ public:
         return m_assignment[v]; 
     }
 
+    void set_assignment(dl_var v, numeral const & n) {
+        m_assignment[v] = n; 
+    }
+
     unsigned get_timestamp() const {
         return m_timestamp;
     }

src/smt/smt_context.cpp

@@ -3944,10 +3944,12 @@ namespace smt {
         if (refinalize) {
             fcs = final_check();
         }
+        TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);
         if (fcs == FC_DONE) {
             mk_proto_model(l_true);
             m_model = m_proto_model->mk_model();
         }
+            
         return fcs == FC_DONE;
     }
 

src/smt/theory_arith.h

@@ -894,7 +894,7 @@ namespace smt {
         void init_gains(theory_var x, bool inc, inf_numeral& min_gain, inf_numeral& max_gain);
         bool update_gains(bool inc, theory_var x_i, numeral const& a_ij, 
                           inf_numeral& min_gain, inf_numeral& max_gain);
-        bool move_to_bound_new(theory_var x_i, bool inc, bool& best_effort, bool& has_shared);
+        bool move_to_bound_new(theory_var x_i, bool inc, unsigned& best_efforts, bool& has_shared);
         bool pick_var_to_leave(
             theory_var x_j, bool inc, numeral & a_ij, 
             inf_numeral& min_gain, inf_numeral& max_gain, 
@@ -1036,7 +1036,7 @@ namespace smt {
         virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker, bool& has_shared);
         virtual inf_eps_rational<inf_rational> value(theory_var v);
         virtual theory_var add_objective(app* term);
-        virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
+        virtual expr_ref 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, 
                           unsigned num_eqs, enode_pair const * eqs,

src/smt/theory_arith_aux.h

@@ -1189,7 +1189,7 @@ namespace smt {
       This allows to handle inequalities with non-standard numbers.
     */
     template<typename Ext>
-    expr* theory_arith<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val) {
+    expr_ref theory_arith<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val) {
         ast_manager& m = get_manager();
         context& ctx = get_context();
         std::ostringstream strm;
@@ -1208,7 +1208,7 @@ namespace smt {
             TRACE("arith", tout << mk_pp(b, m) << "\n";
                   display_atom(tout, a, false););            
         }
-        return b;
+        return expr_ref(b, m);
     }
 
 
@@ -1658,9 +1658,17 @@ namespace smt {
         bool is_tighter = false;
         if (is_int(x_i)) den_aij = denominator(a_ij);
         SASSERT(den_aij.is_pos() && den_aij.is_int());
+
+        if (is_int(x_i) && !den_aij.is_one()) {
+            SASSERT(min_gain.is_pos());
+            min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij));
+            normalize_gain(min_gain.get_rational(), max_gain);
+        }
+
         if (!max_inc.is_minus_one()) {
             if (is_int(x_i)) {
-                normalize_gain(den_aij, max_inc);
+                max_inc = floor(max_inc);
+                normalize_gain(min_gain.get_rational(), max_inc);
             }
             if (unbounded_gain(max_gain)) {
                 max_gain = max_inc;
@@ -1671,13 +1679,6 @@ namespace smt {
                 is_tighter = true;
             }
         }
-        if (is_int(x_i)) {
-            SASSERT(min_gain.is_pos());
-            if (!den_aij.is_one()) {
-                min_gain = inf_numeral(lcm(min_gain.get_rational(), den_aij));
-                normalize_gain(den_aij, max_gain);
-            }
-        }
         TRACE("opt",
               tout << "v" << x_i << " a_ij " << a_ij << " "
               << "min gain: " << min_gain << " " 
@@ -1701,7 +1702,8 @@ namespace smt {
         bool max, 
         bool& has_shared) {
         m_stats.m_max_min++;
-        bool best_effort = false, inc = false;
+        unsigned best_efforts = 0;
+        bool inc = false;
 
         SASSERT(valid_assignment());
 
@@ -1712,7 +1714,8 @@ namespace smt {
 #endif
         max_min_t result = OPTIMIZED;
         has_shared = false;
-        while (true) {
+        unsigned max_efforts = 10 + (get_context().get_random_value() % 20);
+        while (best_efforts < max_efforts) {
             theory_var x_j = null_theory_var;
             theory_var x_i = null_theory_var;
             max_gain.reset();
@@ -1734,10 +1737,11 @@ namespace smt {
                 if (!pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
                                        curr_min_gain, curr_max_gain, 
                                        has_shared, curr_x_i)) {
-                    best_effort = true;
-                    continue;
+                    best_efforts++;
+                }
+                else {
+                    SASSERT(safe_gain(curr_min_gain, curr_max_gain));
                 }
-                SASSERT(safe_gain(curr_min_gain, curr_max_gain));
                 if (curr_x_i == null_theory_var) {
                     TRACE("opt", tout << "unbounded\n";);
                     // we can increase/decrease curr_x_j as much as we want.
@@ -1770,7 +1774,7 @@ namespace smt {
             }
 
             TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
-                  tout << "skipped row: " << (best_effort?"yes":"no") << "\n";
+                  tout << "best efforts: " << best_efforts << "\n";
                   display(tout););
             
             if (x_j == null_theory_var) {
@@ -1781,7 +1785,7 @@ namespace smt {
             }
             
             if (min_gain.is_pos() && !min_gain.is_one()) {
-                best_effort = true;
+                ++best_efforts;
             }
             if (x_i == null_theory_var) {
                 // can increase/decrease x_j as much as we want.
@@ -1802,7 +1806,7 @@ namespace smt {
                     continue;
                 }
                 SASSERT(unbounded_gain(max_gain));
-                best_effort = false;
+                best_efforts = 0;
                 result = UNBOUNDED;
                 break;
             }
@@ -1836,9 +1840,8 @@ namespace smt {
             SASSERT(is_base(x_j));
             
             bool inc_xi = inc?a_ij.is_neg():a_ij.is_pos();
-            if (!move_to_bound_new(x_i, inc_xi, best_effort, has_shared)) {
-                best_effort = true;
-                break;
+            if (!move_to_bound_new(x_i, inc_xi, best_efforts, has_shared)) {
+                // break;
             }
             
             row & r2 = m_rows[get_var_row(x_j)];
@@ -1848,7 +1851,7 @@ namespace smt {
             SASSERT(valid_assignment());
         }
         TRACE("opt", display(tout););
-        return best_effort?BEST_EFFORT:result;
+        return (best_efforts>0)?BEST_EFFORT:result;
     }
 
     /**
@@ -1862,7 +1865,7 @@ namespace smt {
     bool theory_arith<Ext>::move_to_bound_new(
         theory_var x_i,         // variable to move
         bool inc,               // increment variable or decrement
-        bool& best_effort,      // is bound move a best effort?
+        unsigned& best_efforts, // is bound move a best effort?
         bool& has_shared) {     // does move include shared variables?
         inf_numeral min_gain, max_gain;
         init_gains(x_i, inc, min_gain, max_gain);        
@@ -1877,6 +1880,7 @@ namespace smt {
             update_gains(inc, s, coeff, min_gain, max_gain);
             has_shared |= get_context().is_shared(get_enode(s));
         }
+        bool result = false;
         if (safe_gain(min_gain, max_gain)) {
             TRACE("opt", tout << "Safe delta: " << max_gain << "\n";);
             SASSERT(!unbounded_gain(max_gain));
@@ -1884,12 +1888,15 @@ namespace smt {
                 max_gain.neg();
             }
             update_value(x_i, max_gain);
-            best_effort = min_gain.is_pos() && !min_gain.is_one();
-            return !max_gain.is_zero();
+            if (!min_gain.is_pos() || min_gain.is_one()) {
+                ++best_efforts;
+            }
+            result = !max_gain.is_zero();
         }
-        else {
-            return false;
+        if (!result) {
+            ++best_efforts;
         }
+        return result;
     }
 
     /**
@@ -2004,7 +2011,7 @@ namespace smt {
                     add_tmp_row_entry<true>(m_tmp_row, it->m_coeff, it->m_var);
             }            
         }
-        max_min_t r = max_min_orig(m_tmp_row, max, has_shared);
+        max_min_t r = max_min_new(m_tmp_row, max, has_shared);
         if (r == OPTIMIZED) {
             TRACE("opt", tout << mk_pp(e, get_manager()) << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n";
                   display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row););

src/smt/theory_dense_diff_logic.h

@@ -198,6 +198,7 @@ namespace smt {
         void del_vars(unsigned old_num_vars);
         void init_model();
         bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
+        expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict);
 #ifdef Z3DEBUG
         bool check_vector_sizes() const;
         bool check_matrix() const;
@@ -270,8 +271,8 @@ namespace smt {
         virtual inf_eps_rational<inf_rational> value(theory_var v);
         virtual theory_var add_objective(app* term);
         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; }
-
+        virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val);
+        
         // -----------------------------------
         //
         // Main

src/smt/theory_dense_diff_logic_def.h

@@ -1030,6 +1030,17 @@ namespace smt {
 
     template<typename Ext>
     expr_ref theory_dense_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
+        return mk_ineq(v, val, true);
+    }
+
+    template<typename Ext>
+    expr_ref theory_dense_diff_logic<Ext>::mk_ge(
+        filter_model_converter& fm, theory_var v, inf_rational const& val) {
+        return mk_ineq(v, val, false);
+    }
+
+    template<typename Ext>
+    expr_ref theory_dense_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
         ast_manager& m = get_manager();
         objective_term const& t = m_objectives[v];
         expr_ref e(m), f(m), f2(m);
@@ -1052,19 +1063,32 @@ namespace smt {
         else {
             // 
             expr_ref_vector const& core = m_objective_assignments[v];
-            f = m.mk_not(m.mk_and(core.size(), core.c_ptr()));
+            f = m.mk_and(core.size(), core.c_ptr());
+            if (is_strict) {
+                f = m.mk_not(f);
+            }
             TRACE("arith", tout << "block: " << f << "\n";);
             return f;
         }
         
-        inf_rational new_val = val - inf_rational(m_objective_consts[v]);
-        e = m_autil.mk_numeral(new_val.get_rational(), m.get_sort(f));
+        e = m_autil.mk_numeral(val.get_rational(), m.get_sort(f));
         
-        if (new_val.get_infinitesimal().is_neg()) {
-            f = m_autil.mk_ge(f, e);
+        if (val.get_infinitesimal().is_neg()) {
+            if (is_strict) {
+                f = m_autil.mk_ge(f, e);
+            }
+            else {
+                expr_ref_vector const& core = m_objective_assignments[v];
+                f = m.mk_and(core.size(), core.c_ptr());
+            }
         }
         else {
-            f = m_autil.mk_gt(f, e);
+            if (is_strict) {
+                f = m_autil.mk_gt(f, e);
+            }
+            else {
+                f = m_autil.mk_ge(f, e);
+            }
         }
         return f;
     }

src/smt/theory_diff_logic.h

@@ -324,13 +324,13 @@ namespace smt {
         virtual inf_eps value(theory_var v);
         virtual theory_var add_objective(app* term);
         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; }
+        virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val);
 
         bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
 
     private:     
 
-        expr_ref block_objective(theory_var v, inf_rational const& val);
+        expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict);
 
         virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j);
 

src/smt/theory_diff_logic_def.h

@@ -546,7 +546,7 @@ void theory_diff_logic<Ext>::propagate_core() {
 template<typename Ext>
 bool theory_diff_logic<Ext>::propagate_atom(atom* a) {
     context& ctx = get_context();
-    TRACE("arith", a->display(*this, tout); );
+    TRACE("arith", a->display(*this, tout); tout << "\n";);
     if (ctx.inconsistent()) {
         return false;
     }
@@ -1236,6 +1236,13 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
                 core.push_back(tmp);
             }
         }
+        compute_delta();
+        for (unsigned i = 0; i < m_graph.get_num_nodes(); ++i) {
+            unsigned w = node2simplex(i);
+            simplex::mpq_ext::eps_numeral const& val = S.get_value(w);
+            rational r = rational(val.first) + m_delta*rational(val.second);
+            m_graph.set_assignment(i, numeral(r));
+        }
         blocker = mk_gt(v, r);
         return inf_eps(rational(0), r + m_objective_consts[v]);
     }
@@ -1267,7 +1274,7 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
 }
 
 template<typename Ext>
-expr_ref theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
     ast_manager& m = get_manager();
     objective_term const& t = m_objectives[v];
     expr_ref e(m), f(m), f2(m);
@@ -1290,7 +1297,10 @@ expr_ref theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational cons
     else {
         // 
         expr_ref_vector const& core = m_objective_assignments[v];
-        f = m.mk_not(m.mk_and(core.size(), core.c_ptr()));
+        f = m.mk_and(core.size(), core.c_ptr());
+        if (is_strict) {
+            f = m.mk_not(f);
+        }
         TRACE("arith", tout << "block: " << f << "\n";);
         return f;
     }
@@ -1299,18 +1309,35 @@ expr_ref theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational cons
     e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));
     
     if (new_val.get_infinitesimal().is_neg()) {
-        f = m_util.mk_ge(f, e);
+        if (is_strict) {
+            f = m_util.mk_ge(f, e);
+        }
+        else {
+            expr_ref_vector const& core = m_objective_assignments[v];
+            f = m.mk_and(core.size(), core.c_ptr());            
+        }
     }
     else {
-        f = m_util.mk_gt(f, e);
+        if (is_strict) {
+            f = m_util.mk_gt(f, e);
+        }
+        else {
+            f = m_util.mk_ge(f, e);
+        }
     }
     return f;
 }
 
 template<typename Ext>
 expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
-    expr_ref o = block_objective(v, val);
-    return o;
+    return mk_ineq(v, val, true);
+}
+
+template<typename Ext>
+expr_ref theory_diff_logic<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) {
+    return mk_ineq(v, val, false);
+}
+
 #if 0
     context & ctx = get_context();
     model_ref mdl;
@@ -1321,7 +1348,6 @@ expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
     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>
 bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) {

src/smt/theory_opt.h

@@ -33,7 +33,7 @@ namespace smt {
         virtual inf_eps value(theory_var) = 0;
         virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0; 
         virtual theory_var add_objective(app* term) = 0;
-        virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; }
+        virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return expr_ref(*((ast_manager*)0)); }
         bool is_linear(ast_manager& m, expr* term);
         bool is_numeral(arith_util& a, expr* term);
     };