From bc3d8580c9bf0c28e7aa2b4b9eadac59480dd0bd Mon Sep 17 00:00:00 2001
From: Bernhard Gleiss <bgleiss@forsyte.tuwien.ac.at>
Date: Tue, 1 Aug 2017 10:12:29 +0200
Subject: [PATCH 1/3] fixed typo in optimized unsat core plugin code

---
 src/muz/spacer/spacer_unsat_core_plugin.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index 66abb32c6..5383fdc12 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -330,8 +330,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                 {
                     SASSERT(!m_learner.is_a_marked(premise));
 
-                    // XXX AG: why is this condition is based on step and not on premise?
-                    if (m_learner.only_contains_symbols_b(m_learner.m.get_fact(step)) && !m_learner.is_h_marked(step))
+                    if (m_learner.only_contains_symbols_b(m_learner.m.get_fact(premise)) && !m_learner.is_h_marked(premise))
                     {
                         rational coefficient;
                         VERIFY(params[i].is_rational(coefficient));

From 4559092a0c3a38dd51df459222978aab094afab5 Mon Sep 17 00:00:00 2001
From: Bernhard Gleiss <bgleiss@forsyte.tuwien.ac.at>
Date: Tue, 1 Aug 2017 11:06:17 +0200
Subject: [PATCH 2/3] refactored variable names and added comments to
 min_cut-related methods for unsat-core-computation

---
 src/muz/spacer/spacer_unsat_core_plugin.cpp | 56 ++++++++++++++++-----
 src/muz/spacer/spacer_unsat_core_plugin.h   |  2 +-
 2 files changed, 44 insertions(+), 14 deletions(-)

diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index 5383fdc12..0d90d2653 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -588,6 +588,17 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
 
     unsat_core_plugin_min_cut::unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner), m(m){}
 
+    /*
+     * traverses proof rooted in step and constructs graph, which corresponds to the proof-DAG, with the following differences:
+     *
+     * 1) we want to skip vertices, which have a conclusion, which we don't like (call those steps bad and the other ones good). In other words, we start at a good step r and compute the smallest subproof with root r, which has only good leaves. Then we add an edge from the root to each of the leaves and remember that we already dealt with s. Then we recurse on all leaves.
+     * 2) we want to introduce two vertices for all (unskipped) edges in order to run the min-cut algorithm
+     * 3) we want to introduce a single super-source vertex, which is connected to all source-vertices of the proof-DAG and a
+     * single super-sink vertex, to which all sink-vertices of the proof-DAG are connected
+     *
+     * 1) is dealt with using advance_to_lowest_partial_cut
+     * 2) and 3) are dealt with using add_edge
+     */
     void unsat_core_plugin_min_cut::compute_partial_core(proof* step)
     {
         ptr_vector<proof> todo;
@@ -603,21 +614,28 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
             proof* current = todo.back();
             todo.pop_back();
 
+            // if we need to deal with the node and if we haven't added the corresponding edges so far
             if (!m_learner.is_closed(current) && !m_visited.is_marked(current))
             {
-                m_visited.mark(current, true);
+                // compute smallest subproof rooted in current, which has only good edges
+                // add an edge from current to each leaf of that subproof
+                // add the leaves to todo
                 advance_to_lowest_partial_cut(current, todo);
+                
+                m_visited.mark(current, true);
+
             }
         }
         m_learner.set_closed(step, true);
     }
 
-    void unsat_core_plugin_min_cut::advance_to_lowest_partial_cut(proof* step, ptr_vector<proof>& todo2)
+    
+    void unsat_core_plugin_min_cut::advance_to_lowest_partial_cut(proof* step, ptr_vector<proof>& todo)
     {
         bool is_sink = true;
 
         ast_manager &m = m_learner.m;
-        ptr_vector<proof> todo;
+        ptr_vector<proof> todo_subproof;
 
         for (unsigned i = 0, sz = m.get_num_parents(step); i < sz; ++i)
         {
@@ -625,16 +643,16 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
             {
                 if (m_learner.is_b_marked(premise))
                 {
-                    todo.push_back(premise);
+                    todo_subproof.push_back(premise);
                 }
             }
         }
-        while (!todo.empty())
+        while (!todo_subproof.empty())
         {
-            proof* current = todo.back();
-            todo.pop_back();
+            proof* current = todo_subproof.back();
+            todo_subproof.pop_back();
 
-            // if current step hasn't been processed,
+            // if we need to deal with the node
             if (!m_learner.is_closed(current))
             {
                 SASSERT(!m_learner.is_a_marked(current)); // by I.H. the step must be already visited
@@ -647,26 +665,28 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                         (m.is_asserted(current) ||
                          is_literal(m, m.get_fact(current))))
                     {
-                        // add corresponding edges and continue original traversel
+                        // we found a leaf of the subproof, so
+                        // 1) we add corresponding edges
                         if (m_learner.is_a_marked(step))
                         {
                             add_edge(nullptr, current); // current is sink
                         }
                         else
                         {
-                            add_edge(step, current);
+                            add_edge(step, current); // standard edge
                         }
-                        todo2.push_back(current);
+                        // 2) add the leaf to todo
+                        todo.push_back(current);
                         is_sink = false;
                     }
-                    // otherwise recurse on premises
+                    // otherwise continue search for leaves of subproof
                     else
                     {
                         for (unsigned i = 0; i < m_learner.m.get_num_parents(current); ++i)
                         {
                             SASSERT(m_learner.m.is_proof(current->get_arg(i)));
                             proof* premise = m.get_parent (current, i);
-                            todo.push_back(premise);
+                            todo_subproof.push_back(premise);
                         }
                     }
                 }
@@ -679,6 +699,12 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
         }
     }
 
