From 0a32337f0aa3608ae2368676cebac8ee03126a2f Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 18 Mar 2026 16:15:37 +0100 Subject: [PATCH] Removed some brackets --- src/smt/seq/seq_nielsen.cpp | 90 ++++++++++++++++++++++--------------- src/smt/seq/seq_nielsen.h | 2 +- src/smt/seq_model.cpp | 34 ++++++++------ 3 files changed, 76 insertions(+), 50 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 02eaf4006..7c70f9b5b 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -102,8 +102,10 @@ namespace seq { // ----------------------------------------------- void str_eq::sort() { - if (m_lhs && m_rhs && m_lhs->id() > m_rhs->id()) + if (m_lhs && m_rhs && m_lhs->id() > m_rhs->id()) { std::swap(m_lhs, m_rhs); + std::swap(m_l, m_r); + } } bool str_eq::is_trivial() const { @@ -112,19 +114,24 @@ namespace seq { } bool str_eq::contains_var(euf::snode* var) const { - if (!var) return false; + if (!var) + return false; // check if var appears in the token list of lhs or rhs if (m_lhs) { euf::snode_vector tokens; m_lhs->collect_tokens(tokens); - for (euf::snode* t : tokens) - if (t == var) return true; + for (euf::snode* t : tokens) { + if (t == var) + return true; + } } if (m_rhs) { euf::snode_vector tokens; m_rhs->collect_tokens(tokens); - for (euf::snode* t : tokens) - if (t == var) return true; + for (euf::snode* t : tokens) { + if (t == var) + return true; + } } return false; } @@ -142,12 +149,14 @@ namespace seq { } bool str_mem::contains_var(euf::snode* var) const { - if (!var) return false; + SASSERT(var); if (m_str) { euf::snode_vector tokens; m_str->collect_tokens(tokens); - for (euf::snode* t : tokens) - if (t == var) return true; + for (const euf::snode* t : tokens) { + if (t == var) + return true; + } } return false; } @@ -157,12 +166,14 @@ namespace seq { // ----------------------------------------------- bool nielsen_subst::is_eliminating() const { - if (!m_var || !m_replacement) return true; + SASSERT(m_var && m_replacement) // check if var appears in replacement euf::snode_vector tokens; m_replacement->collect_tokens(tokens); - for (euf::snode* t : tokens) - if (t == m_var) return false; + for (const euf::snode* t : tokens) { + if (t == m_var) + return false; + } return true; } @@ -171,16 +182,14 @@ namespace seq { // ----------------------------------------------- nielsen_edge::nielsen_edge(nielsen_node* src, nielsen_node* tgt, bool is_progress): - m_src(src), m_tgt(tgt), m_is_progress(is_progress) { - } + m_src(src), m_tgt(tgt), m_is_progress(is_progress) { } // ----------------------------------------------- // nielsen_node // ----------------------------------------------- nielsen_node::nielsen_node(nielsen_graph& graph, unsigned id): - m_id(id), m_graph(graph), m_is_progress(true) { - } + m_id(id), m_graph(graph), m_is_progress(true) { } void nielsen_node::clone_from(nielsen_node const& parent) { m_str_eq.reset(); @@ -190,17 +199,21 @@ namespace seq { m_char_ranges.reset(); m_var_lb.reset(); m_var_ub.reset(); - for (auto const& eq : parent.m_str_eq) + for (auto const& eq : parent.m_str_eq) { m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs,eq.m_l, eq.m_r, eq.m_dep)); - for (auto const& mem : parent.m_str_mem) + } + for (auto const& mem : parent.m_str_mem) { m_str_mem.push_back(str_mem(mem.m_str, mem.m_regex, mem.m_lit, mem.m_history, mem.m_id, mem.m_dep)); - for (auto const& ic : parent.m_int_constraints) + } + for (auto const& ic : parent.m_int_constraints) { m_int_constraints.push_back(ic); + } // clone character disequalities for (auto const& kv : parent.m_char_diseqs) { ptr_vector diseqs; - for (euf::snode* s : kv.m_value) + for (euf::snode* s : kv.m_value) { diseqs.push_back(s); + } m_char_diseqs.insert(kv.m_key, diseqs); } // clone character ranges @@ -208,10 +221,12 @@ namespace seq { m_char_ranges.insert(kv.m_key, kv.m_value.clone()); } // clone per-variable integer bounds - for (auto const& kv : parent.m_var_lb) + for (auto const& kv : parent.m_var_lb) { m_var_lb.insert(kv.m_key, kv.m_value); - for (auto const& kv : parent.m_var_ub) + } + for (auto const& kv : parent.m_var_ub) { m_var_ub.insert(kv.m_key, kv.m_value); + } // clone regex occurrence tracking m_regex_occurrence = parent.m_regex_occurrence; } @@ -229,7 +244,8 @@ namespace seq { // NSB review: optimize sg.subst to apply join only if the substitution had an effect. void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { - if (!s.m_var) return; + if (!s.m_var) + return; for (unsigned i = 0; i < m_str_eq.size(); ++i) { str_eq& eq = m_str_eq[i]; eq.m_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement); @@ -272,8 +288,10 @@ namespace seq { m_char_diseqs.insert(id, ptr_vector()); ptr_vector& existing = m_char_diseqs.find(id); // check for duplicates - for (euf::snode* s : existing) - if (s == other) return; + for (euf::snode* s : existing) { + if (s == other) + return; + } existing.push_back(other); } @@ -283,21 +301,21 @@ namespace seq { // ----------------------------------------------- unsigned nielsen_node::var_lb(euf::snode* var) const { - if (!var) return 0; + SASSERT(var); unsigned v = 0; m_var_lb.find(var->id(), v); return v; } unsigned nielsen_node::var_ub(euf::snode* var) const { - if (!var) return UINT_MAX; + SASSERT(!var); unsigned v = UINT_MAX; m_var_ub.find(var->id(), v); return v; } bool nielsen_node::add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep) { - if (!var || !var->is_var()) return false; + SASSERT(var && var->is_var()); unsigned id = var->id(); // check against existing lower bound unsigned cur_lb = 0; @@ -356,26 +374,27 @@ namespace seq { // - for multiple variables: each gets an upper bound hi-const_len // Mirrors ZIPT's VarBoundWatcher mechanism. void nielsen_node::watch_var_bounds(nielsen_subst const& s) { - if (!s.m_var) return; + SASSERT(s.m_var); unsigned id = s.m_var->id(); unsigned lo = 0, hi = UINT_MAX; m_var_lb.find(id, lo); m_var_ub.find(id, hi); - if (lo == 0 && hi == UINT_MAX) return; // no bounds to propagate + if (lo == 0 && hi == UINT_MAX) + return; // no bounds to propagate // decompose replacement into constant length + variable tokens - if (!s.m_replacement) return; + if (!s.m_replacement) + return; euf::snode_vector tokens; s.m_replacement->collect_tokens(tokens); unsigned const_len = 0; euf::snode_vector var_tokens; for (euf::snode* t : tokens) { - if (t->is_char() || t->is_unit()) { + if (t->is_char() || t->is_unit()) ++const_len; - } else if (t->is_var()) { + else if (t->is_var()) var_tokens.push_back(t); - } else // power or unknown token: cannot propagate simply, abort return; @@ -415,8 +434,9 @@ namespace seq { return; } unsigned each_ub = hi - const_len; - for (euf::snode* y : var_tokens) + for (euf::snode* y : var_tokens) { add_upper_int_bound(y, each_ub, s.m_dep); + } } } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index d8b612e84..7dab8807e 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -356,7 +356,7 @@ namespace seq { smt::enode *m_l, *m_r; dep_tracker m_dep; - str_eq(): m_lhs(nullptr), m_rhs(nullptr), m_dep(nullptr) {} + str_eq() = default; str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r, dep_tracker const& dep): m_lhs(lhs), m_rhs(rhs), m_l(l), m_r(r), m_dep(dep) {} diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 8e54559b1..2b78c5b96 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -161,7 +161,8 @@ namespace smt { if (n->is_empty()) { sort* srt = n->get_sort(); - if (!srt) srt = m_seq.str.mk_string_sort(); + if (!srt) + srt = m_seq.str.mk_string_sort(); return expr_ref(m_seq.str.mk_empty(srt), m); } @@ -179,8 +180,10 @@ namespace smt { expr_ref rhs = snode_to_value(n->arg(1)); if (lhs && rhs) return expr_ref(m_seq.str.mk_concat(lhs, rhs), m); - if (lhs) return lhs; - if (rhs) return rhs; + if (lhs) + return lhs; + if (rhs) + return rhs; return expr_ref(m); } @@ -203,31 +206,34 @@ namespace smt { // finally fall back to the proto_model from model_generator. if (exp_expr && arith.is_numeral(exp_expr, exp_val)) { // already concrete - } else if (exp_expr && m_int_model.get()) { + } + else if (exp_expr && m_int_model.get()) { expr_ref result(m); if (m_int_model->eval_expr(exp_expr, result, true) && arith.is_numeral(result, exp_val)) { // evaluated from int model - } else if (m_mg) { + } + else if (m_mg) { proto_model& pm = m_mg->get_model(); if (pm.eval(exp_expr, result, true) && arith.is_numeral(result, exp_val)) { // evaluated from proto_model - } else { - exp_val = rational(0); } - } else { - exp_val = rational(0); + else + exp_val = rational(0); } - } else if (exp_expr && m_mg) { + else + exp_val = rational(0); + } + else if (exp_expr && m_mg) { expr_ref result(m); proto_model& pm = m_mg->get_model(); if (pm.eval(exp_expr, result, true) && arith.is_numeral(result, exp_val)) { // evaluated from proto_model - } else { - exp_val = rational(0); } - } else { - exp_val = rational(0); + else + exp_val = rational(0); } + else + exp_val = rational(0); if (exp_val.is_neg()) exp_val = rational(0);