From 3a7cdc36d634d95565dbec1645381d8022603452 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 28 Jun 2023 10:23:35 +0200 Subject: [PATCH] slicing: mark --- src/math/polysat/slicing.cpp | 2 ++ src/math/polysat/slicing.h | 16 ++++++++++++++++ 2 files changed, 18 insertions(+) diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index d0eb214b3..29a10b558 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -64,6 +64,7 @@ namespace polysat { m_slice2var.push_back(null_var); m_proof_parent.push_back(null_slice); m_proof_reason.push_back(null_dep); + m_mark.push_back(0); m_trail.push_back(trail_item::alloc_slice); return s; } @@ -78,6 +79,7 @@ namespace polysat { m_slice2var.pop_back(); m_proof_parent.pop_back(); m_proof_reason.pop_back(); + m_mark.pop_back(); } slicing::slice slicing::find_sub_hi(slice parent) const { diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h index e5f24bc1a..0d3b40e33 100644 --- a/src/math/polysat/slicing.h +++ b/src/math/polysat/slicing.h @@ -87,6 +87,22 @@ namespace polysat { pvar_vector m_slice2var; // slice -> pvar, or null_var if slice is not equivalent to a variable slice_vector m_var2slice; // pvar -> slice + unsigned_vector m_mark; + unsigned m_mark_timestamp = 0; +#if Z3DEBUG + bool m_mark_active = false; +#endif + + void begin_mark() { + DEBUG_CODE({ SASSERT(!m_mark_active); m_mark_active = true; }); + m_mark_timestamp++; + if (!m_mark_timestamp) + m_mark_timestamp++; + } + void end_mark() { DEBUG_CODE({ SASSERT(!m_mark_active); m_mark_active = false; }); } + bool is_marked(slice s) const { SASSERT(m_mark_active); return m_mark[s] == m_mark_timestamp; } + void mark(slice s) { SASSERT(m_mark_active); m_mark[s] = m_mark_timestamp; } + slice alloc_slice(); slice var2slice(pvar v) const { return find(m_var2slice[v]); }