From 5072a2a869f2b312649a815a8b495009840ea92f Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 29 May 2018 21:23:32 -0700
Subject: [PATCH] spacer: pobs keep track of their lemmas

---
 src/muz/spacer/spacer_context.cpp | 33 +++++++++++++++++++++----------
 src/muz/spacer/spacer_context.h   |  8 ++++++++
 2 files changed, 31 insertions(+), 10 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index e826e19aa..3d7e9a921 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -70,7 +70,6 @@ pob::pob (pob* parent, pred_transformer& pt,
     }
 }
 
-
 void pob::set_post(expr* post) {
     app_ref_vector empty_binding(get_ast_manager());
     set_post(post, empty_binding);
@@ -1800,36 +1799,48 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma)
           << m_pt.head()->get_name() << " "
           << mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
 
-    for (unsigned i = 0, sz = m_lemmas.size(); i < sz; ++i) {
-        if (m_lemmas[i]->get_expr() == new_lemma->get_expr()) {
+    unsigned i = 0;
+    for (auto *old_lemma : m_lemmas) {
+        if (old_lemma->get_expr() == new_lemma->get_expr()) {
             m_pt.get_context().new_lemma_eh(m_pt, new_lemma);
+
+            // register existing lemma with the pob
+            if (new_lemma->has_pob()) {
+                pob_ref &pob = new_lemma->get_pob();
+                if (!pob->lemmas().contains(old_lemma))
+                    pob->add_lemma(old_lemma);
+            }
+
             // extend bindings if needed
             if (!new_lemma->get_bindings().empty()) {
-                m_lemmas[i]->add_binding(new_lemma->get_bindings());
+                old_lemma->add_binding(new_lemma->get_bindings());
             }
             // if the lemma is at a higher level, skip it,
-            if (m_lemmas[i]->level() >= new_lemma->level()) {
+            if (old_lemma->level() >= new_lemma->level()) {
                 TRACE("spacer", tout << "Already at a higher level: "
-                      << pp_level(m_lemmas[i]->level()) << "\n";);
+                      << pp_level(old_lemma->level()) << "\n";);
                 // but, since the instances might be new, assert the
                 // instances that have been copied into m_lemmas[i]
                 if (!new_lemma->get_bindings().empty()) {
-                    m_pt.add_lemma_core(m_lemmas[i], true);
+                    m_pt.add_lemma_core(old_lemma, true);
                 }
                 // no new lemma added
                 return false;
             }
 
             // update level of the existing lemma
-            m_lemmas[i]->set_level(new_lemma->level());
+            old_lemma->set_level(new_lemma->level());
             // assert lemma in the solver
-            m_pt.add_lemma_core(m_lemmas[i], false);
+            m_pt.add_lemma_core(old_lemma, false);
             // move the lemma to its new place to maintain sortedness
-            for (unsigned j = i; (j + 1) < sz && m_lt(m_lemmas[j + 1], m_lemmas[j]); ++j) {
+            unsigned sz = m_lemmas.size();
+            for (unsigned j = i;
+                 (j + 1) < sz && m_lt(m_lemmas[j + 1], m_lemmas[j]); ++j) {
                 m_lemmas.swap (j, j+1);
             }
             return true;
         }
+        i++;
     }
 
     // new_lemma is really new
@@ -1840,6 +1851,8 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma)
     m_sorted = false;
     m_pt.add_lemma_core(new_lemma);
 
+    if (new_lemma->has_pob()) {new_lemma->get_pob()->add_lemma(new_lemma);}
+
     if (!new_lemma->external()) {
         m_pt.get_context().new_lemma_eh(m_pt, new_lemma);
     }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index f1b852cc3..2adf23007 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -486,7 +486,11 @@ class pob {
     /// derivation representing the position of this node in the parent's rule
     scoped_ptr<derivation>   m_derivation;
 
+    /// pobs created as children of this pob (at any time, not
+    /// necessarily currently active)
     ptr_vector<pob>  m_kids;
+    // lemmas created to block this pob (at any time, not necessarily active)
+    ptr_vector<lemma> m_lemmas;
 
     // depth -> watch
     std::map<unsigned, stopwatch> m_expand_watches;
@@ -542,9 +546,13 @@ public:
     bool is_closed () const { return !m_open; }
     void close();
 
+    const ptr_vector<pob> &children() {return m_kids;}
     void add_child (pob &v) {m_kids.push_back (&v);}
     void erase_child (pob &v) {m_kids.erase (&v);}
 
+    const ptr_vector<lemma> &lemmas() {return m_lemmas;}
+    void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);}
+
     bool is_ground () { return m_binding.empty (); }
     unsigned get_free_vars_size() { return m_binding.size(); }
     app_ref_vector const &get_binding() const {return m_binding;}