From 0f25e9e831a85fb3647fb8cc8e45e369bc01dd21 Mon Sep 17 00:00:00 2001
From: Bernhard Gleiss <bgleiss@forsyte.tuwien.ac.at>
Date: Fri, 1 Dec 2017 15:23:07 +0100
Subject: [PATCH] Moved farkas stats printing to before and after the
 hyp-reduction

---
 src/muz/spacer/spacer_itp_solver.cpp         | 16 ++++++++++++++
 src/muz/spacer/spacer_unsat_core_learner.cpp | 22 ++++++--------------
 2 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp
index f91cc6bb3..9c11e0c1c 100644
--- a/src/muz/spacer/spacer_itp_solver.cpp
+++ b/src/muz/spacer/spacer_itp_solver.cpp
@@ -281,7 +281,23 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
         // preprocess proof in order to get a proof which is better suited for unsat-core-extraction
         proof_ref pr(get_proof(), m);
         
+        if (m_print_farkas_stats)
+        {
+            iuc_proof iuc_before(m, pr.get(), B);
+            verbose_stream() << "Stats before transformation:";
+            iuc_before.print_farkas_stats();
+        }
+
         spacer::reduce_hypotheses(pr);
+        spacer::reduce_hypotheses(pr);
+
+        if (m_print_farkas_stats)
+        {
+            iuc_proof iuc_after(m, pr.get(), B);
+            verbose_stream() << "Stats after transformation:";
+            iuc_after.print_farkas_stats();
+        }
+        
         STRACE("spacer.unsat_core_learner",
                verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";
                );
diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp
index fa5e17239..cb7ebff76 100644
--- a/src/muz/spacer/spacer_unsat_core_learner.cpp
+++ b/src/muz/spacer/spacer_unsat_core_learner.cpp
@@ -41,7 +41,7 @@ void unsat_core_learner::register_plugin(unsat_core_plugin* plugin)
 void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
 {
     // traverse proof
-   proof_post_order it(m_pr.get(), m);
+    proof_post_order it(m_pr.get(), m);
     while (it.hasNext())
     {
         proof* currentNode = it.next();
@@ -54,7 +54,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
             {
                 SASSERT(m.is_proof(currentNode->get_arg(i)));
                 proof* premise = to_app(currentNode->get_arg(i));
-
+                
                 need_to_mark_closed = need_to_mark_closed && (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
             }
 
@@ -75,16 +75,6 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
 
     // TODO: remove duplicates from unsat core?
 
-    // count both number of all Farkas lemmas and number of Farkas lemmas in the cut
-    if (m_print_farkas_stats)
-    {
-        m_pr.print_farkas_stats();
-                        }
-    //TODO remove this
-    if(m_iuc_debug_proof)
-    {
-    }
-    
     verbose_stream() << std::endl;
     // move all lemmas into vector
     for (expr* const* it = m_unsat_core.begin(); it != m_unsat_core.end(); ++it)
@@ -119,14 +109,14 @@ void unsat_core_learner::set_closed(proof* p, bool value)
 {
     m_closed.mark(p, value);
 }
-
+  
 bool unsat_core_learner::is_b_open(proof *p)
-    {
+{
      return m_pr.is_b_marked(p) && !is_closed (p);
-    }
+}
 
 void unsat_core_learner::add_lemma_to_core(expr* lemma)
 {
     m_unsat_core.push_back(lemma);
-    }
+}
 }