mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

break self recursion #5937

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-03-31 21:49:08 -07:00
parent dd27f7e937
commit 28e94583da
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/model/datatype_factory.cpp
View file

@ -48,10 +48,8 @@ expr * datatype_factory::get_some_value(sort * s) {
*/ */
expr * datatype_factory::get_last_fresh_value(sort * s) { expr * datatype_factory::get_last_fresh_value(sort * s) {
expr * val = nullptr; expr * val = nullptr;
if (m_last_fresh_value.find(s, val)) { if (m_last_fresh_value.find(s, val))
TRACE("datatype", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
return val; return val;
}
value_set * set = get_value_set(s); value_set * set = get_value_set(s);
if (set->empty()) if (set->empty())
val = get_some_value(s); val = get_some_value(s);
@ -200,7 +198,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (m_util.is_recursive(s)) { if (m_util.is_recursive(s)) {
while (true) { while (true) {
++num_iterations; ++num_iterations;
TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); TRACE("datatype", tout << num_iterations << " " << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
for (func_decl * constructor : constructors) { for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager); expr_ref_vector args(m_manager);
@ -219,7 +217,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
expr * maybe_new_arg = nullptr; expr * maybe_new_arg = nullptr;
if (!m_util.is_datatype(s_arg)) if (!m_util.is_datatype(s_arg))
maybe_new_arg = m_model.get_fresh_value(s_arg); maybe_new_arg = m_model.get_fresh_value(s_arg);
else if (num_iterations <= 1) else if (num_iterations <= 1 || s == s_arg)
maybe_new_arg = get_almost_fresh_value(s_arg); maybe_new_arg = get_almost_fresh_value(s_arg);
else else
maybe_new_arg = get_fresh_value(s_arg); maybe_new_arg = get_fresh_value(s_arg);