mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Pin lemmas so that they don't disappear

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-29 21:22:32 -07:00
parent ebfb2a4a1e
commit 61cd74818f
2 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_context.cpp
View file

@ -1834,6 +1834,9 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma)
// new_lemma is really new // new_lemma is really new
m_lemmas.push_back(new_lemma); 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_sorted = false;
m_pt.add_lemma_core(new_lemma); m_pt.add_lemma_core(new_lemma);

11
src/muz/spacer/spacer_context.h
View file

@ -198,12 +198,13 @@ class pred_transformer {
#include "muz/spacer/spacer_legacy_frames.h" #include "muz/spacer/spacer_legacy_frames.h"
class frames { class frames {
private: private:
pred_transformer &m_pt; pred_transformer &m_pt; // parent pred_transformer
lemma_ref_vector m_lemmas; lemma_ref_vector m_pinned_lemmas; // all created lemmas
unsigned m_size; lemma_ref_vector m_lemmas; // active lemmas
unsigned m_size; // num of frames
bool m_sorted; bool m_sorted; // true if m_lemmas is sorted by m_lt
lemma_lt_proc m_lt; lemma_lt_proc m_lt; // sort order for m_lemmas
void sort (); void sort ();