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

Refactor theory_char::get_char_value to use std::optional (#8302)

Browse source 
* Initial plan

* Refactor theory_char::get_char_value to use std::optional

- Updated function signature to return std::optional<unsigned>
- Added const qualifier to function
- Updated both call sites to use modern C++17 patterns
- Used std::as_const to disambiguate overload resolution

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 13:32:18 -08:00 • committed by GitHub
parent c0583b828d
commit c73d623dfd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_char.cpp
View file

@ -314,11 +314,11 @@ namespace smt {
// extract the initial set of constants.
uint_set values;
unsigned c = 0, d = 0;
for (unsigned v = get_num_vars(); v-- > 0; ) {
expr* e = get_expr(v);
if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) {
CTRACE(seq_verbose, seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
if (auto c_opt = std::as_const(*this).get_char_value(v); seq.is_char(e) && m_var2value[v] == UINT_MAX && c_opt) {
unsigned c = *c_opt;
CTRACE(seq_verbose, seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << c << "\n";);
enode* r = get_enode(v)->get_root();
m_value2var.reserve(c + 1, null_theory_var);
theory_var u = m_value2var[c];
@ -334,7 +334,7 @@ namespace smt {
u = n->get_th_var(get_id());
if (u == null_theory_var)
continue;
if (get_char_value(u, d) && d != c) {
if (auto d_opt = std::as_const(*this).get_char_value(u); d_opt && *d_opt != c) {
enforce_ackerman(u, v);
return false;
}
@ -346,11 +346,11 @@ namespace smt {
}
// assign values to other unassigned nodes
c = 'A';
unsigned c = 'A';
for (unsigned v = get_num_vars(); v-- > 0; ) {
expr* e = get_expr(v);
if (seq.is_char(e) && m_var2value[v] == UINT_MAX) {
d = c;
unsigned d = c;
while (values.contains(c)) {
c = (c + 1) % seq.max_char();
if (d == c) {
@ -420,18 +420,18 @@ namespace smt {
return m_var2value[v];
}
bool theory_char::get_char_value(theory_var v, unsigned& c) {
std::optional<unsigned> theory_char::get_char_value(theory_var v) const {
if (!has_bits(v))
return false;
auto const & b = get_bits(v);
c = 0;
return std::nullopt;
auto const & b = m_bits[v];
unsigned c = 0;
unsigned p = 1;
for (literal lit : b) {
if (ctx.get_assignment(lit) == l_true)
c += p;
p *= 2;
}
return true;
return c;
}
// a stand-alone theory.

3
src/smt/theory_char.h
View file

@ -20,6 +20,7 @@ Author:
#include "ast/rewriter/bit_blaster/bit_blaster.h"
#include "model/char_factory.h"
#include "smt/smt_theory.h"
#include <optional>
namespace smt {
@ -49,7 +50,7 @@ namespace smt {
expr_ref_vector const& get_ebits(theory_var v);
bool has_bits(theory_var v) const;
void init_bits(theory_var v);
bool get_char_value(theory_var v, unsigned& c);
std::optional<unsigned> get_char_value(theory_var v) const;
void enforce_ackerman(theory_var v, theory_var w);
void enforce_value_bound(theory_var v);
void enforce_bits();