mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 03:48:51 +00:00
Code Activity

add depth guard

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-31 17:41:34 -07:00
parent 3e0a350411
commit ab259b6830
2 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/model/datatype_factory.cpp
View file

@ -139,6 +139,9 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
expr * datatype_factory::get_fresh_value(sort * s) { expr * datatype_factory::get_fresh_value(sort * s) {
if (!m_util.is_datatype(s)) if (!m_util.is_datatype(s))
return m_model.get_fresh_value(s); return m_model.get_fresh_value(s);
if (m_fresh_depth >= m_max_fresh_depth)
return get_last_fresh_value(s);
struct depth_guard { unsigned& d; depth_guard(unsigned& d) : d(d) { ++d; } ~depth_guard() { --d; } } _dg(m_fresh_depth);
TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";); TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";);
auto& [set, values] = get_value_set(s); auto& [set, values] = get_value_set(s);
// Approach 0) // Approach 0)

2
src/model/datatype_factory.h
View file

@ -24,6 +24,8 @@ Revision History:
class datatype_factory : public struct_factory { class datatype_factory : public struct_factory {
datatype_util m_util; datatype_util m_util;
obj_map<sort, expr *> m_last_fresh_value; obj_map<sort, expr *> m_last_fresh_value;
unsigned m_fresh_depth = 0;
static const unsigned m_max_fresh_depth = 512;
expr * get_last_fresh_value(sort * s); expr * get_last_fresh_value(sort * s);
expr * get_almost_fresh_value(sort * s); expr * get_almost_fresh_value(sort * s);