Clean up

src/model/model_implicant.h

@@ -98,7 +98,7 @@ public:
        expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
     
     /**
-       \brief extract literals from formulas that satisfy formulas.
+       \brief extract literals from model that satisfy formulas.
        
        \pre model satisfies formulas
     */

src/opt/opt_solver.cpp

@@ -104,8 +104,6 @@ namespace opt {
         }
     }
 
-    static unsigned g_checksat_count = 0;
-
     bool opt_solver::dump_benchmarks() {
         return m_dump_benchmarks;
     }

src/smt/network_flow.h

@@ -34,6 +34,17 @@ Notes:
 
 namespace smt {
 
+    enum min_flow_result {
+        // Min cost flow problem is infeasible.
+        // Diff logic optimization could be unbounded or infeasible.
+        INFEASIBLE,
+        // Min cost flow and diff logic optimization are both optimal.
+        OPTIMAL,
+        // Min cost flow problem is unbounded.
+        // Diff logic optimization has to be infeasible.
+        UNBOUNDED,
+    };
+
     enum pivot_rule {
         // First eligible edge pivot rule
         // Edges are traversed in a wraparound fashion
@@ -281,6 +292,7 @@ namespace smt {
 
         bool edge_in_tree(edge_id id) const;
 
+        bool is_infeasible();
         bool check_well_formed();
         bool check_optimal();
 
@@ -294,7 +306,7 @@ namespace smt {
         
         // Minimize cost flows
         // Return true if found an optimal solution, and return false if unbounded
-        bool min_cost(pivot_rule pr = FIRST_ELIGIBLE);
+        min_flow_result min_cost(pivot_rule pr = FIRST_ELIGIBLE);
 
         // Compute the optimal solution
         numeral get_optimal_solution(vector<numeral> & result, bool is_dual);

src/smt/network_flow_def.h

@@ -263,13 +263,12 @@ namespace smt {
     }
 
     // Minimize cost flows
-    // Return true if found an optimal solution, and return false if unbounded
     template<typename Ext>
-    bool network_flow<Ext>::min_cost(pivot_rule pr) {
+    min_flow_result network_flow<Ext>::min_cost(pivot_rule pr) {
         initialize();
         while (choose_entering_edge(pr)) { 
             bool bounded = choose_leaving_edge();
-            if (!bounded) return false;
+            if (!bounded) return UNBOUNDED;
             update_flows();
             if (m_enter_id != m_leave_id) {
 				SASSERT(edge_in_tree(m_leave_id));
@@ -282,9 +281,23 @@ namespace smt {
                 SASSERT(check_well_formed());
             }
         }
+        if (is_infeasible()) return INFEASIBLE;
         TRACE("network_flow", tout << "Found optimal solution.\n";);
         SASSERT(check_optimal());
-        return true;
+        return OPTIMAL;
+    }
+
+    template<typename Ext>
+    bool network_flow<Ext>::is_infeasible() {
+#if 0
+        // Flows of artificial arcs should be zero
+        unsigned num_nodes = m_graph.get_num_nodes();
+        unsigned num_edges = m_graph.get_num_edges();
+        for (unsigned i = 1; i < num_nodes; ++i) {
+            if (m_flows[num_edges - i].is_pos()) return true;
+        }
+#endif
+        return false;
     }
 
     // Get the optimal solution

src/smt/theory_arith.h

@@ -434,7 +434,7 @@ namespace smt {
         bool                    m_eager_gcd; // true if gcd should be applied at every add_row
         unsigned                m_final_check_idx;
 
-        u_map<uint_set>        m_objective_vars;
+        u_map<uint_set>        m_objective_theory_vars;
 
         // backtracking
         svector<bound_trail>    m_bound_trail;

src/smt/theory_arith_aux.h

@@ -1015,7 +1015,7 @@ namespace smt {
         theory_var v = internalize_term_core(term);
         uint_set vars;
         if (get_theory_vars(term, vars)) {
-            m_objective_vars.insert(v, vars);
+            m_objective_theory_vars.insert(v, vars);
         }
         return v;
     }
@@ -1024,9 +1024,9 @@ namespace smt {
     inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v) {
         bool r = max_min(v, true); 
         if (r || at_upper(v)) {
-            if (m_objective_vars.contains(v)) {
+            if (m_objective_theory_vars.contains(v)) {
                 // FIXME: put this block inside verbose code
-                uint_set & vars = m_objective_vars[v];
+                uint_set & vars = m_objective_theory_vars[v];
                 uint_set::iterator it = vars.begin(), end = vars.end();
                 ast_manager& m = get_manager();
                 IF_VERBOSE(1,

src/smt/theory_arith_core.h

@@ -1226,6 +1226,7 @@ namespace smt {
         m_nl_rounds              = 0;
         m_nl_gb_exhausted        = false;
         m_nl_strategy_idx        = 0;
+        m_objective_theory_vars  .reset();
         theory::reset_eh();
     }
 

src/smt/theory_diff_logic_def.h

@@ -1027,8 +1027,8 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
     }
 
     network_flow<GExt> net_flow(m_graph, balances);
-    bool is_optimal = net_flow.min_cost();
+    min_flow_result result = net_flow.min_cost();
-    if (is_optimal) {
+    if (result == OPTIMAL) {
         numeral objective_value = net_flow.get_optimal_solution(m_objective_assignments[v], true) + numeral(m_objective_consts[v]);
         IF_VERBOSE(1, verbose_stream() << "Optimal value of objective " << v << ": " << objective_value << std::endl;);