mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

pattern_inference: use auto for structured binding; drop debug well_sorted asserts in rewriter

Browse source 
Fixes a build error (C3694) from an illegal specifier in the structured
binding at pattern_inference.cpp:127, and removes the temporary
is_well_sorted SASSERTs (and well_sorted.h include) from rewriter_def.h
that were used during pattern-inference diagnosis.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-06 17:14:22 -07:00
parent 5534dba680
commit ca6d6e3977
2 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/pattern/pattern_inference.cpp
View file

@ -124,7 +124,7 @@ void pattern_inference_cfg::collect::operator()(expr * n, unsigned num_bindings)
m_num_bindings = num_bindings;
m_todo.push_back(entry(n, 0));
while (!m_todo.empty()) {
entry [n, delta] = m_todo.back();
auto [n, delta] = m_todo.back();
TRACE(collect, tout << "processing: " << n->get_id() << " " << delta << " kind: " << n->get_kind() << "\n";);
TRACE(collect_info, tout << mk_pp(n, m) << "\n";);
if (visit_children(n, delta)) {

3
src/ast/rewriter/rewriter_def.h
View file

@ -21,7 +21,6 @@ Notes:
#include "ast/rewriter/rewriter.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "ast/ast_pp.h"
template<typename Config>
@ -553,7 +552,6 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
SASSERT(fr.m_spos + num_children == result_stack().size());
expr * const * it = result_stack().data() + fr.m_spos;
expr * new_body = *it;
SASSERT(is_well_sorted(m_manager, q));
unsigned num_pats = q->get_num_patterns();
unsigned num_no_pats = q->get_num_no_patterns();
expr_ref_vector new_pats(m_manager, num_pats, q->get_patterns());
@ -606,7 +604,6 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
if (!m_cfg.reduce_quantifier(q, new_body, new_pats.data(), new_no_pats.data(), m_r, m_pr)) {
if (fr.m_new_child) {
m_r = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body);
SASSERT(is_well_sorted(m(), m_r));
}
else {
TRACE(rewriter_reuse, tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";);