From 61cd74818f3fb22c5b835d732922d18b75eb3df1 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 29 May 2018 21:22:32 -0700 Subject: [PATCH] Pin lemmas so that they don't disappear --- src/muz/spacer/spacer_context.cpp | 3 +++ src/muz/spacer/spacer_context.h | 11 ++++++----- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 5e2d0f1f4..e826e19aa 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1834,6 +1834,9 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma) // new_lemma is really new m_lemmas.push_back(new_lemma); + // XXX because m_lemmas is reduced, keep secondary vector of all lemmas + // XXX so that pob can refer to its lemmas without creating reference cycles + m_pinned_lemmas.push_back(new_lemma); m_sorted = false; m_pt.add_lemma_core(new_lemma); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index cb6d1fc23..f1b852cc3 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -198,12 +198,13 @@ class pred_transformer { #include "muz/spacer/spacer_legacy_frames.h" class frames { private: - pred_transformer &m_pt; - lemma_ref_vector m_lemmas; - unsigned m_size; + pred_transformer &m_pt; // parent pred_transformer + lemma_ref_vector m_pinned_lemmas; // all created lemmas + lemma_ref_vector m_lemmas; // active lemmas + unsigned m_size; // num of frames - bool m_sorted; - lemma_lt_proc m_lt; + bool m_sorted; // true if m_lemmas is sorted by m_lt + lemma_lt_proc m_lt; // sort order for m_lemmas void sort ();