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

Replace custom util/optional with std::optional (#8162)

Browse source 
* Initial plan

* Replace optional with std::optional in source files

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

* Fix array_map contains() and remove optional_benchmark test

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

* Address code review feedback - simplify array_map and test

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-11 19:47:39 -08:00 • committed by GitHub
parent 40250bfcb8
commit 4d188f07e9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
15 changed files with 34 additions and 592 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.h
View file

@ -26,7 +26,7 @@ Revision History:
#include "util/symbol.h"
#include "util/rational.h"
#include "util/hash.h"
#include "util/optional.h"
#include <optional>
#include "util/trace.h"
#include "util/bit_vector.h"
#include "util/symbol_table.h"

4
src/ast/sls/sls_arith_base.h
View file

@ -18,7 +18,7 @@ Author:
#include "util/obj_pair_set.h"
#include "util/checked_int64.h"
#include "util/optional.h"
#include <optional>
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.h"
#include "ast/sls/sls_context.h"
@ -115,7 +115,7 @@ namespace sls {
sat::bool_var_vector m_bool_vars_of;
unsigned_vector m_clauses_of;
unsigned_vector m_muls, m_adds, m_ops, m_ifs;
optional<bound> m_lo, m_hi;
std::optional<bound> m_lo, m_hi;
vector<num_t> m_finite_domain;
num_t const& value() const { return m_value; }

2
src/ast/sls/sls_arith_clausal.h
View file

@ -18,7 +18,7 @@ Author:
#pragma once
#include "util/checked_int64.h"
#include "util/optional.h"
#include <optional>
#include "util/nat_set.h"
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.h"

2
src/ast/sls/sls_arith_lookahead.h
View file

@ -18,7 +18,7 @@ Author:
#pragma once
#include "util/checked_int64.h"
#include "util/optional.h"
#include <optional>
#include "util/nat_set.h"
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.h"

4
src/math/lp/lp_api.h
View file

@ -10,7 +10,7 @@ Author:
#pragma once
#include "util/inf_rational.h"
#include "util/optional.h"
#include <optional>
namespace lp_api {
@ -89,7 +89,7 @@ namespace lp_api {
}
typedef optional<inf_rational> opt_inf_rational;
typedef std::optional<inf_rational> opt_inf_rational;
struct stats {

3
src/math/simplex/network_flow.h
View file

@ -30,6 +30,7 @@ Notes:
#include "util/inf_rational.h"
#include "smt/diff_logic.h"
#include "smt/spanning_tree.h"
#include <optional>
namespace smt {
@ -152,7 +153,7 @@ namespace smt {
unsigned m_step;
edge_id m_enter_id;
edge_id m_leave_id;
optional<numeral> m_delta;
std::optional<numeral> m_delta;
// Initialize the network with a feasible spanning tree
void initialize();

2
src/math/simplex/network_flow_def.h
View file

@ -237,7 +237,7 @@ namespace smt {
bool network_flow<Ext>::choose_leaving_edge() {
node src = m_graph.get_source(m_enter_id);
node tgt = m_graph.get_target(m_enter_id);
m_delta.set_invalid();
m_delta.reset();
edge_id leave_id = null_edge_id;
svector<edge_id> path;
bool_vector against;

2
src/opt/opt_parse.cpp
View file

@ -550,7 +550,7 @@ class lp_parse {
};
struct bound {
optional<rational> m_lo, m_hi;
std::optional<rational> m_lo, m_hi;
bool m_int;
bound() : m_int(false) {}
};

2
src/smt/theory_lra.cpp
View file

@ -27,7 +27,7 @@
#include "math/polynomial/algebraic_numbers.h"
#include "math/polynomial/polynomial.h"
#include "util/nat_set.h"
#include "util/optional.h"
#include <optional>
#include "util/inf_rational.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"

4
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -24,7 +24,7 @@ Notes:
#include "ast/pb_decl_plugin.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/expr_replacer.h"
#include "util/optional.h"
#include <optional>
#include "tactic/arith/bv2int_rewriter.h"
#include "tactic/arith/bv2real_rewriter.h"
#include "ast/converters/generic_model_converter.h"
@ -209,7 +209,7 @@ class nla2bv_tactic : public tactic {
void add_int_var(app* n) {
expr_ref s_bv(m_manager);
sort_ref bv_sort(m_manager);
optional<numeral> low, up;
std::optional<numeral> low, up;
numeral tmp;
bool is_strict;
if (m_bounds.has_lower(n, tmp, is_strict)) {

1
src/test/main.cpp
View file

@ -156,7 +156,6 @@ int main(int argc, char ** argv) {
TST(inf_rational);
TST(ast);
TST(optional);
TST(optional_benchmark);
TST(bit_vector);
TST(fixed_bit_vector);
TST(tbv);

11
src/test/optional.cpp
View file

@ -19,12 +19,11 @@ Revision History:
#include "util/trace.h"
#include "util/debug.h"
#include "util/memory_manager.h"
#include "util/optional.h"
#include <optional>
static void tst1() {
optional<int> v;
ENSURE(!v);
ENSURE(v == false);
std::optional<int> v;
ENSURE(!v.has_value());
v = 10;
ENSURE(v);
ENSURE(*v == 10);
@ -45,7 +44,7 @@ struct OptFoo {
};
static void tst2() {
optional<OptFoo> v;
std::optional<OptFoo> v;
ENSURE(!v);
v = OptFoo(10, 20);
ENSURE(v->m_x == 10);
@ -57,7 +56,7 @@ static void tst2() {
}
static void tst3() {
optional<int *> v;
std::optional<int *> v;
ENSURE(!v);
int x = 10;
v = &x;

404
src/test/optional_benchmark.cpp
View file

@ -1,404 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
optional_benchmark.cpp
Abstract:
Benchmark std::optional vs custom optional implementation
Author:
GitHub Copilot 2026-01-11
Revision History:
--*/
#include "util/trace.h"
#include "util/debug.h"
#include "util/memory_manager.h"
#include "util/optional.h"
#include <optional>
#include <chrono>
#include <iostream>
#include <iomanip>
// Simple struct for testing
struct BenchData {
int x;
int y;
int z;
BenchData(int a = 0, int b = 0, int c = 0) : x(a), y(b), z(c) {}
};
// Benchmark helper
template<typename Func>
double measure_time_ms(Func f, int iterations = 1000000) {
auto start = std::chrono::high_resolution_clock::now();
f();
auto end = std::chrono::high_resolution_clock::now();
std::chrono::duration<double, std::milli> elapsed = end - start;
return elapsed.count();
}
// Prevent compiler optimization
// Prevent compiler optimization (portable for GCC/Clang and MSVC)
#if defined(_MSC_VER)
#include <intrin.h>
template<typename T>
inline void do_not_optimize(T const& value) {
// Trick MSVC into thinking value is used
volatile const T* volatile ptr = &value;
(void)ptr;
_ReadWriteBarrier();
}
#else
template<typename T>
inline void do_not_optimize(T const& value) {
asm volatile("" : : "m"(value) : "memory");
}
#endif
void benchmark_construction() {
const int iterations = 1000000;
std::cout << "\n=== Construction Benchmark ===" << std::endl;
// Test 1: Default construction
{
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<int> opt;
do_not_optimize(opt);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<int> opt;
do_not_optimize(opt);
}
});
std::cout << "Default construction (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
// Test 2: Value construction
{
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<int> opt(i);
do_not_optimize(opt);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<int> opt(i);
do_not_optimize(opt);
}
});
std::cout << "\nValue construction (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
// Test 3: Struct construction
{
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<BenchData> opt(BenchData(i, i+1, i+2));
do_not_optimize(opt);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<BenchData> opt(BenchData(i, i+1, i+2));
do_not_optimize(opt);
}
});
std::cout << "\nValue construction (struct):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
}
void benchmark_copy() {
const int iterations = 1000000;
std::cout << "\n=== Copy Benchmark ===" << std::endl;
// Test 1: Copy construction (int)
{
optional<int> custom_src(42);
std::optional<int> std_src(42);
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<int> opt(custom_src);
do_not_optimize(opt);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<int> opt(std_src);
do_not_optimize(opt);
}
});
std::cout << "Copy construction (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
// Test 2: Copy assignment (int)
{
optional<int> custom_src(42);
std::optional<int> std_src(42);
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<int> opt;
opt = custom_src;
do_not_optimize(opt);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<int> opt;
opt = std_src;
do_not_optimize(opt);
}
});
std::cout << "\nCopy assignment (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
}
void benchmark_move() {
const int iterations = 1000000;
std::cout << "\n=== Move Benchmark ===" << std::endl;
// Test 1: Move construction (int)
{
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<int> src(i);
optional<int> dst(std::move(src));
do_not_optimize(dst);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<int> src(i);
std::optional<int> dst(std::move(src));
do_not_optimize(dst);
}
});
std::cout << "Move construction (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
// Test 2: Move assignment (int)
{
double custom_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
optional<int> src(i);
optional<int> dst;
dst = std::move(src);
do_not_optimize(dst);
}
});
double std_time = measure_time_ms([&]() {
for (int i = 0; i < iterations; i++) {
std::optional<int> src(i);
std::optional<int> dst;
dst = std::move(src);
do_not_optimize(dst);
}
});
std::cout << "\nMove assignment (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
}
void benchmark_access() {
const int iterations = 10000000;
std::cout << "\n=== Access Benchmark ===" << std::endl;
// Test 1: Dereference operator
{
optional<int> custom_opt(42);
std::optional<int> std_opt(42);
double custom_time = measure_time_ms([&]() {
int sum = 0;
for (int i = 0; i < iterations; i++) {
sum += *custom_opt;
}
do_not_optimize(sum);
});
double std_time = measure_time_ms([&]() {
int sum = 0;
for (int i = 0; i < iterations; i++) {
sum += *std_opt;
}
do_not_optimize(sum);
});
std::cout << "Dereference operator (int):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
// Test 2: Arrow operator
{
optional<BenchData> custom_opt(BenchData(1, 2, 3));
std::optional<BenchData> std_opt(BenchData(1, 2, 3));
double custom_time = measure_time_ms([&]() {
int sum = 0;
for (int i = 0; i < iterations; i++) {
sum += custom_opt->x;
}
do_not_optimize(sum);
});
double std_time = measure_time_ms([&]() {
int sum = 0;
for (int i = 0; i < iterations; i++) {
sum += std_opt->x;
}
do_not_optimize(sum);
});
std::cout << "\nArrow operator (struct):" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
// Test 3: Boolean conversion
{
optional<int> custom_opt(42);
std::optional<int> std_opt(42);
double custom_time = measure_time_ms([&]() {
int count = 0;
for (int i = 0; i < iterations; i++) {
if (custom_opt) count++;
}
do_not_optimize(count);
});
double std_time = measure_time_ms([&]() {
int count = 0;
for (int i = 0; i < iterations; i++) {
if (std_opt) count++;
}
do_not_optimize(count);
});
std::cout << "\nBoolean conversion:" << std::endl;
std::cout << " Custom optional: " << std::fixed << std::setprecision(2)
<< custom_time << " ms" << std::endl;
std::cout << " std::optional: " << std::fixed << std::setprecision(2)
<< std_time << " ms" << std::endl;
std::cout << " Ratio (custom/std): " << std::fixed << std::setprecision(2)
<< (custom_time / std_time) << "x" << std::endl;
}
}
void benchmark_memory() {
std::cout << "\n=== Memory Footprint ===" << std::endl;
std::cout << "Size of optional<int>:" << std::endl;
std::cout << " Custom optional: " << sizeof(optional<int>) << " bytes" << std::endl;
std::cout << " std::optional: " << sizeof(std::optional<int>) << " bytes" << std::endl;
std::cout << "\nSize of optional<BenchData>:" << std::endl;
std::cout << " Custom optional: " << sizeof(optional<BenchData>) << " bytes" << std::endl;
std::cout << " std::optional: " << sizeof(std::optional<BenchData>) << " bytes" << std::endl;
std::cout << "\nSize of optional<int*>:" << std::endl;
std::cout << " Custom optional: " << sizeof(optional<int*>) << " bytes" << std::endl;
std::cout << " std::optional: " << sizeof(std::optional<int*>) << " bytes" << std::endl;
}
void tst_optional_benchmark() {
std::cout << "\n╔═══════════════════════════════════════════════════════════════╗" << std::endl;
std::cout << "║ std::optional vs Custom optional Performance Benchmark ║" << std::endl;
std::cout << "╚═══════════════════════════════════════════════════════════════╝" << std::endl;
benchmark_memory();
benchmark_construction();
benchmark_copy();
benchmark_move();
benchmark_access();
std::cout << "\n═══════════════════════════════════════════════════════════════" << std::endl;
std::cout << "Benchmark completed!" << std::endl;
std::cout << "\nNotes:" << std::endl;
std::cout << "- Custom optional uses heap allocation (alloc/dealloc)" << std::endl;
std::cout << "- std::optional uses in-place storage (no heap allocation)" << std::endl;
std::cout << "- Ratios > 1.0 indicate custom optional is slower" << std::endl;
std::cout << "- Ratios < 1.0 indicate custom optional is faster" << std::endl;
std::cout << "═══════════════════════════════════════════════════════════════\n" << std::endl;
}

29
src/util/array_map.h
View file

@ -19,7 +19,7 @@ Revision History:
#pragma once
#include "util/vector.h"
#include "util/optional.h"
#include <optional>
/**
\brief Implements a mapping from Key to Data.
@ -43,29 +43,30 @@ class array_map {
unsigned m_garbage = 0;
unsigned m_non_garbage = 0;
static const unsigned m_gc_threshold = 10000;
vector<optional<entry>, CallDestructors > m_map;
vector<std::optional<entry>, CallDestructors > m_map;
Plugin m_plugin;
bool is_current(optional<entry> const& e) const {
bool is_current(std::optional<entry> const& e) const {
return e->m_timestamp == m_timestamp;
}
optional<entry> const & get_core(Key const & k) const {
std::optional<entry> const & get_core(Key const & k) const {
unsigned id = m_plugin.to_int(k);
if (id < m_map.size()) {
optional<entry> const & e = m_map[id];
std::optional<entry> const & e = m_map[id];
if (e && is_current(e)) {
return e;
}
}
return optional<entry>::undef();
static const std::optional<entry> s_undef;
return s_undef;
}
void really_flush() {
for (optional<entry> & e : m_map) {
for (std::optional<entry> & e : m_map) {
if (e) {
m_plugin.del_eh(e->m_key, e->m_data);
e.set_invalid();
e.reset();
}
}
m_garbage = 0;
@ -81,11 +82,11 @@ public:
~array_map() { really_flush(); }
bool contains(Key const & k) const {
return get_core(k);
return get_core(k).has_value();
}
Data const & get(Key const & k) const {
optional<entry> const & e = get_core(k);
std::optional<entry> const & e = get_core(k);
SASSERT(e);
return e->m_data;
}
@ -103,11 +104,11 @@ public:
void insert(Key const & k, Data const & d) {
unsigned id = m_plugin.to_int(k);
if (id >= m_map.size()) {
m_map.resize(id + 1, optional<entry>::undef());
m_map.resize(id + 1, std::nullopt);
}
m_plugin.ins_eh(k, d);
optional<entry> & e = m_map[id];
std::optional<entry> & e = m_map[id];
if (e) {
if (!is_current(e)) {
--m_garbage;
@ -124,7 +125,7 @@ public:
void erase(Key const & k) {
unsigned id = m_plugin.to_int(k);
if (id < m_map.size()) {
optional<entry> & e = m_map[id];
std::optional<entry> & e = m_map[id];
if (e) {
m_plugin.del_eh(e->m_key, e->m_data);
if (is_current(e)) {
@ -135,7 +136,7 @@ public:
SASSERT(m_garbage > 0);
--m_garbage;
}
e.set_invalid();
e.reset();
}
}
}

154
src/util/optional.h
View file

@ -1,154 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
optional.h
Abstract:
Discriminated union of a type T.
It defines the notion of initialized/uninitialized objects.
Author:
Leonardo de Moura (leonardo) 2006-09-29.
Revision History:
--*/
#pragma once
template<class T>
class optional {
T* m_obj = nullptr;
void destroy() {
dealloc(m_obj);
m_obj = nullptr;
}
public:
optional() = default;
explicit optional(const T & val) {
m_obj = alloc(T, val);
}
explicit optional(T && val) {
m_obj = alloc(T, std::move(val));
}
optional(optional<T> && val) noexcept {
std::swap(m_obj, val.m_obj);
}
optional(const optional<T> & val) {
if (val.m_obj) {
m_obj = alloc(T, *val);
}
}
~optional() {
destroy();
}
static optional const & undef() { static optional u; return u; }
bool initialized() const { return m_obj; }
operator bool() const { return m_obj; }
bool operator!() const { return !m_obj; }
T * get() const {
return m_obj;
}
void set_invalid() {
destroy();
}
T * operator->() {
SASSERT(m_obj);
return m_obj;
}
T const * operator->() const {
SASSERT(m_obj);
return m_obj;
}
const T & operator*() const {
SASSERT(m_obj);
return *m_obj;
}
T & operator*() {
SASSERT(m_obj);
return *m_obj;
}
optional & operator=(const T & val) {
destroy();
m_obj = alloc(T, val);
return * this;
}
optional & operator=(optional && val) noexcept {
std::swap(m_obj, val.m_obj);
return *this;
}
optional & operator=(const optional & val) {
if (&val != this) {
destroy();
if (val.m_obj) {
m_obj = alloc(T, *val);
}
}
return *this;
}
};
/**
\brief Template specialization for pointers. NULL represents uninitialized pointers.
*/
template<typename T>
class optional<T*> {
T * m_ptr = nullptr;
static optional m_undef;
public:
optional() = default;
explicit optional(T * val):m_ptr(val) {}
static optional const & undef() { return m_undef; }
bool initialized() const { return m_ptr != 0 ; }
operator bool() const { return m_ptr != 0; }
bool operator!() const { return m_ptr == nullptr; }
void reset() { m_ptr = 0; }
optional & operator=(T * val) {
m_ptr = val;
return *this;
}
optional & operator=(const optional & val) {
m_ptr = val.m_ptr;
return *this;
}
T ** operator->() { return &m_ptr; }
T * operator*() const { return m_ptr; }
T * & operator*() { return m_ptr; }
};