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

Refactor sym_mux::find_idx to use std::optional (#8293)

Browse source 
* Initial plan

* Refactor sym_mux::find_idx to use std::optional

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-23 09:06:12 -08:00 • committed by GitHub
parent fc3bf1e6d8
commit b778bf09f9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/muz/spacer/spacer_sym_mux.cpp
View file

@ -65,10 +65,12 @@ void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) const {
}
}
bool sym_mux::find_idx(func_decl * sym, unsigned & idx) const {
std::optional<unsigned> sym_mux::find_idx(func_decl * sym) const {
std::pair<sym_mux_entry *, unsigned> entry;
if (m_muxes.find(sym, entry)) {idx = entry.second; return true;}
return false;
if (m_muxes.find(sym, entry)) {
return entry.second;
}
return std::nullopt;
}
func_decl * sym_mux::find_by_decl(func_decl* fdecl, unsigned idx) const {
@ -101,10 +103,10 @@ struct formula_checker {
if (m_found || !is_app(e)) { return; }
func_decl * sym = to_app(e)->get_decl();
unsigned sym_idx;
if (!m_parent.find_idx(sym, sym_idx)) { return; }
auto sym_idx = m_parent.find_idx(sym);
if (!sym_idx) { return; }
bool have_idx = sym_idx == m_idx;
bool have_idx = *sym_idx == m_idx;
m_found = !have_idx;
}

5
src/muz/spacer/spacer_sym_mux.h
View file

@ -21,6 +21,7 @@ Revision History:
#pragma once
#include <optional>
#include <string>
#include "ast/ast.h"
@ -53,9 +54,9 @@ public:
ast_manager & get_manager() const { return m; }
void register_decl(func_decl *fdecl);
bool find_idx(func_decl * sym, unsigned & idx) const;
std::optional<unsigned> find_idx(func_decl * sym) const;
bool has_index(func_decl * sym, unsigned idx) const
{unsigned v; return find_idx(sym, v) && idx == v;}
{auto v = find_idx(sym); return v && *v == idx;}
bool is_muxed(func_decl *fdecl) const {return m_muxes.contains(fdecl);}