Add facilities to get optimal assignments

src/smt/network_flow.h

@@ -93,8 +93,8 @@ namespace smt {
 
             bool choose_entering_edge() {
                 TRACE("network_flow", tout << "choose_entering_edge...\n";);        
-                unsigned num_edges = m_graph.get_num_edges();
+                int num_edges = m_graph.get_num_edges();
-                for (unsigned i = m_next_edge; i < m_next_edge + num_edges; ++i) {
+                for (int i = m_next_edge; i < m_next_edge + num_edges; ++i) {
                     edge_id id = (i >= num_edges) ? (i - num_edges) : i;
                     node src = m_graph.get_source(id);
                     node tgt = m_graph.get_target(id);
@@ -106,6 +106,10 @@ namespace smt {
                                 tout << "Found entering edge " << id << " between node ";
                                 tout << src << " and node " << tgt << " with reduced cost = " << cost << "...\n";
                             });
+                            m_next_edge = m_enter_id;
+                            if (m_next_edge >= num_edges) {
+                                m_next_edge -= num_edges;
+                            }
                             return true;
                         }
                     }

src/smt/network_flow_def.h

@@ -295,6 +295,13 @@ namespace smt {
             }
         }
 
+        for (unsigned i = 0; i < num_edges; ++i) {
+            dl_var src = m_graph.get_source(i);
+            dl_var tgt = m_graph.get_target(i);
+            numeral weight = m_graph.get_weight(i);
+            SASSERT(m_potentials[src] - m_potentials[tgt] <= weight);
+        }
+
         // m_flows are zero on non-basic edges
         for (unsigned i = 0; i < m_flows.size(); ++i) {
             SASSERT(m_states[i] == BASIS || m_flows[i].is_zero());

src/smt/theory_arith.h

@@ -37,6 +37,7 @@ Revision History:
 #include"arith_simplifier_plugin.h"
 #include"arith_eq_solver.h"
 #include"theory_opt.h"
+#include"uint_set.h"
 
 namespace smt {
     
@@ -433,7 +434,7 @@ namespace smt {
         bool                    m_eager_gcd; // true if gcd should be applied at every add_row
         unsigned                m_final_check_idx;
 
-        inf_eps_rational<inf_rational>   m_objective_value;
+        u_map<uint_set>        m_objective_vars;
 
         // backtracking
         svector<bound_trail>    m_bound_trail;
@@ -1008,6 +1009,7 @@ namespace smt {
     private:
         bool_var m_bound_watch;
         inf_eps_rational<inf_rational> m_upper_bound;
+        bool get_theory_vars(expr * n, uint_set & vars);
     public:
         // -----------------------------------
         //

src/smt/theory_arith_aux.h

@@ -966,28 +966,78 @@ namespace smt {
         return x_i;
     }
 
+    template<typename Ext>
+    bool theory_arith<Ext>::get_theory_vars(expr * n, uint_set & vars) {
+        rational r;
+        expr* x, *y;
+        if (m_util.is_numeral(n, r)) {
+            return true;
+        }
+        else if (m_util.is_add(n)) {
+            for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) {
+                if (!get_theory_vars(to_app(n)->get_arg(i), vars)) {
+                    return false;
+                }
+            }
+        }
+        else if (m_util.is_mul(n, x, y) && m_util.is_numeral(x, r)) {
+            return get_theory_vars(y, vars);
+        }
+        else if (m_util.is_mul(n, y, x) && m_util.is_numeral(x, r)) {
+            return get_theory_vars(y, vars);
+        }
+        else if (!is_app(n)) {
+            return false;
+        }
+        else if (to_app(n)->get_family_id() == m_util.get_family_id()) {
+            return false;
+        }
+        else {
+            context & ctx = get_context();
+            SASSERT(ctx.e_internalized(n));
+            enode * e    = ctx.get_enode(n);
+            if (is_attached_to_var(e)) {
+                vars.insert(e->get_th_var(get_id()));
+            }
+            return true;
+        }
+        return true;
+    }
+
     //
     // 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);
+        theory_var v = internalize_term_core(term);
+        uint_set vars;
+        if (get_theory_vars(term, vars)) {
+            m_objective_vars.insert(v, vars);
+        }
+        return v;
     }
 
     template<typename Ext>
     inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v) {
         bool r = max_min(v, true); 
-        if (at_upper(v)) {
+        if (r || at_upper(v)) {
-            m_objective_value = get_value(v);
+            if (m_objective_vars.contains(v)) {
+                // FIXME: put this block inside verbose code
+                uint_set & vars = m_objective_vars[v];
+                uint_set::iterator it = vars.begin(), end = vars.end();
+                ast_manager& m = get_manager();
+                IF_VERBOSE(1,
+                    verbose_stream() << "Optimal assigment:" << std::endl;
+                    for (; it != end; ++it) {
+                        verbose_stream() << mk_pp(get_enode(*it)->get_owner(), m) << " |-> " << get_value(*it) << std::endl;
+                    };);
             }
-        else if (!r) {
+            return inf_eps_rational<inf_rational>(get_value(v));
-            m_objective_value = inf_eps_rational<inf_rational>::infinity();
         }
-        return m_objective_value;        
+        return inf_eps_rational<inf_rational>::infinity();
     }
 
     /**
@@ -1414,8 +1464,6 @@ namespace smt {
             TRACE("maximize", tout << "v" << v << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n";
                   display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row););
             
-            m_objective_value = get_value(v);            
-
             mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row);
             
             return true;

src/smt/theory_diff_logic.h

@@ -318,6 +318,8 @@ namespace smt {
 
     private:     
 
+        virtual expr* block_objective(theory_var v, inf_rational const& val);
+
         virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j);
 
         virtual void new_diseq_eh(theory_var v1, theory_var v2, justification& j);

src/smt/theory_diff_logic_def.h

@@ -29,6 +29,7 @@ Revision History:
 #include"warning.h"
 #include"smt_model_generator.h"
 #include"network_flow_def.h"
+#include"model_implicant.h"
 
 using namespace smt;
 
@@ -1036,9 +1037,12 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
 
         vector<numeral> & current_assigments = m_objective_assignments[v];        
         SASSERT(!current_assigments.empty());
-        TRACE("network_flow",
+        ast_manager& m = get_manager();
-            for (unsigned i = 0; i < current_assigments.size(); ++i) {
+        IF_VERBOSE(1,
-                tout << "v" << i << " -> " << current_assigments[i] << std::endl;
+            verbose_stream() << "Optimal assigment:" << std::endl;
+            for (unsigned i = 0; i < objective.size(); ++i) {
+                theory_var v = objective[i].first;
+                verbose_stream() << mk_pp(get_enode(v)->get_owner(), m) << " |-> " << current_assigments[v] << std::endl;
             });
         rational r = objective_value.get_rational().to_rational();
         rational i = objective_value.get_infinitesimal().to_rational();    
@@ -1068,7 +1072,7 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
 }
 
 template<typename Ext>
-expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const& val) {
+expr* 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);
@@ -1135,6 +1139,19 @@ expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const
     }
 }
 
+template<typename Ext>
+expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const& val) {
+    expr * o = block_objective(v, val);
+    context & ctx = get_context();
+    model_ref mdl;
+    ctx.get_model(mdl);
+    ptr_vector<expr> formulas(ctx.get_num_asserted_formulas(), ctx.get_asserted_formulas());
+    ast_manager& m = get_manager();
+    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())));
+}
+
 template<typename Ext>
 bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) {