mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-29 07:13:37 +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 Nikolaj Bjorner
parent 059d936e08
commit f5cdff407f
2 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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();