From 45500ff7d348d6ff50e93f568f130f6e46ea9bc7 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 16 May 2018 12:57:35 -0700
Subject: [PATCH] Cleanup iuc_proof

---
 src/muz/spacer/spacer_iuc_proof.cpp | 25 ++++++++++++++++---------
 src/muz/spacer/spacer_iuc_proof.h   | 12 ++++++++----
 2 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/src/muz/spacer/spacer_iuc_proof.cpp b/src/muz/spacer/spacer_iuc_proof.cpp
index 4ee887df5..1123a7c76 100644
--- a/src/muz/spacer/spacer_iuc_proof.cpp
+++ b/src/muz/spacer/spacer_iuc_proof.cpp
@@ -11,13 +11,21 @@ namespace spacer {
  * init
  * ====================================
  */
-iuc_proof::iuc_proof(ast_manager& m, proof* pr, expr_set& core_lits) :
+iuc_proof::iuc_proof(ast_manager& m, proof* pr, const expr_set& core_lits) :
     m(m), m_pr(pr,m) {
+    for (auto lit : core_lits) m_core_lits.insert(lit);
     // init A-marks and B-marks
-    collect_core_symbols(core_lits);
-    compute_marks(core_lits);
+    collect_core_symbols();
+    compute_marks();
 }
 
+iuc_proof::iuc_proof(ast_manager& m, proof* pr, const expr_ref_vector& core_lits) :
+    m(m), m_pr(pr,m) {
+    for (auto lit : core_lits) m_core_lits.insert(lit);
+    // init A-marks and B-marks
+    collect_core_symbols();
+    compute_marks();
+}
 /*
  * ====================================
  * methods for computing symbol colors
@@ -37,13 +45,12 @@ public:
     void operator()(quantifier*) {}
 };
 
-void iuc_proof::collect_core_symbols(expr_set& core_lits)
+void iuc_proof::collect_core_symbols()
 {
     expr_mark visited;
     collect_pure_proc proc(m_core_symbols);
-    for (expr_set::iterator it = core_lits.begin(); it != core_lits.end(); ++it) {
-        for_each_expr(proc, visited, *it);
-    }
+    for (auto lit : m_core_lits)
+        for_each_expr(proc, visited, lit);
 }
 
 class is_pure_expr_proc {
@@ -84,7 +91,7 @@ bool iuc_proof::is_core_pure(expr* e) const
     return true;
 }
 
-void iuc_proof::compute_marks(expr_set& core_lits)
+void iuc_proof::compute_marks()
 {
     proof_post_order it(m_pr, m);
     while (it.hasNext())
@@ -95,7 +102,7 @@ void iuc_proof::compute_marks(expr_set& core_lits)
             switch(cur->get_decl_kind())
             {
             case PR_ASSERTED:
-                if (core_lits.contains(m.get_fact(cur)))
+                if (m_core_lits.contains(m.get_fact(cur)))
                     m_b_mark.mark(cur, true);
                 else
                     m_a_mark.mark(cur, true);
diff --git a/src/muz/spacer/spacer_iuc_proof.h b/src/muz/spacer/spacer_iuc_proof.h
index 97c00ea9b..aeb18ef37 100644
--- a/src/muz/spacer/spacer_iuc_proof.h
+++ b/src/muz/spacer/spacer_iuc_proof.h
@@ -17,7 +17,8 @@ public:
 
     // Constructs an iuc_proof given an ast_manager, a proof, and a set of
     // literals core_lits that might be included in the unsat core
-    iuc_proof(ast_manager& m, proof* pr, expr_set& core_lits);
+    iuc_proof(ast_manager& m, proof* pr, const expr_set& core_lits);
+    iuc_proof(ast_manager& m, proof* pr, const expr_ref_vector &core_lits);
 
     // returns the proof object
     proof* get() {return m_pr.get();}
@@ -44,15 +45,18 @@ private:
     ast_mark m_b_mark;
     ast_mark m_h_mark;
 
+    // -- literals that are part of the core
+    expr_set m_core_lits;
+
     // symbols that occur in any literals in the core
     func_decl_set m_core_symbols;
 
-    // collect symbols occuring in B (the core)
-    void collect_core_symbols(expr_set& core_lits);
+    // collect symbols occurring in B (the core)
+    void collect_core_symbols();
 
     // compute for each formula of the proof whether it derives
     // from A or from B
-    void compute_marks(expr_set& core_lits);
+    void compute_marks();
 };