mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

Add std::optional vs custom optional performance benchmark (#8160)

Browse source 
* Initial plan

* Complete optional benchmark implementation

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

* Add comprehensive benchmark results documentation

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

* Address code review feedback - improve benchmark portability and remove redundant volatile

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

* Final refinement: fix inline assembly constraint for const reference

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

* Delete OPTIONAL_BENCHMARK_RESULTS.md

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-01-11 14:30:45 -08:00 • committed by GitHub
parent 5aac5c98b3
commit 5cf59ea5e4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 394 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/test/CMakeLists.txt
View file

@ -98,6 +98,7 @@ add_executable(test-z3
object_allocator.cpp
old_interval.cpp
optional.cpp
optional_benchmark.cpp
parray.cpp
pb2bv.cpp
pdd.cpp

1
src/test/main.cpp
View file

@ -156,6 +156,7 @@ 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);

392
src/test/optional_benchmark.cpp Normal file
View file

@ -0,0 +1,392 @@
/*++
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
template<typename T>
void do_not_optimize(T const& value) {
asm volatile("" : : "m"(value) : "memory");
}
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;
}