+    /*
+     * adds an edge from the out-vertex of i to the in-vertex of j to the graph
+     * if i or j isn't already present, it adds the corresponding in- and out-vertices to the graph
+     * if i is a nullptr, it is treated as source vertex
+     * if j is a nullptr, it is treated as sink vertex
+     */
     void unsat_core_plugin_min_cut::add_edge(proof* i, proof* j)
     {
         unsigned node_i;
@@ -747,6 +773,10 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
         m_min_cut.add_edge(node_i, node_j, 1);
     }
 
+    /*
+     * computes min-cut on the graph constructed by compute_partial_core-method
+     * and adds the corresponding lemmas to the core
+     */
     void unsat_core_plugin_min_cut::finalize()
     {
         vector<unsigned int> cut_nodes;
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h
index 388a2bd38..743d7af4a 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.h
+++ b/src/muz/spacer/spacer_unsat_core_plugin.h
@@ -104,7 +104,7 @@ private:
         ast_mark m_visited; // saves for each node i whether the subproof with root i has already been added to the min-cut-problem
         obj_map<proof, unsigned> m_proof_to_node_minus; // maps proof-steps to the corresponding minus-nodes (the ones which are closer to source)
         obj_map<proof, unsigned> m_proof_to_node_plus; // maps proof-steps to the corresponding plus-nodes (the ones which are closer to sink)
-        void advance_to_lowest_partial_cut(proof* step, ptr_vector<proof>& todo2);
+        void advance_to_lowest_partial_cut(proof* step, ptr_vector<proof>& todo);
         void add_edge(proof* i, proof* j);
 
         vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof

From 81a7f37acc4013f8ee82f24a2ff3b4918ed53608 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 1 Aug 2017 18:33:40 +0100
Subject: [PATCH 3/3] Fixed LP tests

---
 src/test/lp.cpp | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/test/lp.cpp b/src/test/lp.cpp
index f76850e38..695a31cf4 100644
--- a/src/test/lp.cpp
+++ b/src/test/lp.cpp
@@ -2779,7 +2779,7 @@ If b becomes basic variable, then it is likely the old solver ends up with a row
     vector<implied_bound> ev;
     ls.add_var_bound(a, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
     std::cout << " bound ev from test_bound_propagation_one_small_sample1" << std::endl;
     for (auto & be : bp.m_ibounds)  {
@@ -2832,7 +2832,7 @@ void test_bound_propagation_one_row() {
     vector<implied_bound> ev;
     ls.add_var_bound(x0, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 } 
 void test_bound_propagation_one_row_with_bounded_vars() {
@@ -2848,7 +2848,7 @@ void test_bound_propagation_one_row_with_bounded_vars() {
     ls.add_var_bound(x0, LE, mpq(3));
     ls.add_var_bound(x0, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 }
 void test_bound_propagation_one_row_mixed() {
@@ -2862,7 +2862,7 @@ void test_bound_propagation_one_row_mixed() {
     vector<implied_bound> ev;
     ls.add_var_bound(x1, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 } 
 
@@ -2885,7 +2885,7 @@ void test_bound_propagation_two_rows() {
     vector<implied_bound> ev;
     ls.add_var_bound(y, LE, mpq(1));
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 } 
 
@@ -2905,7 +2905,7 @@ void test_total_case_u() {
     vector<implied_bound> ev;
     ls.add_var_bound(z, GE, zero_of_type<mpq>());
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
 }
 bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const vector<implied_bound> & ev) {
@@ -2932,7 +2932,7 @@ void test_total_case_l(){
     vector<implied_bound> ev;
     ls.add_var_bound(z, LE, zero_of_type<mpq>());
     ls.solve();
-    bound_propagator bp(ls);
+    lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
     lean_assert(ev.size() == 4);
     lean_assert(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));